An Upper Bound for the Provability of Transfinite Induction in Systems with N-Times Iterated Inductive Definitions.

1983 ◽  
Vol 48 (3) ◽  
pp. 878
Author(s):  
Kurt Schutte ◽  
W. Pohlers ◽  
J. Diller ◽  
G. H. Muller
Keyword(s):  
Upper Bound ◽  
Transfinite Induction ◽  
Inductive Definitions

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}$.

A system of abstract constructive ordinals

1972 ◽  
Vol 37 (2) ◽  
pp. 355-374 ◽  
Author(s):  
W. A. Howard
Keyword(s):  
Finite Type ◽  
Free Variable ◽  
Transfinite Induction ◽  
Functional Interpretation ◽  
Variable Theory ◽  
Inductive Definitions ◽  
Heyting Arithmetic ◽  
Abstract Notion ◽  
Primitive Recursive ◽  
Primitive Recursive Functionals

As Gödel [6] has pointed out, there is a certain interchangeability between the intuitionistic notion of proof and the notion of constructive functional of finite type. He achieves this interchange in the direction from logic to functionals by his functional interpretation of Heyting arithmetic H in a free variable theory T of primitive recursive functionals of finite type. In the present paper we shall extend Gödel's functional interpretation to the case in which H and T are extended by adding an abstract notion of constructive ordinal. In other words, we obtain the Gödel functional interpretation of an intuitionistic theory U of numbers (i.e., nonnegative integers) and constructive ordinals in a free variable theory V of finite type over both numbers and constructive ordinals. This allows us to obtain an analysis of noniterated positive inductive definitions [8].The notion of constructive ordinal to be treated is as follows. There is given a function J which embeds the nonnegative integers in the constructive ordinals. A constructive ordinal of the form Jn is said to be minimal. There is also given a function δ which associates to each constructive ordinal Z and number n a constructive ordinal δZn which we denote by Zn. When Z is nonminimal, each Zn is called an immediate predecessor of Z. The basic principle for forming constructive ordinals says: for every function f from numbers n to constructive ordinals, there exists a constructive ordinal Z such that Zn = fn for all n. The principle of transfinite induction with respect to constructive ordinals says: if a property Q(Z) of constructive ordinals Z holds for minimal Z, and if ∀nQ(Zn) → Q(Z) holds for all Z, then Q(Z) holds for all Z.

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 Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions

10.29007/vkmj ◽  
2020 ◽  
Author(s):  
Jens Pagel ◽  
Florian Zuleger
Keyword(s):  
Recent Work ◽  
Upper Bound ◽  
Separation Logic ◽  
Satisfiability Problem ◽  
Magic Wand ◽  
Inductive Definitions ◽  
Direct Model

Symbolic-heap separation logic with inductive definitions is a popular formalism for reasoning about heap-manipulating programs. The fragment SLIDbtw introduced by Iosif, Rogalewicz and Simacek, is one of the most expressive fragments with a decidable entailment problem. In recent work, we improved on the original decidability proof by providing a direct model-theoretic construction, obtaining a 2-Exptime upper bound. In this paper, we investigate separation logics built on top of the inductive definitions from SLIDbtw, i.e., logics that feature the standard Boolean and separation-logic operators. We give an almost tight delineation between decidability and undecidabilty. We establish the decidability of the satisfiability problem (in 2-Exptime) of a separation logic with conjunction, disjunction, separating conjunction and guarded forms of negation, magic wand, and septraction. We show that any further generalization leads to undecidabilty (under mild assumptions).

Addendum to “The truth is never simple”

1988 ◽  
Vol 53 (2) ◽  
pp. 390-392
Author(s):  
John P. Burgess
Keyword(s):  
Upper Bound ◽  
Present Note ◽  
Recent Survey ◽  
Survey Article ◽  
Inductive Definitions ◽  
Complete Set ◽  
Image Position

The present note outlines an answer to a question listed as open in our recent survey article [1], familiarity with which is assumed.Let Γ be the class of all X ⊆ ω such that X is reducible to for some some arithmetical and some positive with Y ⊆ p(Y) for all Y.A.1. Theorem. is a complete set of class Γ.A.2. Corollary, (a) is-in-a--parameter.(b) (i) Every set-in-a--parameter is reducible to.(ii) Every set-in-a--parameter is reducible to.Remarks. A.1 answers 7.3 of [1]. A.2 says as much as can be said about in terms of the coarse classifications of the analytical hierarchy. A.2 follows from A.1 by general methods and results in the theory of inductive definitions (having nothing specifically to do with truth), and its proof will be omitted.Proof of A.1. We omit subscripts vF.Upper Bound. Define

Sign in / Sign up

Export Citation Format

Share Document