Proof-theoretic reflection principles are schemas which attempt to express the soundness of arithmetical theories within their own language, e.g., ${\mathtt{{Prov}_{\mathsf {PA}} \rightarrow \varphi }}$ can be understood to assert that any statement provable in Peano arithmetic is true. It has been repeatedly suggested that justification for such principles follows directly from acceptance of an arithmetical theory $\mathsf {T}$ or indirectly in virtue of their derivability in certain truth-theoretic extensions thereof. This paper challenges this consensus by exploring relationships between reflection principles (...) and principles of mathematical and transfinite induction as well as the status of the latter with respect to various foundational characterizations of number theory. (shrink)

We show that the name “Lucas-Penrose thesis” encompasses several different theses. All these theses refer to extremely vague concepts, and so are either practically meaningless, or obviously false. The arguments for the various theses, in turn, are based on confusions with regard to the meaning of these vague notions, and on unjustified hidden assumptions concerning them. All these observations are true also for all interesting versions of the much weaker thesis known as “Gö- del disjunction”. Our main conclusions are that (...) pure mathematical theorems cannot decide alone any question which is not purely mathematical, and that an argument that cannot be fully formalized cannot be taken as a mathematical proof. (shrink)

Philosophers of language have drawn on metamathematical results in varied ways. Extensionalist philosophers have been particularly impressed with two, not unrelated, facts: the existence, due to Frege/Tarski, of a certain sort of semantics, and the seeming absence of intensional contexts from mathematical discourse. The philosophical import of these facts is at best murky. Extensionalists will emphasize the success and clarity of the model theoretic semantics; others will emphasize the relative poverty of the mathematical idiom; still others will question the aptness (...) of the standard extensional semantics for mathematics. In this paper I investigate some implications of the Gödel Second Incompleteness Theorem for these positions. I argue that the realm of mathematics, proof theory in particular, has been a breeding ground for intensionality and that satisfactory intensional semantic theories are implicit in certain rigorous technical accounts. (shrink)

We analyse Kreisel’s notion of human-effective computability. Like Kreisel, we relate this notion to a concept of informal provability, but we disagree with Kreisel about the precise way in which this is best done. The resulting two different ways of analysing human-effective computability give rise to two different variants of Church’s thesis. These are both investigated by relating them to transfinite progressions of formal theories in the sense of Feferman.

This anthology of the very latest research on truth features the work of recognized luminaries in the field, put together following a rigorous refereeing process. Along with an introduction outlining the central issues in the field, it provides a unique and unrivaled view of contemporary work on the nature of truth, with papers selected from key conferences in 2011 such as Truth Be Told, Truth at Work, Paradoxes of Truth and Denotation and Axiomatic Theories of Truth. Studying the nature of (...) the concept of ‘truth’ has always been a core role of philosophy, but recent years have been a boom time in the topic. With a wealth of recent conferences examining the subject from various angles, this collection of essays recognizes the pressing need for a volume that brings scholars up to date on the arguments. Offering academics and graduate students alike a much-needed repository of today’s cutting-edge work in this vital topic of philosophy, the volume is required reading for anyone needing to keep abreast of developments, and is certain to act as a catalyst for further innovation and research. (shrink)

