Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic

(1.1) A well-known example of a theory with built-in Skolem functions is (first-order) Peano arithmetic (or rather a certain definitional extension of it). See [C-K, pp. 143, 162] for the notion of a theory with built-in Skolem functions, and for a treatment of the example just mentioned. This property of Peano arithmetic obviously comes from the fact that in each nonempty definable subset of a model we can definably choose an element, namely, its least member.(1.2) Consider now a real closed field R and a nonempty subset D of R which is definable (with parameters) in R. Again we can definably choose an element of D, as follows: D is a union of finitely many singletons and intervals (a, b) where – ∞ ≤ a < b ≤ + ∞; if D has a least element we choose that element; if not, D contains an interval (a, b) for which a ∈ R ∪ { − ∞}is minimal; for this a we choose b ∈ R ∪ {∞} maximal such that (a, b) ⊂ D. Four cases have to be distinguished:(i) a = − ∞ and b = + ∞; then we choose 0;(ii) a = − ∞ and b ∈ R; then we choose b − 1;(iii) a ∈ R and b ∈ = + ∞; then we choose a + 1;(iv) a ∈ R and b ∈ R; then we choose the midpoint (a + b)/2.It follows as in the case of Peano arithmetic that the theory RCF of real closed fields has a definitional extension with built-in Skolem functions.

Download Full-text

Minimal readability of intuitionistic arithmetic and elementary analysis

Journal of Symbolic Logic ◽

10.2307/2275884 ◽

1995 ◽

Vol 60 (4) ◽

pp. 1208-1241 ◽

Cited By ~ 2

Author(s):

Zlatan Damnjanovic

Keyword(s):

Finite Type ◽

Peano Arithmetic ◽

New Method ◽

Recursive Functions ◽

Heyting Arithmetic ◽

Elementary Analysis ◽

Skolem Functions ◽

Definable Functions ◽

Intuitionistic Arithmetic

AbstractA new method of “minimal” readability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)—functions f such that HA ⊢ ∀x∃!yA(x, y) ⇒ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of ℒ(HA) with only x,y free—are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the < ε0-recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be < ε0-recursive. The method is extended to intuitionistic finite-type arithmetic, , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived.

Download Full-text

The Natural Numbers

10.1093/oso/9780199641314.003.0010 ◽

2018 ◽

Author(s):

Øystein Linnebo

Keyword(s):

Natural Number ◽

Peano Arithmetic ◽

Number Sequence ◽

Natural Numbers ◽

Ordinal Numbers ◽

Cardinal Numbers

How are the natural numbers individuated? That is, what is our most basic way of singling out a natural number for reference in language or in thought? According to Frege and many of his followers, the natural numbers are cardinal numbers, individuated by the cardinalities of the collections that they number. Another answer regards the natural numbers as ordinal numbers, individuated by their positions in the natural number sequence. Some reasons to favor the second answer are presented. This answer is therefore developed in more detail, involving a form of abstraction on numerals. Based on this answer, a justification for the axioms of Dedekind–Peano arithmetic is developed.

Download Full-text

Modal Structuralism with Theoretical Terms

Erkenntnis ◽

10.1007/s10670-021-00378-w ◽

2021 ◽

Author(s):

Holger Andreas ◽

Georg Schiemer

Keyword(s):

Philosophy Of Mathematics ◽

Formal Semantics ◽

Peano Arithmetic ◽

Theoretical Terms ◽

Structural Interpretation ◽

Oxford University ◽

Structuralist Approach ◽

Modal Semantics ◽

Oxford University Press

AbstractIn this paper, we aim to explore connections between a Carnapian semantics of theoretical terms and an eliminative structuralist approach in the philosophy of mathematics. Specifically, we will interpret the language of Peano arithmetic by applying the modal semantics of theoretical terms introduced in Andreas (Synthese 174(3):367–383, 2010). We will thereby show that the application to Peano arithmetic yields a formal semantics of universal structuralism, i.e., the view that ordinary mathematical statements in arithmetic express general claims about all admissible interpretations of the Peano axioms. Moreover, we compare this application with the modal structuralism by Hellman (Mathematics without numbers: towards a modal-structural interpretation. Oxford University Press: Oxford, 1989), arguing that it provides us with an easier epistemology of statements in arithmetic.

Download Full-text

NOTES ON BOUNDED INDUCTION FOR THE COMPOSITIONAL TRUTH PREDICATE

The Review of Symbolic Logic ◽

10.1017/s1755020316000368 ◽

2017 ◽

Vol 10 (3) ◽

pp. 455-480 ◽

Cited By ~ 3

Author(s):

BARTOSZ WCISŁO ◽

MATEUSZ ŁEŁYK

Keyword(s):

Reflection Principle ◽

Peano Arithmetic ◽

Truth Predicate ◽

Base Theory ◽

Modified Theory ◽

Induction Scheme

AbstractWe prove that the theory of the extensional compositional truth predicate for the language of arithmetic with Δ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.

Download Full-text

Beyond polynomials and Peano arithmetic—automation of elementary and ordinal interpretations

Journal of Symbolic Computation ◽

