Note on the fan theorem

1974 ◽  
Vol 39 (3) ◽  
pp. 584-596 ◽  
Author(s):  
A. S. Troelstra
Keyword(s):  
Consistency Proof ◽  
Conservative Extension ◽  
First Order ◽  
Fan Theorem ◽  
Elementary Analysis ◽  
Elementary Methods ◽  
Order Arithmetic ◽  
Image Position

The principal aim of this paper is to establish a theorem stating, roughly, that the addition of the fan theorem and the. continuity schema to an intuitionistic system of elementary analysis results in a conservative extension with respect to arithmetical statements.The result implies that the consistency of first order arithmetic cannot be proved by use of the fan theorem, in addition to standard elementary methods—although it was the opposite assumption which led Gentzen to withdraw the first version of his consistency proof for arithmetic (see [B]).We must presuppose acquaintance with notation and principal results of [K, T], and with §1.6, Chapter II, and Chapter III, §4-6 of [T1]. In one respect we shall deviate from the notation in [K, T]: We shall use (n)x (instead of g(n, x)) to indicate the xth component of the sequence coded by n, if x < lth(n), 0 otherwise.We also introduce abbreviations n ≤* m, a ≤ b which will be used frequently below:

A weak absolute consistency proof for some systems of illative combinatory logic

1983 ◽  
Vol 48 (3) ◽  
pp. 771-776 ◽  
Author(s):  
M.W. Bunder
Keyword(s):  
Set Theory ◽  
Combinatory Logic ◽  
Weak Consistency ◽  
Consistency Proof ◽  
First Order ◽  
Formal Systems ◽  
Elementary Methods ◽  
Order Arithmetic ◽  
Strongly Consistent ◽  
Order Predicate Calculus

A large number of formal systems based on combinatory logic or λ-calculus have been extended to include first order predicate calculus. Several of these however have been shown to be inconsistent, all, as far as the author knows, in the strong sense that all well formed formulas (which here include all strings of symbols) are provable. We will call the corresponding consistency notion—an arbitrary wff ⊥ is provable—weak consistency. We will say that a system is strongly consistent if no formula and its negation are provable.Now for some systems, such as that of Kuzichev [11], the strong and weak consistency notions are equivalent, but in the systems of [5] and [6], which we will be considering, they are not. Each of these systems is strong enough to have all of ZF set theory, except Grounding and Choice, interpretable in it, and the system of [5] can also encompass first order arithmetic (see [7]). It therefore seems unlikely that a strong consistency result could be proved for these systems using elementary methods. In this paper however, we prove the weak consistency of both these systems by means that could be formulated, at least within the theory of [5]. The method also applies to the typed systems of Curry, Hindley and Seldin [10] and to Seldin's generalised types [12].

Relativized realizability in intuitionistic arithmetic of all finite types

1978 ◽  
Vol 43 (1) ◽  
pp. 23-44 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Extension Theorem ◽  
General Notion ◽  
Conservative Extension ◽  
First Order ◽  
New Information ◽  
Reflection Theorem ◽  
Order Arithmetic ◽  
Special Case ◽  
Dependent Choice ◽  
Intuitionistic Arithmetic

In this paper we introduce a new notion of realizability for intuitionistic arithmetic in all finite types. The notion seems to us to capture some of the intuition underlying both the recursive realizability of Kjeene [5] and the semantics of Kripke [7]. After some preliminaries of a syntactic and recursion-theoretic character in §1, we motivate and define our notion of realizability in §2. In §3 we prove a soundness theorem, and in §4 we apply that theorem to obtain new information about provability in some extensions of intuitionistic arithmetic in all finite types. In §5 we consider a special case of our general notion and prove a kind of reflection theorem for it. Finally, in §6, we consider a formalized version of our realizability notion and use it to give a new proof of the conservative extension theorem discussed in Goodman and Myhill [4] and proved in our [3]. (Apparently, a form of this result is also proved in Mine [13]. We have not seen this paper, but are relying on [12].) As a corollary, we obtain the following somewhat strengthened result: Let Σ be any extension of first-order intuitionistic arithmetic (HA) formalized in the language of HA. Let Σω be the theory obtained from Σ by adding functionals of finite type with intuitionistic logic, intensional identity, and axioms of choice and dependent choice at all types. Then Σω is a conservative extension of Σ. An interesting example of this theorem is obtained by taking Σ to be classical first-order arithmetic.

