Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics

Author(s):  
Clifford Spector



Author(s):  
Michael Detlefsen

AbstractFormalism in the philosophy of mathematics has taken a variety of forms and has been advocated for widely divergent reasons. In Sects. 1 and 2, I briefly introduce the major formalist doctrines of the late nineteenth and early twentieth centuries. These are what I call empirico-semantic formalism (advocated by Heine), game formalism (advocated by Thomae) and instrumental formalism (advocated by Hilbert). After describing these views, I note some basic points of similarity and difference between them. In the remainder of the paper, I turn my attention to Hilbert’s instrumental formalism. My primary aim there will be to develop its formalist elements more fully. These are, in the main, (i) its rejection of the axiom-centric focus of traditional model-construction approaches to consistency problems, (ii) its departure from the traditional understanding of the basic nature of proof and (iii) its distinctively descriptive or observational orientation with regard to the consistency problem for arithmetic. More specifically, I will highlight what I see as the salient points of connection between Hilbert’s formalist attitude and his finitist standard for the consistency proof for arithmetic. I will also note what I see as a significant tension between Hilbert’s observational approach to the consistency problem for arithmetic and his expressed hope that his solution of that problem would dispense with certain epistemological concerns regarding arithmetic once and for all.



2021 ◽  
Vol 14 ◽  
pp. 26-38
Author(s):  
Samuel R. Elliott ◽  

The classical interpretation of mathematical statements can be seen as comprising two separate but related aspects: a domain and a truth-schema. L. E. J. Brouwer’s intuitionistic project lays the groundwork for an alternative conception of the objects in this domain, as well as an accompanying intuitionistic truth-schema. Drawing on the work of Arend Heyting and Michael Dummett, I present two objections to classical mathematical semantics, with the aim of creating an opening for an alternative interpretation. With this accomplished, I then make the case for intuitionism as a suitable candidate to fill this void.



1959 ◽  
Vol 14 ◽  
pp. 95-107
Author(s):  
Sigekatu Kuroda

The V-system T(V) is defined in §2 by using §1, and its consistency is proved in §3. The definition of T(V) is given in such a way that the consistency proof of T(V) in §3 shows a typical way to prove the consistency of some subsystems of UL. Otherwise we could define T(V) more simply by using truth values. After T(V)-sets are treated in §4, it is proved in §5 as a T(V)-theorem that T(V)-sets are all equal to V.



1985 ◽  
Vol 50 (4) ◽  
pp. 895-902 ◽  
Author(s):  
R. C. Flagg

In [6] Gödel observed that intuitionistic propositional logic can be interpreted in Lewis's modal logic (S4). The idea behind this interpretation is to regard the modal operator □ as expressing the epistemic notion of “informal provability”. With the work of Shapiro [12], Myhill [10], Goodman [7], [8], and Ščedrov [11] this simple idea has developed into a successful program of integrating classical and intuitionistic mathematics.There is one question quite central to the above program that has remained open. Namely:Does Ščedrov's extension of the Gödel translation to set theory provide a faithful interpretation of intuitionistic set theory into epistemic set theory?In the present paper we give an affirmative answer to this question.The main ingredient in our proof is the construction of an interpretation of epistemic set theory into intuitionistic set theory which is inverse to the Gödel translation. This is accomplished in two steps. First we observe that Funayama's theorem is constructively provable and apply it to the power set of 1. This provides an embedding of the set of propositions into a complete topological Boolean algebra . Second, in a fashion completely analogous to the construction of Boolean-valued models of classical set theory, we define the -valued universe V(). V() gives a model of epistemic set theory and, since we use a constructive metatheory, this provides an interpretation of epistemic set theory into intuitionistic set theory.





Sign in / Sign up

Export Citation Format

Share Document