bluuebunny/crossref_metadata_2025 huggingface dataset:
On the reduction of the decision problem. Third paper. Pepis prefix, a single binary predicate
Authors: Kalmár László , Surányi János
Published: May 2006

It has been proved by Pepis that any formula of the first-order predicate calculus is equivalent (in respect of being satisfiable) to another with a prefix of the form

containing a single existential quantifier. In this paper, we shall improve this theorem in the like manner as the Ackermann and the Gödel reduction theorems have been improved in the preceding papers of the same main title. More explicitly, we shall prove the

Theorem 1. To any given first-order formula it is possible to construct an equivalent one with a prefix of the form (1) and a matrix containing no other predicate variable than a single binary one.

An analogous theorem, but producing a prefix of the form

has been proved in the meantime by Surányi; some modifications in the proof, suggested by Kalmár, led to the above form.
On virtual classes and real numbers
Authors: Martin R. M.
Published: May 2006

In a simple, applied functional calculus of first order (i.e., one admitting no functional variables but at least one functional constant), abstracts or schematic expressions may be introduced to play the role of variables over designatable sets or classes. The entities or quasi-entities designated or quasi-designated by such abstracts may be called, following Quine, virtual classes and relations. The notion of virtual class is always relative to a given formalism and depends upon what functional constants are taken as primitive. The first explicit introduction of a general notation for virtual classes (relative to a given formalism) appears to be D4.1 of the author's A homogeneous system for formal logic. That paper develops a system admitting only individuals as values for variables and is adequate for the theory of general recursive functions of natural numbers. Numbers and functions are in fact identified with certain kinds of virtual classes and relations.

In the present paper it will be shown how certain portions of the theory of real numbers can be constructed upon the basis of the theory of virtual classes and relations of H.L.

The method of building up the real numbers to be employed is essentially an adaptation of standard procedure. Although the main ideas underlying this method are well known, the mirroring of these ideas within the framework of the restricted concepts admitted here presents possibly some novelty. In particular, a basis for the real numbers is provided which in no way admits classes or relations or other "abstract" objects as values for variables. Presupposing the natural numbers, the essential steps are to construct the simple rationals as virtual dyadic relations between natural numbers, to construct the generalized or signed rationals as virtual tetradic relations among natural numbers, and then to formulate a notation for real numbers as virtual classes (of a certain kind) of generalized rationals. Of course, there are several alternative methods. This procedure, however, appears to correspond more to the usual one.
Note on two theorems of Mostowski
Authors: Doss Raouf
Published: May 2006

The present note is conceived as a sequel to Mostowki's paper, Über die Unabhängigkeit des Wohlordnungssatzes vom Ordnungsprinzip (which will be quoted as “M.”).

In that paper Mostowski considers a system of axioms , very close to the system of axiomatic set theory of Bernays, but where the axiom of choice is not supposed to hold. Mostowski proves that the well-ordering theorem (Wohlordnungssatz) cannot be derived from the system plus the principle of simple ordering (Ordnungsprinzip).
On the reduction of the decision problem
Authors: Kalmár László , Surányi János
Published: May 2006

In the first paper of the above main title, one of us has proved that any formula of the first order predicate calculus is equivalent (as to being satisfiable or not) to some binary first order formula having a prefix of the form (Ex1)(x2)(Ex3) … (xn) and containing a single predicate variable. This result is an improvement of a theorem of Ackermann stating that any first order formula is equivalent to another with a prefix of the above form but saying nothing about the number of predicate variables appearing therein. Hence the question arises if other theorems reducing the decision problem to the satisfiability question of the first order formulas with a prefix of a special form can be improved in like manner. In the present paper we shall answer this question concerning Gödel's reduction theorem stating that any first order formula is equivalent to another the prefix of which has the form
Deducibility with respect to necessary and impossible propositions
Authors: Emch Arnold F.
Published: May 2006

Inasmuch as my discussion of the formal properties of “System L,” presented elsewhere, is substantially the same as that presented by Lewis in a previous issue of this Journal, I shall confine my remarks in this brief rejoinder to the problem of deducibility with respect to necessary and impossible propositions—since it is specifically the solution of this problem which will determine the adequacy of the calculus of logical implication as a canon and critique of deductive inference.

The problem, as originally presented, can be stated succinctly in the following inconsistent triad: (1) All necessarily true principles are logically dependent on or deducible from one another, i.e., are equivalent, (2) All principles of logic and mathematics are necessarily true, and (3) Some principles of logic and mathematics are not logically dependent on or deducible from one another, i.e., are independent. These three propositions are logically inconsistent in the sense that the conjunction of any two of them will logically imply the falsity of the third. Now if Lewis should affirm the first and third of these propositions, then he should concede the falsity of the second. This concession, it was believed, he was not likely to make, inasmuch as it would seem to involve a repudiation of a doctrine (the tautological character of every logical and mathematical truth) with which he has particularly identified himself. If, in view of this fact, he should accept, instead, the second and third of these propositions, then he should concede the falsity of the first.
Systems of transfinite types involving λ-conversion
Authors: L'Abbé Maurice
Published: May 2006