Some properties of epistemic set theory with collection

1986 ◽  
Vol 51 (3) ◽  
pp. 748-754 ◽  
Author(s):  
Andre Scedrov
Keyword(s):  
Set Theory ◽  
Intuitionistic Logic ◽  
Existential Quantifier ◽  
Modal Interpretation ◽  
Conservative Extension ◽  
Disjunction Property ◽  
First Order ◽  
Slight Extension ◽  
Order Arithmetic ◽  
Epistemic Systems

Myhill [12] extended the ideas of Shapiro [15], and proposed a system of epistemic set theory IST (based on modal S4 logic) in which the meaning of the necessity operator is taken to be the intuitive provability, as formalized in the system itself. In this setting one works in classical logic, and yet it is possible to make distinctions usually associated with intuitionism, e.g. a constructive existential quantifier can be expressed as (∃x) □ …. This was first confirmed when Goodman [7] proved that Shapiro's epistemic first order arithmetic is conservative over intuitionistic first order arithmetic via an extension of Gödel's modal interpretation [6] of intuitionistic logic.Myhill showed that whenever a sentence □A ∨ □B is provable in IST, then A is provable in IST or B is provable in IST (the disjunction property), and that whenever a sentence ∃x.□A(x) is provable in IST, then so is A(t) for some closed term t (the existence property). He adapted the Friedman slash [4] to epistemic systems.Goodman [8] used Epistemic Replacement to formulate a ZF-like strengthening of IST, and proved that it was a conservative extension of ZF and that it had the disjunction and existence properties. It was then shown in [13] that a slight extension of Goodman's system with the Epistemic Foundation (ZFER, cf. §1) suffices to interpret intuitionistic ZF set theory with Replacement (ZFIR, [10]). This is obtained by extending Gödel's modal interpretation [6] of intuitionistic logic. ZFER still had the properties of Goodman's system mentioned above.

Epistemic arithmetic is a conservative extension of intuitionistic arithmetic

1984 ◽  
Vol 49 (1) ◽  
pp. 192-203 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Propositional Calculus ◽  
Cut Elimination ◽  
Conservative Extension ◽  
First Order ◽  
Classical Mathematics ◽  
Order Arithmetic ◽  
Classical Propositional Calculus ◽  
Epistemic Arithmetic ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

Questions about the constructive or effective character of particular arguments arise in several areas of classical mathematics, such as in the theory of recursive functions and in numerical analysis. Some philosophers have advocated Lewis's S4 as the proper logic in which to formalize such epistemic notions. (The fundamental work on this is Hintikka [4].) Recently there have been studies of mathematical theories formalized with S4 as the underlying logic so that these epistemic notions can be expressed. (See Shapiro [7], Myhill [5], and Goodman [2]. The motivation for this work is discussed in Goodman [3].) The present paper is a contribution to the study of the simplest of these theories, namely first-order arithmetic as formalized in S4. Following Shapiro, we call this theory epistemic arithmetic (EA). More specifically, we show that EA is a conservative extension of Hey ting's arithmetic HA (ordinary first-order intuitionistic arithmetic). The question of whether EA is conservative over HA was raised but left open in Shapiro [7].The idea of our proof is as follows. We interpret EA in an infinitary propositional S4, pretty much as Tait, for example, interprets classical arithmetic in his infinitary classical propositional calculus in [8]. We then prove a cut-elimination theorem for this infinitary propositional S4. A suitable version of the cut-elimination theorem can be formalized in HA. For cut-free infinitary proofs, there is a reflection principle provable in HA. That is, we can prove in HA that if there is a cut-free proof of the interpretation of a sentence ϕ then ϕ is true. Combining these results shows that if the interpretation of ϕ is provable in EA, then ϕ is provable in HA.

On deciding the truth of certain statements involving the notion of consistency

