We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the West or the original presentation can be improved using notions or results which appeared later. This includes such topics as Novikov's cut-elimination method (regular formulas) and Maslov's inverse method for the predicate logic.

An error has been found in the cited paper; namely, Theorem 3.1 is false.

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.

Indescribability is closely related to the reflection principles of Zermelo-Fränkel set theory. In this axiomatic setting the universe of all sets stratifies into a natural cumulative hierarchy (Vα: α ϵ On) such that any formula of the language for set theory that holds in the universe already holds in the restricted universe of all sets obtained by some stage.

The axioms of ZF prove the existence of many ordinals α such that this reflection scheme holds in the world Vα. Hanf and Scott noticed that one arrives at a large cardinal notion if the reflecting formulas are allowed to contain second order free variables to which one assigns subsets of Vα. For a given collection Ω of formulas in the ϵ language of set theory with higher type variables and a unary predicate symbol they define an ordinal α to be Ω indescribable if for all sentences Φ in Ω and A ⊆ Vα

Since a sufficient coding apparatus is available, this definition is (for the classes of formulas that we are going to consider) equivalent to the one that one obtains by allowing finite sequences of relations over Vα, some of which are possibly k-ary. We will be interested mainly in certain standardized classes of formulas: Let (, respectively) denote the class of all formulas in the language introduced above whose prenex normal form has n alternating blocks of quantifiers of type m (i.e. (m + 1)th order) starting with ∃ (∀, respectively) and no quantifiers of type greater than m. In Hanf and Scott [1961] it is shown that in ZFC, indescribability is equivalent to inaccessibility and indescribability coincides with weak compactness.

We generalize Specker's theorem on typical ambiguity, that NF and TST + Ambiguity have the same stratified consequences, to the subschemes Amb(Γ) of ambiguity restricted to classes of sentences Γ with certain natural closure conditions.

Via the formulas-as-types embedding certain extensions of Heyting Arithmetic can be represented in intuitionistic type theories. In this paper we discuss the embedding of ω-sorted Heyting Arithmetic HAω into a type theory WL, that can be described as Troelstra's system with so-called weak Σ-elimination rules. By syntactical means it is proved that a formula is derivable in HAω if and only if its corresponding type in WL is inhabited. Analogous results are proved for Diller's so-called restricted system and for a type theory based on predicate logic instead of arithmetic.

Let be p-adic closures of a countable Hilbertian field K. The main result of [EJ] asserts that the field has the following properties for almost all σ1,…,σe + m ϵ G(K) (in the sense of the unique Haar measure on G(K)e+m):

(a) Kσ is pseudo p-adically closed (abbreviation: PpC), i.e., each nonempty absolutely irreducible variety defined over Kσ has a Kσ-rational point, provided that it has a simple rational point in each p-adic closure of Kσ.

(b) G(Kσ) ≅ De,m, where De,m is the free profinite product of e copies Γ1,…, Γe of G(ℚp) and a free profinite group of rank m.

(c) Kσ has exactly e nonequivalent p-adic valuation rings. They are the restrictions Oσ1,…, Oσe of the unique p-adic valuation rings on , respectively.

In this paper we show that this result is in a certain sense the best possible. More precisely, we first show that the class of fields which satisfy (a)–(c) above is elementary in the appropriate language e(K), which is the ordinary first-order language of rings augmented by constant symbols for the elements of K and by e new unary relation symbols (interpreted as e p-adic valuation rings).

The mathematical treatment of the concepts of vagueness and approximation is of increasing importance in artificial intelligence and related research. The theory of fuzzy sets was created by Zadeh [Z] to allow representation and mathematical manipulation of situations of partial truth, and proceeding from this a large amount of theoretical and applied development of this concept has occurred. The aim of this paper is to develop a natural logic and set theory that is a candidate for the formalisation of the theory of fuzzy sets. In these theories the underlying logic of properties and sets is intuitionistic, but there is a subset of formulae that are ‘crisp’, classical and two-valued, which represent the certain information. Quantum logic or logics weaker than intuitionistic can also be adopted as the basis, as described in [L]. The relationship of this theory to the intensional set theory MZF of [Gd] and the global intuitionistic set theory GIZF of Takeuti and Titani [TT] is also treated.

By means of models in toposes of C-sets (where C is a small category), necessary conditions are found for the minimum quantified extension of a propositional (intermediate, modal) logic to be complete with respect to Kripke semantics; in particular, many well-known systems turn out to be incomplete.

