We will study several weak axiom systems that use the Subtraction and Division primitives (rather than Addition and Multiplication) to formally encode the theorems of Arithmetic. Provided such axiom systems do not recognize Multiplication as a total function, we will show that it is feasible for them to verify their Semantic Tableaux, Herbrand, and Cut-Free consistencies. If our axiom systems additionally do not recognize Addition as a total function, they will be capable of recognizing the consistency of their Hilbert-style deductive proofs. Our axiom systems will not be strong enough to recognize their Canonical Reflection principle, but they will be capable of recognizing an approximation of it, called the “Tangibility Reflection Principle”. We will also prove some new versions of the Second Incompleteness Theorem stating essentially that it is not possible to extend our exceptions to the Incompleteness Theorem much further.

In 1981, Takeuti introduced quantum set theory as the quantum counterpart of Boolean valued models of set theory by constructing a model of set theory based on quantum logic represented by the lattice of closed subspaces in a Hilbert space and showed that appropriate quantum counterparts of ZFC axioms hold in the model. Here, Takeuti's formulation is extended to construct a model of set theory based on the logic represented by the lattice of projections in an arbitrary von Neumann algebra. A transfer principle is established that enables us to transfer theorems of ZFC to their quantum counterparts holding in the model. The set of real numbers in the model is shown to be in one-to-one correspondence with the set of self-adjoint operators affiliated with the von Neumann algebra generated by the logic. Despite the difficulty pointed out by Takeuti that equality axioms do not generally hold in quantum set theory, it is shown that equality axioms hold for any real numbers in the model. It is also shown that any observational proposition in quantum mechanics can be represented by a corresponding statement for real numbers in the model with the truth value consistent with the standard formulation of quantum mechanics, and that the equality relation between two real numbers in the model is equivalent with the notion of perfect correlation between corresponding observables (self-adjoint operators) in quantum mechanics. The paper is concluded with some remarks on the relevance to quantum set theory of the choice of the implication connective in quantum logic.

We initiate the study of reducts of relational structures up to primitive positive interdefinability: After providing the tools for such a study, we apply these tools in order to obtain a classification of the reducts of the logic of equality. It turns out that there exists a continuum of such reducts. Equivalently, expressed in the language of universal algebra, we classify those locally closed clones over a countable domain which contain all permutations of the domain.

In investigations of the foundations of mathematics we can distinguish two separate tendencies. On the one hand, one may seek to define his subject with greatest possible explicitness: to obtain a formulation which satisfies the most exacting demands for precision, and which is at the same time free from paradoxes and adequate for the purpose. On the other hand, besides the problem of formulation, there is that of simplification; one can seek to find systems based upon processes of greater and greater primitiveness. The reduction of a piece of mathematics to a formal system, and still further to a completely formalized system (as explained, for example, in my New York address a year ago), is a step toward the first of these objectives. But it is evident that one can formalize in various ways, and that some of these ways constitute a more profound analysis than others. Although from some points of view one way of formalization is as good as any other, yet a certain interest attaches to the problem of simplification, as is shown by the attention which some of the greatest mathematicians have devoted to it.

The researches about which I am reporting today are directed toward the second of these objectives. In fact we are concerned with constructing systems of an extremely rudimentary character, which analyze processes ordinarily taken for granted. This is properly part of the business of mathematical logic. Of course there are those, even among logicians, who doubt the utility of this sort of thing—who profess to have no interest in improvements which do not lead to increases in deductive power or what not. However that may be, this second objective certainly has some interest in its own right; and it is this interest which has formed the primary motivation for these researches.

In this paper we answer some of the questions left open in [2]. We use the terminology of [2]. In particular, a theory will be a formal system formulated within the first-order calculus with identity. A theory is identified with the set of Gödel numbers of the theorems of the theory. Thus Craig's theorem [1] asserts that a theory is axiomatizable if and only if it is recursively enumerable.

In [2], Feferman showed that if A is any recursively enumerable set, then there is an axiomatizable theory T having the same degree of unsolvability as A. (This result was proved independently by D. B. Mumford.) We show in Theorem 2 that if A is not recursive, then T may be chosen essentially undecidable. This depends on Theorem 1, which is a result on recursively enumerable sets of some independent interest.

Our second result, given in Theorem 3, gives sufficient conditions for a theory to be creative. These conditions are more general than those given by Feferman. In particular, they show that the system of Kreisel described in [2] is creative.

Syntactic translations of classical logic C into intuitionistic logic I are well known (see [Kol25], [Gli29], [Göd32], [Kre58b], [M063], [Cel69] and [Lei71]). Harvey Friedman [Fri78] used a translation of a similar nature, from I into itself, to reprove a theorem of Kreisel [Kre58a] that various theories based on I are closed under Markov's rule: if ¬¬∃x.α is a theorem, where x is a numeric variable and α is a primitive recursive relation, then ∃x.α is a theorem. Composing this with Gödel's translation from classical to intuitionistic theories, it follows that the functions provably recursive in the classical version of the theories considered are provably recursive already in their intuitionistic version. This conservation result is important in that it guarantees that no information about the convergence of recursive functions is lost when proofs are restricted to constructive logic, thus removing a potential objection to the use of constructive logic in reasoning about programs (see [C078] for example). Conversely, no objection can be raised by intuitionists to proofs of formulas that use classical reasoning, because such proofs can be converted to constructive proofs (this has been exploited extensively; see [Smo82]).

