We prove independence results concerning the number of nonisomorphic models (using the S-chain condition and S-properness) and the consistency of "ZCF + 2 ℵ 0 = ℵ 2 + there is a universal linear order of power ℵ 1 ". Most of these results were announced in [Sh 4], [Sh 5]. In subsequent papers we shall prove an analog f MA for forcing which does not destroy stationary subsets of ω 1 , investigate D-properness for various filters (...) and prove the consistency with G.C.H. of an axiom implying SH (for ℵ 1 ), and connected results. (shrink)

The theory , axiomatized by the induction scheme for sharply bounded formulae in Buss’ original language of bounded arithmetic , has recently been unconditionally separated from full bounded arithmetic S2. The method used to prove the separation is reminiscent of those known from the study of open induction.We make the connection to open induction explicit, showing that models of can be built using a “nonstandard variant” of Wilkie’s well-known technique for building models of IOpen. This makes it possible to transfer (...) many results and methods from open to sharply bounded induction with relative ease.We provide two applications: the Shepherdson model of IOpen can be embedded into a model of , which immediately implies some independence results for ; extended by an axiom which roughly states that every number has a least 1 bit in its binary notation, while significantly stronger than plain , does not prove the infinity of primes. (shrink)

This paper proves some independence results for weak fragments of Heyting arithmetic by using Kripke models. We present a necessary condition for linear Kripke models of arithmetical theories which are closed under the negative translation and use it to show that the union of the worlds in any linear Kripke model of HA satisfies PA. We construct a two-node PA-normal Kripke structure which does not force iΣ2. We prove i∀1 ⊬ i∃1, i∃1 ⊬ i∀1, iΠ2 ⊬ iΣ2 and (...) iΣ2 ⊬ iΠ2. We use Smorynski's operation Σ′ to show HA ⊬ lΠ1. (shrink)

We formulate several statements in Algebraic Logic that turn out to be independent of ZFC. We relate such statements to Martin's axiom, omitting types for variants of first order logic and topological properties of Baire spaces.

We extend an independence result proved in our earlier paper "Solovay's Theorem Cannot Be Simplified" (Annals of Pure and Applied Logic 112 (2001)). Our method uses the Barwise.

A Kripke-style semantics developed by de Jongh and Veltman is used to investigate relations between several extensions of interpretability logic, IL.

We present some new set and class theoretic independence results from ZFC and NBGC that are particularly simple and close to the primitives of membership and equality. They are shown to be equivalent to familiar small large cardinal hypotheses. We modify these independendent statements in order to give an example of a sentence in set theory with 5 quantifiers which is independent of ZFC. It is known that all 3 quantifier sentences are decided in a weak fragment of (...) ZF without power set. (shrink)

A bi-infinite approximate fixed point of type (n,k) is an approximate fixed point of type (n,k) whose terms are biinfinite; i.e., contain infin-itely many positive and infinitely many negative elements.

CZF is an intuitionistic set theory that does not contain Power Set, substituting instead a weaker version, Subset Collection. In this paper a Kripke model of CZF is presented in which Power Set is false. In addition, another Kripke model is presented of CZF with Subset Collection replaced by Exponentiation, in which Subset Collection fails.

We investigate the problem how to lift the non - $\forall \Sigma^b_1(\alpha)$ - conservativity of $T^2_2(\alpha)$ over $S^2_2(\alpha)$ to the expected non - $\forall \Sigma^b_i(\alpha)$ - conservativity of $T^{i+1}_2(\alpha)$ over $S^{i+1}_2(\alpha)$ , for $i > 1$ . We give a non-trivial refinement of the “lifting method” developed in [4,8], and we prove a sufficient condition on a $\forall \Sigma^b_1(f)$ -consequence of $T_2(f)$ to yield the non-conservation result. Further we prove that Ramsey's theorem, a $\forall \Sigma^b_1(\alpha)$ - formula, is not provable (...) in $T^1_2(\alpha)$ , and that $\forall \Sigma^b_j(\alpha)$ - conservativity of $T^{i+1}_2(\alpha)$ over $T^{i}_2(\alpha)$ implies $\forall \Sigma^b_j(\alpha)$ - conservativity of the whole $T_2(\alpha)$ over $T^{i}_2(\alpha)$ , for any $j \geq 2$. (shrink)

