Recent work on formal theories of truth has revived an approach, due originally to Tarski, on which syntax and truth theories are sharply distinguished—‘disentangled’—from mathematical base theories. In this paper, we defend a novel philosophical constraint on disentangled theories. We argue that these theories must be epistemically stable: they must possess an intrinsic motivation justifying no strictly stronger theory. In a disentangled setting, even if the base and the syntax theory are individually stable, they may be jointly unstable. We contend (...) that this flaw afflicts many proposals discussed in the literature; we defend a new, stable disentangled theory, double second-order arithmetic. (shrink)

According to Kant, the axioms of intuition, i.e. space and time, must provide an organization of the sensory experience. However, this first orderliness of empirical sensations seems to depend on a kind of faculty pertaining to subjectivity, rather than to the encounter of these same intuitions with the real properties of phenomena. Starting from an analysis of some very significant developments in mathematical and theoretical physics in the last decades, in which intuition played an important role, we argue that nevertheless (...) intuition comes into play in a fundamentally different way to that which Kant had foreseen: in the form of a formal or “categorical” yet not sensible intuition. We show further that the statement that our space is mathematically three-dimensional and locally Euclidean by no means follows from a supposed a priori nature of the sensible or subjective space as Kant claimed. In fact, the three-dimensional space can bear many different geometrical and topological structures, as particularly the mathematical results of Milnor, Smale, Thurston and Donaldson demonstrated. On the other hand, it has been stressed that even the phenomenological or perceptual space, and especially the visual system, carries a very rich geometrical organization whose structure is essentially non-Euclidean. Finally, we argue that in order to grasp the meaning of abstract geometric objects, as n-dimensional spaces, connections on a manifold, fiber spaces, module spaces, knotted spaces and so forth, where sensible intuition is essentially lacking and where therefore another type of mathematical idealization intervenes, we need to develop a new form of intuition. (shrink)

This is a survey of Gödel's perennial preoccupations with the limits of finitism, its relations to constructivity, and the significance of his incompleteness theorems for Hilbert's program, using his published and unpublished articles and lectures as well as the correspondence between Bernays and Gödel on these matters. There is also an important subtext, namely the shadow of Hilbert that loomed over Gödel from the beginning to the end.

This paper contains five observations concerning the intended meaning of the intuitionistic logical constants: (1) if the explanations of this meaning are to be based on a non-decidable concept, that concept should not be that of `proof"; (2) Kreisel"s explanations using extra clauses can be significantly simplified; (3) the impredicativity of the definition of → can be easily and safely ameliorated; (4) the definition of → in terms of `proofs from premises" results in a loss of the inductive character of (...) the definitions of ∨ and ∃ and (5) the same occurs with the definition of ∀ in terms of `proofs with free variables". (shrink)

In a note appended to the translation of “On consistency and completeness” (), Gödel reexamined the problem of the unprovability of consistency. Gödel here focuses on an alternative means of expressing the consistency of a formal system, in terms of what would now be called a ‘reflection principle’, roughly, the assertion that a formula of a certain class is provable in the system only if it is true. Gödel suggests that it is this alternative means of expressing consistency that we (...) should be interested in from a foundational point of view, and he gives a result that shows certain reflection principles to be underivable in extensions of elementary number theory under conditions significantly weaker than the Hilbert-Bernays derivability conditions. In this paper I shall discuss the background to Gödel's result and the foundational significance he claims for it. Along the way, I shall present a new proof of the result which places it in an even more general context than the one considered by Gödel in the 1960s. (shrink)

Semantics connected to some information based metaphor are well-known in logic literature: a paradigmatic example is Kripke semantic for Intuitionistic Logic. In this paper we start from the concrete problem of providing suitable logic-algebraic models for the calculus of attribute dependencies in Formal Contexts with information gaps and we obtain an intuitive model based on the notion of passage of information showing that Kleene algebras, semi-simple Nelson algebras, three-valued ukasiewicz algebras and Post algebras of order three are, in a sense, (...) naturally and directly connected to partially defined information systems. In this way wecan provide for these logic-algebraic structures a raison dêetre different from the original motivations concerning, for instance, computability theory. (shrink)

We describe an emerging field, that of nonclassical computability and nonclassical computing machinery. According to the nonclassicist, the set of well-defined computations is not exhausted by the computations that can be carried out by a Turing machine. We provide an overview of the field and a philosophical defence of its foundations.

Brouwer’s view on induction has relatively recently been characterised as one on which it is not only intuitive (as expected) but functional, by van Dalen. He claims that Brouwer’s ‘Ur-intuition’ also yields the recursor. Appealing to Husserl’s phenomenology, I offer an analysis of Brouwer’s view that supports this characterisation and claim, even if assigning the primary role to the iterator instead. Contrasts are drawn to accounts of induction by Poincaré, Heyting, and Kreisel. On the phenomenological side, the analysis provides an (...) alternative to that in Tieszen’s Mathematical Intuition, and confirms a view of Gödel on his Dialectica Interpretation. (shrink)

