bluuebunny/crossref_metadata_2025_split huggingface dataset:
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.
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 postulateto 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 postulateto 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).
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 withALCLpLqLCLqLp,is complete with respect to this interpretation when time is taken to be continuous, and that D, the extension of S4.3 withALNLpLCLCLCpLpLpLp,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 andCLCLCpLpLpCMLpLp.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.
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.
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.
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.
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).
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

AbstractSeveral 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-axiomwhere the rank of εx∃yD(x, y) is ≤ the rank of εyB (see p. 70) and where B is D(t,y), then A′ iswhich 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 thatholds for arbitrary X.The other results from that are required areModus Ponens, and the Deduction Theorem for implication:Assuming ⊦HA, we define as in [1]:and letwhere 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.