Acceptable programming systems have many nice properties like s-m-n-Theorem, Composition and Kleene Recursion Theorem. Those properties are sometimes called control structures, to emphasize that they yield tools to implement programs in programming systems. It has been studied, among others by Riccardi and Royer, how these control structures influence or even characterize the notion of acceptable programming system. The following is an investigation, how these control structures behave in the more general setting of complete numberings as defined by Mal'cev and Eršov.

Acceptable programming systems have many nice properties like s-m-n-Theorem, Composition and Kleene Recursion Theorem. Those properties are sometimes called control structures, to emphasize that they yield tools to implement programs in programming systems. It has been studied, among others by Riccardi and Royer, how these control structures influence or even characterize the notion of acceptable programming system. The following is an investigation, how these control structures behave in the more general setting of complete numberings as defined by Mal'cev and Eršov.

Let NBG be von Neumann-Bernays-Gödel set theory without the axiom of choice and let NBGA be the modification which allows atoms. In this paper we consider some of the well-known class or global forms of the wellordering theorem, the axiom of choice, and maximal principles which are known to be equivalent in NBG and show they are not equivalent in NBGA.

The purpose of this note is to show that the independence results for sharply bounded arithmetic of Takeuti [4] and Tada and Tatsuta [3] can be obtained and, in case of the latter, improved by the model-theoretic method developed by the author in [2].

We consider all combinatorially possible systems corresponding to subsets of finite set theory (i.e., Zermelo-Fraenkel set theory without the axiom of infinity) and for each of them either provide a well-founded locally finite graph that is a model of that theory or show that this is impossible. To that end, we develop the technique of axiom closure of graphs.

There are shown to many ε-Hermitian spaces, and an isometry criterion is stated which holds under MA ℵ 1 and is false under $2^{\aleph_0}.