According to Schroeder-Heister 2018, proof-theoretic semantics is ‘an alternative to truth-condition semantics. It is based on the fundamental assumption that the central notion in terms of which meanings are assigned to certain expressions of our language, in particular to logical constants, is that of proof rather than truth. In this sense proof-theoretic semantics is semantics in terms of proof. Proof-theoretic semantics also means the semantics of proofs, i.e. the semantics of entities which describe how we arrive at certain assertions given (...) certain assumptions.' This text advocates that proof-theoretic semantics, as described above, was an approach to semantical issues in logic that appeared in mainstream philosophical literature at least a couple of centuries before the tradition of general proof theory (cf. Prawitz 1971) came into being. This is done by means of an interpretive analysis of Kant’s 1762 essay Die falsche Spitzfindigkeit der vier syllogistischen Figuren, in which two theses are argued: first, that the issue of justifying the logical validity of inferences is approached by Kant in this text, in a strong sense, in terms of proofs; and second, that the purpose of his effort is to establish a point concerning the semantical equivalence between certain distinct valid inferences. (shrink)

This paper explores the relationship borne by the traditional paradoxes of set theory and semantics to formal incompleteness phenomena. A central tool is the application of the Arithmetized Completeness Theorem to systems of second-order arithmetic and set theory in which various “paradoxical notions” for first-order languages can be formalized. I will first discuss the setting in which this result was originally presented by Hilbert & Bernays (1939) and also how it was later adapted by Kreisel (1950) and Wang (1955) in (...) order to obtain formal undecidability results. A generalization of this method will then be presented whereby Russell’s paradox, a variant of Mirimanoff’s paradox, the Liar, and the Grelling–Nelson paradox may be uniformly transformed into incompleteness theorems. Some additional observations are then framed relating these results to the unification of the set theoretic and semantic paradoxes, the intensionality of arithmetization (in the sense of Feferman, 1960), and axiomatic theories of truth. (shrink)

The concept of the (full) unfolding of a schematic system is used to answer the following question: Which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted ? The program to determine for various systems of foundational significance was previously carried out for a system of nonfinitist arithmetic, ; it was shown that is proof-theoretically equivalent to predicative analysis. In the present paper we work out the unfolding notions for a basic schematic system (...) of finitist arithmetic, , and for an extension of that by a form of the so-called Bar Rule. It is shown that and are proof-theoretically equivalent, respectively, to Primitive Recursive Arithmetic, , and to Peano Arithmetic,. (shrink)

Pour le philosophe intéressé aux structures et aux fondements du savoir théorétique, à la constitution d'une « méta-théorétique «, θεωρíα., qui, mieux que les « Wissenschaftslehre » fichtéenne ou husserlienne et par-delà les débris de la métaphysique, veut dans une intention nouvelle faire la synthèse du « théorétique », la logique mathématique se révèle un objet privilégié.

The starting point of this article is an old question asked by Feferman in his paper on Hancock's conjecture [6] about the strength of ${\rm ID}_{1}^{\ast}$. This theory is obtained from the well-known theory ID₁ by restricting fixed point induction to formulas that contain fixed point constants only positively. The techniques used to perform the proof-theoretic analysis of ${\rm ID}_{1}^{\ast}$ also permit to analyze its transfinitely iterated variants ${\rm ID}_{\alpha}^{\ast}$. Thus, we eventually know that $|\widehat{{\rm ID}}_{\alpha}|=|{\rm ID}_{\alpha}^{\ast}|$.

This paper examines the question of the extensional correctness of Tarskian definitions of logical truth and logical consequence. I identify a few different informal properties which are necessary for a sentence to be an informal logical truth and look at whether they are necessary properties of Tarskian logical truths. I examine arguments by John Etchemendy and Vann McGee to the effect that some of those properties are not necessary properties of some Tarskian logical truths, and find them unconvincing. I stress (...) the point that since the hypothesis that Tarski's definitions are extensionally correct is deeply entrenched, the burden of proof is still on the shoulders of Tarski's critics, who have not lifted the burden. (shrink)

We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation.

The metamathematical theorems of Gödel and Church are frequently applied to the philosophy of mind, typically as rational evidence against mechanism. Using methods of Post and Smullyan, these results are presented as purely mathematical theorems and various such applications are discussed critically. In particular, J. Lucas's use of Gödel's theorem to distinguish between conscious and unconscious beings is refuted, while more generally, attempts to extract philosophy from metamathematics are shown to involve only dramatizations of the constructivity problem in foundations. More (...) specifically, philosophical extrapolations from metamathematics are shown to involve premature extensions of Church's thesis. (shrink)