Ali Enayat had asked whether two halves of Disjunctive Correctness ([Formula: see text]) for the compositional truth predicate are conservative over Peano Arithmetic (PA). In this paper, we show that the principle “every true disjunction has a true disjunct” is equivalent to bounded induction for the compositional truth predicate and thus it is not conservative. On the other hand, the converse implication “any disjunction with a true disjunct is true” can be conservatively added to [Formula: see text]. The methods introduced (...) here allow us to give a direct nonconservativeness proof for [Formula: see text]. (shrink)

By a well-known result of Kotlarski et al., first-order Peano arithmetic \ can be conservatively extended to the theory \ of a truth predicate satisfying compositional axioms, i.e., axioms stating that the truth predicate is correct on atomic formulae and commutes with all the propositional connectives and quantifiers. This result motivates the general question of determining natural axioms concerning the truth predicate that can be added to \ while maintaining conservativity over \. Our main result shows that conservativity fails even (...) for the extension of \ obtained by the seemingly weak axiom of disjunctive correctness \ that asserts that the truth predicate commutes with disjunctions of arbitrary finite size. In particular, \ implies \\). Our main result states that the theory \ coincides with the theory \ obtained by adding \-induction in the language with the truth predicate. This result strengthens earlier work by Kotlarski and Cieśliński. For our proof we develop a new general form of Visser’s theorem on non-existence of infinite descending chains of truth definitions and prove it by reduction to Gödel’s second incompleteness theorem, rather than by using the Visser–Yablo paradox, as in Visser’s original proof. (shrink)

The prevalent interpretation of Gödel’s Second Theorem states that a sufficiently adequate and consistent theory does not prove its consistency. It is however not entirely clear how to justify this informal reading, as the formulation of the underlying mathematical theorem depends on several arbitrary formalisation choices. In this paper I examine the theorem’s dependency regarding Gödel numberings. I introducedeviantnumberings, yielding provability predicates satisfying Löb’s conditions, which result in provable consistency sentences. According to the main result of this paper however, these (...) “counterexamples” do not refute the theorem’s prevalent interpretation, since once a natural class ofadmissiblenumberings is singled out, invariance is maintained. (shrink)

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)

It is well-known that natural axiomatic theories are well-ordered by consistency strength. However, it is possible to construct descending chains of artificial theories with respect to consistency strength. We provide an explanation of this well-orderedness phenomenon by studying a coarsening of the consistency strength order, namely, the$\Pi ^1_1$reflection strength order. We prove that there are no descending sequences of$\Pi ^1_1$sound extensions of$\mathsf {ACA}_0$in this ordering. Accordingly, we can attach a rank in this order, which we call reflection rank, to any$\Pi (...) ^1_1$sound extension of$\mathsf {ACA}_0$. We prove that for any$\Pi ^1_1$sound theoryTextending$\mathsf {ACA}_0^+$, the reflection rank ofTequals the$\Pi ^1_1$proof-theoretic ordinal ofT. We also prove that the$\Pi ^1_1$proof-theoretic ordinal of$\alpha $iterated$\Pi ^1_1$reflection is$\varepsilon _\alpha $. Finally, we use our results to provide straightforward well-foundedness proofs of ordinal notation systems based on reflection principles. (shrink)

We prove that the theory of the extensional compositional truth predicate for the language of arithmetic with \Delta 0 -induction scheme for the truth predicate and the full arithmetical induction scheme is not conservative over Peano Arithmetic. In addition, we show that a slightly modified theory of truth actually proves the global reflection principle over the base theory.

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 investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics (i.e., which part is equiconsistent with$\textbf {PRA}$or consistent provably in$\textbf {PRA}$) already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them (...) are:(i)fan theorem for decidable fans but arbitrary bars;(ii)continuity principle and the axiom of choice both for arbitrary formulae; and(iii)$\Sigma _2$induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO (except the choice along functions); but that limited principle of omniscience LPO makes the situation completely classical. (shrink)

