This paper discusses lower bounds for proof length, especially as measured by number of steps (inferences). We give the first publicly known proof of Gödel's claim that there is superrecursive (in fact, unbounded) proof speedup of (i + l)st-order arithmetic over ith-order arithmetic, where arithmetic is formalized in Hilbert-style calculi with + and • as function symbols or with the language of PRA. The same results are established for any weakly schematic formalization of higher-order logic: this allows all tautologies as axioms and allows all generalizations of axioms as axioms.

Our first proof of Gödel's claim is based on self-referential sentences: we give a second proof that avoids the use of self-reference based loosely on a method of Statman.

Let G be a Polish topological group, let X be a Polish space, let J: G × X → X be a Borel-measurable action of G on X, and let A ⊂ X be a Borel set which is invariant with respect to J, i.e., a Borel set of orbits. The following statement, or various equivalent versions of it, is known as the Topological Vaught's Conjecture.

We say that A contains perfectly many orbits if there is a perfect set P ⊂ A such that no two elements of P are in the same orbit. (Assuming ¬CH, A contains perfectly many orbits iff it contains 2ℵ0 orbits.) The Topological Vaught's Conjecture implies the usual, model theoretic, Vaught's Conjecture for Lω1ω, since the isomorphism classes are the orbits of an action of the group of permutations of ω; we give details in §0. The “Borel” assumption cannot be weakened for either A or J.

Given a Borel-measurable Polish action (G,X,J) and an invariant Borel set B ⊂ X, we say that B is a minimal counterexample if (G,X,J,B) is a counterexample to the Topological Vaught's Conjecture and for every invariant Borel C ⊂ B, either C or B\C contains only countably many orbits. This paper is concerned with counterexamples to the Topological Vaught's Conjecture (of course, there may not be any), and in particular, with minimal counterexamples. First, there is a theorem on the existence of minimal counterexamples. This theorem was known for the model theoretic case (it is due to Harnik and Makkai), and is here generalized to arbitrary Borel-measurable Polish actions. Second, we study the properties of minimal counterexamples. We give two different necessary and sufficient conditions for a counterexample to be minimal, as well as some consequences of minimality. Some of these results are proved assuming determinacy axioms.This second part seems to be new even in the model theoretic case.

We investigate the theory IΔ0+Ω1 and strengthen [Bu86, Theorem 8.6] to the following: if NP ≠ co-NP, then Σ-completeness for witness comparison foumulas is not provable in bounded arithmetic. i.e.,

Next we study a “small reflection principle” in bounded arithmetic. We prove that for all sentences φ

The proof hinges on the use of definable cuts and partial satisfaction predicates akin to those introduced by Pudlák in [Pu86].

Finally, we give some applications of the small reflection principle, showing that the principle can sometimes be invoked in order to circumvent the use of provable Σ-completeness for witness comparison formulas.

In the author's Relative lawlessness in intuitionistic analysis [this Journal, vol. 52 (1987), pp. 68–88] and An intuitionistic theory of lawlike, choice and lawless sequences [Logic Colloquium ’90, Springer-Verlag, Berlin, 1993, pp. 191–209] a notion of lawlessness relative to a countable information base was developed for classical and intuitionistic analysis. Here we simplify the predictability property characterizing relatively lawless sequences and derive it from the new axiom of closed data (classically equivalent to open data) together with a natural principle of invariance under finite translation. We characterize relative lawlessness in terms of a notion of forcing. Finally, we study relative lawlessness on an arbitrary fan and show that the collection of lawless binary sequences (which is comeager in the sense of Baire) has probability measure zero. The reasoning is predominantly constructive.

Classical logic is not adequate to face the essential vagueness of human reasoning, which is approximate rather than precise in nature. The logical treatment of the concepts of vagueness and approximation is of increasing importance in artificial intelligence and related research. Consequently, many logicians have proposed different systems of many-valued logic as a formalization of approximate reasoning (see, for example, Goguen [G], Gerla and Tortora [GT], Novak [No], Pavelka [P], and Takeuti and Titani [TT]). As far as we know, all the proposals are obtained by extending the range of truth values of propositions. In these logical systems reasoning is still exact and to make a conclusion the antecedent clause of its rule must match its premise exactly. In addition. Wang [W] pointed out: “If we compare calculation with proving,... Procedures of calculation... can be made so by fairly well-developed methods of approximation; whereas... we do not have a clear conception of approximate methods in theorem proving.... The concept of approximate proofs, though undeniably of another kind than approximations in numerical calculations, is not incapable of more exact formulation in terms of, say, sketches of and gradual improvements toward a correct proof” (see pp, 224–225). As far as the author is aware, however, no attempts have been made to give a conception of approximate methods in theorem proving.