The problem of constructing formal systems involving transfinite types was briefly suggested many times in the literature. Actually few attempts have been made to develop such systems. In particular, there exists a system based on a set of axioms and rules of inference suggested by Church and worked out in detail by E. Bustamante in his dissertation. Recently, John Kemeny has reformulated this system in a simplified way and has obtained an interesting hierarchy of systems. It so happens that all these systems considered by Kemeny may be regarded as successive extensions of a particular formulation of the theory of finite types, namely a certain monadic functional calculus of order ω whose main ideas are due to Tarski.

There exists on the other hand a quite different formulation of the theory of finite types which is due to Church. It is a formulation which incorporates certain features of the calculus of λ-conversion, and which has revealed itself quite advantageous for certain purposes. The formulation of the theory of transfinite types which we are going to introduce in this paper may be considered as an attempt to generalize Church's formulation of the theory of finite types.
On syntactical categories
Authors: Bar-Hillel Yehoshua
Published: May 2006

Up to now, most constructed calculi had the following common property: Whenever the rules of formation of a calculus laid down that expressions of the designs ‘Pa’, ‘Qa’, ‘Pb’ were sentences—‘P’ and ‘Q’ being first-level one-place predicates, ‘a’ and ‘b’ individual-symbols—, ‘Qb’ was a sentence too, according to the same rules. This self-imposed restriction of the logicians is historically understandable, since calculi of this common feature have a certain simplicity which differently constructed calculi will not have. So far, calculi of this type have proved to be sufficient for the formalization of mathematics and small parts of other sciences. We may ask ourselves, however, whether such a restriction will still be desirable when attempting to construct calculi covering more ground. It is quite possible that insistence on this kind of simplicity will involve a greater complexity in other respects. Inquiry into types of calculi which do not possess this simplicity should therefore be of some interest. To such an inquiry we are led also from another point of view. More and more stress has been laid in recent researches on the construction of calculi which should show close connection with ordinary languages, and it is obvious that ordinary language does not have the mentioned property. To use an example given by Carnap: Whereas ‘This stone is red,’ ‘Aluminium is red,’ ‘This stone weighs five pounds’ are all meaningful sentences of ordinary English, ‘Aluminium weighs five pounds’ is not and it does not matter in this connection whether we formulate this fact by saying that ‘Aluminium weighs five pounds,’ though grammatically an impeccable sentence, is logically meaningless, or whether we prefer the more modern formulation that this word-sequence does not form a sentence at all.
Two concepts from the theory of models
Authors: Henkin Leon
Published: May 2006

In this note we point out that two concepts which have been introduced separately into the theory of models are extensionally equivalent. The basic ideas can be expressed conveniently in the terminology of Tarski's theory of arithmetical classes. It will be recalled that an arithmetical class is a class consisting of all algebraic structures which satisfy some fixed sentence of the first-order functional calculus. A more general concept is that of a quasi-arithmetical class, whose elements are all algebraic structures which satisfy some fixed set of first-order sentences.

Now where H and K are any two classes of algebraic structures, Abraham Robinson has defined the relation H is persistent with respect to K to mean that (i) H∩K is non-empty, and (ii) whenever M ϵ H∩K, M′ is an extension of M, and M′ ϵ K, then M′ ϵ H. Concerning this notion Robinson has established the following theorem: If K is the class of abelian groups (or of commutative fields) and H is an arithmetical class which is persistent with respect to K, then H∩K contains a group (or field) which is finite. This leads us to the following definition.
Axiom schemes for m-valued functional calculi of first order. Part II
Authors: Rosser J. B. , Turquette A. R.
Published: May 2006

In part I of the present paper axiom schemes and rules of inference were defined for m-valued functional calculi of first order with s(m > s > 1) designated truth-values. A proof of plausibility was given, and it was shown that it is not difficult to extend to m-valued functional calculi of first order certain concepts that are closely analogous to the ordinary 2-valued notions of “consistency with respect to an operator” and “absolute consistency.” The purpose of the present paper is to show that the concept of “deductive completeness” may be extended to m-valued functional calculi of first order. For this purpose we define “analytic formula” for the m-valued case and show that if a formula is analytic, then it is provable in our formalization of m-valued functional calculi of first order.

In proving deductive completeness for the m-valued case, it is possible to use a method which is analogous to that used by Gödel in establishing the completeness of 2-valued functional calculi of first order. However, in the present paper we will indicate only very briefly how the Gödel procedure may be extended to the m-valued case. Our chief concern will be the problem of extending to our formalization of m-valued functional calculi the more elegant proof of deductive completeness for the 2-valued case which has recently been developed by Leon Henkin.
A system of axiomatic set theory—Part I
Authors: Bernays Paul
Published: May 2006

