We employ the lens provided by formal truth theory to study axiomatizations of Peano Arithmetic ${\textsf {(PA)}}$. More specifically, let Elementary Arithmetic ${\textsf {(EA)}}$ be the fragment $\mathsf {I}\Delta _0 + \mathsf {Exp}$ of ${\textsf {PA}}$, and let ${\textsf {CT}}^-[{\textsf {EA}}]$ be the extension of ${\textsf {EA}}$ by the commonly studied axioms of compositional truth ${\textsf {CT}}^-$. We investigate both local and global properties of the family of first order theories of the form ${\textsf {CT}}^-[{\textsf (...) {EA}}] +\alpha $, where $\alpha $ is a particular way of expressing “ ${\textsf {PA}}$ is true” (using the truth predicate). Our focus is dominantly on two types of axiomatizations, namely: (1) schematic axiomatizations that are deductively equivalent to ${\textsf {PA}}$ and (2) axiomatizations that are proof-theoretically equivalent to the canonical axiomatization of ${\textsf {PA}}$. (shrink)

Let M be a model of first order Peano arithmetic and I an initial segment of M that is closed under multiplication. LetM0 be the {0, 1,+}-reduct ofM. We show that there is another model N of PA that is also an expansion of M0 such that a · Ma = a · Na if and only if a ∈ I for all a ∈ M.

In the Handbook of Mathematical Logic, the Paris-Harrington variant of Ramsey's theorem is celebrated as the first result of a long ‘search’ for a purely mathematical incompleteness result in first-order Peano arithmetic. This paper questions the existence of any such search and the status of the Paris-Harrington result as the first mathematical incompleteness result. In fact, I argue that Gentzen gave the first such result, and that it was restated by Goodstein in a (...) number-theoretic form. (shrink)

Theorem 1. If T is a sound formalized theory whose language contains the language of basic arithmetic, then there will be a true sentence GT of basic arithmetic such that T ￿ GT and ￿ ¬GT, so T must be negation incomplete.

The existence of non-standard models of first-order Peano-Arithmetic (PA) threatens to undermine the claim of the moderate mathematical realist that non-mysterious access to the natural number structure is possible on the basis of our best arithmetical theories. The move to logics stronger than FOL is denied to the moderate realist on the grounds that it merely shifts the indeterminacy “one level up” into the meta-theory by, illegitimately, assuming the determinacy of the notions needed to formulate such (...) logics. This paper argues that the challenge can be met. We show how the quantifier “there are infinitely many” can be uniquely determined in a naturalistically acceptable fashion and thus be used in the formulation of a theory of arithmetic. We compare the approach pursued here with Field’s justification of the same device and the popular strategy of invoking a second-order formalism, and argue that it is more robust than either of the alternative proposals. (shrink)

For α less than ε0 let $N\alpha$ be the number of occurrences of ω in the Cantor normal form of α. Further let $\mid n \mid$ denote the binary length of a natural number n, let $\mid n\mid_h$ denote the h-times iterated binary length of n and let inv(n) be the least h such that $\mid n\mid_h \leq 2$ . We show that for any natural number h first order Peano arithmetic, PA, does not prove the (...) following sentence: For all K there exists an M which bounds the lengths n of all strictly descending sequences $\langle \alpha_0, ..., \alpha_n\rangle$ of ordinals less than ε0 which satisfy the condition that the Norm $N\alpha_i$ of the i-th term αi is bounded by $K + \mid i \mid \cdot \mid i\mid_h$ . As a supplement to this (refined Friedman style) independence result we further show that e.g., primitive recursive arithmetic, PRA, proves that for all K there is an M which bounds the length n of any strictly descending sequence $\langle \alpha_0,..., \alpha_n\rangle$ of ordinals less than ε0 which satisfies the condition that the Norm $N\alpha_i$ of the i-th term αi is bounded by $K + \mid i \mid\cdot inv(i)$ . The proofs are based on results from proof theory and techniques from asymptotic analysis of Polya-style enumerations. Using results from Otter and from Matou $\breve$ ek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856... (shrink)

In this paper we study the model theory of extensions of models of first-order Peano Arithmetic by means of the arithmetized completeness theorem applied to a definable complete extension of PA in the original model. This leads us to many interesting model theoretic properties equivalent to reflection principles and ω-consistency, and these properties together with the associated first-order schemes extending PA are studied.

In this paper we consider three potential simplifications to a result of Solovay’s concerning the Turing degrees of nonstandard models of arbitrary completions of first-order Peano Arithmetic (PA). Solovay characterized the degrees of nonstandard models of completions T of PA, showing that they are the degrees of sets X such that there is an enumeration R ≤T X of an “appropriate” Scott set and there is a family of functions (tn)n∈ω, ∆0 n(X) uniformly in n, such (...) that lim tn(s) s→∞. (shrink)

