We continue the work of [14, 3, 1, 19, 16, 4, 12, 11, 20] investigating the strength of set existence axioms needed for separable Banach space theory. We show that the separation theorem for open convex sets is equivalent to WKL0 over RCA0. We show that the separation theorem for separably closed convex sets is equivalent to ACA0 over RCA0. Our strategy for proving these geometrical Hahn–Banach theorems is to reduce to the finite-dimensional case by means of a compactness argument.

This paper is divided into three sections. §1 consists of an argument against the validity of Berry's paradox; §2 consists of supporting arguments for the thesis presented in §1; and §3 examines the possibility of re-establishing the paradox.

Berry's paradox, a semantic antinomy, is described on p. 4 of the textbook [4] as follows:

Let us define the intuitionistic part of a classical theory T as the intuitionistic theory whose proper axioms are identical with the proper axioms of T. For example, Heyting arithmetic HA is the intuitionistic part of classical Peano arithmetic PA.

It's a well-known fact, proved by Heyting and Myhill, that ZF is identical with its intuitionistic part.

In this paper, we mainly prove that TT, Russell's Simple Theory of Types, and NF, Quine's “New Foundations,” are not equal to their intuitionistic part. So, an intuitionistic version of TT or NF seems more naturally definable than an intuitionistic version of ZF.

In the first section, we present a simple technique to build Kripke models of the intuitionistic part of TT (with short examples showing bad properties of finite sets if they are defined in the usual classical way).

In the remaining sections, we show how models of intuitionistic NF2 and NF can be obtained from well-chosen classical ones. In these models, the excluded middle will not be satisfied for some non-stratified sentences.

We consider countably additive, nonnegative, extended real-valued measures which vanish on singletons. Such a measure is universal on a set X iff it is defined on all subsets of X and is semiregular iff every set of positive measure contains a subset of positive finite measure. We study the problem of existence of a universal semiregular measure on X which is invariant under a given group of bijections of X. Moreover we discuss some properties of universal, semiregular, invariant measures on groups.

We determine the modal logic of fixed-point models of truth and their axiomatizations by Solomon Feferman via Solovay-style completeness results. Given a fixed-point model $\mathcal {M}$ , or an axiomatization S thereof, we find a modal logic M such that a modal sentence $\varphi $ is a theorem of M if and only if the sentence $\varphi ^*$ obtained by translating the modal operator with the truth predicate is true in $\mathcal {M}$ or a theorem of S under all such translations. To this end, we introduce a novel version of possible worlds semantics featuring both classical and nonclassical worlds and establish the completeness of a family of noncongruent modal logics whose internal logic is nonclassical with respect to this semantics.

We prove that for every simple theory T (or even simple thick compact abstract theory) there is a (unique) compact abstract theory whose saturated models are the lovely pairs of T. Independence-theoretic results that were proved in [5] when is a first order theory are proved for the general case: in particular is simple and we characterise independence.

In [9] and [10] P. Kolaitis and M. Vardi proved that the 0-1 law holds for the second-order existential sentences whose first-order parts are formulas of Bernays-Schonfinkel or Ackermann prefix classes. They also provided several examples of second-order formulas for which the 0-1 law does not hold, and noticed that the classification of second-order sentences for which the 0-1 law holds resembles the classification of decidable cases of first-order prenex sentences. The only cases they have not settled are the cases of Gödel classes with and without equality.

In this paper we confirm the conjecture of Kolaitis and Vardi that the 0-1 law does not hold for the existential second-order sentences whose first-order part is in Gödel prenex form with equality. The proof we give is based on a modification of the example employed by W. Goldfarb [5] in his proof that, contrary to the Gödel claim [6], the class of Gödel prenex formulas with equality is undecidable.