Introduction. The system of axioms for set theory to be exhibited in this paper is a modification of the axiom system due to von Neumann. In particular it adopts the principal idea of von Neumann, that the elimination of the undefined notion of a property (“definite Eigenschaft”), which occurs in the original axiom system of Zermelo, can be accomplished in such a way as to make the resulting axiom system elementary, in the sense of being formalizable in the logical calculus of first order, which contains no other bound variables than individual variables and no accessory rule of inference (as, for instance, a scheme of complete induction).

The purpose of modifying the von Neumann system is to remain nearer to the structure of the original Zermelo system and to utilize at the same time some of the set-theoretic concepts of the Schröder logic and of Principia mathematica which have become familiar to logicians. As will be seen, a considerable simplification results from this arrangement.

The theory is not set up as a pure formalism, but rather in the usual manner of elementary axiom theory, where we have to deal with propositions which are understood to have a meaning, and where the reference to the domain of facts to be axiomatized is suggested by the names for the kinds of individuals and for the fundamental predicates.

On the other hand, from the formulation of the axioms and the methods used in making inferences from them, it will be obvious that the theory can be formalized by means of the logical calculus of first order (“Prädikatenkalkul” or “engere Funktionenkalkül”) with the addition of the formalism of equality and the ι-symbol for “descriptions” (in the sense of Whitehead and Russell).
A system of axiomatic set theory - Part VII
Authors: Bernays Paul
Published: May 2006

The reader of Part VI will have noticed that among the set-theoretic models considered there some models were missing which were announced in Part II for certain proofs of independence. These models will be supplied now.

Mainly two models have to be constructed: one with the property that there exists a set which is its own only element, and another in which the axioms I–III and VII, but not Va, are satisfied. In either case we need not satisfy the axiom of infinity. Thereby it becomes possible to set up the models on the basis of only I–III, and either VII or Va, a basis from which number theory can be obtained as we saw in Part II.

On both these bases the Π0-system of Part VI, which satisfies the axioms I–V and VII, but not VI, can be constructed, as we stated there. An isomorphic model can also be obtained on that basis, by first setting up number theory as in Part II, and then proceeding as Ackermann did.

Let us recall the main points of this procedure.

For the sake of clarity in the discussion of this and the subsequent models, it will be necessary to distinguish precisely between the concepts which are relative to the basic set-theoretic system, and those which are relative to the model to be defined.
Constructible falsity
Authors: Nelson David
Published: May 2006

The present note introduces a constructible interpretation for the logical connectives of number theory which is divergent from that of the intuitionists. Under the intuitionistic interpretation, the principle of excluded middle and certain other classically acceptable principles of logic must be rejected. Under the present interpretation, while some classical principles may be reinstated, other principles, acceptable both classically and intuitionistically, may be shown to be invalid. Among these is the principle of contradiction.
A note on the deductive completeness of m-valued propositional calculi
Authors: Rosser J. B. , Turquette A. R.
Published: May 2006

In this note we present a simplification of the axiom schemes which were given in our earlier paper Axiom schemes for m-valued propositional calculi. Except for new concepts that are needed for our present purposes, the terminology used will be the same as that introduced in the earlier paper. Hence, we can say that in addition to listing our simplified specifications for axiom schemes, we shall indicate how our new axiom schemes may be used to establish deductive completeness.

The simplification of our axiom schemes is achieved by using only the operators ⊃ and Jk( ) with the resulting elimination of ∨ and ·. This does not constitute an actual reduction in functional complexity since the latter operators can be denned in terms of the former. For example,

However, by dispensing with ∨ and · one can greatly reduce the number of axioms without an appreciable increase in the difficulties of proving deductive completeness.

Our simplified specifications for axiom schemes will retain conditions (1) and (3) of our earlier set but (2) and (4) will be changed to (2*) and (4*) which we will now state.

(2*) Assume that an implication function (P ⊃ Q) can be defined exclusively in terms of the basic functions Fi(P1, …:, Pαi).

The statement of what follows is simplified by introducing a chain symbol defined recursively as follows:

The variable i of a chain symbol which takes values from u to v will be called the chain variable. When it is clear that i is the chain variable we will use the notation in place of . Hence, denotes (P5 ⊃ (P4 ⊃ (P3 ⊃ Q))).
Results concerning the decision problem of Lewis's calculi S3 and S6
Authors: Halldén Sören
Published: May 2006

The calculus generated by the addition of the postulate

to S2 will, after Miss Alban, be called “S6”, the calculus generated by the addition of the same postulate to S3, “S7”, and the calculus generated by the addition of the postulate

to S3, “S8”. No interesting interpretation of the calculi S6–8 is known, but they are of some indirect interest because of the connections between them and the five calculi S1–S5. Certain questions concerning them will be treated in the following. In §1 it will be shown that every method of decision for S7 can be turned into a method of decision for S3, and in §2 that the number of complete extensions of S3 is equal to the number of complete extensions of S7 plus one. In §3 it will be shown that McKinsey's method of decision for S2 and S4 can be modified so as to cover S6.