The parameter-free part $$\textbf{PA}_2^*$$ of $$\textbf{PA}_2$$, second order Peano arithmetic, is considered. We make use of a product/iterated Sacks forcing to define an $$\omega $$ -model of $$\textbf{PA}_2^*+ \textbf{CA}(\Sigma ^1_2)$$, in which an example of the full Comprehension schema $$\textbf{CA}$$ fails. Using Cohen’s forcing, we also define an $$\omega $$ -model of $$\textbf{PA}_2^*$$, in which not every set has its complement, and hence the full $$\textbf{CA}$$ fails in a rather elementary way.

In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic PA one can find ordinal recursive functionals Φ A of order type 0 which realize the Herbrand normal form A H of A. Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and (...) cut-elimination were found. These proofs however do not carry out the no-counterexample interpretation as a local proof interpretation and don't respect the modus ponens on the level of the no-counterexample interpretation of formulas A and A → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and--at least not constructively-- (γ) which are part of the definition of an 'interpretation of a formal system' as formulated in [15]. In this paper we determine the complexity of the no-counterexample interpretation of the modus ponens rule for (i) PA-provable sentences, (ii) for arbitrary sentences A, B ∈ L(PA) uniformly in functionals satisfying the no-counterexample interpretation of (prenex normal forms of) A and A → B, and (iii) for arbitrary A, B ∈ L(PA) pointwise in given α( 0 ) -recursive functionals satisfying the no-counterexample interpretation of A and A → B. This yields in particular perspicuous proofs of new uniform versions of the conditions (γ), (δ). Finally we discuss a variant of the concept of an interpretation presented in [17] and show that it is incomparable with the concept studied in [15], [16]. In particular we show that the no-counterexample interpretation of PA n by α( n (ω))-recursive functionals (n ≥ 1) is an interpretation in the sense of [17] but not in the sense of [15] since it violates the condition (δ). (shrink)

The parameter-free part \(\textbf{PA}_2^*\) of \(\textbf{PA}_2\), second order Peano arithmetic, is considered. We make use of a product/iterated Sacks forcing to define an \(\omega \) -model of \(\textbf{PA}_2^*+ \textbf{CA}(\Sigma ^1_2)\), in which an example of the full Comprehension schema \(\textbf{CA}\) fails. Using Cohen’s forcing, we also define an \(\omega \) -model of \(\textbf{PA}_2^*\), in which not every set has its complement, and hence the full \(\textbf{CA}\) fails in a rather elementary way.

For every sequence |p n } n of formulas of Peano ArithmeticPA with, every formulaA of the first-order theory diagonalizable algebras, we associate a formula 0 A, called the value ofA inPA with respect to the interpretation. We show that, ifA is true in every diagonalizable algebra, then, for every, 0 A is a theorem ofPA.

We propose a rudimentary formal framework for reasoning about recursion equations over inductively generated data. Our formalism admits all equational programs , and yet singles out none. While being simple, this framework has numerous extensions and applications. Here we lay out the basic concepts and definitions; show that the deductive power of our formalism is similar to that of Peano's Arithmetic; prove a strong normalization theorem; and exhibit a mapping from natural deduction derivations to an applied λ -calculus, (...) à la Curry–Howard, which provides a transparent proof of Gödel's result that the provably recursive functions of PA are definable by primitive recursion in finite types. Also of interest is the extent, uncommon among similar constructions, to which our mapping is oblivious to first order terms, including first order quantification and equality. Additional applications and extensions of the method will be presented in sequel papers. In particular, the methodology introduced here lends itself to systematic links between natural sub-formalisms and computational complexity classes. Since these sub-formalisms are largely transparent, allowing one to reason formally in the full system while leaving to automatic software tools the task of verifying that restrictions are complied with, the framework is particularly attractive for the development of Feasible Mathematics. (shrink)

In this paper, I will argue from a historical perspective that Gentzen’s 1935 consistency proof of 1st order Peano Arithmetic PA principally aimed to give a finitist interpretation of implication and this aspect of the 1935 proof emerged as the attempt to cope with the non-finiteness in BHK-interpretation of implication. My argument consists of two parts. First, I will explain that the fundamental idea of the 1935 proof is to show the soundness of PA on some (...) finitist interpretation and Gentzen had attempted to use BHK-interpretation as such an interpretation. It is claimed that he eventually thought that there is a ‘circularity’ which is due to the non-finiteness of BHK-interpretation of implication, so it cannot be used as a finitist interpretation. Secondly, I will argue that the principal aim of the 1935 proof is to give his own finitist interpretation of implication which avoids such a ‘circularity’. Finally, this paper’s conclusion and an open question are presented. (shrink)

This paper develops the philosophy and technology needed for adding a supremum operator to the interpretability logic ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document} of Peano Arithmetic. It is well-known that any theories extending PA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {PA}$$\end{document} have a supremum in the interpretability ordering. While provable in PA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {PA}$$\end{document}, this fact is not reflected in the theorems of (...) the modal system ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document}, due to limited expressive power. Our goal is to enrich the language of ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document} by adding to it a new modality for the interpretability supremum. We explore different options for specifying the exact meaning of the new modality. Our final proposal involves a unary operator, the dual of which can be seen as a provability predicate satisfying the axioms of the provability logic GL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {GL}$$\end{document}. (shrink)