Proofs of closure under Markov's rule had required, until Friedman's proof, a relatively sophisticated mathematical apparatus. The chief method used Godel's “Dialectica” interpretation (see [Tro73, §3]). Other proofs used cut-elimination, provable reflection for subsystems [Gir73], and Kripke models [Smo73]. Moreover, adapting these proofs to new theories had required that the underlying meta-mathematical techniques be adapted first, not always a trivial step.

Some syntactically simple fragments of intuitionistic logic possess considerable expressive power compared with their classical counterparts.

In particular, we consider in this paper intuitionistic second order propositional logic (ISPL) a formalisation of which may be obtained by adding to the intuitionistic propositional calculus quantifiers binding propositional variables together with the usual quantifier rules and the axiom scheme (Ex), where is a formula not containing x.

The main purpose of this paper is to show that the classical first order predicate calculus with identity can be (isomorphically) embedded in ISPL.

It turns out an immediate consequence of this that the classical first order predicate calculus with identity can also be embedded in the fragment (PLA) of the intuitionistic first order predicate calculus whose only logical symbols are → and (.) (universal quantifier) and the only nonlogical symbol (apart from individual variables and parentheses) a single monadic predicate letter.

Another consequence is that the classical first order predicate calculus can be embedded in the theory of Heyting algebras.

The undecidability of the formal systems under consideration evidently follows immediately from the present results.

We shall indicate how the methods employed may be extended to show also that the intuitionistic first order predicate calculus with identity can be embedded in both ISPL and PLA.

For the purpose of the present paper it will be convenient to use the following formalisation (S) of ISPL based on [3], rather than the one given above.

It was shown by Cholak, Jockusch, and Slaman that every computable 2-coloring of pairs admits an infinite low2 homogeneous set H. We answer a question of the same authors by showing that H may be chosen to satisfy in addition C ≰rH, where C is a given noncomputable set. This is shown by analyzing a new and simplified proof of Seetapun's cone avoidance theorem for Ramsey's theorem. We then extend the result to show that every computable 2-coloring of pairs admits a pair of low2 infinite homogeneous sets whose degrees form a minimal pair.

Nonprincipal ultrafilters are harder to define in ZFC, and harder to obtain in ZF + DC, than nonprincipal measures.

The function μ from P(X) to the closed interval [0, 1] is a measure on X if μ. is finitely additive on disjoint sets and μ(X) = 1. (P is the power set.) μ is nonprincipal if μ ({x}) = 0 for each x Є X. μ is an ultrafilter if Range μ= {0, 1}. The existence of nonprincipal measures and ultrafilters on any infinite X follows from the axiom of choice.

Nonprincipal measures cannot necessarily be defined in ZFC. (ZF is Zermelo–Fraenkel set theory. ZFC is ZF with choice.) In ZF alone they cannot even be proved to exist. This was first established by Solovay [14] using an inaccessible cardinal. In the model of [14] no nonprincipal measure on ω is even ODR (definable from ordinal and real parameters). The HODR (hereditarily ODR) sets of this model form a model of ZF + DC (dependent choice) in which no nonprincipal measure on ω exists. Pincus [8] gave a model with the same properties making no use of an inaccessible. (This model was also known to Solovay.) The second model can be combined with ideas of A. Blass [1] to give a model of ZF + DC in which no nonprincipal measures exist on any set. Using this model one obtains a model of ZFC in which no nonprincipal measure on the set of real numbers is ODR. H. Friedman, in private communication, previously obtained such a model of ZFC by a different method. Our construction will be sketched in 4.1.