In this paper we show (cf. Theorem 22) that in a language L* with equality, whose relation symbols denote arbitrary relations over ω* (=rational integers) and whose function symbols denote (= ∃∀ definable in the arithmetic hierarchy) functions over ω*, (i) a positive sentence is true in Λ* (= isolic integers) iff some Horn reduct is true in ω* with Skolem functions. We also show (cf Theorem 20) that (ii) a universally quantified sentence is true in Λ* iff some Horn reduct is true in Λ*.The latter result is nontrivial because our relations are arbitrary and our functions are In order to obtain (i) it was necessary to generalize the frame extensions of [7]. This is done in §2. Our extension procedure agrees with that of [7] for recursive relations (cf. Theorem 12), and is certainly more general for − relations. What happens in the case is still open. In §3 we develop the basic properties of our extension so that in §4 we can prove a metatheorem (cf. Theorems 8 and 10) about Λ (=isols), in a language L with equality whose relation symbols denote arbitrary relations over ω (=nonnegative integers) and whose function symbols denote almost R↑ combinatorial functions. In Theorem 11 this is generalized to infinitary universal sentences. In §5 generic isols are introduced. These are used (cf. Theorems 16–19) to generalize and simplify the “fundamental lemma” of [8]. The basic induction is patterned after Lemma 4.1 of [8], but is stronger in that any sufficiently generic assignment attainable from a frame yields Skolem functions. Finally in §6 these results are applied to Λ*, yielding the titled result (i) of our paper. Immediately following Theorem 15 there is a discussion which attempts to justify the way we extend relations to Λ.

The dominical categories were introduced by Di Paola and Heller, as a first step toward a category-theoretic treatment of the generalized first Godel incompleteness theorem [1]. In his Ph.D. dissertation [7], Rosolini subsequently defined the closely related p-categories, which should prove pertinent to category-theoretic representations of incompleteness for intuitionistic systems. The precise relationship between these two concepts is as follows: every dominical category is a pointed p-category, but there are p-categories, indeed pointed p-isotypes (all pairs of objects being isomorphic) with a Turing morphism that are not dominical. The first of these assertions is an easy consequence of the fact that in a dominical category C by definition the near product functor when restricted to the subcategory Ct, of total morphisms of C (as “total” is defined in [1]) constitutes a bona fide product such that the derived associativity and commutativity isomorphisms are natural on C × C × C and C × C, respectively, as noted in [7]. As to the second, p-recursion categories (that is, pointed p-isotypes having a Turing morphism) that are not dominical were defined and studied by Montagna in [6], the syntactic p-categories ST and S′T associated with consistent, recursively enumerable extensions of Peano arithmetic, PA. These merit detailed investigation on several counts.

In a recent paper (here referred to as “IDP”) the writer outlined a decision procedure for Lewis's system S4 of modal logic. One of the clauses in definition 3.1 of IDP requires correction. Clause II of 3.1 (2) should read as follows.

II. Some constituent of the form ◊β, of degree n1 ≤ n, has the value T in Row (i), and some constituents of the forms ◊δ1, … ◊δh, and ◊η1, …, ◊ηm, all have the value F in Row (i) (h ≥ 0, m ≥ 0, h+m ≥ 1), where β → (δ1 ∨ … ∨ δh ∨ ◊η1 ∨ … ∨ ◊ηm) is an (n1 − 1)-tautology of S4.

This change is required in order to carry out the proof of Metathcorcm 3.19. In particular, the change guarantees the following. If the expression η of the second paragraph of 3.20 is of degree n − 1, then the antecedent λ of formula ζ on page 210 of IDP is also of degree n − 1; and consequently the formula ζ of 3.19 is of degree n (since ◊λ is a constituent of ζ). (If we fail to make the correction, then it might be the case that both ζ and (3) are of degree n − 1, in which case Row (i) would not satisfy clause II as originally stated, contrary to the claim at the end of 3.20.) The proofs for the remaining cases of 3.20 can then be carried out, using the revised clause II, in the way originally indicated.

The proof of Metatheorem 3.2 requires only trivial corrections for case 2.

We show: The procedure mentioned in the title is often impossible. It requires at least an inner model with a measurable cardinal. The consistency strength of changing and from a regular κ to some regular δ < κ is a measurable of Mitchell order δ. There is an application to Cichoń's diagram.

Let N, O and S denote the set of nonnegative integers, the graph of the constant 0 function and the graph of the successor function respectively. For sets P, Q, R ⊆ N2 operations of transposition, composition, and bracketing are defined as follows: P∪ = {〈x, y〉 ∣ 〈y, x〉 ∈ P}, PQ = {〈x, z〉 ∣ ∃y〈x, y〉 ∈ P & 〈y, z〉 ∈ Q}, and [P, Q, R] = ⋃n ∈ M(Pn Q Rn).