Let= {0,1, +,·,<} be the usual first-order language of arithmetic. We show that Peano arithmetic is the least first-order-theory containingIΔ0+ exp such that every complete extensionTof it has a countable modelKsatisfying(i)Khas no proper elementary substructures, and(ii) wheneverL≻Kis a countable elementary extension there isandsuch that.Other model-theoretic conditions similar to (i) and (ii) are also discussed and shown to characterize Peano arithmetic.

This paper is mainly concerned with proof-theoretic analysis of some second-order systems of explicit mathematics with a non-constructive minimum operator. By introducing axioms for variable types we extend our first-order theory BON to the elementary explicit type theory EET and add several forms of induction as well as axioms for μ. The principal results then state: EET plus set induction is proof-theoretically equivalent to Peano arithmetic PA <0).

It is often remarked that first-order Peano Arithmetic is non-categorical but deductively well-behaved, while second-order Peano Arithmetic is categorical but deductively ill-behaved. This suggests that, when it comes to axiomatizations of mathematical theories, expressive power and deductive power may be orthogonal, mutually exclusive desiderata. In this paper, I turn to Hintikka’s :69–90, 1989) distinction between descriptive and deductive approaches in the foundations of mathematics to discuss the implications of this observation for the (...) class='Hi'>first-order logic versus second-order logic divide. The descriptive approach is illustrated by Dedekind’s ‘discovery’ of the need for second-order concepts to ensure categoricity in his axiomatization of arithmetic; the deductive approach is illustrated by Frege’s Begriffsschrift project. I argue that, rather than suggesting that any use of logic in the foundations of mathematics is doomed to failure given the impossibility of combining the descriptive approach with the deductive approach, what this apparent predicament in fact indicates is that the first-order versus second-order divide may be too crude to investigate what an adequate axiomatization of arithmetic should look like. I also conclude that, insofar as there are different, equally legitimate projects one may engage in when working on the foundations of mathematics, there is no such thing as the One True Logic for this purpose; different logical systems may be adequate for different projects. (shrink)

The relative strengths of first-order theories axiomatized by transfinite induction, for ordinals less-than 0, and formulas restricted in quantifier complexity, is determined. This is done, in part, by describing the provably recursive functions of such theories. Upper bounds for the provably recursive functions are obtained using model-theoretic techniques. A variety of additional results that come as an application of such techniques are mentioned.

The theory PA(aa), which is Peano Arithmetic in the context of stationary logic, is shown to be consistent. Moreover, the first-order theory of the class of finitely determinate models of PA(aa) is characterized.

The shortest definition of a number by a first order formula with one free variable, where the notion of a formula defining a number extends a notion used by Boolos in a proof of the Incompleteness Theorem, is shown to be non computable. This is followed by an examination of the complexity of sets associated with this function.

This paper is devoted to the reconstruction of the implicit logic of Plato’s Par-menides. The reconstructed logic, F, makes it possible to form a new semi-intuitionistic system of logic of predicates, FN. The axioms of Peano Arithmetic (PA) and an axiom of infinity follow from FN. Therefore, FN can be seen as a new attempt at the realization of Frege’s logicist program. Some very strong systems can be seen as other variants of FN, e.g. Leśniewski’s ontology. The hypothesis (...) from Parmenides II contains proof of the existence of the two highest principles, i.e. the One and the Dyad, their mutual relationship, their relations to other things, and the reasoning regarding the mutual relationship follows some exact formal rules. Six types of Plato’s negation of a predicate are defined. The system is a first-order logic with non-classical negation of a predicate (local negation) that is non-definable by classical sentential negation. Therefore, the implicit logic of Plato’s Parmenides differs from classical syllogistics (formed in the Łukasiewicz’s style) as well as from the classical predicate calculus. (shrink)

By using a provability predicate of PA, we define ThmPA(M) as the set of theorems of PA in a modelMof PA. We say a modelMof PA is (1) illusory if ThmPA(M) ⊈ ThmPA(ℕ), (2) heterodox if ThmPA(M) ⊈ TA, (3) sane ifM⊨ ConPA, and insane if it is not sane, (4) maximally sane if it is sane and ThmPA(M) ⊆ ThmPA(N) implies ThmPA(M) = ThmPA(N) for every sane modelNof PA. We firstly show thatMis heterodox if and only if it is (...) illusory, and that ThmPA(M) ∩ TA ≠ ThmPA(ℕ) for any illusory modelM. Then we show that there exists a maximally sane model, every maximally sane model satisfies ¬ConPA+ConPA, and there exists a sane model of ¬ConPA+ConPAwhich is not maximally sane. We define that an insane model is (5) illusory by nature if its every initial segment being a nonstandard model of PA is illusory, and (6) going insane suddenly if its every initial segment being a sane model of PA is not illusory. We show that there exists a model of PA which is illusory by nature, and we prove the existence of a model of PA which is going insane suddenly. (shrink)

