bluuebunny/crossref_metadata_2025_split huggingface dataset:
Addendum to early history of the Association for Symbolic Logic
Authors: Ducasse C. J. , Curry Haskell B. 
Published: May 2006

Since publication of our account of the early history of the Association for Symbolic Logic in the September 1962 issue of its Journal, the fact has been called to our attention that — because much of the correspondence at that time is no longer available and we had therefore to depend on our memory — we failed to mention an important item of that early history.This was a letter from Professor Paul Weiss to the Editor of Philosophy of Science, which appeared in the April, 1934, issue of that periodical. This letter, entitled “A Home for Logic,” called attention to the fact that papers on logic were scattered in heterogeneous periodicals, and suggested that the Philosophy of Science Association take under its wing the establishment of a Logical Association.
The next admissible set
Authors: Barwise K. J. , Gandy R. O. , Moschovakis Y. N. 
Published: May 2006

In this paper we describe generalizations of several approaches to the hyperarithmetic hierarchy, show how they are related to the Kripke-Platek theory of admissible ordinals and sets, and study conditions under which the various approaches remain equivalent.To put matters in some perspective, let us first review various approaches to the theory of hyperarithmetic sets. For most purposes, it is convenient to first define the semi-hyperarithmetic (semi-HA) subsets of N. A set is then said to be hyperarithmetic (HA) if both it and its complement are semi-HA. A total number-theoretic function is HA if its graph is HA.
Consistency notions in illative combinatory logic
Authors: Bunder M. W. 
Published: May 2006

In this paper we show that certain notions of consistency currently in use in illative combinatory logic are not always necessary nor always sufficient for the acceptability of the system.The three notions of consistency we will consider are:(A) Not all terms of the system are assertible.(B) Not all propositions of the system are assertible.(C) The system is Q-consistent, i.e. if Q (for equality) is in or is added to the system as a primitive with axioms such asPost defined a system of propositional calculus to be inconsistent if all propositions were assertible. In a more general system where there may be terms which are not propositions (although all propositions are terms), we need to distinguish notions (A) and (B) as two possible consistency notions “in the sense of Post”.In [3] Curry and Feys assume that Q is in the system defined as λxλy.Ξ(C*x)(C*y) or as a primitive, but Seldin in [5] also talks about Q-consistency of a system (F22) to which Q has to be added. We therefore consider the definition of Q-consistency that includes all three possibilities.In [3] Curry and Feys state that Q-consistency is essential for acceptability. This is because there the purpose was to have an assertional system of illative combinatory logic in which combinatory equality was represented by the assertion of QXY. However if Q is to represent some other form of equality, Q-consistency may become inessential for acceptability or even incompatible with it.
An intuitionistically plausible interpretation of intuitionistic logic
Authors: de Swart H. C. M. 
Published: May 2006

Let IPC be the intuitionistic first-order predicate calculus. From the definition of derivability in IPC the following is clear:(1) If A is derivable in IPC, denoted by “⊦IPCA”, then A is intuitively true, that means, true according to the intuitionistic interpretation of the logical symbols. To be able to settle the converse question: “if A is intuitively true, then ⊦IPCA”, one should make the notion of intuitionistic truth more easily amenable to mathematical treatment. So we have to look then for a definition of “A is valid”, denoted by “⊨A”, such that the following holds:(2) If A is intuitively true, then ⊨ A.Then one might hope to be able to prove(3) If ⊨ A, then ⊦IPCA.If one would succeed in finding a notion of “⊨ A”, such that all the conditions (1), (2) and (3) are satisfied, then the chain would be closed, i.e. all the arrows in the scheme below would hold.Several suggestions for ⊨ A have been made in the past: Topological and algebraic interpretations, see Rasiowa and Sikorski [1]; the intuitionistic models of Beth, see [2] and [3]; the interpretation of Grzegorczyk, see [4] and [5]; the models of Kripke, see [6] and [7]. In Thirty years of foundational studies, A. Mostowski [8] gives a review of the interpretations, proposed for intuitionistic logic, on pp. 90–98.
Provable wellorderings of formal theories for transfinitely iterated inductive definitions
Authors: Buchholz W. , Pohlers W. 
Published: May 2006

