In this paper a method will be described which is intended to exhibit some relationships between sets of tautologies determined by truth-tables. This method is an attempt to form an algebra of truth-tables. The results sketched below are restricted to sets of tautologies determined by truth-tables with a finite number of elements and involving a single binary connective Δ. However, most of the results can be easily extended to the case of Tarski's logical matrix and even to a more general case.

We denote by S() the set of all tautologies (-tautologies) according to a given truth-table . Let describe a binary connective Δ. Then Δ()(x, y) stands for the truth-value of ΔPQ, when P has the truth-value x and Q has the truth-value y. If no ambiguity may arise we write Δ(x, y) or Δ() for Δ()(x, y).

Makkai [10] produced an arithmetical structure of Scott rank ω1CK. In [9], Makkai's example is made computable. Here we show that there are computable trees of Scott rank ω1CK. We introduce a notion of “rank homogeneity”. In rank homogeneous trees, orbits of tuples can be understood relatively easily. By using these trees, we avoid the need to pass to the more complicated “group trees” of [10] and [9], Using the same kind of trees, we obtain one of rank ω1CK that is “strongly computably approximable”. We also develop some technology that may yield further results of this kind.

Let κ be an infinite cardinal. A subset of (κκ)n is a -subset if it is the projection p[T] of all cofinal branches through a subtree T of (>κκ)n+1 of height κ. We define and -subsets of (κκ)n as usual.

Given an uncountable regular cardinal κ with κ = κ<κ and an arbitrary subset A of κκ, we show that there is a <κ-closed forcing ℙ that satisfies the κ+-chain condition and forces A to be a -subset of κκ in every ℙ-generic extension of V. We give some applications of this result and the methods used in its proof.

(i) Given any set x, we produce a partial order with the above properties that forces x to be an element of L.

(ii) We show that there is a partial order with the above properties forcing the existence of a well-ordering of κκ whose graph is a -subset of κκ × κκ.

(iii) We provide a short proof of a result due to Mekler and Väänänen by using the above forcing to add a tree T of cardinality and height κ such that T has no cofinal branches and every tree from the ground model of cardinality and height κ without a cofinal branch quasi-order embeds into T.

(iv) We will show that generic absoluteness for -formulae (i.e., formulae with parameters which define -subsets of κκ) under <κ-closed forcings that satisfy the κ+-chain condition is inconsistent.

In another direction, we use methods from the proofs of the above results to show that - and -subsets have some useful structural properties in certain ZFC-models.

R. Parikh has shown that in the predicate calculus without function symbols it is possible to decide whether or not a given formula A is provable in a Hilbert-style proof of k lines. He has also shown that for any formula A(x 1, …, xn ) of arithmetic in which addition and multiplication are represented by three-place predicates, {(a 1, …, an ): A(a 1, …, an ) is provable from the axioms of arithmetic in k lines} is definable in (N,′, +,0). See [2].

In §1 of this paper it is shown that if S is a definable set of n-tuples in (N,′, +, 0), then there is a formula A(x 1, …, xn ) and a number k so that (a 1 …, a n) ∈ S if and only if A(a 1 …, an ) can be proved in a proof of complexity k from the axioms of arithmetic. The result does not depend on which formalization of arithmetic is used or which (reasonable) measure of proof complexity. In particular, this gives a converse to Parikh's result.

In §II, a measure of proof complexity is given which is based on counting the quantifier steps in semantic tableaux. The idea behind this measure is that A is k provable if in the attempt to construct a counterexample one meets insurmountable difficulties in the definition of the appropriate Skolem functions over sets of cardinality ≤ k. A method is given for deciding whether or not a sentence A in the full predicate calculus is k provable. The question for the full predicate calculus and Hilbert-style systems of proof remains open.

We continue the investigation of the Laver ideal ℓ0 and Miller ideal m0 started in [GJSp] and [GRShSp]; these are the ideals on the Baire space associated with Laver forcing and Miller forcing. We solve several open problems from these papers. The main result is the construction of models for t < add(ℓ0), < add(m0), where add denotes the additivity coefficient of an ideal. For this we construct amoeba forcings for these forcings which do not add Cohen reals. We show that = ω2 implies add(m0) ≤ . We show that , implies cov(ℓ0) ≤ +, cov(m0) ≤ + respectively. Here cov denotes the covering coefficient. We also show that in the Cohen model cov(m0) < holds. Finally we prove that Cohen forcing does not add a superperfect tree of Cohen reals.

We prove conjugacy and generic disjointness of generous Carter subgroups in groups of finite Morley rank. We elaborate on groups with a generous Carter subgroup and on a minimal counterexample to the Genericity Conjecture.

Our main results are:

Theorem 1. Con(ZFC + “every function f: ω1 → ω1 is dominated by a canonical function”) implies Con(ZFC + “there exists an inaccessible limit of measurable cardinals”). [In fact equiconsistency holds.]