Self-reference has played a prominent role in the development of metamathematics in the past century, starting with Gödel’s first incompleteness theorem. Given the nature of this and other results in the area, the informal understanding of self-reference in arithmetic has sufficed so far. Recently, however, it has been argued that for other related issues in metamathematics and philosophical logic a precise notion of self-reference and, more generally, reference is actually required. These notions have been so far elusive and are surrounded (...) by an aura of scepticism that has kept most philosophers away. In this paper I suggest we shouldn’t give up all hope. First, I introduce the reader to these issues. Second, I discuss the conditions a good notion of reference in arithmetic must satisfy. Accordingly, I then introduce adequate notions of reference for the language of first-order arithmetic, which I show to be fruitful for addressing the aforementioned issues in metamathematics. (shrink)

The conservativeness argument poses a dilemma to deflationism about truth, according to which a deflationist theory of truth must be conservative but no adequate theory of truth is conservative. The debate on the conservativeness argument has so far been framed in a specific formal setting, where theories of truth are formulated over arithmetical base theories. I will argue that the appropriate formal setting for evaluating the conservativeness argument is provided not by theories of truth over arithmetic but by those over (...) subject matters ‘richer’ than arithmetic, such as set theory. The move to this new formal setting provides deflationists with better defence and brings a broader perspective to the debate. (shrink)

A crucial part of the contemporary interest in logicism in the philosophy of mathematics resides in its idea that arithmetical knowledge may be based on logical knowledge. Here an implementation of this idea is considered that holds that knowledge of arithmetical principles may be based on two things: (i) knowledge of logical principles and (ii) knowledge that the arithmetical principles are representable in the logical principles. The notions of representation considered here are related to theory-based and structure-based notions of representation (...) from contemporary mathematical logic. It is argued that the theory-based versions of such logicism are either too liberal (the plethora problem) or are committed to intuitively incorrect closure conditions (the consistency problem). Structure-based versions must on the other hand respond to a charge of begging the question (the circularity problem) or explain how one may have a knowledge of structure in advance of a knowledge of axioms (the signature problem). This discussion is significant because it gives us a better idea of what a notion of representation must look like if it is to aid in realizing some of the traditional epistemic aims of logicism in the philosophy of mathematics. (shrink)

This paper attempts to address the question what logical strength theories of truth have by considering such questions as: If you take a theory T and add a theory of truth to it, how strong is the resulting theory, as compared to T? Once the question has been properly formulated, the answer turns out to be about as elegant as one could want: Adding a theory of truth to a finitely axiomatized theory T is more or less equivalent to a (...) kind of abstract consistency statement. A large part of the interest of the paper lies in the way syntactic theories are 'disentangled' from object theories. (shrink)

This paper attempts to address the question what logical strength theories of truth have by considering such questions as: If you take a theory T and add a theory of truth to it, how strong is the resulting theory, as compared to T? It turns out that, in a wide range of cases, we can get some nice answers to this question, but only if we work in a framework that is somewhat different from those usually employed in discussions of (...) axiomatic theories of truth. These results are then used to address a range of philosophical questions connected with truth, such as what Tarski meant by "essential richness" and the so-called conservativeness argument against deflationism. -/- This draft dates from about 2009, with some significant updates having been made around 2011. Around then, however, I decided that the paper was becoming unmanageable and that I was trying to do too many things in it. I have therefore exploded the paper into several pieces, which will be published separately. These include "Disquotationalism and the Compositional Principles", "The Logical Strength of Compositional Principles", "Consistency and the Theory of Truth", and "What Is Essential Richness?" You should probably read those instead, since this draft remains a bit of a mess. Terminology and notation are inconsistent, and some of the proofs aren't quite right. So, caveat lector. I make it public only because it has been cited in a few places now. (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)