By [12] we know that transfinite induction up to ΘεΩN+10 is not provable in IDN, the theory of N-times iterated inductive definitions. In this paper we will show that conversely transfinite induction up to any ordinal less than ΘεΩN+10 is provable in IDNi, the intuitionistic version of IDN, and extend this result to theories for transfinitely iterated inductive definitions.In [14] Schütte proves the wellordering of his notational systems using predicates is wellordered) with Mκ ≔ {x ∈ and 0 ≤ κ ≤ N. Obviously the predicates are definable in IDNi with the defining axioms:where Prog [Mκ, X] means that X is progressive with respect to Mκ, i.e.The crucial point in Schütte's wellordering proof is Lemma 19 [14, p. 130] which can be modified towhere TI[Mκ + 1, a] is the scheme of transfinite induction over Mκ + 1 up to a.
On complexity properties of recursively enumerable sets
Authors: Blum M. , Marques I. 
Published: May 2006

An important goal of complexity theory, as we see it, is to characterize those partial recursive functions and recursively enumerable sets having some given complexity properties, and to do so in terms which do not involve the notion of complexity.As a contribution to this goal, we provide characterizations of the effectively speedable, speedable and levelable [2] sets in purely recursive theoretic terms. We introduce the notion of subcreativeness and show that every program for computing a partial recursive function f can be effectively speeded up on infinitely many integers if and only if the graph of f is subcreative.In addition, in order to cast some light on the concepts of effectively speedable, speedable and levelable sets we show that all maximal sets are levelable (and hence speedable) but not effectively speedable and we exhibit a set which is not levelable in a very strong sense but yet is effectively speedable.
On definable subsets of p-adic fields
Authors: MacIntyre Angus 
Published: May 2006

The brilliant work of Ax-Kochen [1], [2], [3] and Ersov [6], and later work by Kochen [7] have made clear very striking resemblances between real closed fields and p-adically closed fields, from the model-theoretical point of view. Cohen [5], from a standpoint less model-theoretic, also contributed much to this analogy.In this paper we shall point out a feature of all the above treatments which obscures one important resemblance between real and p-adic fields. We shall outline a new treatment of the p-adic case (not far removed from the classical treatments cited above), and establish an new analogy between real closed and p-adically closed fields.We want to describe the definable subsets of p-adically closed fields. Tarski [9] in his pioneering work described the first-order definable subsets of real closed fields. Namely, if K is a real-closed field and X is a subset of K first-order definable on K using parameters from K then X is a finite union of nonoverlapping intervals (open, closed, half-open, empty or all of K). In particular, if X is infinite, X has nonempty interior.Now, there is an analogous question for p-adically closed fields. If K is p-adically closed, what are the definable subsets of K? To the best of our knowledge, this question has not been answered until now.What is the difference between the two cases? Tarski's analysis rests on elimination of quantifiers for real closed fields. Elimination of quantifiers for p-adically closed fields has been achieved [3], but only when we take a cross-section π as part of our basic data. The problem is that in the presence of π it becomes very difficult to figure out what sort of set is definable by a quantifier free formula. We shall see later that use of the cross-section increases the class of definable sets.
Definability of measures and ultrafilters
Authors: Pincus David , Solovay Robert M. 
Published: May 2006

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.
Definability in well quasi-ordered sets of structures
Authors: Landraitis Charles K. 
Published: May 2006

The theorem introduced here provides a sufficient condition for an axiomatic class to be elementary. It resulted from consideration of a definability problem in , but is introduced in a less specific context and accompanied by applications to .As in [La, 1], [La, 2], a reflexive, transitive binary relation R on a nonempty set S will be called a quasi-ordering or q.o. of S. A set of pairwise incomparable elements of S is an antichain and a subset of S linearly ordered by R is a chain. A chain {Si: i ∈ ω} with i > j if and only if (siRsj ∧ ¬ sjRSi) will be called an infinite descending chain. If S has no infinite antichains nor any infinite descending chains, S is well quasi-ordered by R, and is called a well quasi-ordering or w.q.o. Any subset of a w.q.o. is a w.q.o. An element s of a q.o. S is minimal in S if ∀t ∈ S(tRs → sRt). A subset S′ of S is a foundation for S if ∀t ∈ S∃s ∈ S′(sRt).
Uniform enumeration operations
Authors: Lachlan A. H. 
Published: May 2006

AbstractSacks [2] has asked whether there exists a uniform solution to Post's problem, i.e. an enumeration operation W such that d < W(d) < d′ for every degree d. It is shown here that if such an operation W exists it cannot itself in a particular technical sense be uniform. In fact, the jump operation is characterized amongst such uniform enumeration operations by the condition: d < W(d) for all d. In addition, it is proved that the only other uniform enumeration operations such that d ≤ W(d) for all d are those which equal the identity operation above some fixed degree.
Krom formulas with one dyadic predicate letter
Authors: Lewis Harry R. 
Published: May 2006

Let Kr be the class of all those quantificational formulas whose matrices are conjunctions of binary disjunctions of signed atomic formulas. Decision problems for subclasses of Kr do not invariably coincide with those for the corresponding classes of quantificational formulas with unrestricted matrices; for example, the ∀∃∀ prefix subclass of Kr is solvable, but the full ∀∃∀ class is not ([AaLe],- [KMW]). Moreover, the straightforward encodings of automata which have been used to show the unsolvability of various subclasses of Kr ([Aa], [Bö], [AaLe]) yield but little information about signature subclasses, i.e. subclasses determined by the number and degrees of the predicate letters occurring in a formula. By a new and highly complex construction Theorem 1 establishes the best possible result on classification by signature.Theorem 1. Let C be the class of all formulas in Kr with a single predicate letter, which is dyadic; then C is a reduction class for satisfiability.Thus a signature subclass of Kr is solvable just in case the corresponding class of unrestricted quantificational formulas is solvable, to wit, just in case no predicate letter of degree exceeding one may occur. To obtain a richer classification by signature we consider further restrictions on the matrix. Let Or be the class of formulas in Kr having disjunctive normal forms with only two disjuncts. Theorem 2 sharpens Orevkov's proof of the unsolvability of Or ([Or]; see also [LeGo]).Theorem 2. Let D be the class of formulas in Or with just two predicate letters, both pentadic; then D is a reduction class for satisfiability.
Congruence relations, filters, ideals, and definability in lattices of α-recursively enumerable sets
Authors: Lerman Manuel 
Published: May 2006

Throughout this paper, α will denote an admissible ordinal. Let (α) denote the lattice of α-r.e. sets, i.e., the lattice whose elements are the α-r.e. sets, and whose ordering is given by set inclusion. Call a set A ∈ (α)α*-finite if it is α-finite and has ordertype < α* (the Σ1-projectum of α). The α*-finite sets form an ideal of (α), and factoring (α) by this ideal, we obtain the quotient lattice *(α).We will fix a language ℒ suitable for lattice theory, and discuss decidability in terms of this language. Two approaches have succeeded in making some progress towards determining the decidability of the elementary theory of (α). Each approach was first used by Lachlan for α = ω. The first approach is to relate the decidability of the elementary theory of (α) to that of a suitable quotient lattice of (α) by a congruence relation definable in ℒ. This technique was used by Lachlan [4, §1] to obtain the equidecidability of the elementary theories of (ω) and *(ω), and was generalized by us [6, Corollary 1.2] to yield the equidecidability of the elementary theories of (α) and *(α) for all α. Lachlan [3] then adopted a different approach.
The decision problem for standard classes
Authors: Gurevich Yuri 
Published: May 2006

The standard classes of a first-order theory T are certain classes of prenex T-sentences defined by restrictions on prefix, number of monadic, dyadic, etc. predicate variables, and number of monadic, dyadic, etc. operation variables. In [3] it is shown that, for any theory T, (1) the decision problem for any class of prenex T-sentences specified by such restrictions reduces to that for the standard classes, and (2) there are finitely many standard classes K1, …, Kn such that any undecidable standard class contains one of K1, …, Kn. These results give direction to the study of the decision problem.Below T is predicate logic with identity and operation variables. The Main Theorem solves the decision problem for the standard classes admitting at least one operation variable.
An introduction to recursively saturated and resplendent models
Authors: Barwise Jon , Schlipf John 
Published: May 2006

The notions of recursively saturated and resplendent models grew out of the study of admissible sets with urelements and admissible fragments of Lω1ω, but, when applied to ordinary first order model theory, give us new tools for research and exposition. We will discuss their history in §3.The notion of saturated model has proven to be important in model theory. Its most important property for applications is that if , are saturated and of the same cardinality then = iff ≅ . See, e.g., Chang-Keisler [3]. The main drawback is that saturated models exist only under unusual assumptions of set theory. For example, if 2κ = κ+ then every theory T of L has a saturated model of power κ+. (Similarly, if κ is strongly inaccessible, then every T has a saturated model of power κ.) On the other hand, a theory T like Peano arithmetic, with types, cannot have a saturated model in any power κ with ω ≤ κ ≤ .One method for circumventing these problems of existence (or rather non-existence) is the use of “special” models (cf. [3]). If κ = Σλ<κ2λ, κ < ω, then every theory T of L has a special model of power κ. Such cardinals are large and, themselves, rather special. There are definite aesthetic objections to the use of these large, singular models to prove results about first order logic.
A complete Lω1ω-sentence characterizing ℵ1
Authors: Knight Julia F. 
Published: May 2006

Here an example will be given of a complete Lω1ω-sentence with a model of power ℵ1 but with no model of higher power. The continuum hypothesis is not assumed. The question of whether such an example exists was brought to the author's attention by Professor M. Makkai.An Lω1ω-sentence is said to be complete if its models all satisfy the same Lω1ω-sentences, or, equivalently, if all of the countable L-structures satisfying the sentence are isomorphic. Scott [5] showed that any countable L -structure (where L is countable) must satisfy a complete Lω1ω-sentence. Such a sentence is called a Scott sentence for the structure. An uncountable L-structure need not satisfy any complete Lω1ω -sentence.A complete Lω1ω-sentence σ is said to characterize the infinite cardinal k if σ has a model of power k but not of any higher power. The set of cardinals characterized by complete Lω1ω -sentences will be denoted by CC. By a result of Lopez-Escobar [3], if k ∈ CC, k <⊐ω1.Assuming GCH (so that ⊐α = ℵα, ), Malitz [4] showed that CC = {ℵα: α < ω1}.Without assuming GCH, Baumgartner [1] showed that ⊐α ∈ CC for all α < ω1.Without GCH, it is unknown whether ℵn ∈ CC for n ≥ 2. Now it will be shown that ℵ1, ∈ CC.
Σ1-compactness and ultraproducts
Authors: Cutland Nigel 
Published: May 2006

This paper is devoted to a description of the way in which ultraproducts can be used in proofs of various well-known Σ1-compactness theorems for infinitary languages ℒA associated with admissible sets A; the method generalises the ultra-product proof of compactness for finitary languages.The compactness theorems we consider are (§2) the Barwise Compactness Theorem for ℒA when A is countable admissible [1], and (§3) the Cofinality (ω) Compactness Theorem of Barwise and Karp [2] and [4]. Our proof of the Barwise theorem unfortunately has the defect that it relies heavily on the Completeness Theorem for ℒA. This defect has, however, been avoided in the case of the Cf(ω) Compactness Theorem, so we have a purely model-theoretic proof.
Sets of theorems with short proofs
Authors: Richardson Daniel 
Published: May 2006

R. Parikh has shown that in the predicate calculus without function symbols it is possible to decide whether or not a given formula A is provable in a Hilbert-style proof of k lines. He has also shown that for any formula A(x1, …, xn) of arithmetic in which addition and multiplication are represented by three-place predicates, {(a1, …, an): A(a1, …, an) is provable from the axioms of arithmetic in k lines} is definable in (N,′, +,0). See [2].In §1 of this paper it is shown that if S is a definable set of n-tuples in (N,′, +, 0), then there is a formula A(x1, …, xn) and a number k so that (a1 …, an) ∈ S if and only if A(a1 …, an) can be proved in a proof of complexity k from the axioms of arithmetic. The result does not depend on which formalization of arithmetic is used or which (reasonable) measure of proof complexity. In particular, this gives a converse to Parikh's result.In §II, a measure of proof complexity is given which is based on counting the quantifier steps in semantic tableaux. The idea behind this measure is that A is k provable if in the attempt to construct a counterexample one meets insurmountable difficulties in the definition of the appropriate Skolem functions over sets of cardinality ≤ k. A method is given for deciding whether or not a sentence A in the full predicate calculus is k provable. The question for the full predicate calculus and Hilbert-style systems of proof remains open.
Boolean extensions which efface the Mahlo property
Authors: Boos William 
Published: May 2006

The results that follow are intended to be understood as informal counterparts to formal theorems of Zermelo-Fraenkel set theory with choice. Basic notation not explained here can usually be found in [5]. It will also be necessary to assume a knowledge of the fundamentals of boolean and generic extensions, in the style of Jech's monograph [3]. Consistency results will be stated as assertions about the existence of certain complete boolean algebras, B, C, etc., either outright or in the sense of a countable standard transitive model M of ZFC augmented by hypotheses about the existence of various large cardinals. Proofs will usually be phrased in terms of the forcing relation ⊩ over such an M, especially when they make heavy use of genericity. They are then assertions about Shoenfield-style P-generic extensions M(G), in which the ‘names’ are required without loss of generality to be elements of MB = (VB)M, B is the boolean completion of P in M (cf. [3, p. 50]: the notation there is RO(P)), the generic G is named by Ĝ ∈ MB such that (⟦p ∈ Ĝ⟧B = p and (cf. [11, p. 361] and [3, pp. 58–59]), and for p ∈ P and c1, …, cn ∈ MB, p ⊩ φ(c1, …, cn) iff ⟦φ(c1, …, cn)⟧B ≥ p (cf. [3, pp. 61–62]).Some prior acquaintance with large cardinal theory is also needed. At this writing no comprehensive introductory survey is yet in print, though [1], [10], [12]and [13] provide partial coverage. The scheme of definitions which follows is intended to fix notation and serve as a glossary for reference, and it is followed in turn by a description of the results of the paper. We adopt the convention that κ, λ, μ, ν, ρ and σ vary over infinite cardinals, and all other lower case Greek letters (except χ, φ, ψ, ϵ) over arbitrary ordinals.