In this paper we prove two theorems. They answer questions raised by Myhill in 1956. (We recall the well-known fact that Myhill's invention of the maximal set in 1956 [2] stemmed from his attempt to prove I below.)

I. There exists an axiomatizable, essentially undecidable theory in standard formalization such that all axiomatizable extensions of are finite extensions.

II. There exists an axiomatizable but undecidable theory in standard formalization such that

(a) has a consistent, complete, decidable extension ,

(b) If is an axiomatizable extension of then either

(i) is a finite extension of , or

(ii) is a finite extension of .

We can use the compositional semantics of Hodges [9] to show that any compositional semantics for logics of imperfect information must obey certain constraints on the number of semantically inequivalent formulas. As a corollary, there is no compositional semantics for the ‘independence-friendly’ logic of Hintikka and Sandu (henceforth IF) in which the interpretation in a structure A of each 1 -ary formula is a subset of the domain of A (Corollary 6.2 below proves this and more). After a fashion, this rescues a claim of Hintikka and provides the proof which he lacked:

… there is no realistic hope of formulating compositional truth-conditions for [sentences of IF], even though I have not given a strict impossibility proof to that effect.

(Hintikka [6] page 110ff.) One curious spinoff is that there is a structure of cardinality 6 on which the logic of Hintikka and Sandu gives nearly eight million inequivalent formulas in one free variable (which is more than the population of Finland).

We thank the referee for a sensible change of notation, and Joel Berman and Stan Burris for bringing us up to date with the computation of Dedekind's function (see section 4). Our own calculations, utterly trivial by comparison, were done with Maple V.

The paper Hodges [9] (cf. [10]) gave a compositional semantics for a language with some devices of imperfect information. The language was complicated, because it allowed imperfect information both at quantifiers and at conjunctions and disjunctions.

Preservation and interpolation results are obtained for L∞ω and sublogics ⊆ L∞ω such that equivalence in can be characterized by suitable back-and-forth conditions on sets of partial isomorphisms.

This article is a continuation of our search for tautologies that are hard even for strong propositional proof systems like EF. cf. [14, 15]. The particular tautologies we study, the τ-formulas. are obtained from any /poly map g; they express that a string is outside of the range of g, Maps g considered here are particular pseudorandom generators. The ultimate goal is to deduce the hardness of the τ-formulas for at least EF from some general, plausible computational hardness hypothesis.

In this paper we introduce the notions of pseudo-surjective and iterable functions (related to free functions of [15]). These two properties imply the hardness of the τ-formulas from the function but unlike the hardness they are preserved under composition and iteration. We link the existence of maps with these two properties to the provability of circuit lower bounds, and we characterize maps g yielding hard τ-formulas in terms of a hitting set type property (all relative to a propositional proof system). We show that a proof system containing EF admits a pseudo-surjective function unless it simulates a proof system WF introduced by Jeřábek [11]. an extension of EF.

We propose a concrete map g as a candidate function possibly pseudo-surjective or free for strong proof systems. The map is defined as a Nisan-Wigderson generator based on a random function and on a random sparse matrix. We prove that it is iterable in a particular way in resolution, yielding the output/input ratio n3 −ε (that improves upon a direct construction of Alekhnovich et al. [2]).

We show that the theory ATR0 is equivalent to a second-order generalization of the theory . As a result, ATR0 is conservative over for arithmetic sentences, though proofs in ATR0 can be much shorter than their counterparts.

Our main result is the equivalence of two notions of reducibility between structures. One is a syntactical notion which is an effective version of interpretability as in model theory, and the other one is a computational notion which is a strengthening of the well-known Medvedev reducibility. We extend our result to effective bi-interpretability and also to effective reductions between classes of structures.

We develop Fraïssé theory, namely the theory of Fraïssé classes and Fraïssé limits, in the context of metric structures. We show that a class of finitely generated structures is Fraïssé if and only if it is the age of a separable approximately homogeneous structure, and conversely, that this structure is necessarily the unique limit of the class, and is universal for it.

We do this in a somewhat new approach, in which “finite maps up to errors” are coded by approximate isometries.

Subcreative sets, introduced by Blum, are known to coincide with the effectively speedable sets. Subcreative sets are shown to be the complete sets with respect to S-reducibility, a special case of Turing reducibility. Thus a set is effectively speedable exactly when it contains the solution to the halting problem in an easily decodable form. Several characterizations of subcreative sets are given, including the solution of an open problem of Blum, and are used to locate the subcreative sets with respect to the complete sets of other reducibilities. It is shown that q-cylindrification is an order-preserving map from the r.e. T-degrees to the r.e. S-degrees. Consequently, T-complete sets are precisely the r.e. sets whose q-cylindrifications are S-complete.

It has been stated by Tarski [5] and “proved” by Grzegorczyk [3] that:

Proved has been put in quotes, not because Grzegorczyk's proof is faulty but because the system he describes as mereology is in fact not Leśniewski's mereology.

Leśniewski's first attempt at describing the collective class, i.e. mereology, was done in ordinary language with no rigorous logical foundation. In describing the collective class, he needed to use the notion of distributive class. So as to clearly distinguish and expose the interplay between the two notions of class, he introduced his calculus of name (name being the distributive notion), which is also called ontology, since he used the primitive term “is.” At this stage, mereology included ontology. Then, in order to have a logically rigorous system, he developed as a basis, a propositional calculus with quantifiers and semantical categories (types), called protothetic. At this final stage, what is properly called mereology includes both protothetic and ontology.

What Grzegorczyk describes as mereology is even weaker than Leśniewski's initial version. To quote from [3]:

Consider functions whose variables, finite in number, range over a fixed finite set N and whose values are elements of N. The elements of N are denoted simply by the natural numbers 1,2, …, n. There are nnm distinct m-place functions. If N is chosen to be the set of n truth-values then the functions considered are obviously truth-functions in n-valued logic.