Hercules and Hydra
Hercules and Hydra, a game on rooted finite trees
Interpreting reflexive theories in finitely many axioms
For finitely axiomatized sequential theories F and reflexive theories R, we give a characterization of the relation ’F interprets R’ in terms of provability of restricted consistency statements on cuts. This characterization is used in a proof that the set of (as well as ) sentences π such that GB interprets ZF+π is -complete.
Logiche modali con la proprietà del punto fisso
We introduce various kinds of fixed-point properties for modal logics, and we classify the most prominent systems according to these. Our goal is to do a first step towards a complete characterization of provability logics of (possibly non standard) derivability predicates for Peano Arithmetic.
Lower and upper bounds for the provability of Herbrand consistency in weak arithmetics
We prove that for i ≥ 1, the arithmetic does not prove a variant of its own Herbrand consistency restricted to the terms of depth in , where ε is an arbitrarily small constant greater than zero. On the other hand, the provability holds for the set of terms of depths in .
Majorizing provably recursive functions in fragments of PA.
Modal Translations of Heyting and Peano Arithmetic
More on extending automorphisms of models of Peano Arithmetic
Continuing the earlier research [Fund. Math. 129 (1988) and 149 (1996)] we give some information about extending automorphisms of models of PA to cofinal extensions.
O struktuře modelů omezené -indukce
On elementary cuts in models of arithmetic
On interpretability in theories containing arithmetic. II.
On the weak pigeonhole principle
We investigate the proof complexity, in (extensions of) resolution and in bounded arithmetic, of the weak pigeonhole principle and of the Ramsey theorem. In particular, we link the proof complexities of these two principles. Further we give lower bounds to the width of resolution proofs and to the size of (extensions of) tree-like resolution proofs of the Ramsey theorem. We establish a connection between provability of WPHP in fragments of bounded arithmetic and cryptographic assumptions (the existence...
On valued function fields III. Reductions of algebraic curves.
Order-types of models of arithmetic and a connection with arithmetic saturation.
Partial conservativity revisited
Provability in arithmetic and a schema of Grzegorczyk
Strong initial segments of models of IΔ₀
McAloon showed that if 𝓐 is a nonstandard model of IΔ₀, then some initial segment of 𝓐 is a nonstandard model of PA. Sommer and D'Aquino characterized, in terms of the Wainer functions, the elements that can belong to such an initial segment. The characterization used work of Ketonen and Solovay, and Paris. Here we give conditions on a model 𝓐 of IΔ₀ guaranteeing that there is an n-elementary initial segment that is a nonstandard model of PA. We also characterize the elements that can be included....
Subalgebras of diagonalizable algebras of theories containing arithmetic [Book]
The Consistency Of A Variant Of Church's Thesis With An Axiomatic Theory Of An Epistemic Notion.
The limit lemma in fragments of arithmetic
The recursion theoretic limit lemma, saying that each function with a graph is a limit of certain function with a graph, is provable in .