We show, roughly speaking, that it requires ω iterations of the Turing jump to decode nontrivial information from Boolean algebras in an isomorphism invariant fashion. More precisely, if α is a recursive ordinal, is a countable structure with finite signature, and d is a degree, we say that has αth-jump degreed if d is the least degree which is the αth jump of some degree c such there is an isomorphic copy of with universe ω in which the functions and relations have degree at most c. We show that every degree d ≥ 0(ω) is the ωth jump degree of a Boolean algebra, but that for n < ω no Boolean algebra has nth-jump degree d < 0(n). The former result follows easily from work of L. Feiner. The proof of the latter result uses the forcing methods of J. Knight together with an analysis of various equivalences between Boolean algebras based on a study of their Stone spaces. A byproduct of the proof is a method for constructing Stone spaces with various prescribed properties.

Introduction. In [Sh, Chapter IX], Shelah constructs a model of set theory in which Suslin's hypothesis is true, yet there is an Aronszajn tree which is not special. In his model, we have . He asks whether the same result could be obtained consistently with CH. In this paper, we answer his question in the affirmative.

Let us say that a tree T is S-st-special iff there is a function ƒ with dom(f) = {t ∈ T: rank(t) ∈ S} and for every t1 < t2 both in dom(t) we have f(t2) ≠ f(t1) < rank(t1). In Shelah's model, every tree is S-st-special for some fixed stationary costationary set S. Also, there is some tree T such that T is not S′-st-special whenever S′ – S is stationary. These properties, which are sufficient to ensure that Suslin's hypothesis holds and that T is not special, also hold in the model constructed in this paper. These properties also ensure that every Aronszajn tree has a stationary antichain (i.e., an antichain A such that {rank(t): t ∈ A} is stationary). Hence, it is natural to ask whether there is a model of Suslin's hypothesis in which some Aronszajn tree has no stationary antichain. We answer in the affirmative in [S].

The construction we use owes much to Shelah's approach to the theorem, due to Jensen (see [DJ]), that CH is consistent with Suslin's hypothesis. This is given in [Sh, Chapter V].

Davis, Matijasevic, and Robinson, in their admirable survey article [D-M-R], interpret the negative solution of Hilbert's Tenth Problem as a resounding positive statement about the versatility of Diophantine equations (that any listable set can be coded as the set of parameter values for which a suitable polynomial possesses integral solutions).

One can also view the Matijasevic result as implying that there are families of Diophantine equations parametrized by a variable t, which have integral solutions for some integral values t = a > 0, and yet there is no computable function of t which provides an upper bound for the smallest integral solution for these values a. The smallest integral solutions of the Diophantine equation for these values are, at least sporadically, too large to be bounded by any computable function. This is somewhat difficult to visualize, since there is quite an array of computable functions. But let us take an explicit example. Consider the function

Matijasevic's result guarantees the existence of parametrized families of Diophantine equations such that even this function fails to yield an upper bound for its smallest integral solutions (for all values of the parameter t for which there are integral solutions).

Families of Diophantine equations in a parameter t, whose integral solutions for t = 1, 2, 3,… exhibit a certain arythmia in terms of their size, have fascinated mathematicians for centuries, and this phenomenon (the size of smallest integral solution varying wildly with the parameter-value) is surprising, even when the equations are perfectly “decidable”.

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.

In this paper the modal operator “x is provable in Peano Arithmetic” is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.

The present article is an attempt to bridge the gap between the researchers that work in the areas adjacent to Hilbert's Tenth Problem (for short, HTP), mainly, number theory and mathematical logic. It presents the main results that have been obtained and asks some of the open questions in the area, leading to the main unanswered question (at least in the opinion of the author)—the analogue of HTP for the rational numbers. In this respect, the article is a successor of [Da] where the reader can find more information on the solution of the initial problem. Most of the results that are presented are not new, but some of the proofs are. As the purpose of a survey article is the “unification” of the methods involved, we present a proof of the analogue of HTP in the case of polynomial rings which is more geometric in nature than the initial proof of Denef (although it uses essentially the same tools). This allows, in our opinion, an easy introduction to the utilisation of the concepts used in the more recent approaches, like that of elliptic curves. We must say that the approach to the subject that we suggest through the questions we ask (mostly consisting of generalisations of HTP to various algebraic and analytic domains) is not the only one.

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.

In this paper, we consider certain cardinals in ZF (set theory without AC, the axiom of choice). In ZFC (set theory with AC), given any cardinals and , either ≤ or ≤ . However, in ZF this is no longer so. For a given infinite set A consider seq1-1(A), the set of all sequences of A without repetition. We compare |seq1-1(A)|, the cardinality of this set, to ||, the cardinality of the power set of A. What is provable about these two cardinals in ZF? The main result of this paper is that ZF ⊢ ∀A(| seq1-1(A)| ≠ ||), and we show that this is the best possible result. Furthermore, it is provable in ZF that if B is an infinite set, then | fin(B)| < | (B*)| even though the existence for some infinite set B* of a function ƒ from fin(B*) onto (B*) is consistent with ZF.