Among the main theorems obtained in mathematical logic in this century are the so called limitation theorems, i.e., the Löwenheim-Skolem theorem on the cardinality of models of first-order theories, Gödel’s incompleteness theorems and Tarski’s theorem on the undefinability of truth. Problems connected with the latter are the subject of this paper. In Section 1 we shall consider Tarski’s theorem. In particular the original formulation of it as well as some specifications will be provided. Next various meanings of the (...) notion of a satisfaction predicate will be studied. In Section 2 the problem of definability of the notion of truth, in particular of the notion of truth for the language of Peano arithmetic PA, will be discussed. It will be explicitly shown that the notion of satisfaction for the language of PA can be defined in a certain weak fragment of the second order arithmetic. Finally the axiomatic characterization of satisfaction and truth as well and its mathematical and philosophical meaning will be discussed. (shrink)

Let T 0?T 1 denote that each computable function, which is provable total in the first order theory T 0, is also provable total in the first order theory T 1. Te relation ? induces a degree structure on the sound finite Π2 extensions of EA (Elementary Arithmetic). This paper is devoted to the study of this structure. However we do not study the structure directly. Rather we define an isomorphic subrecursive degree structure <≤,?>, and (...) then we study <≤,?> by ubrecursive and computability-theoretic means. Furthermore, we introduce and investigate some operators on the degrees of <≤,?>. These operators corresponds to inferencerules in formal arithmetic. One operator corresponds to the Σ1 collection rule. Another operator corresponds to the Σ1 induction rule. (shrink)

The paper is concerned with the old conjecture that there are infinitely many twin primes. In the paper we show that this conjecture is true, that is, it is true in the standard model of arithmetic. The proof is based on Rasiowa–Sikorski Lemma. The key role are played by the derived notion of a Rasiowa–Sikorski set and the method of forcing adjusted to arbitrary first–order languages. This approach was developed in the papers Czelakowski [ 4, 5 ]. (...) The central idea consists in constructing an appropriate countable model \(\textbf{A}\) of Peano arithmetic by means of a Rasiowa–Sikorski set. This model validates the twin prime conjecture. Since \(\textbf{A}\) is elementarily equivalent to the standard model, the conjecture follows. Thus the standard model validates the twin primes conjecture. More generally, it is shown that de Polignac’s conjecture has a positive solution. The paper employs methods borrowed from the contemporary mathematical logic. Such a ’logical’ approach may be viewed as a useful addition to the dominant methodology in number theory based on mathematical analysis. (shrink)

We elaborate Weiermann-style phase transitions for well-partial-orderings (wpo) determined by iterated finite sequences under Higman-Friedman style embedding with Gordeev’s symmetric gap condition. For every d-times iterated wpo \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\left({\rm S}\text{\textsc{eq}}^{d}, \trianglelefteq _{d}\right)}$$\end{document} in question, d > 1, we fix a natural extension of Peano Arithmetic, \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${T \supseteq \sf{PA}}$$\end{document}, that proves the corresponding second-order sentence \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} (...) \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{WPO}\left({\rm S}{\textsc{eq}}^{d}, \trianglelefteq _{d}\right) }$$\end{document}. Having this we consider the following parametrized first-order slow well-partial-ordering sentence \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{d}, \trianglelefteq _{d}, r\right):}$$\end{document}\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\left( \forall K > 0 \right) \left( \exists M > 0\right) \left( \forall x_{0},\ldots,x_{M}\in {\rm S}\text{\textsc{eq}}^{d}\right)$$\end{document}\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\left( \left( \forall i\leq M\right) \left( \left| x_{i}\right| 1}$$\end{document} then \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{d}, \trianglelefteq _{d},r \right) }$$\end{document} is not provable in T.Moreover, by the well-known proof theoretic equivalences we can just as well replace T by PA or ACA0 and \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Delta _{1}^{1}\sf{CA}}$$\end{document}, if d = 2 and d = 3, respectively.In the limit case d → ∞ we replaceEFA-provably computable reals r by EFA-provably computable functions \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${f: \mathbb{N} \rightarrow \mathbb{R}_{+}}$$\end{document} and prove analogous theorems. (In the sequel we denote by \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathbb{R}_{+}}$$\end{document} the set of EFA-provably computable positive reals). In the basic case T = PA we strengthen the basic phase transition result by adding the following static threshold clause\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{2}, \trianglelefteq _{2}, 1\right)}$$\end{document} is still provable in T = PA (actually in EFA). Furthermore we prove the following dynamic threshold clauses which, loosely speaking are obtained by replacing the static threshold t by slowly growing functions 1α given by \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${1_{\alpha }\left( i\right)\,{:=}\,1+\frac{1}{H_{\alpha }^{-1}\left(i\right) }, H_{\alpha}}$$\end{document} being the familiar fast growing Hardy function and \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${H_{\alpha }^{-1}\left( i\right)\,{:=}\,\rm min \left\{ j \mid H_{\alpha } \left ( j\right) \geq i \right\}}$$\end{document} the corresponding slowly growing inversion. If \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\alpha < \varepsilon _{0}}$$\end{document}, then \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{2}, \trianglelefteq _{2}, 1_{\alpha}\right)}$$\end{document} is provable in T = PA. \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left( {\rm S}\text{\textsc{eq}}^{2}, \trianglelefteq _{2},1_{\varepsilon _{0}}\right)}$$\end{document} is not provable in T = PA. We conjecture that this pattern is characteristic for all \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${T\supseteq \sf{PA}}$$\end{document} under consideration and their proof-theoretical ordinals o (T ), instead of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\varepsilon _{0}}$$\end{document}. (shrink)

