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.

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 (see sections 4,5). 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 (see section 6). It is known that all 3 quantifier sentences are decided in (...) a weak fragment of ZF without power set (see [Fr02a]). (shrink)

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)

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.

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.

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.

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)

In this paper, I pursue such a logical foundation for arithmetic in a variant of Zermelo set theory that has axioms of subset separation only for quantifier-free formulae, and according to which all sets are Dedekind finite. In section 2, I describe this variant theory, which I call ZFin0. And in section 3, I sketch foundations for arithmetic in ZFin0 and prove that certain foundational propositions that are theorems of the standard Zermelian foundation for arithmetic are independent of ZFin0.<br><br>An equivalent (...) theory of sets and an equivalent foundation for arithmetic was introduced by John Mayberry and developed by the current author in his doctoral thesis. In that thesis, the independence results mentioned above are proved using proof-theoretic methods. In this paper, I offer model-theoretic proofs of the central independence results using the technique of cumulation models, which was introduced by Steve Popham, a doctoral student of Mayberry<br>from the early 1980s. (shrink)

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)

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