The aim of this paper is twofold: first, I provide a cluster of theories of truth in classical logic that is (internally) consistent with global reflection principles: the theories of positive truth (and falsity). After that, I analyse the _epistemic value_ of such theories. I do so employing the framework of cognitive projects introduced by Wright (Proc Aristot Soc 78:167–245, 2004), and employed—in the context of theories of truth—by Fischer et al. (Noûs 2019. https://doi.org/10.1111/nous.12292 ). In particular, I will argue (...) that theories of positive truth are _trustworthy_, analogously to the theories of full disquotational truth. Moreover, I argue that, for a given cognitive project, _if_ the acceptance of trustworthy theories is taken to be an _epistemic norm_ of cognitive project, then one has good reasons to accept theories of positive truth over other rival theories of truth in classical logic. On the other hand, the latter theories are deemed epistemically unacceptable. (shrink)

We will study several weak axiom systems that use the Subtraction and Division primitives (rather than Addition and Multiplication) to formally encode the theorems of Arithmetic. Provided such axiom systems do not recognize Multiplication as a total function, we will show that it is feasible for them to verify their Semantic Tableaux, Herbrand, and Cut-Free consistencies. If our axiom systems additionally do not recognize Addition as a total function, they will be capable of recognizing the consistency of their Hilbert-style deductive (...) proofs. Our axiom systems will not be strong enough to recognize their Canonical Reflection principle, but they will be capable of recognizing an approximation of it, called the "Tangibility Reflection Principle". We will also prove some new versions of the Second Incompleteness Theorem stating essentially that it is not possible to extend our exceptions to the Incompleteness Theorem much further. (shrink)

Many philosophers believe that a deflationist theory of truth must conservatively extend any base theory to which it is added. But when applied to arithmetic, it's argued, the imposition of a conservativeness requirement leads to a serious objection to deflationism: for the Gödel sentence for Peano Arithmetic is not a theorem of PA, but becomes one when PA is extended by adding plausible principles governing truth. This paper argues that no such objection succeeds. The issue turns on how we understand (...) the notion of logical consequence implicit in any conservativeness requirement, and whether we possess a categorical conception of the natural numbers. I offer a disjunctive response: if we possess a categorical conception of arithmetic, then deflationists have principled reason to accept a rich notion of logical consequence according to which the Gödel sentence follows from PA. But if we do not, then the reasons for requiring the derivation of the Gödel sentence lapse, and deflationists are free to accept a conservativeness requirement stated proof-theoretically. Either way, deflationism is in the clear. (shrink)

Sections 3.16 and 3.23 of Roger Penrose's Shadows of the mind (Oxford, Oxford University Press, 1994) contain a subtle and intriguing new argument against mechanism, the thesis that the human mind can be accurately modeled by a Turing machine. The argument, based on the incompleteness theorem, is designed to meet standard objections to the original Lucas-Penrose formulations. The new argument, however, seems to invoke an unrestricted truth predicate (and an unrestricted knowability predicate). If so, its premises are inconsistent. The usual (...) ways of restricting the predicates either invalidate Penrose's reasoning or require presuppositions that the mechanist can reject. (shrink)

This paper is an attempt to bring together two separated areas of research: classical mathematics and metamathematics on the one side, non-monotonic reasoning on the other. This is done by simulating nonmonotonic logic through antitonic theory extensions. In the first half, the specific extension procedure proposed here is motivated informally, partly in comparison with some well-known non-monotonic formalisms. Operators V and, more generally, U are obtained which have some plausibility when viewed as giving nonmonotonic theory extensions. In the second half, (...) these operators are treated from a mathematical and metamathematical point of view. Here an important role is played by U -closed theories and U -fixed points. The last section contains results on V-closed theories which are specific for V. (shrink)

According to the implicit commitment thesis, once accepting a mathematical formal system S, one is implicitly committed to additional resources not immediately available in S. Traditionally, this thesis has been understood as entailing that, in accepting S, we are bound to accept reflection principles for S and therefore claims in the language of S that are not derivable in S itself. It has recently become clear, however, that such reading of the implicit commitment thesis cannot be compatible with well-established positions (...) in the foundations of mathematics which consider a specific theory S as self-justifying and doubt the legitimacy of any principle that is not derivable in S: examples are Tait’s finitism and the role played in it by Primitive Recursive Arithmetic, Isaacson’s thesis and Peano Arithmetic, Nelson’s ultrafinitism and sub-exponential arithmetical systems. This casts doubts on the very adequacy of the implicit commitment thesis for arithmetical theories. In the paper we show that such foundational standpoints are nonetheless compatible with the implicit commitment thesis. We also show that they can even be compatible with genuine soundness extensions of S with suitable form of reflection. The analysis we propose is as follows: when accepting a system S, we are bound to accept a fixed set of principles extending S and expressing minimal soundness requirements for S, such as the fact that the non-logical axioms of S are true. We call this invariant component the semantic core of implicit commitment. But there is also a variable component of implicit commitment that crucially depends on the justification given for our acceptance of S in which, for instance, may or may not appear reflection principles for S. We claim that the proposed framework regulates in a natural and uniform way our acceptance of different arithmetical theories. (shrink)

Truth-theoretic deflationism holds that truth is simple, and yet that it can fulfil many useful logico-linguistic roles. Deflationism focuses on axioms for truth: there is no reduction of the notion of truth to more fundamental ones such as sets or higher-order quantifiers. In this paper I argue that the fundamental properties of reasonable, primitive truth predicates are at odds with the core tenets of classical truth-theoretic deflationism that I call fix, express, and quantify. Truth may be regarded as a broadly (...) logical, sui generis notion. However, this has little to do with the original aims of the deflationary theory of truth. (shrink)

Beall and Murzi :143–165, 2013) introduce an object-linguistic predicate for naïve validity, governed by intuitive principles that are inconsistent with the classical structural rules. As a consequence, they suggest that revisionary approaches to semantic paradox must be substructural. In response to Beall and Murzi, Field :1–19, 2017) has argued that naïve validity principles do not admit of a coherent reading and that, for this reason, a non-classical solution to the semantic paradoxes need not be substructural. The aim of this paper (...) is to respond to Field’s objections and to point to a coherent notion of validity which underwrites a coherent reading of Beall and Murzi’s principles: grounded validity. The notion, first introduced by Nicolai and Rossi, is a generalisation of Kripke’s notion of grounded truth, and yields an irreflexive logic. While we do not advocate the adoption of a substructural logic, we take the notion of naïve validity to be a legitimate semantic notion that points to genuine expressive limitations of fully structural revisionary approaches. (shrink)