Theorem. The class of recursively enumerable subsets of N2 is the smallest class of sets with O and S as members and closed under transposition, composition, and bracketing.

This result is derived from a characterization by Julia Robinson of the class of general recursive functions of one variable in terms of function composition and “definition by general recursion.” A key step in the proof is to show that if a function F is defined by general recursion from functions A, M, P and R then F = [P∪, A∪M, R].

The above definitions of the transposition, composition, and bracketing operations on subsets of N2 can be generalized to subsets of X2 for an arbitrary set X. In this abstract setting it is possible to show that the bracket operation can be defined in terms of K, L, transposition, composition, intersection, and reflexive transitive closure where K: X → X and L: X → X are functions for decoding pairs.

Let S be a recursive theory. Let a theory T* consisting of Σ1 sentences be called maximal (with respect to S) if T* is maximal consistent with S, i.e. there is no Σ1 sentence consistent with T* + S which is not in T*.

A maximal theory with respect to IΔ0 was considered by Wilkie and Paris in [WP] in connection with the end-extension problem.

Let us recall that IΔ0 is the fragment of Peano arithmetic consisting of the finite collection of algebraic axioms PA− together with the induction scheme restricted to bounded formulas.

The main open problem concerning the end-extendability of models of IΔ0 is the following:

(*) Does every model of IΔ0 + BΣ1 have a proper end-extension to a model of IΔ0?

Here BΣ1 is the following collection scheme:

where φ runs over bounded formulas and may contain parameters.

It is well known(see [KP]) that if I is a proper initial segment of a model M of IΔ0, then I satisfies IΔ0 + BΣ1.

For a wide discussion of the problem (*) see [WP]. Wilkie and Paris construct in [WP] a model M of IΔ0 + BΣ1 which has no proper end-extension to a model of IΔ0 under the assumption IΔ0 ⊢¬Δ0 H (see [WP] for an explanation of this assumption). Their model M is a model of a maximal theory T* where S = IΔ0.

Moreover, T*, which is the set Σ1(M) of all Σ1 sentences true in M, is not codable in M.

The purpose of this note is to give a short proof of a conjecture of Feiner that every countable Boolean algebra has an ordered basis that is a lexicographic sum of well-ordered sets over the ordered set η of all rational numbers. Actually, we prove a slightly more precise fact, which is formulated below as Theorem 3. An earlier proof of Feiner's conjecture was obtained by David Cossack (unpublished), using a different method.

Our proof will use the following property of Cantor's dyadic discontinuum D.

Assuming AD + (V = L(R)), it is shown that for κ an admissible Suslin cardinal, o(κ) (= the order type of the stationary subsets of κ) is “essentially” regular and closed under ultrapowers in a manner to be made precise. In particular, o(κ) ≫ κ+, κ++, etc. It is conjectured that this characterizes admissibility for L(R).

We prove the following algebraic characterization of elementary equivalence: ≡ restricted to countable structures of finite type is minimal among the equivalence relations, other than isomorphism, which are preserved under reduct and renaming and which have the Robinson property; the latter is a faithful adaptation for equivalence relations of the familiar model theoretical notion. We apply this result to Friedman's fourth problem by proving that if is an (ω1, ω)-compact logic satisfying both the Robinson consistency theorem on countable structures of finite type and the Löwenheim-Skolem theorem for some λ < ωω for theories having ω1 many sentences, then ≡L = ≡ on such structures.

Unter der Peano-Arithmetik verstehe ich im Folgenden eine über dem Prädikatenkalkül der ersten Stufe formalisierte Arithmetik der natürlichen Zahlen, in der als außerlogische Konstanten nur Symbole für die Null, die Nachfolgeroperation und die Gleichheitsbeziehung (die als mathematischer Grundbegriff aufgefaßt wird) vorkommen.

Ein Ausdruck H(c), in dem c die einzige freie Variable ist, heiße: ∀-defekt in Bezug auf ein (deduktives) System S, wenn (a) für jede Ziffer , und (b) nicht ∀xH(x) ϵ S.

Im allgemeinen wird das deduktive System durch ein Axiomensystem in Verbindung mit einer Syntax gegeben sein. Auf diesen Fall soil die Redeweise sinngemäß übertragen werden.