H. Friedman proved that the following sentence SWQO() is true but not provable in the theory ATR0 (cf. [S]; ≔ the set of finite rooted trees, ∣T∣ ≔ the cardinality of T ∈ ).

Since ATR0 is stronger than PA, SWQO() is not provable in PA, either. Furthermore, SWQO() is proof-theoretically stronger than PA. A similar sentence whose proof-theoretical strength is exactly that of PA was obtained by replacing finite trees by finite sequences of bounded natural numbers under the embeddability with H. Friedman's asymmetrical gap-condition (see [SS]). The latter sentence was modified by using the weaker symmetrical gap-condition (see the corresponding particular case in [Gl]). Further improvement is indicated in [G2, Corollary 4.5]. Namely, the assertion ∣Xi∣ ≤ k · (i + 1) as in SWQO(J), above, can be weakened to

.

(in fact, to wt(Xi) ≤ k + ε · i for an arbitrary fixed ε = l−1, l < 0, where wt(X) is the weight of the “word” X).

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.

If K is a class of semiassociative relation algebras and K contains the relation algebra of all binary relations on a denumerable set, then the word problem for the free algebra over K on one generator is unsolvable. This result implies that the set of sentences which are provable in the formalism ℒw× is an undecidable theory. A stronger algebraic result shows that the set of logically valid sentences in ℒw× forms a hereditarily undecidable theory in ℒw×. These results generalize similar theorems, due to Tarski, concerning relation algebras and the formalism ℒ×.

Let T be an uncountable, superstable theory. In this paper we prove

Theorem A. If T has finite rank, then I(|T|, T) ≥ ℵ0.

Theorem B. If T is trivial, then I(|T|, T) ≥ ℵ0.

In this paper we study the consistency strength of the theory

and we prove the consistency of this theory relative to the consistency of the existence of a supercompact cardinal and an inaccessible above it.

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.

In analogy to the definition of the halting problem K, an r.e. set A is called a diagonal iff there is a computable numbering ψ of the class of all partial recursive functions such that A = {i ∈ ω: ψi(i)↓} (in that case we say that A is the diagonal of ψ). This notion has been introduced in [10]. It captures all r.e. sets that can be constructed by diagonalization.

It was shown that any nonrecursive r.e. T-degree contains a diagonal, that for any diagonal A there is an r.e. nonrecursive nondiagonal B ≤TA, and that there are r.e. degrees a such that any r.e. set from a is a diagonal.

In §2 of the present paper we show that the property “A is a diagonal” is elementary lattice theoretic (e.l.t.). This result complements and generalizes previous results of Harrington and Lachlan, respectively. Harrington (see [16, XV. 1]) proved that the property of being the diagonal of some Gödelnumbering (i.e., of being creative) is e.l.t., and Lachlan [12] proved that the property of being a simple diagonal (i.e., of being simple and not hh-simple [10]) is e.l.t.

In §§3 and 4 we study the position of diagonals and nondiagonals inside the lattice of r.e. sets. We concentrate on an important class of nondiagonals, generalizing the maximal and hemimaximal sets: the -maximal sets. Using the results from [6] we are able to classify the -maximal sets that can be obtained as halfs of splittings of hh-simple sets.

We study interpolation for elementary fragments of classical linear logic. Unlike in intuitionistic logic (see [Renardel de Lavalette, 1989]) there are fragments in linear logic for which interpolation does not hold. We prove interpolation for a lot of fragments and refute it for the multiplicative fragment (→, +), using proof nets and quantum graphs. We give a separate proof for the fragment with implication and product, but without the structural rule of permutation. This is nearly the Lambek calculus. There is an appendix explaining what quantum graphs are and how they relate to proof nets.

The paper is a continuation of [The SCH revisited], In § 1 we define a forcing with countably many nice systems. It is used, for example, to construct a model “GCH below κ, c f κ = ℵ0, and 2κ > κ+ω” from 0(κ) = κ+ω. In §2 we define a triangle iteration and use it to construct a model satisfying “{μ ≤ λ∣c f μ = ℵ0 and pp(μ) > λ} is countable for some λ”. The question of whether this is possible was asked by S. Shelah. In §3 a forcing for blowing the power of a singular cardinal without collapsing cardinals or adding new bounded subsets is presented. Answering a question of H. Woodin, we show that it is consistent to have “c f κ = ℵ0. GCH below κ, 2κ > κ+, and ”. In §4 a variation of the forcing of [The SCH revisited, §1] is defined. It behaves nicely in iteration processes. As an application, we sketch a construction of a model satisfying:

“κ is a measurable and 2κ ≥ κ+α for some α, κ < c f α < α” starting with 0(κ) = κ+α. This answers the question from Gitik's On measurable cardinals violating the continuum hypothesis.

We analyse the Mitchell ordering in a model where κ is -hypermeasurable and > .

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and ∧,∨ (both of bounded arity). Then for every d ≥ 0 and n ≥ 2, there is a set of depth d sequents of total size O(n3+d) which are refutable in LK by depth d + 1 proof of size exp(O(log2n)) but such that every depth d refutation must have the size at least exp(nΩ(1)). The sets express a weaker form of the pigeonhole principle.

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.