Theorem 3. Con(ZFC + “there exists a non-regular uniform ultrafilter on ω1”) implies Con(ZFC + “there exists an inaccessible stationary limit of measurable cardinals”).

Theorem 5. Con (ZFC + “there exists an ω1-sequence of ω1-complete uniform filters on ω1 s.t. every A ⊆ ω1 is measurable w.r.t. a filter in (Ulam property)”) implies Con(ZFC + “there exists an inaccessible stationary limit of measurable cardinals”).

We start with a discussion of the canonical functions and look at some combinatorial principles. Assuming the domination property of Theorem 1, we use the Ketonen diagram to show that ω2V is a limit of measurable cardinals in Jensen's core model KMO for measures of order zero. Using related arguments we show that ω2V is a stationary limit of measurable cardinals in KMO, if there exists a weakly normal ultrafilter on ω1. The proof yields some other results, e.g., on the consistency strength of weak*-saturated filters on ω1, which are of interest in view of the classical Ulam problem.

The system of sentential calculus presented below has peculiarities which may be of some interest. It is complete in the sense that every classical (two-valued) tautology is provable. In spite of this it is not Post complete (nor is it absolutely complete), i.e., one can add to the system an unprovable formula without proving a sentential variable as a theorem (or without making every formula a theorem). Thus the system may be extended by adjoining an unprovable formula without making the system inconsistent in the Post (or in absolute) sense. There are many distinct extensions of this kind. For every formula α1 that is not a theorem and which adjoined to the system does not make the system Post (or absolutely) inconsistent there is a formula α2 such that adjunction of α2 to the original system leaves α1 unprovable.

Let N denote the natural numbers. If A ⊆ N, we write Ā for the complement of A in N. A set A ⊆ N is cohesive if (i) A is infinite and (ii) for any recursively enumerable set W either W ∩ A or ∩ A is finite. A r.e. set M ⊆ N is maximal if is cohesive.

A recursively presented vector space (r.p.v.s.) U over a recursive field F consists of a recursive set U ⊆ N and operations of vector addition and scalar multiplication which are partial recursive and under which U becomes a vector space. A r.p.v.s. U has a dependence algorithm if there is a uniform effective procedure which applied to any n-tuple ν0, ν1, …, νn−1 of elements of U determines whether or not ν0, ν1 …, νn−1 are linearly dependent. Throughout this paper we assume that if U is a r.p.v.s. over a recursive field F then U is infinite dimensional and U = N. If W ⊆ U, then we say W is recursive (r.e., etc.) iff W is a recursive (r.e., etc.) subset of N. If S ⊆ U, we write (S)* for the subspace generated by S. If V1 and V2 are subspaces of U such that V1 ∩ V2 ={} (where is the zero vector of U), then we write V1 ⊕ V2 for (V1 ∪ V2)*. If V1 ⊆ V2⊆U are subspaces, we write V2/V1 for the quotient space.

A proof is given that the set of maximal intermediate propositional logics with the disjunction property and the set of maximal intermediate predicate logics with the disjunction property and the explicit definability property have the power of continuum. To prove our results, we introduce various notions which might be interesting by themselves. In particular, we illustrate a method to generate wide sets of pairwise “constructively incompatible constructive logics”. We use a notion of “semiconstructive” logic and define wide sets of “constructive” logics by representing the “constructive” logics as “limits” of decreasing sequences of “semiconstructive” logics. Also, we introduce some generalizations of the usual filtration techniques for propositional logics. For instance, “fitrations over rank formulas” are used to show that any two different logics belonging to a suitable uncountable set of “constructive” logics are “constructively incompatible”.

The comprehension principle of set theory asserts that a set can be formed from the objects satisfying any given property. The principle leads to immediate contradictions if it is formalized as an axiom scheme within classical first order logic. A resolution of the set paradoxes results if the principle is formalized instead as two rules of deduction in a natural deduction presentation of logic. This presentation of the comprehension principle for sets as semantic rules, instead of as a comprehension axiom scheme, can be viewed as an extension of classical logic, in contrast to the assertion of extra-logical axioms expressing truths about a pre-existing or constructed universe of sets. The paradoxes are disarmed in the extended classical semantics because truth values are only assigned to those sentences that can be grounded in atomic sentences.

§1. Introduction. It is a well-known phenomenon in set theory that problems in infinite combinatorics involving singular cardinals and their successors tend to be harder than the parallel problems for regular cardinals. Examples include the behaviour of cardinal exponentiation, the extent of the tree property, the extent of stationary reflection, and the existence of non-free almost-free abelian groups. The explanation for this phenomenon lies in inner model theory, in particular core models and covering lemmas. If W is an inner model of V then

1. W strongly covers V if every uncountable set of ordinals is covered by a set of the same V -cardinality lying in W.

2. W weakly covers V if W computes the successor of every V-singular cardinal correctly.

Strong covering implies weak covering.