We show that length initial submodels of S12 can be extended to a model of weak second order arithmetic. As a corollary we show that the theory of length induction for polynomially bounded second order existential formulae cannot define the function division.

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...) interpolation theorems for the following proof systems: (a) resolution (b) a subsystem of LK corresponding to the bounded arithmetic theory S 2 2 (α) (c) linear equational calculus (d) cutting planes. (2) New proofs of the exponential lower bounds (for new formulas) (a) for resolution ([15]) (b) for the cutting planes proof system with coefficients written in unary ([4]). (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory S 2 2 (α). In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

The logicD-J of the weak exluded middle with constant domains is proved to be incomplete with respect to Kripke semantics, by introducing models in presheaves on an arbitrary category. Additional incompleteness results are obtained for the modal systems with nested domains extendingQ-S4.1.

S. Adams, W. Ambrose, A. Andretta, H. Becker, R. Camerlo, C. Champetier, J.P.R. Christensen, D.E. Cohen, A. Connes. C. Dellacherie, R. Dougherty, R.H. Farrell, F. Feldman, A. Furman, D. Gaboriau, S. Gao, V. Ya. Golodets, P. Hahn, P. de la Harpe, G. Hjorth, S. Jackson, S. Kahane, A.S. Kechris, A. Louveau,, R. Lyons, P.-A. Meyer, C.C. Moore, M.G. Nadkarni, C. Nebbia, A.L.T. Patterson, U. Krengel, A.J. Kuntz, J.-P. Serre, S.D. Sinel'shchikov, T. Slaman, Solecki, R. Spatzier, J. Steel, D. Sullivan, S. (...) Thomas, A. Valette, V.S. Varadarajan, B. Velickovic, B. Weiss, J.D.M. Wright, R.J. Zimmer. (shrink)

We classify the phase transition thresholds from provability to unprovability for certain Friedman-style miniaturizations of Kruskal's Theorem and Higman's Lemma. In addition we prove a new and unexpected phase transition result for ε0. Motivated by renormalization and universality issues from statistical physics we finally state a universality hypothesis.

This paper is intended to give for a general mathematical audience a survey of intriguing connections between analytic combinatorics and logic. We define the ordinals below ε0 in non-logical terms and we survey a selection of recent results about the analytic combinatorics of these ordinals. Using a versatile and flexible compression technique we give applications to phase transitions for independence results, Hilbert’s basis theorem, local number theory, Ramsey theory, Hydra games, and Goodstein sequences. We discuss briefly universality (...) and renormalization issues in this context. Finally, we indicate how regularity properties of ordinal count functions can be used to prove logical limit laws. (shrink)

This article attempts a subjectively based approach, in fact one phenomenologically motivated, toward some key concepts of forcing theory, primarily the concepts of a generic set and its global properties and the absoluteness of certain fundamental relations in the extension to a forcing model M[G]. By virtue of this motivation and referring both to the original and current formulation of forcing I revisit certain set-theoretical notions serving as underpinnings of the theory and try to establish their deeper subjectively founded content (...) and also their influence in reaching relative consistency results by the forcing method. In this perspective, the present approach may be seen as offering an alternative view of the consistency results of K. Gödel and P. Cohen in mathematical foundations reaching a subjective level that may be taken as ultimately conditioning the non-decidability of key infinity statements on the level of formal theory. (shrink)

It is relatively consistent with ZFC that every countable $FU_{fin} $ space of weight N₁ is metrizable. This provides a partial answer to a question of G. Gruenhage and P. Szeptycki [GS1].

We study the measure independent character of Godel speed-up theorems. In particular, we strengthen Arbib's necessary condition for the occurrence of a Godel speed-up [2, p. 13] to an equivalence result and generalize Di Paola's speed-up theorem [4]. We also characterize undecidable theories as precisely those theories which possess consistent measure independent Godel speed-ups and show that a theory τ 2 is a measure independent Godel speed-up of a theory τ 1 if and only if the set of undecidable sentences (...) of τ 1 which are provable in τ 2 is not recursively enumerable. (shrink)

We study the expressive power of independence-friendly quantifier prefixes composed of universal$\left$, existential$\left$, and majority quantifiers$\left$. We provide four quantifier prefixes that can express NP hard properties and show that all quantifier prefixes capable of expressing NP-hard properties embed at least one of these four quantifier prefixes. As for the quantifier prefixes that do not embed any of these four quantifier prefixes, we show that they are equivalent to a first-order quantifier prefix composed of$\forall x$,$\exists x$, and Mx. In (...) unison, our results imply a dichotomy result: every independence-friendly quantifier prefix is either decidable in LOGSPACE or NP hard. (shrink)

This paper reports the findings of a study comparing the public examination results at GCE advanced and advanced supplementary levels of pupils with assisted places in the independent sector and pupils in the state sector of similar ability. The examination entries and results of pupils with APs were compared with those of pupils who had gained an AP at the same school but had not attended that school; they had, instead, taken their A levels in the state sector. (...) After controlling for ability it was found that the AP pupils achieved a significantly higher total point score in their A/AS levels than the pupils in the state sector and that the average point score per examination entry was higher for AP than state pupils. The results suggest that there is an advantage in taking up an AP but the possibility cannot be ruled out that the advantage for AP pupils arises from factors other than their education in the independent sector. (shrink)

Dividing independence for ultraimaginaries is neither symmetric nor transitive. Moreover, any notion of independence satisfying certain axioms (weaker than those for independence in a simple theory) and defined for all ultraimaginary sorts, is necessarily trivial.

In this paper we extend to non-classical set theories the standard strategy of proving independence using Boolean-valued models. This extension is provided by means of a new technique that, combining algebras (by taking their product), is able to provide product-algebra-valued models of set theories. In this paper we also provide applications of this new technique by showing that: (1) we can import the classical independence results to non-classical set theory (as an example we prove the independence (...) of $\mathsf {CH}$ ); and (2) we can provide new independence results. We end by discussing the role of non-classical algebra-valued models for the debate between universists and multiversists and by arguing that non-classical models should be included as legitimate members of the multiverse. (shrink)