The purpose of this paper is. unlike all the previous proposals, to develop a propositional calculus, a predicate calculus in which the truth values of propositions are still true or false exactly and in which the reasoning may be approximate and allow the antecedent clause of a rule to match its premise only approximately. In a forthcoming paper we shall establish set theory, based on the logic introduced here, in which there are ∣L∣ binary predicates ∈λ, λ ∈ L such that R(∈, ∈λ) = λ where ∈ stands for ∈1 and 1 is the greatest element in L, and x ∈λy is interpreted as that x belongs to y in the degree of λ, and relate it to intuitionistic fuzzy set theory of Takeuti and Titani [TT] and intuitionistic modal set theory of Lano [L]. In another forthcoming paper we shall introduce the resolution principle under approximate match and illustrate its applications in production systems of artificial intelligence.

Finitely axiomatizable ℵ1 categorical theories are locally modular.

Kernel contraction is a natural nonrelational generalization of safe contraction. All partial meet contractions are kernel contractions, but the converse relationship does not hold. Kernel contraction is axiomatically characterized. It is shown to be better suited than partial meet contraction for formal treatments of iterated belief change.

Let κ be a regular cardinal, and let B be a subalgebra of an interval algebra of size κ. The existence of a chain or an antichain of size κ in ℬ is due to M. Rubin (see [7]). We show that if the density of B is countable, then the same conclusion holds without this assumption on κ. Next we also show that this is the best possible result by showing that it is consistent with 2ℵ0 = ℵω1 that there is a boolean algebra B of size ℵω1 such that length(B) = ℵω1 is not attained and the incomparability of B is less than ℵω1. Notice that B is a subalgebra of an interval algebra. For more on chains and antichains in boolean algebras see. e.g., [1] and [2].

There is a family of questions in relativized complexity theory—weak analogs of the Friedberg Jump-Inversion Theorem—that are resolved by 1-generic sets but which cannot be resolved by essentially any weaker notion of genericity. This paper defines aw2-generic sets, i.e., sets which meet every dense set of strings that is re. in some incomplete r.e. set. Aw2-generic sets are very close to 1-generic sets in strength, but are too weak to resolve these questions. In particular, it is shown that for any set X there is an aw2-generic set G such that NPG ∩ co-NPG ⊈ PG⊕x. (On the other hand, if G is 1-generic, then NPG ∩ co-NPG ⊆ PG⊕SAT, where SAT is the NP-complete satisfiability problem [6].) This result runs counter to the fact that most finite extension constructions in complexity theory can be made effective. These results imply that any finite extension construction that ensures any of the Friedberg analogs must be noneffective, even relative to an arbitrary incomplete r.e. set. It is then shown that the recursion theoretic properties of aw2-generic sets differ radically from those of 1-generic sets: every degree above 0′ contains an aw2-generic set: no aw2-generic set exists below any incomplete r.e. set: there is an aw2-generic set which is the join of two Turing equivalent aw2-generic sets. Finally, a result of Shore is presented [30] which states that every degree above 0′ is the jump of an aw2-generic degree.

We present a sequent calculus for the modal logic S4, and building on some relevant features of this system (the absence of contraction rules and the confinement of weakenings into axioms and modal rules) we show how S4 can easily be translated into full prepositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities (exponentials) only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.

Let us consider countable languages L containing a unary predicate symbol P and L− =L\{P}. We also assume that L is relational. Then for any L-structure M, N = PM can naturally be considered as an L−-substructure of M. The main object of this paper will be the study of the following question: Under what condition does M have to be ℵ0-categorical. ℵ1-categorical, or stable if N is?

Hodges and Pillay [6] proved that if M is a countable symmetric extension of N and T = Th(M) is minimal over P (they said that T is one-cardinal over P), then the total categoricity of N implies that of M. This is a solution to a problem in Ahlbrandt and Ziegler [1]. The condition that “M is a symmetric extension of N” is an interpretation of the condition “every relation on N definable in M is definable within N”. We shall give several interpretations of this phrase: They are the Ø-reduction property, the reduction property, the strong reduction property, and the uniform reduction property (Definition 1). Under the assumptions, we study the question proposed above.

In §3 we treat the case that M is countable and show that if T is minimal over P and M has the strong reduction property over N, then M is ℵ0-categorical if N is (Theorem 5). This is a slight extension of the result of Hodges and Pillay mentioned above. (If M is countable and saturated, then the strong reduction property is equivalent to the condition that M will be symmetric over N if we add a finite number of appropriate constants.) A counterexample to this theorem has been obtained by Hrushovski in the case that only the Ø-reduction property is assumed. We also give a stronger result: If M has the Ø-reduction property over N and is ℵ0-categorical, M\N is infinite, and N is algebraically closed, then there is an expansion M* of M such that M* is not ℵo-categorical but M* still has the Ø-reduction property over N (Theorem 6). Moreover, we give an example such that M has the uniform reduction property over N. Th(M*) is minimal over P. N is ℵ0-categorical but M is not.