The letters “P”, “Q”, “R”, and “S” will be employed as syntactic variables denoting formulas. Logical expressions will sometimes be used as selfdenotative. “C” and “C” stand for arbitrary calculi. “C + P” is the calculus which is the result of adding to C as new postulates all formulas which can be derived from P by substitution. With “substitution” I mean the operation performed on propositional variables.
Metarecursive sets
Authors: Kreisel G. , Sacks Gerald E.
Published: May 2006

Our ultimate purpose is to give an axiomatic treatment of recursion theory sufficient to develop the priority method. The direct or abstract approach is to keep in mind as clearly as possible the methods actually used in recursion theory, and then to formulate them explicitly. The indirect or experimental approach is to look first for other mathematical theories which seem similar to recursion theory, to formulate the analogies precisely, and then to search for an axiomatic treatment which covers not only recursion theory but also the analogous theories as particular cases.

The first approach is more general because it does not depend on the existence of (familiar) analogues. A concrete mathematical theory, it seems, need have no such analogues and still be important, as e.g. classical number theory. In such a case, an axiomatic treatment may still be useful for exhibiting the mathematical structure of the theory considered and the assumptions on which it rests. However, it will lack one of the most heavily advertised advantages of the axiomatic method, namely, the “economy of thought” which results from an uniform theory for several different and interesting cases: we cannot hope for this if, by hypothesis, we know of only one particular case. In contrast, the second approach, if successful at all, is bound to achieve such “economy” because we start out with several interesting particular cases. Another possible virtue of the second approach is that of field work over insight: the abstract pattern that we are looking for and hoping to formalize in axioms, may not be evident in any one mathematical theory, but may spring to the eye if one happens to look simultaneously at several theories which happen to realize the pattern.
Decision problems for tag systems
Authors: Aanderaa Stål , Belsnes Dag
Published: May 2006

The aim of this paper is to study tag systems as defined by Post [Post 1943, pp. 203–205 and Post, 1965, pp. 370–373]. The existence of a tag system with unsolvable halting problem was proved by Minsky by constructing a universal tag system [Minsky 1961, see also Cocke and Minsky 1964, Wang 1963, and Minsky 1967, pp. 267–273]. Hence the halting problem of a tag system can be of the complete degree 0′. We shall prove that the halting problem for a tag system can have an arbitrary (recursively enumerable) degree of undecidability (Corollary III).

A related problem arises when we ask if there exists a uniform procedure for determining, given a tag system, whether or not there is any word on which the tag system does not halt, an “immortal” word in the system. The alternative, of course, being that the system eventually halts on every (finite) word. It is shown here that this problem, the immortality problem for tag systems, is recursively unsolvable of degree 0″ (Corollary II).
Hauptsatz for higher order logic
Authors: Prawitz Dag
Published: May 2006

I shall prove in this paper that Gentzen's Hauptsatz is extendible to simple type theory, i.e., to the predicate logic obtained by admitting quantification over predicates of arbitrary finite type and generalizing the second order quantification rules to cover quantifiers of other types. (That Gentzen's Hauptsatz is extendible to this logic has been known as Takeuti's conjecture; see [4].) Gentzen's Hauptsatz has been extended to second order logic in a recent paper by Tait [3]. However, as remarked by Tait, his proof seems not to be extendible to higher orders. The present proof is rather an extension of a different proof of the Hauptsatz for second order logic that I have presented in [1].
Hierarchies over recursive well-orderings
Authors: Enderton Herbert , Luckham David
Published: May 2006

In the original example of a transfinite hierarchy of degrees of unsolvability, a predicate Ha is associated with each a in the set 0 of ordinal notations. (See Kleene [K1], Spector [S1], and the references there to Davis and Mostowski.) The predicates are defined by means of induction over the partial well-ordering relation ≤0 on the set 0 of notations for the recursive ordinals. The usefulness of this hierarchy of predicates is enhanced by Spector's proof [S1] of the “uniqueness” property: viz. that the degree of Ha depends only on the ordinal |a| for which a is a notation.
Trees and nest structures
Authors: Smullyan Raymond M.
Published: May 2006

This paper is a sequel to [1]. Our purpose is to exhibit certain basic relationships between (ordered dyadic) trees and regular nest structures. We introduce the notion of a tree being isomorphic to a nest structure, and we study some necessary and sufficient conditions for the existence of such isomorphisms. By virtue of some of our results, Kónig's lemma on infinite trees, and our fundamental lemma of [1] concerning infinite regular nest structures become intimately related — either yields an alternative proof of the other.
An algebraic study of Diodorean modal systems
Authors: Bull R. A.
Published: May 2006

Attention was directed to modal systems in which ‘necessarily α’ is interpreted as ‘α. is and always will be the case’ by Prior in his John Locke Lectures of 1956. The present paper shows that S4.3, the extension of S4 with

ALCLpLqLCLqLp,

is complete with respect to this interpretation when time is taken to be continuous, and that D, the extension of S4.3 with

ALNLpLCLCLCpLpLpLp,

is complete with respect to this interpretation when time is taken to be discrete. The method employed depends upon the application of an algebraic result of Garrett Birkhoff's to the models for these systems, in the sense of Tarski.