This article bears on four topics: observational predicates and phenomenal properties, vagueness, strict finitism as a philosophy of mathematics, and the analysis of feasible computability. It is argued that reactions to strict finitism point towards a semantics for vague predicates in the form of nonstandard models of weak arithmetical theories of the sort originally introduced to characterize the notion of feasibility as understood in computational complexity theory. The approach described eschews the use of nonclassical logic and related devices like degrees (...) of truth or supervaluation. Like epistemic approaches to vagueness, it may thus be smoothly integrated with the use of classical model theory as widely employed in natural language semantics. But unlike epistemicism, the described approach fails to imply either the existence of sharp boundaries or the failure of tolerance for soritical predicates. Applications ofmeasurement theory(in the sense of Krantz, Luce, Suppes, & Tversky (1971)) to vagueness in the nonstandard setting are also explored. (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)

We show that the theory ATR 0 is equivalent to a second-order generalization of the theory $\widehat{ID}_{ . As a result, ATR 0 is conservative over $\widehat{ID}_{ for arithmetic sentences, though proofs in ATR 0 can be much shorter than their $\widehat{ID}_{ counterparts.

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)

By a classical result of Kotlarski, Krajewski and Lachlan, pathological satisfaction classes can be constructed for countable, recursively saturated models of Peano arithmetic. In this paper we consider the question of whether the pathology can be eliminated; we ask in effect what generalities involving the notion of truth can be obtained in a deflationary truth theory (a theory of truth which is conservative over its base). It is shown that the answer depends on the notion of pathology we adopt. It (...) turns out in particular that a certain natural closure condition imposed on a satisfaction class—namely, closure of truth under sentential proofs—generates a nonconservative extension of a syntactic base theory (Peano arithmetic). (shrink)

The primary purpose of this note is to demonstrate that predicative Frege arithmetic naturally interprets certain weak but non-trivial arithmetical theories. It will take almost as long to explain what this means and why it matters as it will to prove the results.

The knower paradox states that the statement ‘We know that this statement is false’ leads to inconsistency. This article presents a fresh look at this paradox and some well-known solutions from the literature. Paul Égré discusses three possible solutions that modal provability logic provides for the paradox by surveying and comparing three different provability interpretations of modality, originally described by Skyrms, Anderson, and Solovay. In this article, some background is explained to clarify Égré’s solutions, all three of which hinge on (...) intricacies of provability logic and its arithmetical interpretations. To check whether Égré’s solutions are satisfactory, we use the criteria for solutions to paradoxes defined by Susan Haack and we propose some refinements of them. This article aims to describe to what extent the knower paradox can be solved using provability logic and to what extent the solutions proposed in the literature satisfy Haack’s criteria. Finally, the article offers some reflections on the relation between knowledge, proof, and provability, as inspired by the knower paradox and its solutions. (shrink)

This paper presents a systematic study of the prehistory of the traditional subsystems of second-order arithmetic that feature prominently in the reverse mathematics program of Friedman and Simpson. We look in particular at: (i) the long arc from Poincar\'e to Feferman as concerns arithmetic definability and provability, (ii) the interplay between finitism and the formalization of analysis in the lecture notes and publications of Hilbert and Bernays, (iii) the uncertainty as to the constructive status of principles equivalent to Weak K\"onig's (...) Lemma, and (iv) the large-scale intellectual backdrop to arithmetical transfinite recursion in descriptive set theory and its effectivization by Borel, Lusin, Addison, and others. (shrink)

We show that \, the basic theory of bounded arithmetic corresponding to the complexity class \, proves the \ axiom expressing the totality of iterated multiplication satisfying its recursive definition, by formalizing a suitable version of the \ iterated multiplication algorithm by Hesse, Allender, and Barrington. As a consequence, \ can also prove the integer division axiom, and the \-translation of induction and minimization for sharply bounded formulas. Similar consequences hold for the related theories \ and \. As a side (...) result, we also prove that there is a well-behaved \ definition of modular powering in \\). (shrink)

We show that $$ VTC ^0$$, the basic theory of bounded arithmetic corresponding to the complexity class $$\mathrm {TC}^0$$, proves the $$ IMUL $$ axiom expressing the totality of iterated multiplication satisfying its recursive definition, by formalizing a suitable version of the $$\mathrm {TC}^0$$ iterated multiplication algorithm by Hesse, Allender, and Barrington. As a consequence, $$ VTC ^0$$ can also prove the integer division axiom, and (by our previous results) the $$ RSUV $$ -translation of induction and minimization for sharply (...) bounded formulas. Similar consequences hold for the related theories $$\Delta ^b_1\text{- } CR $$ and $$C^0_2$$. As a side result, we also prove that there is a well-behaved $$\Delta _0$$ definition of modular powering in $$I\Delta _0+ WPHP (\Delta _0)$$. (shrink)

In his previous work, the author has introduced the axiom schema of inductive dichotomy, a weak variant of the axiom schema of inductive definition, and used this schema for elementary ) positive operators to separate open and clopen determinacies for those games in which two players make choices from infinitely many alternatives in various circumstances. Among the studies on variants of inductive definitions for bounded ) positive operators, the present article investigates inductive dichotomy for these operators, and applies it to (...) constructive investigations of variants of determinacy statements for those games in which the players make choices from only finitely many alternatives. As a result, three formulations of open determinacy, that are all classically equivalent with each other, are equivalent to three different semi-classical principles, namely Markov’s Principle, Lesser Limited Principle of Omniscience and Limited Principle of Omniscience, over a suitable constructive base theory that proves clopen determinacy. Open and clopen determinacies for these games are thus separated. Some basic results on variants of inductive definitions for \ positive operators will also be given. (shrink)

