In his very interesting address On the calculus of refations, Professor Tarski discussed alternative bases for that calculus. He was there interested in “…different methods of setting up the foundations of this elementary calculus in a rigorously deductive way…” and so did not discuss the method of developing the calculus of relations with which this paper is concerned. Our purpose here is to show how the use of matrix notation for relations permits an algorithmic rather than a postulational-deductive development of the calculus of relations. One limitation of the present approach is to be admitted at the very outset: to enjoy the full benefits of the matrix approach, we are obliged to confine our investigations to Universes of Discourse which are finite. The reason for this restriction will become apparent presently.

We investigate topological properties of subsets S of the real plane, expressed by first-order logic sentences in the language of the reals augmented with a binary relation symbol for S. Two sets are called topologically elementary equivalent if they have the same such first-order topological properties. The contribution of this paper is a natural and effective characterization of topological elementary equivalence of closed semi-algebraic sets.

It is shown how to define forcing semantics within metatheories not containing the power-set construction, in particular, how to construct exponents assuming only (a slightly strengthened form of) exponents in the metatheory. Some straightforward applications (consistency and independence results, and derived rules) are obtained for such systems.

The Inner Model Hypothesis (IMH) and the Strong Inner Model Hypothesis (SIMH) were introduced in [4]. In this article we establish some upper and lower bounds for their consistency strength.

We repeat the statement of the IMH, as presented in [4]. A sentence in the language of set theory is internally consistent iff it holds in some (not necessarily proper) inner model. The meaning of internal consistency depends on what inner models exist: If we enlarge the universe, it is possible that more statements become internally consistent. The Inner Model Hypothesis asserts that the universe has been maximised with respect to internal consistency:

The Inner Model Hypothesis (IMH): If a statement φ without parameters holds in an inner model of some outer model of V (i.e., in some model compatible with V), then it already holds in some inner model of V.

Equivalently: If φ is internally consistent in some outer model of V then it is already internally consistent in V. This is formalised as follows. Regard V as a countable model of Gödel-Bernays class theory, endowed with countably many sets and classes. Suppose that V* is another such model, with the same ordinals as V. Then V* is an outer model of V (V is an inner model of V*) iff the sets of V* include the sets of V and the classes of V* include the classes of V. V* is compatible with V iff V and V* have a common outer model.

We locate winning strategies for various -games in the L-hierarchy in order to prove the following:

Theorem 1. KP + Σ2-Comprehension -Determinacy.”

Alternatively: “there is a β-model of-Determinacy.” The implication is not reversible. (The antecedent here may be replaced with instances of Comprehension with only -lightface definable parameters—or even weaker theories.)

Theorem 2. KP + Δ2-Comprehension + Σ2-Replacement + -Determinacy.

(Here AQI is the assertion that every arithmetical quasi-inductive definition converges.) Alternatively: -Determinacy.

Hence the theories: , and are in strictly descending order of strength.