A considerable amount of work on S4.3 and D precedes this paper. The original model with discrete time is given in Prior's [7] (p. 23, but note the correction in [8]); that taking time to be continuous yields a weaker system is pointed out by him in [9]. S4.3 and D are studied in [3] of Dummett and Lemmon, where it is shown that D includes S4.3 and

CLCLCpLpLpCMLpLp.

While in Oxford in 1963, Kripke proved that these were in fact sufficient for D, using semantic tableaux. A decision procedure for S4.3, using Birkhoff's result, is given in my [2]. Dummett conjectured, in a conversation, that taking time to be continuous yielded S4.3. Thus the originality of this paper lies in giving a suitable completeness proof for S4.3, and in the unified algebraic treatment of the systems. It should be emphasised that the credit for first axiomatising D belongs to Kripke.
A note on the hyperarithmetical hierarchy
Authors: Enderton H. B. , Putnam Hilary
Published: May 2006

The hyperarithmetical hierarchy assigns a degree of unsolvability hγ to each constructive ordinal γ. This assignment has the properties that h0 is the recursive degree and hγ+1 is the jump h′γ of hγ. For a limit ordinal λ < ω1 it is not so easy to define hγ. The original definitions used systems of notations for ordinals, see Spector [6]. There are also later notation-free definitions due to Shoenfield (unpublished) and to Hensel and Putnam [4].
Combinatory logic with discriminators
Authors: Kearns John T.
Published: May 2006

In this paper, I present a modified and extended version of combinatory logic. Schönfinkel originated the study of combinatory logic (in [2]), but its development is primarily due to H. B. Curry. In the present paper, I will make use of both the symbolism (with some modification) and the results of Curry, as found in [1].

What is novel about my version of combinatory logic is a kind of combinators which I call discriminators. These combinators discriminate between different symbols, and yield values which are determined by the symbols which are their arguments. If the normal combinators investigated by Curry are considered as functions taking (combinations of) symbols as arguments and yielding symbols as values, these combinators can rearrange and cancel their arguments or introduce new symbols.
Bar Induction and Π11-CA
Authors: Friedman Harvey
Published: May 2006

This paper compares the subsystem of analysis based on the Π11-comprehension axiom (Π11-CA) with classical Bar Induction (BI). An extension of Bar Induction using infinitary formulae is also considered, which was suggested to us by G. Kreisel (oral communication).

To describe these formal systems, we first describe the language, L, appropriate for their formalization. L contains the language of ENT (1st order arithmetic) plus function variables ƒi, gi, hi, etc. Number-theoretic terms are built up from +, × , ′ , 0, and application.
Generic Embeddings
Authors: Manuel Plotkin Jacob
Published: May 2006

Since Cohen [1] showed the independence of the axiom of choice from the other axioms of ZF, a number of people have used his forcing technique to show how badly choice can fail while certain vestiges of it remain. Many of these arguments involve the introduction of a generic sequence or generic set of generic sets of ordinals into a countable standard model of ZF + V = L. The desired results then follow by the use of clever permutation and forcing arguments. (See Cohen [2, pp. 136–142].)
A normal modal calculus between T and S4 without the finite model property
Authors: Makinson David
Published: May 2006

Given separate though similar proofs of the finite model property for individual modal calculi such as S5, S4, S2, and the Feys-von Wright system T, the problem arises of generalising the arguments and establishing the property for modal calculi en masse. In other words, we would like to be able to show in one fell swoop that any modal calculus satisfying certain general syntactic conditions has the finite model property.
Index sets of finite classes of recursively enumerable sets
Authors: Hay Louise
Published: May 2006

Let q0, q1,… be a standard enumeration of all partial recursive functions of one variable. For each i, let wi = range qi and for any recursively enumerable (r.e.) set α, let θα = {n | wn = α}. If A is a class of r.e. sets, let θA = the index set of A = {n | wn ∈ A}. It is the purpose of this paper to classify the possible recursive isomorphism types of index sets of finite classes of r.e. sets. The main theorem will also provide an answer to the question left open in [2] concerning the possible double isomorphism types of pairs (θα, θβ) where α ⊂ β.
Rich co-ordinals, addition isomorphisms, and RETs
Authors: Manaster Alfred B.
Published: May 2006

In this paper a special type of co-ordinal, called rich, is studied. Basic properties of rich co-ordinals are proved in §1. In §2 rich co-ordinals are seen to be the co-ordinals occurring in paths which are addition isomorphic to initial segments of the classical ordinals. The results of §1 are applied to obtain information about and examples of such paths. In the next section the order types of rich co-ordinals with a given field, X, is seen to be determined essentially by the finite divisors of X. RETs satisfying various divisibility conditions are constructed in §4.
Sets with no subset of higher degree
Authors: Soare Robert I.
Published: May 2006