Deflationists argue that ‘true’ is merely a logico-linguistic device for expressing blind ascriptions and infinite generalisations. For this reason, some authors have argued that deflationary truth must be conservative, i.e. that a deflationary theory of truth for a theory S must not entail sentences in S’s language that are not already entailed by S. However, it has been forcefully argued that any adequate theory of truth for S must be non-conservative and that, for this reason, truth cannot be deflationary :493–521, (...) 1998; Ketland in Mind 108:69–94, 1999). We consider two defences of conservative deflationism, respectively proposed by Waxman :429–463, 2017) and Tennant :551–582, 2002), and argue that they are both unsuccessful. In Waxman’s hands, deflationists are committed either to a non-purely expressive notion of truth, or to a conception of mathematics that does not allow them to justifiably exclude non-conservative theories of truth. Tennant’s conservative deflationism fares no better: if deflationist truth must be conservative over arithmetic, it can be shown to collapse into a non-conservative variety of deflationism. (shrink)

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)

The alleged proof of the non-mechanical, or non-computational, character of the human mind based on Gödel’s incompleteness theorem is revisited. Its history is reviewed. The proof, also known as the Lucas argument and the Penrose argument, is refuted. It is claimed, following Gödel himself and other leading logicians, that antimechanism is not implied by Gödel’s theorems alone. The present paper sets out this refutation in its strongest form, demonstrating general theorems implying the inconsistency of Lucas’s arithmetic and the semantic inadequacy (...) of Penrose’s arithmetic. On the other hand, the limitations to our capacity for mechanizing or programming the mind are also indicated, together with two other corollaries of Gödel’s theorems: that we cannot prove that we are consistent, and that we cannot fully describe our notion of a natural number. (shrink)

In this note we study several topics related to the schema of local reflection \\) and its partial and relativized variants. Firstly, we introduce the principle of uniform reflection with \-definable parameters, establish its relationship with relativized local reflection principles and corresponding versions of induction with definable parameters. Using this schema we give a new model-theoretic proof of the \-conservativity of uniform \-reflection over relativized local \-reflection. We also study the proof-theoretic strength of Feferman’s theorem, i.e., the assertion of 1-provability (...) in S of the local reflection schema \\), and its generalized versions. We relate this assertion to the uniform \-reflection schema and, in particular, obtain an alternative axiomatization of \. (shrink)

Deflationists have argued that truth is an ontologically thin property which has only an expressive function to perform, that is, it makes possible to express semantic generalizations like 'All the theorems are true', 'Everything Peter said is true', etc. Some of the deflationists have also argued that although truth is ontologically thin, it suffices in conjunctions with other facts not involving truth to explain all the facts about truth. The purpose of this paper is to show that in the case (...) of arithmetic, it is difficult to combine the expressive with the explanatory function of truth if the latter is understood in a deflationist way. We will make our point by investigating several logical systems: first-order logic, full second-order logic, and existential second-order (?11-) logic. (shrink)

The present paper discusses a proposal which says,roughly and with several qualifications, that thecollection of mathematical truths is identical withthe set of theorems of ZFC. It is argued that thisproposal is not as easily dismissed as outright falseor philosophically incoherent as one might think. Some morals of this are drawn for the concept ofmathematical knowledge.