In the paper we investigate typed axiomatizations of the truth predicate in which the axioms of truth come with a built-in, minimal and self-sufficient machinery to talk about syntactic aspects of an arbitrary base theory. Expanding previous works of the author and building on recent works of Albert Visser and Richard Heck, we give a precise characterization of these systems by investigating the strict relationships occurring between them, arithmetized model constructions in weak arithmetical systems and suitable set existence axioms. The (...) framework considered will give rise to some methodological remarks on the construction of truth theories and provide us with a privileged point of view to analyze the notion of truth arising from compositional principles in a typed setting. (shrink)

This is a critical analysis of the first part of Go¨del’s 1951 Gibbs lecture on certain philosophical consequences of the incompleteness theorems. Go¨del’s discussion is framed in terms of a distinction between objective mathematics and subjective mathematics, according to which the former consists of the truths of mathematics in an absolute sense, and the latter consists of all humanly demonstrable truths. The question is whether these coincide; if they do, no formal axiomatic system (or Turing machine) can comprehend the mathematizing (...) potentialities of human thought, and, if not, there are absolutely unsolvable mathematical problems of diophantine form. (shrink)

Propositional proof complexity is the study of the sizes of propositional proofs, and more generally, the resources necessary to certify propositional tautologies. Questions about proof sizes have connections with computational complexity, theories of arithmetic, and satisfiability algorithms. This is article includes a broad survey of the field, and a technical exposition of some recently developed techniques for proving lower bounds on proof sizes.

Is a logicist bound to the claim that as a matter of analytic truth there is an actual infinity of objects? If Hume’s Principle is analytic then in the standard setting the answer appears to be yes. Hodes’s work pointed to a way out by offering a modal picture in which only a potential infinity was posited. However, this project was abandoned due to apparent failures of cross-world predication. We re-explore this idea and discover that in the setting of the (...) potential infinite one can interpret first-order Peano arithmetic, but not second-order Peano arithmetic. We conclude that in order for the logicist to weaken the metaphysically loaded claim of necessary actual infinities, they must also weaken the mathematics they recover. (shrink)