The problem of finding an infinite set of natural numbers which contains no subsets of higher (Turing) degree was first posed by W. Miller [3] and was brought to our attention by C. G. Jockusch, Jr., who proved that such a set, if it existed, could not be hyperarithmetic.2 In this paper we construct an infinite set which is not recursive in any of its coinfinite subsets, and thus contains no subset of higher degree. Our original proof made use of the result (attributed to Ehrenfeucht) that every subset of 2ω which is open (in the standard topology) is “Ramsey”.
The independence of Ramsey's theorem
Authors: Kleinberg E. M.
Published: May 2006

In [3] F. P. Ramsey proved as a theorem of Zermelo-Fraenkel set theory (ZF)
with the Axiom of Choice (AC) the following result:

(1) Theorem. Let A be an infinite class. For each integer n and
partition {X, Y} of the size n subsets of A, there
exists an infinite subclass of A all of whose size n subsets are
contained in only one of X or Y.
On an algebra of sets of finite sequences
Authors: Donald Monk J.
Published: May 2006

The algebras studied in this paper were suggested to the author by William Craig as a possible substitute for cylindric algebras. Both kinds of algebras may be considered as algebraic versions of first-order logic. Cylindric algebras can be introduced as follows. Let ℒ be a first-order language, and let be an ℒ-structure. We assume that ℒ has a simple infinite sequence ν0, ν1, … of individual variables, and we take as known what it means for a sequence ν0, ν1, … of individual variables, and we take as known what it means for a sequence x = 〈x0, x1, …〉 of elements of to satisfy a formula ϕ of ℒ in . Let ϕ be the collection of all sequences x which satisfy ϕ in . We can perform certain natural operations on the sets ϕ, of basic model-theoretic significance: Boolean operations = cylindrifications diagonal elements (0-ary operations) . In this way we make the class of all sets ϕ into an algebra; a natural abstraction gives the class of all cylindric set algebras (of dimension ω). Thus this method of constructing an algebraic counterpart of first-order logic is based upon the notion of satisfaction of a formula by an infinite sequence of elements. Since, however, a formula has only finitely many variables occurring in it, it may seem more natural to consider satisfaction by a finite sequence of elements; then ϕ becomes a collection of finite sequences of varying ranks (cf. Tarski [10]). In forming an algebra of sets of finite sequences it turns out to be possible to get by with only finitely many operations instead of the infinitely many ci's and dij's of cylindric algebras. Let be the class of all algebras of sets of finite sequences (an exact definition is given in §1).
Ultraproducts of finite sets
Authors: Jerome Keisler H.
Published: May 2006

It is shown in [1] that an ultraproduct of finite sets can be of arbitrarily large cardinality, but if it is infinite then it must have at least the power of the continuum. In this paper we shall take a closer look at the cardinality of ultraproducts of finite sets. Our results were announced without proof in [5]. A discussion of the cardinality of ultraproducts of infinite sets, and another theorem about ultraproducts of finite sets, can be found in [3].
Support structures for the axiom of choice
Authors: Pincus David
Published: May 2006

The notion of “support” was introduced by Mostowski in [4] in order to prove that a certain universe satisfied the ordering principle but not the axiom of choice. The notion was refined in [3] and in [1] it was shown to be satisfied in a certain Cohen model of full ZF set theory. This paper is an axiomatic study of universes whose undefined relations are ∈ and a “support structure”, T.

In §2 the general theory is introduced and the universes of [4] and [1] are characterized. §3 examines a more complicated universe which will be used in [5] to show that in many cases a consistency in full ZF set theory may be proven directly by the methods of [4]. The embedding theorems of §4 are crucial to this application.
On strongly minimal sets
Authors: Baldwin J. T. , Lachlan A. H.
Published: May 2006

The purpose of this paper is twofold. In §1 and §2 which are largely expository we develop the known theory of ℵ1-categoricity in terms of strongly minimal sets. In §3 we settle affirmatively Vaught's conjecture that a complete ℵ1-categorical theory has either just one or just ℵ0 countable models, and in §4 we present an example which serves to illustrate the ideas of §3.

As far as we know the only work published on strongly minimal sets is that of Marsh [3]. The present exposition goes beyond [3] in showing that any ℵ-categorical theory has a principal extension in which some formula is strongly minimal.
Semantics for RKt
Authors: Rennie M. K.
Published: May 2006

In Chapter XIII of [4], Prior discusses a system QKt, designed to stand to the “minimal” tense logic Kt as the modal system Q of [3] stands to S5. In this paper I provide semantics for a similar system, slightly weaker than QKt: the weakening is due to the fact that Prior's axioms are slightly too strong for a “minimal” system. An extended post-Henkin style completeness proof for the axiomatization with respect to the semantics provided is then given: the underlying three-valued nature of the semantics requires a twist in the proof which is new to its author at least, and also results in some details being set out which could well be glossed over in the two-valued case.
Equational bases of boolean algebras
Authors: Sioson F. M.
Published: May 2006

It is well-known that a Boolean algebra (B, +, ., ‐) may be defined as an algebraic system with at least two elements such that (for all x, y, z ε B):