This article gives an epistemological analysis of the reflection process by means of which you can come to know the consistency of a mathematical theory that you already accept. It is argued that this process can result in warranted belief in new mathematical principles without justifying them.

The proof-theoretic results on axiomatic theories oftruth obtained by different authors in recent years are surveyed.In particular, the theories of truth are related to subsystems ofsecond-order analysis. On the basis of these results, thesuitability of axiomatic theories of truth for ontologicalreduction is evaluated.

This paper propounds a systematic examination of the link between the Knower Paradox and provability interpretations of modal logic. The aim of the paper is threefold: to give a streamlined presentation of the Knower Paradox and related results; to clarify the notion of a syntactical treatment of modalities; finally, to discuss the kind of solution that modal provability logic provides to the Paradox. I discuss the respective strength of different versions of the Knower Paradox, both in the framework of first-order (...) arithmetic and in that of modal logic with fixed point operators. It is shown that the notion of a syntactical treatment of modalities is ambiguous between a self-referential treatment and a metalinguistic treatment of modalities, and that these two notions are independent. I survey and compare the provability interpretations of modality respectively given by Skyrms, B. (1978, The Journal of Philosophy 75: 368–387) Anderson, C.A. (1983, The Journal of Philosophy 80: 338–355) and Solovay, R. (1976, Israel Journal of Mathematics 25: 287–304). I examine how these interpretations enable us to bypass the limitations imposed by the Knower Paradox while preserving the laws of classical logic, each time by appeal to a distinct form of hierarchy. (shrink)

A common objection to hierarchical approaches to truth is that they fragment the concept of truth. This paper defends hierarchical approaches in general against the objection of fragmentation. It argues that the fragmentation required is familiar and unprob-lematic, via a comparison with mathematical proof. Furthermore, it offers an explanation of the source and nature of the fragmentation of truth. Fragmentation arises because the concept exhibits a kind of failure of closure under reflection. This paper offers a more precise characterization of (...) the reflection involved, first in the setting of formal theories of truth, and then in a more general setting. (shrink)

Michael Dummett's argument for intuitionism can be criticized for the implicit reliance on the existence of what might be called absolutely undecidable statements. Neil Tennant attacks epistemic optimism, the view that there are no such statements. I expose what seem serious flaws in his attack, and I suggest a way of defending the use of classical logic in arithmetic that circumvents the issue of optimism. I would like to thank an anonymous referee for helpful comments. CiteULike Connotea Del.icio.us What's this?

Shoenfield’s completeness theorem states that every true first order arithmetical sentence has a recursive \-proof encodable by using recursive applications of the \-rule. For a suitable encoding of Gentzen style \-proofs, we show that Shoenfield’s completeness theorem applies to cut free \-proofs encodable by using primitive recursive applications of the \-rule. We also show that the set of codes of \-proofs, whether it is based on recursive or primitive recursive applications of the \-rule, is \ complete. The same \ completeness (...) results apply to codes of cut free \-proofs. (shrink)

An open formalism for arithmetic is presented based on first-order logic supplemented by a very strictly controlled constructive form of the omega-rule. This formalism (which contains Peano Arithmetic) is proved (nonconstructively, of course) to be complete. Besides this main formalism, two other complete open formalisms are presented, in which the only inference rule is modus ponens. Any closure of any theorem of the main formalism is a theorem of each of these other two. This fact is proved constructively for the (...) stronger of them and nonconstructively for the weaker one. There is, though, an interesting counterpart: the consistency of the weaker formalism can be proved finitarily. (shrink)

Reflection principles are of central interest in the development of axiomatic theories. Whereas they are independent statements they appear to have a specific epistemological status. Our trust in those principles is as warranted as our trust in the axioms of the system itself. This paper is an attempt in clarifying this special epistemic status. We provide a motivation for the adoption of uniform reflection principles by their analogy to a form of the constructive \(\omega \) -rule. Additionally, we analyse the (...) role of informal arithmetic and the conception of natural numbers as an inductive structure, also with regard to extra conceptual resources such as a primitive truth predicate. (shrink)