Ein System S heiße ω-unvollständig, wenn es einen in Bezug auf S ∀-defekten Ausdruck gibt.

Ein Axiomensystem A heiße kategorisch, wenn beliebige absolute Modelle (s. Abschnitt IV) von A isomorph sind.

Die Kategorizität stellt eine gewisse Vollständigkeit des Axiomensystems dar. Daß solche Axiomensysteme ω-unvollstandig sein können (bzw. im Fall der ausdrucksreicheren Arithmetik nach Gödel sogar müssen), ist eben das Überraschende.

Ich werde im Folgenden für zwei kategorische Axiomensysteme der Peano-Arithmetik die ω-Unvollständigkeit in Bezug auf die Prädikatenlogik der ersten Stufe nachweisen. In beiden Fallen gelingt der Nachweis der ω-Unvollständigkeit durch Diskussion eines ∀-defekten Ausdrucks H(c).

Forcing method on Bounded Arithmetic was first introduced by J. B. Paris and A. Wilkie in [10]. Then in [1], [2] and [3], M. Ajtai used the method to get excellent results on the pigeon hole principle and the modulo p counting principle. The forcing method on Bounded arithmetic was further developed by P. Beame, J. Krajíček and S. Riis in [4], [7], [6], [8], [5], [12], [11], [13]. It should be noted that J. Krajíček and P. Pudlák used an idea of Boolean valued in [9] and also Boolean valued notion is efficiently used for model theoretic constructions in [7], [6], [8], [5].

In our previous paper [14], we developed a Boolean valued version of forcing on Bounded Arithmetic using Boolean algebra which is generated by polynomial size circuits from Boolean variables and discussed its relation with NP = co-NP problem and P = NP problem. Especially we proved the following theorem and related theorems as Theorems 2, 3 and 4 in Section 2.

Theorem. If M[G] is not a model of S2, then NP ≠ co-NP and therefore P ≠ NP.

However in the proof of the Theorem, we used a consequence of P = NP. More precisely we used the following as a consequence of NP = co-NP, though it is a consequence of P = NP but not a consequence of NP = co-NP.

Suppose that NP = co-NP holds. Then there exists an NP-complete predicate ∃x ≤ t(a) A(x,a) with sharply bounded A(x, a) and a sharply bounded B(y, a) such that ∃x ≤ t(a) A(x,a) ↔ ∀y ≤ s(a)B(y, a). Then there exists polynomial time computable functions f and g such that the following two sequents hold.

This paper is a contribution to the growing literature on the model theory of nilpotent groups. (See Baumslag and Levin [2]; Eršov [5]; Hodges [9], [10]; Mal′cev [14]; Olin [16] and Saracino [19], [20].) In it we investigate the conditions under which the free product in the variety of all nilpotent of class 2 (nil-2) groups preserves saturation and stability.

It is well known that the direct product preserves both saturation (see Waszkiewicz and Wȩglorz [23]) and stability (see Wierzejewski [24]; Macintyre [13]; Eklof and Fisher [4]). On the other hand it is easy to show that the full free product of groups preserves neither property; indeed, in the case of saturation this failure is extremely bad since no free product of nontrivial groups is even 2-saturated. Our results show that the nil-2 free product falls between these two extremes.

Our proofs are mainly model-theoretic with a smattering of elementary algebra and rely heavily upon the unique normal form for the elements of a nil-2 free product given by MacHenry in [12]. (This normal form and some of its consequences are discussed in §1.) We assume familiarity with the basic ideas of saturation (see Chapter 5 of [3]) and Shelah's treatment of stability in [22].

We prove two main theorems in §3 each giving a necessary and sufficient condition in separate situations for the preservation of saturation. In the first (Theorem 3.1) we allow one finite factor, while in the second (Theorem 3.10) we deal solely with torsion groups. Our motivation for the proof of sufficiency was the paper of Waszkiewicz and Wȩglorz [23] and the principal tool is a “Feferman-Vaught” Theorem for the nil-2 free product which we prove in §2. We also show that if both factors in a nil-2 free product are nontorsion and one factor has a nil-2 basis, then the group is not even 3-saturated. We leave open the case where both factors are infinite but only one is torsion.