These axioms or equations are not independent, in the sense that some of them are logical consequences of the others. B. A. Bernstein [1] thought that the first three and their duals form an independent dual-symmetric definition of a Boolean algebra, but R. Montague and J. Tarski [3] proved later that B1 (or B̅1) follows from B2, B3, B̅1, B̅2, B̅3 (from B1, B2, B3, B̅2, B̅3).
On η-valued functionally complete truth functions
Authors: Graham R. L.
Published: May 2006

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 consistency of number theory via Herbrand's theorem
Authors: Scanlon T. M.
Published: May 2006

That elementary number theory is consistent and can be given a metamathematical consistency proof has been well known since Gentzen's 1936 paper, and a number of different proofs of this result have since been offered. What is presented here is essentially a simplified and generalized version of the proof given by Ackermann in 1940 [1]; but the proof given here applies to systems formalized in standard quantification theory rather than in Hilbert's ε-calculus, and is based upon the analysis of quantificational reasoning given by Herbrand's Fundamental Theorem. Dreben and Denton sketch such a proof in [2], but at a crucial point they follow Ackermann in tying the strategy of their proof too closely to the standard model. This makes the proof more complex than it need be and restricts its application to systems with induction on the standard well-ordering. The present proof is both simpler and more general in that it applies to systems ZR of number theory with induction on arbitrary recursive well-orderings R. This generalization was first obtained by Tait in [11] using functionals of lowest type. Some technical devices employed below are similar to ones used by Tait, but while the proof-theoretic methods employed here are naturally characterizable in terms of functionals of lowest type the present proof avoids the introduction of such functionals into the languages studied.
Permutation methods applied to Quine's “New foundations”
Authors: Henson C. Ward
Published: May 2006

Permutation methods for proving relative consistency results were first applied to Quine's set theory NF by Dana Scott [5]. He showed that the sentence (∃x)(x = {x}), which asserts the existence of individuals in Quine's sense, and its negation are each consistent relative to NF. In this paper Scott's method is shown to apply to any extension T of NF whose axioms are invariant in a certain sense. (Every stratified sentence is invariant, as are many interesting unstratified sentences, such as Rosser's Counting Axiom and the sentence which asserts that every Cantorian set is strongly Cantorian.) We also use this method to prove a number of interesting relative consistency results for such extensions T of NF.

Our main result (Theorem 2.4) asserts that it is consistent relative to T to assume that every well ordering of a strongly Cantorian set is order isomorphic to the well ordering by ∈ of a von Neumann ordinal. (The restriction to strongly Cantorian sets is necessary.) Therefore, although one cannot develop within NF a satisfactory theory of von Neumann ordinals, due to the many unstratified formulas which arise, our result shows that one can consistently assume as rich a theory as is allowed by the extent to which T provides for strongly Cantorian sets. This seems to be the first such “positive” consistency result for NF, and we think that the permutation method will yield others.
Canonical Partition Relations
Authors: Baumgartner James E.
Published: May 2006

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.
Borel sets and Ramsey's theorem
Authors: Galvin Fred , Prikry Karel
Published: May 2006

Definition 1. For a set S and a cardinal κ,

In particular, 2ω denotes the power set of the natural numbers and not the cardinal 2ℵ0. We regard 2ω as a topological space with the usual product topology.

Definition 2. A set S ⊆ 2ω is Ramsey if there is an M ∈ [ω]ω such that either [M]ω ⊆ S or else [M]ω ⊆ 2ω − S.

Erdös and Rado [3, Example 1, p. 434] showed that not every S ⊆ 2ω is Ramsey. In view of the nonconstructive character of the counterexample, one might expect (as Dana Scott has suggested) that all sufficiently definable sets are Ramsey. In fact, our main result (Theorem 2) is that all Borei sets are Ramsey. Soare [10] has applied this result to some problems in recursion theory.

The first positive result on Scott's problem was Ramsey's theorem [8, Theorem A]. The next advance was Nash-Williams' generalization of Ramsey's theorem (Corollary 2), which can be interpreted as saying: If S1 and S2 are disjoint open subsets of 2ω, there is an M ∈ [ω]ω such that either [M]ω ⋂ S1 = ∅ or [M]ω ∩ S2 = ⊆. (This is halfway between “clopen sets are Ramsey” and “open sets are Ramsey.”) Then Galvin [4] stated a generalization of Nash-Williams' theorem (Corollary 1) which says, in effect, that open sets are Ramsey; this was discovered independently by Andrzej Ehrenfeucht, Paul Cohen, and probably many others, but no proof has been published.
Recursive elements and constructive extensions of computable local integral domains
Authors: Suter Glen H.
Published: May 2006