One of the basic theorems in universal algebra is Birkhoff's variety theorem: the smallest equationally axiomatizable class containing a class K of algebras coincides with the class obtained by taking homomorphic images of subalgebras of direct products of elements of K. G. Grätzer asked whether the variety theorem is equivalent to the Axiom of Choice. In 1980, two of the present authors proved that Birkhoff's theorem can already be derived in ZF. Surprisingly, the Axiom of Foundation plays a crucial role here: we show that Birkhoff's theorem cannot be derived in ZF + AC \{Foundation}, even if we add Foundation for Finite Sets. We also prove that the variety theorem is equivalent to a purely set-theoretical statement, the Collection Principle. This principle is independent of ZF\{Foundation}. The second part of the paper deals with further connections between axioms of ZF-set theory and theorems of universal algebra.

Elementary (first-order) and nonelementary (set-theoretic) aspects of the largest bisimulation are considered with a view toward analyzing operational semantics from the perspective of predicate logic. The notion of a bisimulation is employed in two distinct ways: (i) as an extensional notion of equivalence on programs (or processes) generalizing input/output equivalence (at a cost exceeding over certain transition predicates computable in log space), and (ii) as a tool for analyzing the dependence of transitions on data (which can be shown to be elementary or nonelementary, depending on the formulation of the transitions).

Let Ω be the least uncountable ordinal. Let be the category where the objects are the countable ordinals and where the morphisms are the strictly monotonic increasing functions. A dilator is a functor on which preserves direct limits and pullbacks. Let τ < ΩE ≔ min{ξ > Ω: ξ = ωξ}. Then τ has a unique “term”-representation in Ω. λξη.ωξ + η and countable ordinals called the constituents of τ. Let δ < Ω and K(τ) be the set of the constituents of τ. Let β = max K(τ). Let [β] be an occurrence of β in τ such that τ[β] = τ. Let be the fixed point-free version of the binary Aczel-Buchholz-Feferman-function (which is defined explicitly in the text below) which generates the Bachman-hierarchy of ordinals. It is shown by elementary calculations that is a dilator for every γ > max{β.δ.ω}.

By an “inverse iteration” of Sacks forcing over a model of V = L, we produce a model in which the degrees of constructibility of nonconstructible reals have order type

We settle a question in the literature about degrees of models of true arithmetic and upper bounds for the arithmetic sets. We prove that there is a model of true arithmetic whose degree is not a uniform upper bound for the arithmetic sets. The proof involves two forcing constructions.

We study how equivalent nonisomorphic models an unsuperstable theory can have. We measure the equivalence by Ehrenfeucht-Fraisse games. This paper continues the work started in [HT].

Throughout this paper denotes a nonprincipal ultrafilter and ℐ denotes the dual ideal. ℙ(ℐ) is the poset of all partial functions p: ω → 2 such that dom(p) ∈ ℐ. In [2], Grigorieff proved that ω1 is preserved in the corresponding generic extension if and only if is a P-point. Later, when Shelah introduced the notion of a proper poset, many people observed that if is a P-point, then ℙ(ℐ) is proper. One way of proving this is to show that player II has a winning strategy in the game for ℙ(ℐ) (see [3, p. 91].)

The notion of an Axiom A poset was introduced by Baumgartner [1]. If a poset satisfies Axiom A, then player II has a winning strategy in the game for ℙ, and thus, ℙ is proper. Indeed most of the naturally occurring proper posets satisfy Axiom A (e.g., Mathias's poset and Laver's poset). Thus, it is natural to ask whether or not ℙ(ℐ) satisfies Axiom A. The main result of this paper is a negative answer to this question. We will prove this by introducing another game and showing that is a P-point if and only if the corresponding game is undetermined. We will then show that if ℙ(ℐ) satisfied Axiom A, then player II would have a winning strategy in the corresponding game .

We let [X]<ω = {s ⊆ X∣ ∣s∣ < ω}. We let Seq(X) denote the set of finite sequences of elements of X. If s = 〈x0, …, xn〉 ∈ Seq(X) and y ∈ X, then s * 〈y〉 = 〈x0,…,xn,y〉 ∈ Seq(X).

We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.

Let X be a set, and let be the superstructure of X, where X0 = X and is the power set of X) for n ∈ ω. The set X is called a flat set if and only if for each x ∈ X, and x ∩ ŷ = ø for x, y ∈ X such that x ≠ y. where is the superstructure of y. In this article, it is shown that there exists a bijection of any nonempty set onto a flat set. Also, if is an ultrapower of (generated by any infinite set I and any nonprincipal ultrafilter on I), it is shown that is a nonstandard model of X: i.e., the Transfer Principle holds for and , if X is a flat set. Indeed, it is obvious that is not a nonstandard model of X when X is an infinite ordinal number. The construction of flat sets only requires the ZF axioms of set theory. Therefore, the assumption that X is a set of individuals (i.e., x ≠ ϕ and a ∈ x does not hold for x ∈ X and for any element a) is not needed for to be a nonstandard model of X.