In inner model theory there are many theorems of the general form “if there is no inner model of large cardinal hypothesis X then there is an L-like inner model Kx which Y covers V”. Here the L-like properties of Kx always include GCH and Global Square. Examples include

1. X is “0# exists”, Kx is L, Y is “strongly”.

2. X is “there is a measurable cardinal”, Kx is the Dodd-Jensen core model, Y is “strongly”.

3. X is “there is a Woodin cardinal”, Kx is the core model for a Woodin cardinal, Y is “weakly”.

We develop the theory of generically stable types, independence relation based on nonforking and stable weight in the context of dependent theories.

In this paper, we solve the strong uniqueness problem posed in [St2]. That is, we extend the full fine structure theory of [MiSt] to backgrounded models all of whose levels are tame (defined in [St2] and below). As a consequence, more powerful large cardinal properties reflect to fine structural inner models. For example, we get the following extension to [MiSt, Theorem 11.3] and [St2, Theorem 0.3].

Suppose that there is a strong cardinal that is a limit of Woodin cardinals. Then there is a good extender sequence such that

(1) every level of is a sound, tame mouse, and

(2) ⊨ “There is a strong cardinal that is a limit of Woodin cardinals”.

Recall that satisfies GCH if all its levels are sound. Another consequence of our work is the following covering property, an extension to [St1, Theorem 1.4] and [St3, Theorem 1.10].

Suppose that fi is a normal measure on Ω and that all premice are tame. Then Kc, the background certified core model, exists and is a premouse of height Ω. Moreover, for μ-almost every α < Ω.

Ideas similar to those introduced here allow us to extend the fine structure theory of [Sch] to the level of tame mice. The details of this extension shall appear elsewhere. From the extension of [Sch] and Theorem 0.2, new relative consistency results follow. For example, we have the following application.

If there is a cardinal κ such that κ is κ+-strongly compact, then there is a premouse that is not tame.

According to Kleene [8] and Post [13] the definition of recursive relations (or sets) can be given most simply via the definition of recursively enumerable (r.e.) relations. The latter can be defined by finite systems of finite rules for deriving strings of symbols, each rule being of the form

each formula or being obtained by juxtaposition from atomic symbols and variables ranging over strings of atomic symbols.

For several subsystems of second order arithmetic T we show that the proof-theoretic strength of T + (bar rule) can be characterized in terms of T + (bar induction)□, where the latter scheme arises from the scheme of bar induction by restricting it to well-orderings with no parameters. In addition, we demonstrate that , ACA0 + (bar rule) and ACA0 + (bar induction)□ prove the same -sentences.

We look at various notions of a class of definability operations that generalise inductive operations, and are characterised as “revision operations”. More particularly we: (i) characterise the revision theoretically definable subsets of a countable acceptable structure; (ii) show that the categorical truth set of Belnap and Gupta's theory of truth over arithmetic using fully varied revision sequences yields a complete Σ31 set of integers; (iii) the set of stably categorical sentences using their revision operator Ψ is similarly Σ31 and which is complete in GÖdel's universe of constructive sets L; (iv) give an alternative account of a theory of truth—realistic variance that simplifies full variance, whilst at the same time arriving at Kripkean fixed points.

Using a nonLaver modification of Uri Abraham’s minimal $\Delta _3^1$ collapse function, we define a generic extension $L[a]$ by a real a, in which, for a given $n \ge 3$, $\left\{ a \right\}$ is a lightface $\Pi _n^1 $ singleton, a effectively codes a cofinal map $\omega \to \omega _1^L $ minimal over L, while every $\Sigma _n^1 $ set $X \subseteq \omega $ is still constructible.

In what follows, L is a recursive language. The structures to be considered are L-structures with universe named by constants from ω. A structure is recursive A if the open diagram D() is recursive. Lerman and Schmerl [L-S] proved the following result.

Let T be an ℵ0-categorical elementary first-order theory. Suppose that for all n, , and T is arithmetical. Then T has a recursive model.

The aim of this paper is to extend Theorem 0.1. Stating the extension requires some terminology. Consider finitary formulas with symbols from L and sometimes extra constants from ω. For each n ∈ ω, the Σn and Πn formulas are as usual. Then Bnformulas are Boolean combinations of Σn formulas. For an L-structure , Dn() denotes the set of Bn sentences in the complete diagram Dc(). A complete Σn theory is a maximal consistent set of ΣnL-sentences. We may write φ(x), or Γ(x), to indicate that the free variables of the formula φ, or the set Γ, are among those in x. A complete Bn type for x is a maximal consistent set Γ(x) of Bn formulas with just the free variables x.

If T is ℵ0-categorical, then for each x only finitely many complete types Γ(x) are consistent with T. While Lerman and Schmerl stated their result just for ℵ0-categorical theories, essentially the same proof yields the following.

Theorem 0.2. Let T be a consistent, complete theory such that for all n andx, only finitely many complete Bn types Γ(x) are consistent with T.