With reservations, one can think of abstract algebra as the study of what consequences can be drawn from the axioms associated with certain concrete algebraic structures. Two important examples of such concrete algebraic structures are the integers and the rational numbers. The integers and the rational numbers have two properties which are not in general mirrored in the abstract axiom systems associated with them. That is, the integers and the rational numbers both have effectively computable metrics and their algebraic operations are effectively computable. The study of abstract algebraic systems which possess effectively computable algebraic operations has produced many interesting results. One can think of a computable algebraic structure as one whose elements have been labeled by the set of positive integers and whose operations are effectively computable. The formal definition of computable local integral domain will be given in §3. Some specific computable structures which have been studied are the integers, the rational numbers, and the rational numbers with p-adic valuation. Computable structures were studied in general by Rabin [12]. This paper concerns computable local integral domains as exemplified by the local integral domain Zp. Zp is the localization of the integers with respect to the maximal prime ideal generated by the positive prime p. We should note that the concept of local integral domain is not first order.

Let the ordered pair (Q, M) stand for a local ring, where Q is the local ring and M is the unique maximal prime ideal of Q. Since most of my results are proving the existence of certain effective procedures, the assumption that Q has a principal maximal ideal M (rather than M has n generators) greatly simplifies many of the proofs.
Types omitted in uncountable models of arithmetic
Authors: Knight Julia F.
Published: May 2006

In [4] it is shown that if the structure omits a type Σ, and Σ is complete with respect to Th(), then there is a proper elementary extension of which omits Σ. This result is extended in the present paper. It is shown that Th() has models omitting Σ in all infinite powers.

A type is a countable set of formulas with just the variable ν occurring free. A structure is said to omit the type Σ if no element of satisfies all of the formulas of Σ. A type Σ, in the same language as a theory T, is said to be complete with respect to T if (1) T ∪ Σ is consistent, and (2) for every formula φ(ν) of the language of T (with just ν free), either φ or ¬φ is in Σ.

The proof of the result of this paper resembles Morley's proof [5] that the Hanf number for omitting types is . It is shown that there is a model of Th() which omits Σ and contains an infinite set of indiscernibles. Where Morley used the Erdös-Rado generalization of Ramsey's theorem, a definable version of the ordinary Ramsey's theorem is used here.

The “omitting types” version of the ω-completeness theorem ([1], [3], [6]) is used, as it was in Morley's proof and in [4]. In [4], satisfaction of the hypotheses of the ω-completeness theorem followed from the fact that, in , any infinite, definable set can be split into two infinite, definable sets.
On an extension of Hilbert's second ε-theorem
Authors: Flannagan T. B.
Published: May 2006

The aim of this paper is to correct an error in the proof in [2] of a strengthened version of Hilbert's second ε-theorem.

Hilbert's original theorem says (effectively) that formulae of the form ∃xA → A(εxA) can be eliminated from deductions of ∈-free sentences B (i.e. those which do not contain the ε-symbol) from collections X of ε-free sentences. The extended version (Theorem III. 11 of [2]) says that, in addition, instances of Ackermann's schema can also be eliminated.

The error in [2] occurs in the proof of Theorem III.7 and is described as follows. If A′ is the formula obtained from A by replacing every occurrence of ∃yB by B(εyB) (or ∀yC by C(εyB) if B is of the form ¬ C), and if A is a Q3 or Q4-axiom then, contrary to the claim on p. 73 of [2], A′ is not necessarily an axiom of the same form. For example, if A is the Q3-axiom

where the rank of εx∃yD(x, y) is ≤ the rank of εyB (see p. 70) and where B is D(t,y), then A′ is

which is not a Q3-axiom. In other words, the notion of rank as defined in [2] is inadequate for the proof of Theorem III.11.
The inconsistency of
Authors: Bunder M. W.
Published: May 2006

In [4] Curry raised the possibility that his system proposed in ξ15C of [3] might be inconsistent. In this paper this inconsistency is proved using a method also employed in [1].

From Curry's axiom ⊦LH, it follows that

holds for arbitrary X.

The other results from that are required are

Modus Ponens, and the Deduction Theorem for implication:

Assuming ⊦HA, we define as in [1]:

and let

where Y is the paradoxical (or fixed point) combinator.
Lawvere's basic theory of the category of categories
Authors: Blanc Georges , Preller Anne
Published: May 2006

It is long known that Lawvere's theory in The category of categories as foundations of mathematics A[1] does not work, as indicated in Ishell's review [0]. Isbell there gives a counterexample that CDT—Category Description Theorem—[1, p. 15] is in fact not a theorem of BT (the Basic Theory of [1]) and suggests adding CDT to the axioms.

Our starting point was the claim in [1] that “the basic theory needs no explicit axiom of infinity.” We define a model ℳ of BT in which all categories are finite. In particular, the “monoid of nonnegative integers N” coincides in ℳ with the terminal object 1. We study ℳ in some detail in order to establish the true status of various “theorems” or “metatheorems” of BT: The metatheorem of [1, p. 11] saying that the discrete categories form a category of sets, CDT, the theorem on p. 15, and the theorem on p. 16 of [1] are all nontheorems. The remaining results indicated in [1] concerning BT are provable. However, as the Predicative Functor Construction Schema—PFCS—are justified in [1] by using the “metatheorem” and CDT, we provide a proof of these two schemata by showing that the discrete categories of BT (or of convenient extensions of BT) form a two-valued Boolean topos.