1976 ◽  
Vol 41 (4) ◽  
pp. 779-781 ◽  
Author(s):  
George Boolos
Keyword(s):  
Free Variable ◽  
Incompleteness Theorem ◽  
First Order ◽  
Order Arithmetic ◽  
Image Position

Friedman has posed (see [F, p. 117]) the following problem: “35. Define the set E of expressions by (i) Con is an expression; (ii) if A, B are expressions so are (~ A), (A&B), and Con(A). Each expression ϕ in E determines a sentence ϕ in PA [classical first-order arithmetic] by taking Con* to be “PA is consistent,” ( ~ A) * to be ~ (A*), (A&B)* to be A*&B*, and Con(A)* to be “PA + ‘A*’ is consistent.” The set of expressions ϕ ∈ E such that ϕ* is true is recursive.The formalized second incompleteness theorem readsIn order to simplify notation, we will reformulate Friedman's problem slightly. Let Con be the usual sentence of PA expressing the consistency of PA, ~ A the negation of A, (A&B) the conjunction of A and B, etc., and Bew(A) the result of substituting the numeral for the Gödel number of A for the free variable in the usual provability predicate for PA. Let Con(A) = ~ Bew(~ A). (Con(A) is equivalent in PA to the usual sentence expressing the consistency of PA + A.) And let the class of F-sentences be the smallest class which contains Con and which also contains ~ A, (A&B) and Con(A) whenever it contains A and B. Since ⊦PA Bew(A) ↔ Bew(B) if ⊦PAA ↔ B, Friedman's problem is then the question whether the class of true F-sentences is recursive.The answer is that it is recursive. To see why, we need a definition and a theorem.Definition. An atom is a sentence Conn for some n ≥ 1, where Cont = Con and Conn + 1 = Con(Conn).

The mean value theorem in second order arithmetic

2001 ◽  
Vol 66 (3) ◽  
pp. 1353-1358 ◽  
Author(s):  
Christopher S. Hardin ◽  
Daniel J. Velleman
Keyword(s):  
Mean Value ◽  
Second Order ◽  
Mean Value Theorem ◽  
Natural Numbers ◽  
Second Order Arithmetic ◽  
Elementary Analysis ◽  
Logical Connectives ◽  
The Mean ◽  
Order Arithmetic ◽  
Image Position

This paper is a contribution to the project of determining which set existence axioms are needed to prove various theorems of analysis. For more on this project and its history we refer the reader to [1] and [2].We work in a weak subsystem of second order arithmetic. The language of second order arithmetic includes the symbols 0, 1, =, <, +, ·, and ∈, together with number variables x, y, z, … (which are intended to stand for natural numbers), set variables X, Y, Z, … (which are intended to stand for sets of natural numbers), and the usual quantifiers (which can be applied to both kinds of variables) and logical connectives. We write ∀x < t φ and ∃x < t φ as abbreviations for ∀x(x < t → φ) and ∃x{x < t ∧ φ) respectively; these are called bounded quantifiers. A formula is said to be if it has no quantifiers applied to set variables, and all quantifiers applied to number variables are bounded. It is if it has the form ∃xθ and it is if it has the form ∀xθ, where in both cases θ is .The theory RCA0 has as axioms the usual Peano axioms, with the induction scheme restricted to formulas, and in addition the comprehension scheme, which consists of all formulas of the formwhere φ is , ψ is , and X does not occur free in φ(n). (“RCA” stands for “Recursive Comprehension Axiom.” The reason for the name is that the comprehension scheme is only strong enough to prove the existence of recursive sets.) It is known that this theory is strong enough to allow the development of many of the basic properties of the real numbers, but that certain theorems of elementary analysis are not provable in this theory. Most relevant for our purposes is the fact that it is impossible to prove in RCA0 that every continuous function on the closed interval [0, 1] attains maximum and minimum values (see [1]).Since the most common proof of the Mean Value Theorem makes use of this theorem, it might be thought that the Mean Value Theorem would also not be provable in RCA0. However, we show in this paper that the Mean Value Theorem can be proven in RCA0. All theorems stated in this paper are theorems of RCA0, and all of our reasoning will take place in RCA0.