I had the pleasure of renewing my acquaintance with Per Lindström at the meeting of the Seventh Scandinavian Logic Symposium, held in Uppsala in August 1996. There at lunch one day, Per said he had long been curious about the development of some of the ideas in my paper [1960] on the arithmetization of metamathematics. In particular, I had used the construction of a non-standard definition !* of the set of axioms of P (Peano Arithmetic) to show that P + (...) {¬ Con!} is interpretable in P, where ! is a standard definition of the axioms of P and Con! expresses the consistency of P via that presentation. Per pointed out that there is a simple “two-line” proof of this interpretability result which does not require the use of such formulas as !*, and he wondered whether I had been aware of that. In fact, his proof had never occurred to me, and if it had at the time, it is possible I would never have been led to the use of non-natural definitions. Per regarded this as a happy accident, since subsequent work by him and others on interpretability made essential use of such definitions. In our conversation, I enlarged a bit on the background to my work on arithmetization, and when I was invited to contribute to this special issue of Theoria dedicated to Lindström, it seemed a natural choice to use the occasion to fill out the story. One caveat, though: the following is drawn largely from memory, not always reliable, supplemented by consultation of the 1960 paper and the 1957 dissertation from which it was drawn. (shrink)

The notion of implicit commitment has played a prominent role in recent works in logic and philosophy of mathematics. Although implicit commitment is often associated with highly technical studies, it remains an elusive notion. In particular, it is often claimed that the acceptance of a mathematical theory implicitly commits one to the acceptance of a Uniform Reflection Principle for it. However, philosophers agree that a satisfactory analysis of the transition from a theory to its reflection principle is still lacking. We (...) provide an axiomatization of the minimal commitments implicit in the acceptance of a mathematical theory. The theory entails that the Uniform Reflection Principle is part of one’s implicit commitments, and sheds light on why this is so. We argue that the theory has significant epistemological consequences in that it explains how justified belief in the axioms of a theory can be preserved to the corresponding reflection principle. The theory also improves on recent analyses of implicit commitment based on truth or epistemic notions. (shrink)

We discuss Kunen’s algorithmic implementation of a proof for the Paris–Harrington theorem, and the author’s and da Costa’s proposed “exotic” formulation for the P = NP hypothesis. Out of those two examples we ponder the relation between mathematics within an axiomatic framework, and intuitive or informal mathematics.

Definitional and axiomatic theories of truth -- Objects of truth -- Tarski -- Truth and set theory -- Technical preliminaries -- Comparing axiomatic theories of truth -- Disquotation -- Classical compositional truth -- Hierarchies -- Typed and type-free theories of truth -- Reasons against typing -- Axioms and rules -- Axioms for type-free truth -- Classical symmetric truth -- Kripke-Feferman -- Axiomatizing Kripke's theory in partial logic -- Grounded truth -- Alternative evaluation schemata -- Disquotation -- Classical logic -- Deflationism (...) -- Reflection -- Ontological reduction -- Applying theories of truth. (shrink)

The notion of implicit commitment has played a prominent role in recent works in logic and philosophy of mathematics. Although implicit commitment is often associated with highly technical studies, it remains so far an elusive notion. In particular, it is often claimed that the acceptance of a mathematical theory implicitly commits one to the acceptance of a Uniform Reflection Principle for it. However, philosophers agree that a satisfactory analysis of the transition from a theory to its reflection principle is still (...) lacking. We provide an axiomatization of the minimal commitments implicit in the acceptance of a mathematical theory. The theory entails that the Uniform Reflection Principle is part of one's implicit commitments, and sheds light on the reason why this is so. We argue that the theory has interesting epistemological consequences in that it explains how justified belief in the axioms of a theory can be preserved to the corresponding reflection principle. The theory also improves on recent proposals for the analysis of implicit commitment based on truth or epistemic notions. (shrink)

In this paper I would like to indicate that this interpretation of Gödel goes far beyond what he really proved. I would like to show that to get from his result to a conclusion of the above kind requires a train of thought which is fuelled by much more than Gödel's result itself, and that a great deal of the excessive fuel should be utilized with an extra care.

A notion of finitary inductively presented (f.i.p.) logic is proposed here, which includes all syntactically described logics (formal systems)met in practice. A f.i.p. theory FS0 is set up which is universal for all f.i.p. logics; though formulated as a theory of functions and classes of expressions, FS0 is a conservative extension of PRA. The aims of this work are (i)conceptual, (ii)pedagogical and (iii)practical. The system FS0 serves under (i)and (ii)as a theoretical framework for the formalization of metamathematics. The general approach (...) may be used under (iii)for the computer implementation of logics. In all cases, the work aims to make the details manageable in a natural and direct way. (shrink)