Nous considérons des théories d'anneaux locaux reliées aux corps p-adiques, p un nombre premier. Dans le §1 nous établissons les axiomatisations données dans [B1], ainsi qu'une autre axiomatisation des anneaux apparaissant dans [R1]. Il s'agit d'anneaux locaux henséliens dont le corps résiduel est élémentairement équivalent à une extension finie d'un corps p-adique. Nous les appelons anneaux locaux p-adiquement clos. Dans le contexte de [R1] et [B1] ils apparaissent comme fibres du faisceau structural (aussi appelé faisceau de Nash dans [BS]) accompagnant les spectres p-adiques. L'intérêt de nos axiomatisations provient de la simplicité des axiomes qui rendent compte des propriétés henséliennes. Dans le §2 nous donnons une axiomatisation d'une théorie d'anneaux locaux qui apparaît naturellement dans le contexte de la théorie des modèles des corps valués, et se trouve être une complétion d'une théorie du §1. Nous appelons ces anneaux, anneaux intègres p-adiquement clos.

Dans le §3 nous utilisons §2 pour montrer que les anneaux intègres p-adiquement clos apparaissent aussi comme anneaux quotients d'anneaux de fonctions continues définissables sur les courbes affines p-adiques. Nous représentons alors un idéal premier comme le noyau d'un morphisme d'évaluation en un point non-standard de la courbe. Le spectre p-adique fournit un outil commode qui permet de décrire la situation de façon concise.

The logic KM is the smallest normal modal logic that includes the McKinsey axiom

It is shown here that this axiom is not valid in the canonical frame for KM, answering a question first posed in the Lemmon-Scott manuscript [Lemmon, 1966].

The result is not just an esoteric counterexample: apart from interest generated by the long delay in a solution being found, the problem has been of historical importance in the development of our understanding of intensional model theory, and is of some conceptual significance, as will now be explained.

The relational semantics for normal modal logics first appeared in [Kripke, 1963], where a number of well-known systems were shown to be characterised by simple first-order conditions on binary relations (frames). This phenomenon was systematically investigated in [Lemmon, 1966], which introduced the technique of associating with each logic L a canonical frame which invalidates every nontheorem of L. If, in addition, each L-theorem is valid in , then L is said to be canonical. The problem of showing that L is determined by some validating condition C, meaning that the L-theorems are precisely those formulae valid in all frames satisfying C, can be solved by showing that satisfies C—in which case canonicity is also established. Numerous cases were studied, leading to the definition of a first-order condition Cφ associated with each formula φ of the form

where Ψ is a positive modal formula.

Since its introduction in [K1-Po], the upper semilattice of Turing degrees has been an object of fascination to practitioners of the recursion-theoretic art. Starting from relatively simple concepts and definitions, it has turned out to be a structure of enormous complexity and richness. This paper is a contribution to the ongoing study of this structure.

Much of the work on Turing degrees may be formulated in terms of the embeddability of certain first-order structures in a structure whose universe is some set of degrees and whose relations, functions, and constants are natural degree-theoretic ones. Thus, for example, we know that if {P, ≤P) is a partial ordering of cardinality at most ℵ1 which is locally countable—each point has at most countably many predecessors—then there is an embedding

where D is the set of all Turing degrees and <T is Turing reducibility. If (P, ≤P) is a countable partial ordering, then the image of the embedding may be taken to be a subset of R, the set of recursively enumerable degrees. Without attempting to make the notion completely precise, we shall call embeddings of the first sort global, in contrast to local embeddings which impose some restrictions on the image set.

We generalize the ultrapower in a way suitable for choiceless set theory. Given an ultrafilter, forcing is used to construct an extended ultrapower of the universe, designed so that the fundamental theorem of ultrapowers holds even in the absence of the axiom of choice. If, in addition, we assume DC, then an extended ultrapower of the universe by a countably complete ultrafilter must be well-founded. As an application, we prove the Vopěnka-Hrbáček theorem from ZF + DC only (the proof of Vopěnka and Hrbáček used the full axiom of choice): if there exists a strongly compact cardinal, then the universe is not constructible from a set. The same method shows that, in L[2ω], there cannot exist a θ-compact cardinal less than θ (where θ is the least cardinal onto which the continuum cannot be mapped); a similar result can be proven for other models of the form L[A]. The result for L[2ω] is of particular interest in connection with the axiom of determinacy. The extended ultrapower construction of this paper is an improved version of the author's earlier pseudo-ultrapower method, making use of forcing rather than the omitting types theorem.

We consider the language L(Q), where L is a countable first-order language and Q is an additional generalized quantifier. A weak model for L(Q) is a pair 〈, q〉 where is a first-order structure for L and q is a family of subsets of its universe. In case that q is the set of classes of some equivalence relation the weak model 〈, q〉 is called a partition model. The interpretation of Q in partition models was studied by Szczerba [3], who was inspired by Pawlak's paper [2]. The corresponding set of tautologies in L(Q) is called rough logic. In the following we will give a set of axioms of rough logic and prove its completeness. Rough logic is designed for creating partition models.