Shepherdson [14] showed that for a discrete ordered ring I, I is a model of IOpen iff I is an integer part of a real closed ordered field. In this paper, we consider integer parts satisfying PA. We show that if a real closed ordered field R has an integer part I that is a nonstandard model of PA (or even IΣ₄), then R must be recursively saturated. In particular, the real closure of I, RC (I), is recursively saturated. We (...) also show that if R is a countable recursively saturated real closed ordered field, then there is an integer part I such that R = RC(I) and I is a nonstandard model of PA. (shrink)

Let T be a first-order theory. A T-normal Kripke structure is one in which every world is a classical model of T. This paper gives a characterization of the intuitionistic theory T of sentences intuitionistically valid in all T-normal Kripke structures and proves the corresponding soundness and completeness theorems. For Peano arithmetic , the theory PA is a proper subtheory of Heyting arithmetic , so HA is complete but not sound for PA-normal Kripke structures.

The purpose of this paper is to formulate first-order Peano arithmetic within the resources of relevant logic, and to demonstrate certain properties of the system thus formulated. Striking among these properties are the facts that it is trivial that relevant arithmetic is absolutely consistent, but classical first-order Peano arithmetic is straightforwardly contained in relevant arithmetic. Under, I shall show in particular that 0 = 1 is a non-theorem of relevant (...) class='Hi'>arithmetic; this, of course, is exactly the formula whose unprovability was sought in the Hilbert program for proving arithmetic consistent. Under, I shall exhibit the requisite translation, drawing some Goedelian conclusions therefrom. Left open, however, is the critical problem whether Ackermann’s rule γ is admissible for theories of relevant arithmetic. The particular system of relevant Peano arithmetic featured in this paper shall be called R♯. Its logical base shall be the system R of relevant implication, taken in its first-order form RQ. Among other Peano arithmetics we shall consider here in particular the systems C♯, J♯, and RM3♯; these are based respectively on the classical logic C, the intuitionistic logic J, and the Sobocinski-Dunn semi-relevant logic RM3. And another feature of the paper will be the presentation of a system of natural deduction for R♯, along lines valid for first-order relevant theories in general. This formulation of R♯ makes it possible to construct relevantly valid arithmetical deductions in an easy and natural way; it is based on, but is in some respects more convenient than, the natural deduction formulations for relevant logics developed by Anderson and Belnap in Entailment. (shrink)

The incompleteness of formal systems for arithmetic has been a recognized fact of mathematics. The term “incompleteness” suggests that the formal system in question fails to offer a deduction which it ought to. This chapter focuses on the status of a formal system, Peano Arithmetic, and explores a viewpoint on which Peano Arithmetic occupies an intrinsic, conceptually well-defined region of arithmetical truth. The idea is that it consists of those truths which can be perceived directly (...) from the purely arithmetical content of a categorical conceptual analysis of the notion of natural number. The chapter explores its conceptual stability in light of the apparently destabilizing effect, through extensibility, of the phenomenon of incompleteness. It also offers heuristic and conceptual support for the viewpoint that Peano Arithmetic is the strongest natural first-order system for arithmetic, and that there is a sense in which it is complete with respect to purely arithmetical truth. (shrink)

By a theorem of R. Kaye, J. Paris and C. Dimitracopoulos, the class of the Πn+1-sentences true in the standard model is the only consistent Πn+1-theory which extends the scheme of induction for parameter free Πn+1-formulas. Motivated by this result, we present a systematic study of extensions of bounded quantifier complexity of fragments of first-order Peano Arithmetic. Here, we improve that result and show that this property describes a general phenomenon valid for parameter free schemes. As (...) a consequence, we obtain results on the quantifier complexity, finite axiomatizability and relative strength of schemes for Δn+1-formulas. (shrink)

Vardanyan’s Theorems [36, 37] state that $\mathsf {QPL}(\mathsf {PA})$ —the quantified provability logic of Peano Arithmetic—is $\Pi ^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge [38] generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The (...) system $\mathsf {QRC_1}$ was previously introduced by the authors [1] as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf {QRC_1}$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf {QRC_1}$ is the strictly positive fragment of $\mathsf {QGL}$ and a fragment of $\mathsf {QPL}(\mathsf {PA})$. (shrink)