The independence of Peano's fourth axiom from Martin-Löf's type theory without universes

1988 ◽  
Vol 53 (3) ◽  
pp. 840-845 ◽  
Author(s):  
Jan M. Smith
Keyword(s):  
Type Theory ◽  
Predicate Logic ◽  
Single Element ◽  
Simple Type ◽  
Consistency Proof ◽  
Computational System ◽  
First Order ◽  
Simple Type Theory ◽  
Individual Domain ◽  
Order Arithmetic

In Hilbert and Ackermann [2] there is a simple proof of the consistency of first order predicate logic by reducing it to propositional logic. Intuitively, the proof is based on interpreting predicate logic in a domain with only one element. Tarski [7] and Gentzen [1] have extended this method to simple type theory by starting with an individual domain consisting of a single element and then interpreting a higher type by the set of truth valued functions on the previous type.I will use the method of Hilbert and Ackermann on Martin-Löf's type theory without universes to show that ¬Eq(A, a, b) cannot be derived without universes for any type A and any objects a and b of type A. In particular, this proves the conjecture in Martin-Löf [5] that Peano's fourth axiom (∀x ϵ N)¬ Eq(N, 0, succ(x)) cannot be proved in type theory without universes. If by consistency we mean that there is no closed term of the empty type, then the construction will also give a consistency proof by finitary methods of Martin-Löf's type theory without universes. So, without universes, the logic obtained by interpreting propositions as types is surprisingly weak. This is in sharp contrast with type theory as a computational system, since, for instance, the proof that every object of a type can be computed to normal form cannot be formalized in first order arithmetic.

Ordinal bounds for κ-consistency

1974 ◽  
Vol 39 (4) ◽  
pp. 693-699 ◽  
Author(s):  
Warren D. Goldfarb
Keyword(s):  
Nonnegative Integer ◽  
Transfinite Induction ◽  
Axiom Schema ◽  
First Order ◽  
Order Arithmetic ◽  
Definition Of ◽  
Image Position ◽  
Primitive Recursive

In [1] the ω-consistency of arithmetic was proved by a method which yields fine ordinal bounds for κ-consistency, κ ≥ 1. In this paper these bounds are shown to be best possible. The ω-consistency of a number-theoretic system S can be expressed thus: for all sentences ∃xM,where ProvS is the proof predicate for S, if n is a nonnegative integer then n is the formal numeral (of S) for n, and if G is a formula then ˹G˺ is the Gödel number of G. The κ-consistency of S is the restriction of (1) to Σκ0 sentences ∃xM. The proof in [1] establishes the no-counterexample interpretation of (1), that is, the existence of a constructive functional Φ such that, for all sentences ∃xM, all numbers p, and all functions f,(see [1, §2]). A functional Φ is an ω-consistency functional for S if it satisfies (2) for all sentences ∃xM, and a κ-consistency functional for S if it satisfies (2) for all Σκ0 sentences ∃xM.The systems considered in [1] are those obtained from classical first-order arithmetic Z, including the schema for definition of primitive recursive (p.r.) functions, by adjoining, for some p.r. well-founded ordering ≺ of the nonnegative integers, the axiom schemathat is, the least number principle on ≺; it is equivalent to the schema of transfinite induction on ≺.

Undecidability of the real-algebraic structure of models of intuitionistic elementary analysis

2000 ◽  
Vol 65 (3) ◽  
pp. 1014-1030 ◽  
Author(s):  
Miklós Erdélyi-Szabó
Keyword(s):  
Algebraic Structure ◽  
Second Order ◽  
Heyting Algebras ◽  
Real Numbers ◽  
Second Order Arithmetic ◽  
The Real ◽  
First Order ◽  
Elementary Analysis ◽  
Order Arithmetic

AbstractWe show that true first-order arithmetic is interpretable over the real-algebraic structure of models of intuitionistic analysis built upon a certain class of complete Heyting algebras. From this the undecidability of the structures follows. We also show that Scott's model is equivalent to true second-order arithmetic. In the appendix we argue that undecidability on the language of ordered rings follows from intuitionistically plausible properties of the real numbers.

Sign in / Sign up

Export Citation Format

Share Document