scholarly journals Provable wellorderings of formal theories for transfinitely iterated inductive definitions

1978 ◽  
Vol 43 (1) ◽  
pp. 118-125 ◽  
Author(s):  
W. Buchholz ◽  
W. Pohlers
Keyword(s):  
Transfinite Induction ◽  
Crucial Point ◽  
Inductive Definitions ◽  
Image Position ◽  
Intuitionistic Version ◽  
Formal Theories

By [12] we know that transfinite induction up to ΘεΩN+10 is not provable in IDN, the theory of N-times iterated inductive definitions. In this paper we will show that conversely transfinite induction up to any ordinal less than ΘεΩN+10 is provable in IDNi, the intuitionistic version of IDN, and extend this result to theories for transfinitely iterated inductive definitions.In [14] Schütte proves the wellordering of his notational systems using predicates is wellordered) with Mκ ≔ {x ∈ and 0 ≤ κ ≤ N. Obviously the predicates are definable in IDNi with the defining axioms:where Prog [Mκ, X] means that X is progressive with respect to Mκ, i.e.The crucial point in Schütte's wellordering proof is Lemma 19 [14, p. 130] which can be modified towhere TI[Mκ + 1, a] is the scheme of transfinite induction over Mκ + 1 up to a.

scholarly journals PROOF-THEORETIC STRENGTHS OF WEAK THEORIES FOR POSITIVE INDUCTIVE DEFINITIONS

2018 ◽  
Vol 83 (3) ◽  
pp. 1091-1111 ◽  
Author(s):  
TOSHIYASU ARAI
Keyword(s):  
Transfinite Induction ◽  
Boundary Line ◽  
Natural Numbers ◽  
Inductive Definitions ◽  
Image Position ◽  
Weak Theories ◽  
Comprehension Axiom

AbstractIn this article the lightface ${\rm{\Pi }}_1^1$-Comprehension axiom is shown to be proof-theoretically strong even over ${\rm{RCA}}_0^{\rm{*}}$, and we calibrate the proof-theoretic ordinals of weak fragments of the theory ${\rm{I}}{{\rm{D}}_1}$ of positive inductive definitions over natural numbers. Conjunctions of negative and positive formulas in the transfinite induction axiom of ${\rm{I}}{{\rm{D}}_1}$ are shown to be weak, and disjunctions are strong. Thus we draw a boundary line between predicatively reducible and impredicative fragments of ${\rm{I}}{{\rm{D}}_1}$.

Ordinals Connected with Formal Theories for Transfinitely Iterated Inductive Definitions.

1983 ◽  
Vol 48 (3) ◽  
pp. 878
Author(s):  
Kurt Schutte ◽  
W. Pohlers
Keyword(s):  
Inductive Definitions ◽  
Formal Theories

THE ARITHMETIC OF THE EVEN AND THE ODD

2016 ◽  
Vol 9 (2) ◽  
pp. 359-369 ◽  
Author(s):  
VICTOR PAMBUCCIAN
Keyword(s):  
Formal Theory ◽  
Image Position ◽  
Formal Theories

AbstractWe present several formal theories for the arithmetic of the even and the odd, show that the irrationality of $\sqrt 2$ can be proved in one of them, that the proof must involve contradiction, and prove that the irrationality of $\sqrt {17}$ cannot be proved inside any formal theory of the even and the odd.

Replacement and collection in intuitionistic set theory

1985 ◽  
Vol 50 (2) ◽  
pp. 344-348 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Set Theory ◽  
Predicate Calculus ◽  
Transfinite Induction ◽  
Separation Axiom ◽  
Classical Form ◽  
Existence Property ◽  
Membership Relation ◽  
Image Position ◽  
Excluded Middle ◽  
Intuitionistic Set Theory

Intuitionistic Zermelo-Fraenkel set theory, which we call ZFI, was introduced by Friedman and Myhill in [3] in 1970. The idea was to have a theory with the same axioms as ordinary classical ZF, but with Heyting's predicate calculus HPC as the underlying logic. Since some classically equivalent statements are intuitionistically inequivalent, however, it was not always obvious which form of a classical axiom to take. For example, the usual formulation of the axiom of foundation had to be replaced with a principle of transfinite induction on the membership relation in order to avoid having excluded middle provable and thus making the logic classical. In [3] the replacement axiom is taken in its most common classical form:In the presence of the separation axiom,this is equivalent to the axiomIt is this schema Rep that we shall call the replacement axiom.Friedman and Myhill were able to show in [3] that ZFI has a number of desirable “constructive” properties, including the existence property for both numbers and sets. They were not able to determine, however, whether ZFI is proof-theoretically as strong as ZF. This is still open.Three years later, in [2], Friedman introduced a theory ZF− which is like ZFI except that the replacement axiom is changed to the classically equivalent collection axiom:He showed that ZF− is proof-theoretically of the same strength as ZF, and he asked whether ZF− is equivalent to ZFI.

A realizability interpretation of Church's simple theory of types

2016 ◽  
Vol 27 (8) ◽  
pp. 1364-1385
Author(s):  
ULRICH BERGER ◽  
TIE HOU
Keyword(s):  
Lambda Calculus ◽  
Higher Order ◽  
Order Logic ◽  
Simple Theory ◽  
Formal Proofs ◽  
Higher Order Logic ◽  
Mathematical Structures ◽  
Inductive Definitions ◽  
Definition Of ◽  
Intuitionistic Version

We give a realizability interpretation of an intuitionistic version of Church's Simple Theory of Types (CST) which can be viewed as a formalization of intuitionistic higher-order logic. Although definable in CST we include operators for monotone induction and coinduction and provide simple realizers for them. Realizers are formally represented in an untyped lambda–calculus with pairing and case-construct. The purpose of this interpretation is to provide a foundation for the extraction of verified programs from formal proofs as an alternative to type-theoretic systems. The advantages of our approach are that (a) induction and coinduction are not restricted to the strictly positive case, (b) abstract mathematical structures and results may be imported, (c) the formalization is technically simpler than in other systems, for example, regarding the definition of realizability, which is a simple syntactical substitution, and the treatment of nested and simultaneous (co)inductive definitions.

scholarly journals Provable Wellorderings of Formal Theories for Transfinitely Iterated Inductive Definitions.

1983 ◽  
Vol 48 (3) ◽  
pp. 878
Author(s):  
Kurt Schutte ◽  
W. Buchholz ◽  
W. Pohlers
Keyword(s):  
Inductive Definitions ◽  
Formal Theories

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 ≺.

Two questions from Dana Scott: Intuitionistic topologies and continuous functions

2009 ◽  
Vol 74 (2) ◽  
pp. 689-692
Author(s):  
Charles McCarty
Keyword(s):  
Set Theory ◽  
Continuous Functions ◽  
Unit Interval ◽  
Natural Numbers ◽  
Double Negation ◽  
Closed Set ◽  
Closed Sets ◽  
Image Position ◽  
Intuitionistic Set Theory ◽  
Formal Theories

Since intuitionistic sets are not generally stable – their membership relations are not always closed under double negation – the open sets of a topology cannot be recovered from the closed sets of that topology via complementation, at least without further ado. Dana Scott asked, first, whether it is possible intuitionistically for two distinct topologies, given as collections of open sets on the same carrier, to share their closed sets. Second, he asked whether there can be intuitionistic functions that are closed continuous in that the inverse of every closed set is closed without being continuous in the usual, open sense. Here, we prove that, as far as intuitionistic set theory is concerned, there can be infinitely-many distinct topologies on the same carrier sharing a single collection of closed sets. The proof employs Heyting-valued sets, and demonstrates that the intuitionistic set theory IZF [4, 624], as well as the theory IZF plus classical elementary arithmetic, are both consistent with the statement that infinitely many topologies on the set of natural numbers share the same closed sets. Without changing models, we show that these formal theories are also consistent with the statement that there are infinitely many endofunctions on the natural numbers that are closed continuous but not open continuous with respect to a single topology.For each prime k ∈ ω, let Ak be this ω-sequence of sets open in the standard topology on the closed unit interval: for each n ∈ ω,

Sign in / Sign up

Export Citation Format

Share Document