We give a sufficient condition for a countable model M of PA to be expandable to an ω-model of AST with absolute Ω-orderings. The condition is in terms of saturation schemes or, equivalently, in terms of the ability of the model to code sequences which have some kind of definition in (M, ω). We also show that a weaker scheme of saturation leads to the existence of wellorderings of the model with nice properties. Finally, we answer affirmatively the question of (...) whether the intersection of all β-expansions of a β-expandable model M is the set RA(M, ω)--the ramified analytical hierarchy over (M, ω). The results are based on forcing constructions. (shrink)

It is well known that number theory can be interpreted in the usual set theories, e.g. ZF, NF and their extensions. The problem I posed for myself was to see if, conversely, a reasonably strong set theory could be interpreted in number theory. The reason I am interested in this problem is, simply, that number theory is more basic or more concrete than set theory, and hence a more concrete foundation for mathematics. A partial solution to the problem was accomplished (...) by WTN in [2], where it was shown that a predicative set theory could be interpreted in a natural extension of pure number theory, PN, (i.e. classical first-order Peano Arithmetic). In this paper, we go a step further by showing that a reasonably strong fragment of predicative set theory can be interpreted in PN itself. We then make an attempt to show how to develop predicative fragments of mathematics in PN.If one wishes to know what is meant by reasonably strong and fragment please read on. (shrink)

A number of authors have argued that Peano Arithmetic supplemented with a logical validity predicate is inconsistent in much the same manner as is PA supplemented with an unrestricted truth predicate. In this paper I show that, on the contrary, there is no genuine paradox of logical validity—a completely general logical validity predicate can be coherently added to PA, and the resulting system is consistent. In addition, this observation lead to a number of novel, and important, insights into (...) the nature of logical validity itself. (shrink)

We calculate the possible Scott ranks of countable models of Peano arithmetic. We show that no non-standard model can have Scott rank less than $\omega $ and that non-standard models of true arithmetic must have Scott rank greater than $\omega $. Other than that there are no restrictions. By giving a reduction via $\Delta ^{\mathrm {in}}_{1}$ bi-interpretability from the class of linear orderings to the canonical structural $\omega $ -jump of models of an arbitrary completion T of (...) $\mathrm {PA}$ we show that every countable ordinal $\alpha>\omega $ is realized as the Scott rank of a model of T. (shrink)

Since in Heyting Arithmetic all atomic formulas are decidable, a Kripke model for HA may be regarded classically as a collection of classical structures for the language of arithmetic, partially ordered by the submodel relation. The obvious question is then: are these classical structures models of Peano Arithmetic ? And dually: if a collection of models of PA, partially ordered by the submodel relation, is regarded as a Kripke model, is it a model of HA? Some (...) partial answers to these questions were obtained in [6], [3], [1] and [2]. Here we present some results in the same direction, announced in [7]. In particular, it is proved that the classical structures at the nodes of a Kripke model of HA must be models of IΔ1 and that the relation between these classical structures must be that of a Δ1-elementary submodel. MSC: 03F30, 03F55. (shrink)

In this paper the modal operator "x is provable in Peano Arithmetic" is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.

This paper offers an elementary proof that formal arithmetic is consistent. The system that will be proved consistent is a first-order theory R♯, based as usual on the Peano postulates and the recursion equations for + and ×. However, the reasoning will apply to any axiomatizable extension of R♯ got by adding classical arithmetical truths. Moreover, it will continue to apply through a large range of variation of the un- derlying logic of R♯, while on a (...) simple and straightforward translation, the classical first-order theory P♯ of Peano arithmetic turns out to be an exact subsystem of R♯. Since the reasoning is elementary, it is formalizable within R♯ itself; i.e., we can actually demonstrate within R♯ (or within P♯, if we care) a statement that, in a natural fashion, asserts the consistency of R♯ itself. The reader is unlikely to have missed the significance of the remarks just made. In plain English, this paper repeals Goedel’s famous second theorem. (That’s the one that asserts that sufficiently strong systems are inadequate to demonstrate their own consistency.) That theorem (or at least the significance usually claimed for it) was a mis- take—a subtle and understandable mistake, perhaps, but a mistake nonetheless. Accordingly, this paper reinstates the formal program which is often taken to have been blasted away by Goedel’s theorems— namely, the Hilbert program of demonstrating, by methods that everybody can recognize as effective and finitary, that intuitive mathematics is reliable. Indeed, the present consistency proof for arithmetic will be recognized as correct by anyone who can count to 3. (So much, indeed, for the claim that the reliability of arithmetic rests on transfinite induction up to ε0, and for the incredible mythology that underlies it.). (shrink)