10.1016/j.jsc.2014.09.033 ◽

2015 ◽

Vol 69 ◽

pp. 129-158 ◽

Cited By ~ 4

Author(s):

Harald Zankl ◽

Sarah Winkler ◽

Aart Middeldorp

Keyword(s):

Peano Arithmetic

Download Full-text

Interpretability over peano arithmetic

Journal of Symbolic Logic ◽

10.2307/2586787 ◽

1999 ◽

Vol 64 (4) ◽

pp. 1407-1425

Author(s):

Claes Strannegård

Keyword(s):

Modal Logic ◽

Completeness Theorem ◽

Peano Arithmetic ◽

Embedding Theorem ◽

Compactness Theorem ◽

Partial Answer ◽

Recursively Enumerable ◽

Recursively Enumerable Sets ◽

Interpretability Logic

AbstractWe investigate the modal logic of interpretability over Peano arithmetic. Our main result is a compactness theorem that extends the arithmetical completeness theorem for the interpretability logic ILMω. This extension concerns recursively enumerable sets of formulas of interpretability logic (rather than single formulas). As corollaries we obtain a uniform arithmetical completeness theorem for the interpretability logic ILM and a partial answer to a question of Orey from 1961. After some simplifications, we also obtain Shavrukov's embedding theorem for Magari algebras (a.k.a. diagonalizable algebras).

Download Full-text

Automorphism groups of arithmetically saturated models

Journal of Symbolic Logic ◽

10.2178/jsl/1140641169 ◽

2006 ◽

Vol 71 (1) ◽

pp. 203-216 ◽

Cited By ~ 3

Author(s):

Ermek S. Nurkhaidarov

Keyword(s):

Automorphism Group ◽

Automorphism Groups ◽

Open Subgroup ◽

Peano Arithmetic ◽

Standard System ◽

Permutation Groups ◽

Saturated Model ◽

Saturated Models ◽

Homogeneous Set ◽

Image Position

In this paper we study the automorphism groups of countable arithmetically saturated models of Peano Arithmetic. The automorphism groups of such structures form a rich class of permutation groups. When studying the automorphism group of a model, one is interested to what extent a model is recoverable from its automorphism group. Kossak-Schmerl [12] show that if M is a countable, arithmetically saturated model of Peano Arithmetic, then Aut(M) codes SSy(M). Using that result they prove:Let M1. M2 be countable arithmetically saturated models of Peano Arithmetic such that Aut(M1) ≅ Aut(M2). Then SSy(M1) = SSy(M2).We show that if M is a countable arithmetically saturated of Peano Arithmetic, then Aut(M) can recognize if some maximal open subgroup is a stabilizer of a nonstandard element, which is smaller than any nonstandard definable element. That fact is used to show the main theorem:Let M1, M2be countable arithmetically saturated models of Peano Arithmetic such that Aut(M1) ≅ Aut(M2). Then for every n < ωHere RT2n is Infinite Ramsey's Theorem stating that every 2-coloring of [ω]n has an infinite homogeneous set. Theorem 0.2 shows that for models of a false arithmetic the converse of Kossak-Schmerl Theorem 0.1 is not true. Using the results of Reverse Mathematics we obtain the following corollary:There exist four countable arithmetically saturated models of Peano Arithmetic such that they have the same standard system but their automorphism groups are pairwise non-isomorphic.

Download Full-text

Friedberg Numbering in Fragments of Peano Arithmetic and α-Recursion Theory

Journal of Symbolic Logic ◽

10.2178/jsl.7804060 ◽

2013 ◽

Vol 78 (4) ◽

pp. 1135-1163 ◽

Cited By ~ 1

Author(s):

Wei Li

Keyword(s):

Recursion Theory ◽

Peano Arithmetic ◽

Fragments Of Peano Arithmetic

AbstractIn this paper, we investigate the existence of a Friedberg numbering in fragments of Peano Arithmetic and initial segments of Gödel's constructible hierarchy Lα, where α is Σ1 admissible. We prove that(1) Over P− + BΣ2, the existence of a Friedberg numbering is equivalent to IΣ2, and(2) For Lα, there is a Friedberg numbering if and only if the tame Σ2 projectum of α equals the Σ2 cofinality of α.

Download Full-text

On external Scott algebras in nonstandard models of Peano arithmetic

Journal of Symbolic Logic ◽

10.2307/2275677 ◽

1996 ◽

Vol 61 (2) ◽

pp. 586-607

Author(s):

Vladimir Kanovei

Keyword(s):

Peano Arithmetic ◽

Sufficient Condition ◽

Elementary Extension ◽

Necessary And Sufficient Condition ◽

Nonstandard Models ◽

Necessary And Sufficient

AbstractWe prove that a necessary and sufficient condition for a countable set of sets of integers to be equal to the algebra of all sets of integers definable in a nonstandard elementary extension of ω by a formula of the PA language which may include the standardness predicate but does not contain nonstandard parameters, is as follows: is closed under arithmetical definability and contains 0(ω) the set of all (Gödel numbers of) true arithmetical sentences.Some results related to definability of sets of integers in elementary extensions of ω are included.

Download Full-text