Search

This is an introductory paper to a series of results linking generic absoluteness results for second and third order number theory to the model theoretic notion of model companionship. Specifically we develop here a general framework linking Woodin's generic absoluteness results for second order number theory and the theory of universally Baire sets to model companionship and show that (with the required care in details) a Π 2 -property formalized in an appropriate language for second order number theory is forcible from some T ⊇ ZFC + large cardinals if and only if it is consistent with the universal fragment of T if and only if it is realized in the model companion of T. In particular we show that the first order theory of H ω 1 is the model companion of the first order theory of the universe of sets assuming the existence of class many Woodin cardinals, and working in a signature with predicates for Δ 0 -properties and for all universally Baire sets of reals. We will extend these results also to the theory of H ℵ 2 in a follow up of this paper. [ABSTRACT FROM AUTHOR]

Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene's initial realizability laid the ground for more sophisticated notions such as Kreisel's modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion of realizability, namely herbrandized modified realizability. This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, which enables the gathering of witnesses into nonempty finite sets. We also show that the previous analysis can be extended from logic to (Heyting) arithmetic. [ABSTRACT FROM AUTHOR]

Akama et al. [1] introduced a hierarchical classification of first-order formulas for a hierarchical prenex normal form theorem in semi-classical arithmetic. In this paper, we give a justification for the hierarchical classification in a general context of first-order theories. To this end, we first formalize the standard transformation procedure for prenex normalization. Then we show that the classes E k and U k introduced in [1] are exactly the classes induced by Σ k and Π k respectively via the transformation procedure in any first-order theory. [ABSTRACT FROM AUTHOR]

In Arai (An ordinal analysis of a single stable ordinal, submitted) it is shown that an ordinal sup N < ω ψ Ω 1 (ε Ω S + N + 1) is an upper bound for the proof-theoretic ordinal of a set theory KP ℓ r + (M ≺ Σ 1 V) . In this paper we show that a second order arithmetic Σ 2 1 - - CA + Π 1 1 - CA 0 proves the wellfoundedness up to ψ Ω 1 (ε Ω S + N + 1 ) for each N. It is easy to interpret Σ 2 1 - - CA + Π 1 1 - CA 0 in KP ℓ r + (M ≺ Σ 1 V) . [ABSTRACT FROM AUTHOR]

Second-order arithmetic and class theory are second-order theories of mathematical subjects of foundational importance, namely, arithmetic and set theory. Despite the similarity in appearance, there turned out to be significant mathematical dissimilarities between them. The present paper studies various principles in class theory, from such a comparative perspective between second-order arithmetic and class theory, and presents a few new dissimilarities between them. [ABSTRACT FROM AUTHOR]

We systematically study the interrelations between all possible variations of Δ 1 0 variants of the law of excluded middle and related principles in the context of intuitionistic arithmetic and analysis. [ABSTRACT FROM AUTHOR]

In Cieśliński (J Philos Logic 39:325–337, 2010), Cieśliński asked whether compositional truth theory with the additional axiom that all propositional tautologies are true is conservative over Peano Arithmetic. We provide a partial answer to this question, showing that if we additionally assume that truth predicate agrees with arithmetical truth on quantifier-free sentences, the resulting theory is as strong as Δ 0 -induction for the compositional truth predicate, hence non-conservative. On the other hand, it can be shown with a routine argument that the principle of quantifier-free correctness is itself conservative. [ABSTRACT FROM AUTHOR]

In the language { 0 , 1 , ∘ , ⪯ } , where 0 and 1 are constant symbols, ∘ is a binary function symbol and ⪯ is a binary relation symbol, we formulate two theories, WD and D , that are mutually interpretable with the theory of arithmetic R and Robinson arithmetic Q , respectively. The intended model of WD and D is the free semigroup generated by { 0 , 1 } under string concatenation extended with the prefix relation. The theories WD and D are purely universally axiomatised, in contrast to Q which has the Π 2 -axiom ∀ x [ x = 0 ∨ ∃ y [ x = S y ] ] . [ABSTRACT FROM AUTHOR]