My goal in this paper is, to tentatively sketch and try defend some observations regarding the ontological dignity of object references, as they may be used from within in a formalized language. -/- Hence I try to explore, what properties objects are presupposed to have, in order to enter the universe of discourse of an interpreted formalized language. -/- First I review Frege′s analysis of the logical structure of truth value definite sentences of scientific colloquial language, to draw (...) suggestions from his saturated vs. unsaturated sentence components paradigm. -/- Next try investigate, in how far reference to non pure math objects might allow for a role as argument of a truth value function. Object kinds to be considered are: common sense objects, technical objects, humanities object kinds (social, psychical, ...), objects of art, ... , be they abstract, concrete, or in this respect mixed objects. -/- Then have a comment on the just referenced label abstract objects. -/- Next try to get an idea wrt the ontological significance of the fact, that pure math objects and functions in some important classical cases can be uniquely defined by means of categorical theories. Here, in the course of my argument, I have a little corollary wrt the standard model of first order Peano arithmetic, reducing the epistemological significance of the existence of the non standard models. -/- Next, wrt a special concept of a formalized empirical theory, I care for whether the impure math objects and mixed objects described here, and complying best with truth value function mapping, are also reliable candidates for the ontological commitment of such theories: and discuss an alternative, which reduces the ontological significance of the universe of discourse of the theories intended models. -/- In the end I sum up what is - from my point of view - the status quo, according to my respective findings. (shrink)

SummaryAccording to Dummett's understanding of Frege, the sense of a denoting expression is a procedure for determining its denotation. The purpose of this article is to pursue this suggestion and develop a semi‐formal interpretation of Fregean sense for the special case of a first‐order language of arithmetic. In particular, we define the sense of each arithmetic expression to be a hypothetical process to determine the denoted number or truth value. The sense‐process is “hypothetical” in that the (...) senses of some expressions cannot be completed in a finite number of steps. The motivation for this work is to explicate an intensional notion of effectiveness in terms of the senses of function names. It is proposed, in particular, that an expression is effective if and only if its sense can be completed in a finite number of steps. It is shown that a function is computable if and only if it has an effective name.RésuméSelon la lecture que Dummet donne de Frege, le sens ?on;une expression consiste en une procédure pour déterminer sa dénotation. Le but de cet article est de développer cette suggestion par une interprétation semi‐formelle du sens frégéen dans le cas particulier ?on;un langage de premier ordre en arithmétique. En particulier, nous définissons comme sens de toute expression mathématique un procédé hypothétique pour déterminer le nombre dénoté ou la valeur de vérité. Le procédé créateur de sens est hypothetique en ce sens que les sens de certaines expressions ne peuvent pas être donnés en un nombre fini de pas. Le but de cette étude est ?on;expliciter une notion intensionnelle ?on;effectuabilite en termes de sens des noms de fonction. II est en particulier propose qu'une expression soit dite effectuable si et seulement si son sens peut être épuisé en un nombre fini de pas. On montre qu'une fonction est calculable si et seulement si elle a un nom effectuable.ZusammenfassungDummets Auffassung von Frege gemäss besteht der Sinn eines denotierenden Ausdruckes in einem Verfahren, das dessen Denotation bestimmt. Es ist der Zweck der vorliegenden Arbeit, die‐sen Vorschlag weiterzufuUhren und eine halbformale Interpretation des Fregeschen Sinnes fiir den besonderen Fall der Sprache erster Stufe der Arithmetik zu entwickeln. Es wird im besonderen der Sinn eines jeden arithmetischen Ausdruckes als hypothetisches Verfahren zur Bestimmung der denotierten Zahl oder des Wahrheitswertes definiert. Die Sinngebung ist insofern hypothe‐tisch, als der Sinn gewisser Ausdrucke nicht in einer endlichen Zahl von Schritten gegeben wer‐den kann. Das Anliegen der Arbeit grundet in der Absicht, einen intensionalen Begriff der Effek‐tivitat aufgrund des Sinnes von Funktionsnamen zu erlautern. Es wird im besonderen festgelegt, dass ein Ausdruck dann und nur dann effektiv sei, wenn sein Sinn in einer endlichen Zahl von Schritten erreicht werden kann. Es wird gezeigt, dass eine Funktion genau dann berechenbar ist, wenn sie einen effektiven Namen hat. (shrink)

We investigate the theory Peano Arithmetic with Indiscernibles ( \(\textrm{PAI}\) ). Models of \(\textrm{PAI}\) are of the form \(({\mathcal {M}},I)\), where \({\mathcal {M}}\) is a model of \(\textrm{PA}\), _I_ is an unbounded set of order indiscernibles over \({\mathcal {M}}\), and \(({\mathcal {M}},I)\) satisfies the extended induction scheme for formulae mentioning _I_. Our main results are Theorems A and B following. _Theorem A._ _Let_ \({\mathcal {M}}\) _be a nonstandard model of_ \(\textrm{PA}\) _ of any cardinality_. \(\mathcal {M }\) (...) _has an expansion to a model of _ \(\textrm{PAI}\) _iff_ \( {\mathcal {M}}\) _has an inductive partial satisfaction class._ Theorem A yields the following corollary, which provides a new characterization of countable recursively saturated models of \(\textrm{PA}\) : _Corollary._ _A countable model_ \({\mathcal {M}}\) of \(\textrm{PA}\) _is recursively saturated iff _ \({\mathcal {M}}\) _has an expansion to a model of _ \(\textrm{PAI}\). _Theorem B._ _There is a sentence _ \(\alpha \) _ in the language obtained by adding a unary predicate_ _I_(_x_) _to the language of arithmetic such that given any nonstandard model _ \({\mathcal {M}}\) _of_ \(\textrm{PA}\) _ of any cardinality_, \({\mathcal {M}}\) _has an expansion to a model of _ \(\text {PAI}+\alpha \) _iff_ \({\mathcal {M}}\) _has a inductive full satisfaction class._. (shrink)