The partition models are the weak models arising from equivalence relations. For the basic properties of the logic of weak models the reader is referred to Keisler's paper [1]. In a weak model 〈, q〉 the formulas of L(Q) are interpreted as usual with the additional clause for the quantifier Q: 〈, q〉 ⊨ Qx φ(x) iff there is some X ∊ q such that 〈, q〉 ⊨ φ(a) for all a ∊ X.

In case X satisfies the right side of the above equivalence we say that X is contained in φ(x) or, equivalently, φ(x) contains X.

We begin with some notes concerning the genesis of this paper. A preliminary version of it was written by the third author, who was moved by the desire to correct a mistake in Poizat [1987, p. 97], and to refresh some other minor results of the same book, concerning equations which are satisfied generically in a stable group. The book in question will be considered here as our basic reference on stable groups, and these other results will be discussed elsewhere.

This preliminary version contained §§1, 2 and 3 of the present paper, restricted to the context of groups of finite Morley rank. It was observed that a counterexample of finite rank to the above theorem would be an extreme refutation of a conjecture by Zil'ber and Cherlin (cyrillic alphabet order), that may be not so solid as was believed some time ago, which states that a simple group of finite rank should be an algebraic group. Additional motivation for the problem was seen in Reineke's theorem (Reineke [1975]), stating that a connected group of rank one is abelian—the cornerstone for the study of superstable groups—whose proof rests on the fact that a group with two conjugacy classes either has only two elements, or has infinite chains of centralizers (a property that violates stability).

At the source of what is now known as “geometric stability theory” was Zil'ber's intuition that the essential properties of an aleph-one-categorical theory were controlled by the geometries of its minimal types. (However, the situation is much more complex than was assumed in Zil'ber [1984], since the main conjecture of that paper has been disproved by Hrushovski.) This is not unnatural in this unidimensional case, where all these geometries have isomorphic contractions, but it was even realized later, in Cherlin, Harrington and Lachlan [1985] and Buechler [1986], that, for any superstable theory with finite ranks, a certain “local” property, i.e. a property satisfied by the geometry of each type of rank one (namely: to have a projective contraction), was equivalent to a “global” one (the theory is one-based, hence satisfies a coordinatization lemma). Then it was shown, in Pillay [1986], that this situation does not generalize to the infinite rank case, that, even for a theory of rank omega, the (local) assumption of projectivity for all the regular types of the theory does not have an exact global counterpart.

To clarify this kind of phenomena, I suggest here the elimination of their geometrical aspect, considering only the case where all of the geometries are degenerate. I will study various notions of triviality, which make sense in a stable context, and turn out to be equivalent in the finite rank case; some of them have a definite global flavour, others are of local character.

Here we give short and direct proofs of the Feferman-Vaught theorem and other preservation theorems in products of structures. In 1952, Mostowski [5] first showed the preservation of ≡ωω by direct powers of structures. Subsequently, in 1959, Feferman and Vaught [2] proved the preservation of ≡ωω by arbitrary direct products and also by reduced products with respect to cofinite filters. In 1962, Frayne, Morel and Scott [3] noticed that the results extend to arbitrary reduced products. In 1970, Barwise and Eklof [1] showed the preservation of ≡∞λ by products and in 1971 Malitz [4] showed the preservation of ≡κλ with κ strongly inaccessible (or ∞) by products. Below, we give short proofs of the above results. The ideas used here have initiated, in [7], [8], [9], [10], [11], the introduction of several new methods in the theory of products, which on the one hand give new, direct proofs of the known results in the area, including generalizations or strengthenings of some of those, and, on the other hand, give several new results as well in the theory of products and related areas.

Below, L denotes a (first order) language, and by a structure we mean an L-structure. 0 and 1 denote the logically valid and false sentence, respectively. We may write ā ∈ A for ā ∈ An for some n. Also, the values 1 and 2 of a parameter l in the definitions below express a duality corresponding to disjunctive and conjunctive forms.

We give a simple proof characterizing the complexity of Presburger arithmetic augmented with additional predicates. We show that Presburger arithmetic with additional predicates is complete. Adding one unary predicate is enough to get hardness, while adding more predicates (of any arity) does not make the complexity any worse.

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.

A paradigm of scientific discovery is defined within a first-order logical framework. It is shown that within this paradigm there exists a formal scientist that is Turing computable and universal in the sense that it solves every problem that any scientist can solve. It is also shown that universal scientists exist for no regular logics that extend first-order logic and satisfy the Löwenheim-Skolem condition.