-
The strength of SCT soundness
Authors:
Emanuele Frittaion,
Florian Pelupessy,
Silvia Steila,
Keita Yokoyama
Abstract:
In this paper we continue the study, from Frittaion, Steila and Yokoyama (2017), on size-change termination in the context of Reverse Mathematics. We analyze the soundness of the SCT method. In particular, we prove that the statement "any program which satisfies the combinatorial condition provided by the SCT criterion is terminating" is equivalent to $\mathrm{WO}(ω_3)$ over $\mathsf{RCA_0}$
In this paper we continue the study, from Frittaion, Steila and Yokoyama (2017), on size-change termination in the context of Reverse Mathematics. We analyze the soundness of the SCT method. In particular, we prove that the statement "any program which satisfies the combinatorial condition provided by the SCT criterion is terminating" is equivalent to $\mathrm{WO}(ω_3)$ over $\mathsf{RCA_0}$
△ Less
Submitted 26 September, 2017;
originally announced September 2017.
-
The strength of the SCT criterion
Authors:
Emanuele Frittaion,
Silvia Steila,
Keita Yokoyama
Abstract:
We undertake the study of size-change analysis in the context of Reverse Mathematics. In particular, we prove that the SCT criterion is equivalent to $Σ^0_2$-induction over RCA$_0$.
We undertake the study of size-change analysis in the context of Reverse Mathematics. In particular, we prove that the SCT criterion is equivalent to $Σ^0_2$-induction over RCA$_0$.
△ Less
Submitted 16 November, 2016;
originally announced November 2016.
-
A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem
Authors:
Paulo Oliva,
Silvia Steila
Abstract:
In 1979 Schwichtenberg showed that the System $\text{T}$ definable functionals are closed under a rule-like version Spector's bar recursion of lowest type levels $0$ and $1$. More precisely, if the functional $Y$ which controls the stop** condition of Spector's bar recursor is $\text{T}$-definable, then the corresponding bar recursion of type levels $0$ and $1$ is already $\text{T}$-definable. S…
▽ More
In 1979 Schwichtenberg showed that the System $\text{T}$ definable functionals are closed under a rule-like version Spector's bar recursion of lowest type levels $0$ and $1$. More precisely, if the functional $Y$ which controls the stop** condition of Spector's bar recursor is $\text{T}$-definable, then the corresponding bar recursion of type levels $0$ and $1$ is already $\text{T}$-definable. Schwichtenberg's original proof, however, relies on a detour through Tait's infinitary terms and the correspondence between ordinal recursion for $α< \varepsilon_0$ and primitive recursion over finite types. This detour makes it hard to calculate on given concrete system $\text{T}$ input, what the corresponding system $\text{T}$ output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into $\text{T}$-definitions under the conditions of Schwichtenberg's theorem. Finally, with the explicit construction we can also easily state a sharper result: if $Y$ is in the fragment $\text{T}_i$ then terms built from $\text{BR}^{\mathbb{N}, σ}$ for this particular $Y$ are definable in the fragment $\text{T}_{i + \max \{ 1, \text{level}σ \} + 2}$.
△ Less
Submitted 15 August, 2017; v1 submitted 18 July, 2016;
originally announced July 2016.
-
Some algebraic equivalent forms of $\mathbb{R} \subseteq L$
Authors:
Silvia Steila
Abstract:
We study $Σ^1_2$ definable counterparts for some algebraic equivalent forms of the Continuum Hypothesis. All turn out to be equivalent to "all reals are constructible".
We study $Σ^1_2$ definable counterparts for some algebraic equivalent forms of the Continuum Hypothesis. All turn out to be equivalent to "all reals are constructible".
△ Less
Submitted 18 January, 2016;
originally announced January 2016.
-
Ramsey's Theorem for Pairs and $k$ Colors as a Sub-Classical Principle of Arithmetic
Authors:
Stefano Berardi,
Silvia Steila
Abstract:
The purpose is to study the strength of Ramsey's Theorem for pairs restricted to recursive assignments of $k$-many colors, with respect to Intuitionistic Heyting Arithmetic. We prove that for every natural number $k \geq 2$, Ramsey's Theorem for pairs and recursive assignments of $k$ colors is equivalent to the Limited Lesser Principle of Omniscience for $Σ^0_3$ formulas over Heyting Arithmetic. A…
▽ More
The purpose is to study the strength of Ramsey's Theorem for pairs restricted to recursive assignments of $k$-many colors, with respect to Intuitionistic Heyting Arithmetic. We prove that for every natural number $k \geq 2$, Ramsey's Theorem for pairs and recursive assignments of $k$ colors is equivalent to the Limited Lesser Principle of Omniscience for $Σ^0_3$ formulas over Heyting Arithmetic. Alternatively, the same theorem over intuitionistic arithmetic is equivalent to: for every recursively enumerable infinite $k$-ary tree there is some $i < k$ and some branch with infinitely many children of index $i$.
△ Less
Submitted 8 January, 2016;
originally announced January 2016.
-
Reverse Mathematical Bounds for the Termination Theorem
Authors:
Silvia Steila,
Keita Yokoyama
Abstract:
In 2004 Podelski and Rybalchenko expressed the termination of transition-based programs as a property of well-founded relations. The classical proof by Podelski and Rybalchenko requires Ramsey's Theorem for pairs which is a purely classical result, therefore extracting bounds from the original proof is non-trivial task. Our goal is to investigate the termination analysis from the point of view of…
▽ More
In 2004 Podelski and Rybalchenko expressed the termination of transition-based programs as a property of well-founded relations. The classical proof by Podelski and Rybalchenko requires Ramsey's Theorem for pairs which is a purely classical result, therefore extracting bounds from the original proof is non-trivial task. Our goal is to investigate the termination analysis from the point of view of Reverse Mathematics. By studying the strength of Podelski and Rybalchenko's Termination Theorem we can extract some information about termination bounds.
△ Less
Submitted 29 December, 2015;
originally announced December 2015.
-
Generic Large Cardinals and Systems of Filters
Authors:
Giorgio Audrito,
Silvia Steila
Abstract:
We introduce the notion of $\mathcal{C}$-system of filters, generalizing the standard definitions of both extenders and towers of normal ideals. This provides a framework to develop the theory of extenders and towers in a more general and concise way. In this framework we investigate the topic of definability of generic large cardinals properties.
We introduce the notion of $\mathcal{C}$-system of filters, generalizing the standard definitions of both extenders and towers of normal ideals. This provides a framework to develop the theory of extenders and towers in a more general and concise way. In this framework we investigate the topic of definability of generic large cardinals properties.
△ Less
Submitted 5 April, 2017; v1 submitted 17 November, 2015;
originally announced November 2015.
-
Proving termination with transition invariants of height omega
Authors:
Stefano Berardi,
Paulo Oliva,
Silvia Steila
Abstract:
The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose transitive closure, restricted to the accessible states, is included in some finite union of well-founded relations. An alternative statement of the theorem is that terminating reduction relations are precisely those having a…
▽ More
The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose transitive closure, restricted to the accessible states, is included in some finite union of well-founded relations. An alternative statement of the theorem is that terminating reduction relations are precisely those having a "disjunctively well-founded transition invariant". From this result the same authors and Byron Cook designed an algorithm checking a sufficient condition for termination for a while-if program. The algorithm looks for a disjunctively well-founded transition invariant, made of well-founded relations of height omega, and if it finds it, it deduces the termination for the while-if program using the Termination Theorem.
This raises an interesting question: What is the status of reduction relations having a disjunctively well-founded transition invariant where each relation has height omega? An answer to this question can lead to a characterization of the set of while-if programs which the termination algorithm can prove to be terminating. The goal of this work is to prove that they are exactly the set of reduction relations having height omega^n for some n < omega. Besides, if all the relations in the transition invariant are primitive recursive and the reduction relation is the graph of the restriction to some primitive recursive set of a primitive recursive map, then a final state is computable by some primitive recursive map in the initial state.
As a corollary we derive that the set of functions, having at least one implementation in Podelski Rybalchenko while-if language with a well-founded disjunctively transition invariant where each relation has height omega, is exactly the set of primitive recursive functions.
△ Less
Submitted 17 July, 2014;
originally announced July 2014.
-
A Boolean Algebraic Approach to Semiproper Iterations
Authors:
Matteo Viale,
Giorgio Audrito,
Silvia Steila
Abstract:
These notes present a compact and self-contained approach to iterated forcing with a particular emphasis on semiproper forcing. We tried to make our presentation accessible to any scholar who has some familiarity with forcing and boolean valued models and full details of all proofs are given.
We focus our presentation using the boolean algebra language and defining an iteration system as a direc…
▽ More
These notes present a compact and self-contained approach to iterated forcing with a particular emphasis on semiproper forcing. We tried to make our presentation accessible to any scholar who has some familiarity with forcing and boolean valued models and full details of all proofs are given.
We focus our presentation using the boolean algebra language and defining an iteration system as a directed and commutative system of complete and injective homomorphisms between complete and atomless boolean algebras.
It is well known that the boolean algebra approach to forcing and iterations is fully equivalent to the standard one. While there are several monographs where forcing is introduced by means of boolean valued models, to our knowledge no detailed account of iterated forcing following a boolean algebraic approach has yet appeared. We believe that this different approach is fruitful since the richness of the algebraic language simplifies many calculations and definitions, among which that of RCS-limits. Some of the advantages of this approach have been already outlined by Donder and Fuchs in http://arxiv.longhoe.net/abs/math/9207204.
The first part of these notes present the general framework needed to develop the notion of limit of an iterated system of forcings in the boolean algebraic language. The second part contains a proof of the main result of Shelah on semiproper iterations, i.e. that RCS-limit of semiproper iterations are semiproper.
△ Less
Submitted 7 February, 2014;
originally announced February 2014.