This paper investigates the quantifier "there exist unboundedly many" in the context of first-order arithmetic. An alternative axiomatization is found for Peano arithmetic based on an axiom schema of regularity: The union of boundedly many bounded sets is bounded. We also obtain combinatorial equivalents of certain second-order theories associated with cuts in nonstandard models of arithmetic.

In 'On interpretations of arithmetic and set theory', Kaye and Wong proved the following result, which they considered to belong to the folklore of mathematical logic.

THEOREM 1 The first-order theories of Peano arithmetic and Zermelo-Fraenkel set theory with the axiom of infinity negated are bi-interpretable.

In this note, I describe a theory of sets that is bi-interpretable with the theory of bounded arithmetic IDelta0 + exp. Because of the weakness of this theory of sets, I (...) cannot straightforwardly adapt Kaye and Wong's interpretation of the arithmetic in the set theory. Instead, I am forced to produce a different interpretation. (shrink)

Our last big theorem – Theorem 6 – tells us that if a theory meets certain conditions, then it must be negation incomplete. And we made some initial arm-waving remarks to the effect that it seems plausible that we should want theories which meet those conditions. Later, we announced that there actually is a consistent weak arithmetic with a first-order logic which meets the conditions (in which case, stronger arithmetics will also meet the conditions); but we didn’t (...) say anything about what such a weak theory really looks like. In fact, we haven’t looked at any detailed theory of arithmetic yet! It is high time, then, that we stop operating at the extreme level of abstraction of Episodes 1 and 2, and start getting our hands dirty. This Episode introduces a couple of weak arithmetics, before we tackle the canonical first-order arithmetic PA in the following instalment. By all means skip fairly lightly over some of the more boring proof details! But it is certainly worth getting just a flavour of how these two simple formal theories work. (shrink)

I put forward precise and appealing notions of reference, self-reference, and well-foundedness for sentences of the language of first-order Peano arithmetic extended with a truth predicate. These notions are intended to play a central role in the study of the reference patterns that underlie expressions leading to semantic paradox and, thus, in the construction of philosophically well-motivated semantic theories of truth.

Due to Gӧdel’s incompleteness results, the categoricity of a sufficiently rich mathematical theory and the semantic completeness of its underlying logic are two mutually exclusive ideals. For first- and second-order logics we obtain one of them with the cost of losing the other. In addition, in both these logics the rules of deduction for their quantifiers are non-categorical. In this paper I examine two recent arguments –Warren (2020), Murzi and Topey (2021)– for the idea that the natural deduction (...) rules for the first-order universal quantifier are categorical, i.e., they uniquely determine its semantic intended meaning. Both of them make use of McGee’s open-endedness requirement and the second one uses in addition Garson’s (2013) local models for defining the validity of these rules. I argue that the success of both these arguments is relative to their semantic or infinitary assumptions, which could be easily discharged if the introduction rule for the universal quantifier is taken to be an infinitary rule, i.e. non-compact. Consequently, I reconsider the use of the ω-rule and I show that the addition of the ω-rule to the standard formalizations of first-order logic is categorical. In addition, I argue that the open-endedness requirement does not make the first-order Peano Arithmetic categorical and I advance an argument for its categoricity based on the inferential conservativity requirement. (shrink)

Ratajczyk, Z., Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic 64 95–152. The combinatorial method coming from the study of combinatorial sentences independent of PA is developed. Basing on this method we present the detailed analysis of provably recursive functions associated with higher levels of transfinite induction, I, and analyze combinatorial sentences independent of I. Our treatment of combinatorial sentences differs from the one given by McAloon [18] and gives more natural sentences. The (...) same method give also a combinatorial technique with no use of the cut-elimination theorem which is appropriate to study proof-theoretic strength of subsystems of first order arithmetic and some of their expansions. It was used to analyze iterated reflection principle and system of transfinite induction with a satisfaction class. (shrink)

An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details of proofs worked out and examples and exercises to aid the reader's understanding. It also serves as a companion to reading the original pathbreaking articles by Gerhard Gentzen. The first half covers topics in structural proof theory, including the Gödel-Gentzen translation of classical into intuitionistic logic, natural deduction and the normalization theorems, the sequent calculus, including cut-elimination and mid-sequent theorems, and various applications of (...) these results. The second half examines ordinal proof theory, specifically Gentzen's consistency proof for first-order Peano Arithmetic. The theory of ordinal notations and other elements of ordinal theory are developed from scratch, and no knowledge of set theory is presumed. The proof methods needed to establish proof-theoretic results, especially proof by induction, are introduced in stages throughout the text. Mancosu, Galvan, and Zach's introduction will provide a solid foundation for those looking to understand this central area of mathematical logic and the philosophy of mathematics. (shrink)