Among others we will prove that the equational theory of ω dimensional representable polyadic equality algebras (RPEAω's) is not schema axiomatizable. This result is in interesting contrast with the Daigneault-Monk representation theorem, which states that the class of representable polyadic algebras is finite schema-axiomatizable (and hence the equational theory of this class is finite schema-axiomatizable. as well). We will also show that the complexity of the equational theory of RPEAω is also extremely high in the recursion theoretic sense. Finally, comparing the present negative results with the positive results of Ildikó Sain and Viktor Gyuris [12], the following methodological conclusions will be drawn: The negative properties of polyadic (equality) algebras can be removed by switching from what we call the “polyadic algebraic paradigm” to the “cylindric algebraic paradigm”.

Several canonical partition theorems are obtained, including a simultaneous generalization of Neumer's lemma and the Erdös-Rado theorem. The canonical partition relation for infinite cardinals is completely determined, answering a question of Erdös and Rado. Counterexamples are given showing that in several ways these results cannot be improved.

The paper is concerned with the existence of a universal graph at the successor of a strong limit singular μ of cofinality ℵ0. Starting from the assumption of the existence of a supercompact cardinal, a model is built in which for some such μ there are μ++ graphs on μ+ that taken jointly are universal for the graphs on μ+, while .

The paper also addresses the general problem of obtaining a framework for consistency results at the successor of a singular strong limit starting from the assumption that a supercompact cardinal κ exists. The result on the existence of universal graphs is obtained as a specific application of a more general method.

The logic extends first-order logic by a generalized form of counting quantifiers (“the number of elements satisfying … belongs to the set C”). This logic is investigated for structures with an injectively ω-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [6]. It is shown that, as in the case of automatic structures [21], also modulo-counting quantifiers as well as infinite cardinality quantifiers (“there are many elements satisfying …”) lead to decidable theories. For a structure of bounded degree with injective ω-automatic presentation, the fragment of that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (ω-automaticity and bounded degree) are necessary for this result to hold.

Whenever particular ordinals are used as tools in a proof or a definition, it is necessary to find a way of representing them. If the ordinals are sufficiently small, there is a standard way (e.g. Cantor normal forms for ordinals less than ε0); in general, representations are often found by using functions on initial segments of the ordinals: Each term which can be obtained from by applications of a function symbol is regarded as a notation for the ordinal obtained by the same applications of the function f to the ordinal 0. In this way, f provides representations for all the ordinals in Clf(0), the closure set of f (se e §1). (For an introduction to and development of this principle, see Feferman [F1]; and for a discussion of the significance of such representations in proof theory, see Kreisel [K1, pp. 22–34].) Thus it is natural to ask whether there are connections between frequently encountered properties of ordinal functions and the size of the ordinals for which they can provide representations.

The purpose of this paper is to show that, for any integer n, the ordinal (see §2) is a bound for the closure ordinals of replete monotonic increasing n-place functions. This result is optimal for n > 2 (the bound is attained by where θα = 1 + α) but not for n < 2. D. H. de Jongh has recently proved, using a completely different method, that the (least possible) bound for n = 2 is ε0. (Trivially, that for n = 1 is φ.)

We present a critical discussion of the claim (most forcefully propounded by Chaitin) that algorithmic information theory sheds new light on Gödel's first incompleteness theorem.

It is well known that the familiar Sheffer stroke function of the 2-valued propositional calculus is functionally complete (i.e., for any m, all 22m truth functions of m variables can be defined1 in terms of the stroke function). Indeed, it is not difficult to show that of the 16 2-valued functions of two variables, exactly two of them are functionally complete.

The historical researches of Louis Couturat saved the logical work of Leibniz from the oblivion of neglect and forgetfulness. They revealed that Leibniz developed in succession several versions of a “logical calculus” (calculus ratiocinator or calculus universalis). In consequence of Couturat's investigations it has become well known that Leibniz's development of these logical calculi adumbrated the notion of a logistic system; and for these foreshadowings of the logistic treatment of formal logic Leibniz is rightly regarded as the father of symbolic logic.

It is clear from what has been said that it is scarcely possible to overestimate the debt which the contemporary student of Leibniz's logic owes to Couturat. This gratitude must, however, be accompanied by the realization that Couturat's own theory of logic is gravely defective. Couturat was persuaded that the extensional point of view in logic is the only one which is correct, an opinion now quite antiquated, and shared by no one. This prejudice of Couturat's marred his exposition of Leibniz's logic. It led him to battle with windmills: he viewed the logic of Leibniz as rife with shortcomings stemming from an intensional approach.

The task of this paper is a re-examination of Leibniz's logic. It will consider without prejudgment how Leibniz conceived of the major formal systems he developed as logical calculi – that is, these systems will be studied with a view to the interpretation or interpretations which Leibniz himself intends for them. The aim is to undo some of the damage which Couturat's preconception has done to the just understanding of Leibniz's logic and to the proper evaluation of his contribution.

We are inclined to believe that, by means of an argument entirely analogous to that which leads to the Richard antinomy, the notion of definability as applied to entities discussed in a formal system can easily be shown not to be itself definable in this system. It will be seen from this discussion that actually the situation is not quite so simple as it would appear at first glance. Our discussion will have a rather sketchy and informal character.

We consider the following problem: Given a proof of the Skolemization of a formula F, what is the length of the shortest proof of F? For the restriction of this question to cut-free proofs we prove corresponding exponential upper and lower bounds.

We show that there is a restriction, or modification of the finite-variable fragments of First Order Logic in which a weak form of Craig's Interpolation Theorem holds but a strong form of this theorem does not hold. Translating these results into Algebraic Logic we obtain a finitely axiomatizable subvariety of finite dimensional Representable Cylindric Algebras that has the Strong Amalgamation Property but does not have the Superamalgamation Property. This settles a conjecture of Pigozzi [12].

The paper proves a predicate version of Solovay's well-known theorem on provability interpretations of modal logic:

If a closed modal predicate-logical formula R is not valid in some finite Kripke model, then there exists an arithmetical interpretation f such that PA ⊬ fR.

This result implies the arithmetical completeness of arithmetically correct modal predicate logics with the finite model property (including the one-variable fragments of QGL and QS). The proof was obtained by adding “the predicate part” as a specific addition to the standard Solovay construction.

Small forcing always ruins the indestructibility of an indestructible supercompact cardinal. In fact, after small forcing, any cardinal κ becomes superdestructible—any further <κ-closed forcing which adds a subset to κ will destroy the measurability, even the weak compactness, of κ. Nevertheless, after small forcing indestructible cardinals remain resurrectible, but never strongly resurrectible.

The modern theory of computability is based on the works of Church, Markov and Turing who, starting from quite different models of computation, arrived at the same class of computable functions. The purpose of this paper is the show how the main results of the Church-Markov-Turing theory of computable functions may quickly be derived and understood without recourse to the largely irrelevant theories of recursive functions, Markov algorithms, or Turing machines. We do this by ignoring the problem of what constitutes a computable function and concentrating on the central feature of the Church-Markov-Turing theory: that the set of computable partial functions can be effectively enumerated. In this manner we are led directly to the heart of the theory of computability without having to fuss about what a computable function is.

The spirit of this approach is similar to that of [RGRS]. A major difference is that we operate in the context of constructive mathematics in the sense of Bishop [BSH1], so all functions are computable by definition, and the phrase “you can find” implies “by a finite calculation.” In particular if P is some property, then the statement “for each m there is n such that P(m, n)” means that we can construct a (computable) function θ such that P(m, θ(m)) for all m. Church's thesis has a different flavor in an environment like this where the notion of a computable function is primitive.

One point of such a treatment of Church's thesis is to make available to Bishopstyle constructivists the Markovian counterexamples of Russian constructivism and recursive function theory. The lack of serious candidates for computable functions other than recursive functions makes it quite implausible that a Bishopstyle constructivist could refute Church's thesis, or any consequence of Church's thesis. Hence counterexamples such as Specker's bounded increasing sequence of rational numbers that is eventually bounded away from any given real number [SPEC] may be used, as Brouwerian counterexamples are, as evidence of the unprovability of certain assertions.

Zu jedem Zählausdruck A in der allgemeinen pränexen Normalform

kann man bekanntlich einen, in bezug auf die Erfüllbarkeit, gleichwertigen Zählausdruck B in der spezielleren Normalform (Skolemsche Nonnalfonn)

konstruieren, indem man auf A mehrmals (n–1 Mal) das sogenannte Skolemsche Verfahren anwendet. Dieses Verfahren hat nämlich die Eigenschaft, daß es auf einen Zählausdruck in der pränexen Normalform n-ten Grades (n > 1) angewandt zu einem gleichwertigen Zählausdruck in der pränexen Normalform (n–1)-ten Grades führt, wobei unter “Grad eines Zählausdrucks in der pränexen Normalform, die ein mit einem Allzeichen beginnendes und mit einem Seinszeichen endendes Präfix hat” die Anzahl der durch Seinszeichen voneinander getrennten Komplexe von Allzeichen dieses Präfixes zu verstehen ist. Da nun A—wie aus (1) ersichtlich ist—ein Zählausdruck n-ten Grades ist, so kommt man nach (n–1)-maliger Anwendung des Skolemschen Verfahrens tatsächlich zu einem gleichwertigen Zählausdruck ersten Grades, also zu einem gleichwertigen Zählausdruck der Form (2).