In this paper, we investigate the phenomenon ofspeed-upin the context of theories of truth. We focus on axiomatic theories of truth extending Peano arithmetic. We are particularly interested on whether conservative extensions of PA have speed-up and on how this relates to a deflationist account. We show that disquotational theories have no significant speed-up, in contrast to some compositional theories, and we briefly assess the philosophical implications of these results.

In this paper we study the idea of theories with containers, like sets, pairs, sequences. We provide a modest framework to study such theories. We prove two concrete results. First, we show that first-order theories of finite signature that have functional non-surjective ordered pairing are definitionally equivalent to extensions in the same language of the basic theory of non-surjective ordered pairing. Second, we show that a first-order theory of finite signature is sequential (is a theory of sequences) iff it is (...) definitionally equivalent to an extension in the same language of a system of weak set theory called WS. (shrink)

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property.

We determine the modal logic of fixed-point models of truth and their axiomatizations by Solomon Feferman via Solovay-style completeness results. Given a fixed-point model $\mathcal {M}$, or an axiomatization S thereof, we find a modal logic M such that a modal sentence $\varphi $ is a theorem of M if and only if the sentence $\varphi ^*$ obtained by translating the modal operator with the truth predicate is true in $\mathcal {M}$ or a theorem of S under all such translations. (...) To this end, we introduce a novel version of possible worlds semantics featuring both classical and nonclassical worlds and establish the completeness of a family of noncongruent modal logics whose internal logic is nonclassical with respect to this semantics. (shrink)

Computationalism holds that our grasp of notions like ‘computable function’ can be used to account for our putative ability to refer to the standard model of arithmetic. Tennenbaum's Theorem has been repeatedly invoked in service of this claim. I will argue that not only do the relevant class of arguments fail, but that the result itself is most naturally understood as having the opposite of a reference-fixing effect — i.e., rather than securing the determinacy of number-theoretic reference, Tennenbaum's Theorem points (...) towards a sense in which portions of our computational vocabulary should be regarded as model-relative. (shrink)

In comparing classical and non-classical solutions to the semantic paradoxes arguments relying on strength have been influential. In this paper I argue that non-classical solutions should preserve the proof-theoretic strength of classical solutions. Leitgeb’s logic of HYPE is then presented as an interesting possibility to strengthen FDE with a suitable conditional. It is shown that HYPE allows for a non-classical Kripkean theory of truth, called KFL, that is strong enough for the relevant purposes and has additional attractive properties.

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)

After some generalities about connections between functions and relations in Sections 1 and 2 recalls the possibility of taking the semantic values of ‐ary Boolean connectives as ‐ary relations among truth‐values rather than as ‐ary truth functions. Section 3, the bulk of the paper, looks at correlates of these truth‐value relations as applied to formulas, and explores in a preliminary way how their properties are related to the properties of “logical relations” among formulas such as equivalence, implication (entailment) and contrariety (...) (logical incompatibility), concentrating for illustrative purposes on binary logical relations such as those just listed. To avoid an excess of footnotes, some points have been deferred to an Appendix as “Longer Notes”. (shrink)

In this paper we show how to interpret Robinson’s arithmetic Q and the theory R of Tarski, Mostowski, and Robinson as theories of cardinals in very weak theories of relations over a domain.

We study the effective and proof-theoretic content of the polarized Ramsey’s theorem, a variant of Ramsey’s theorem obtained by relaxing the definition of homogeneous set. Our investigation yields a new characterization of Ramsey’s theorem in all exponents, and produces several combinatorial principles which, modulo bounding for ${\Sigma^0_2}$ formulas, lie (possibly not strictly) between Ramsey’s theorem for pairs and the stable Ramsey’s theorem for pairs.

Let us recall that Raphael Robinson's Arithmetic Q is an axiom system that differs from Peano Arithmetic essentially by containing no Induction axioms [13], [18]. We will generalize the semantic-tableaux version of the Second Incompleteness Theorem almost to the level of System Q. We will prove that there exists a single rather long Π 1 sentence, valid in the standard model of the Natural Numbers and denoted as V, such that if α is any finite consistent extension of Q + (...) V then α will be unable to prove its Semantic Tableaux consistency. The same result will also apply to axiom systems α with infinite cardinality when these infinite-sized axiom systems satisfy a minor additional constraint, called the Conventional Encoding Property. Our formalism will also imply that the semantic-tableaux version of the Second Incompleteness Theorem generalizes for the axiom system IΣ 0 , as well as for all its natural extensions. (This answers an open question raised twenty years ago by Paris and Wilkie [15].). (shrink)

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property.

We show that many principles of first-order arithmetic, previously only known to lie strictly between [Formula: see text]-induction and [Formula: see text]-induction, are equivalent to the well-foundedness of [Formula: see text]. Among these principles are the iteration of partial functions of Hájek and Paris, the bounded monotone enumerations principle by Chong, Slaman, and Yang, the relativized Paris–Harrington principle for pairs, and the totality of the relativized Ackermann–Péter function. With this we show that the well-foundedness of [Formula: see text] is a (...) far more widespread than usually suspected. Further, we investigate the [Formula: see text]-iterated version of the bounded monotone iterations principle, and show that it is equivalent to the well-foundedness of the -height [Formula: see text]-tower [Formula: see text]. (shrink)

In Cieśliński (J Philos Logic 39:325–337, 2010), Cieśliński asked whether compositional truth theory with the additional axiom that all propositional tautologies are true is conservative over Peano Arithmetic. We provide a partial answer to this question, showing that if we additionally assume that truth predicate agrees with arithmetical truth on quantifier-free sentences, the resulting theory is as strong as $$\Delta _0$$ Δ 0 -induction for the compositional truth predicate, hence non-conservative. On the other hand, it can be shown with a (...) routine argument that the principle of quantifier-free correctness is itself conservative. (shrink)

One way to study and understand the notion of truth is to examine principles that we are willing to associate with truth, often because they conform to a pre-theoretical or to a semi-formal characterization of this concept. In comparing different collections of such principles, one requires formally precise notions of inter-theoretic reduction that are also adequate to compare these conceptual aspects. In this work I study possible ways to make precise the relation of conceptual equivalence between notions of truth associated (...) with collections of principles of truth. In doing so, I will consider refinements and strengthenings of the notion of relative truth-definability proposed by Fujimoto (2010): in particular I employ suitable variants of notions of equivalence of theories considered in Visser (2006) and Friedman & Visser (2014) to show that there are better candidates than mutual truth-definability for the role of sufficient condition for conceptual equivalence between the semantic notions associated with the theories. In the concluding part of the paper, I extend the techniques introduced in the first and show that there is a precise sense in which ramified truth (either disquotational or compositional) does not correspond to iterations of comprehension. (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)

We describe a model-theoretic approach to ordinal analysis via the finite combinatorial notion of an α-large set of natural numbers. In contrast to syntactic approaches that use cut elimination, this approach involves constructing finite sets of numbers with combinatorial properties that, in nonstandard instances, give rise to models of the theory being analyzed. This method is applied to obtain ordinal analyses of a number of interesting subsystems of first- and second-order arithmetic.

It is well known that Tarski proved a result which can be stated roughly as: no sufficiently rich, consistent, classical language can contain its own truth definition. Tarski's way around this problem is to deal with two languages at a time, an object language for which we are defining truth and a metalanguage in which the definition occurs. An obvious question then is: under what conditions can we construct a definition of truth for a given object language. Tarski claims that (...) it is necessary and sufficient that the metalanguage be "essentially richer". Our contention, put bluntly, is that this claim deserves more scrutiny from philosophers than it usually gets and in fact is false unless "essentially richer" means nothing else than "sufficient to contain a truth definition for the object language.". (shrink)