bluuebunny/crossref_metadata_2025 huggingface dataset:
A converse of the Barwise completeness theorem
Authors: Stavi Jonathan
Published: May 2006

In this paper a converse of Barwise's completeness theorem is proved by cut-elimination considerations applied to inductive definitions. We show that among the transitive sets T satisfying some weak closure conditions (closure under primitive-recursive set-functions is more than enough), only the unions of admissible sets satisfy Barwise's completeness theorem in the form stating that if φ ∊ T is a sentence which has a derivation (in the universe) then φ has a derivation in T. See §1 for the origin of the problem in Barwise's paper [Ba].

Stated quite briefly the proof is as follows (a step-by-step account including relevant definitions is given in the body of the paper):

Let T be a transitive prim.-rec. closed set, and let is nonempty, transitive and closed under pairs}. For each let κ(A) be the supremum of closure ordinals of first-order positive operators on subsets of A (first-order with respect to By Theorem 1 of [BGM], it is enough to prove that rank(T) in order to obtain that T is a union of admissible sets. (The rank of a set is defined by rank(x) = supy ∊ x (rank(y) + 1); since T is prim.-rec. closed, rank(T) = smallest ordinal not in T.)

Let We show how to find in T (in fact, in Lω(A)) a derivable sentence τ that has no derivation D such that rank(D) ≤ α. Thus, if τ is to have a derivation in T, rank(T) > α. α is arbitrary (< κ(A)), so rank(T) ≥ κ(A). Q.E.D.
The relation of A to Prov ˹A˺ in the Lindenbaum sentence algebra
Authors: Kent C. F.
Published: May 2006

Let U be a consistent axiomatic theory containing Robinson's Q [TMRUT, p. 51]. In order for the results below to be of interest, U must be powerful enough to carry out certain arguments involving versions of the “derivability conditions,” DC(i) to DC(iii) below, of [HBGM, p. 285], [F60, Theorem 4.7], or [L55]. Thus it must contain, at least, mathematical induction for formulas whose prenex normal forms contain at most existential quantifiers. For convenience, U is assumed also to contain symbols for primitive recursive functions and relations, and their defining equations. One of these is used to form the standard provability predicate, Prov ˹A˺, “there exists a number which is the Gödel number of a proof of A.” Upper corners denote numerals for Gödel numbers for the enclosed sentences, and parentheses are often omitted in their presence.

This paper contains some results concerning the relation between the sentence A, and the sentence Prov ˹A˺ in the Lindenbaum Sentence Algebra (LSA) for U, the Boolean algebra induced by the pre-order relation A ≤ B ⇔ ⊦A → B. Half of the answer is provided by a theorem of Löb [L55], which states that ⊦Prov ˹A˺ → A ⇔ ⊦A. Hence, in the presence of DC(iii), below, it is never true that Prov ˹A˺ < A in the LSA. However, there is a large and interesting set of sentences, denoted here by Γ, for which A < Prov ⌜A⌝.
The word problem for free fields
Authors: Cohn P. M.
Published: May 2006

It has long been known that every free associative algebra can be embedded in a skew field [11]; in fact there are many different embeddings, all obtainable by specialization from the ‘universal field of fractions’ of the free algebra (cf. [5, Chapter 7]). This makes it reasonable to call the latter the free field; see §2 for precise definitions. The existence of this free field was first established by Amitsur [1], but his proof is rather indirect and does not provide anything like a normal form for the elements of the field. Actually one cannot expect to find such a normal form, since it does not even exist in the field of fractions of a commutative integral domain, but at least one can raise the word problem for free fields: Does there exist an algorithm for deciding whether a given expression for an element of the free field represents zero?

Now some recent work has revealed a more direct way of constructing free fields ([4], [5], [6]), and it is the object of this note to show how this method can be used to solve the word problem for free fields over infinite ground fields. In this connexion it is of interest to note that A. Macintyre [9] has shown that the word problem for skew fields is recursively unsolvable. Of course, every finitely generated commutative field has a solvable word problem (see e.g. [12]).

The construction of universal fields of fractions in terms of full matrices is briefly recalled in §2, and it is shown quite generally for a ringRwith a field of fractions inverting all full matrices, that if the set of full matrices overRis recursive, then the universal field has a solvable word problem. This holds more generally if the precise set of matrices overRinverted over the field is recursive, but it seems difficult to exploit this more general statement.
The consistency of classical set theory relative to a set theory with intu1tionistic logic
Authors: Friedman Harvey
Published: May 2006

Let ZF be the usual Zermelo-Fraenkel set theory formulated without identity, and with the collection axiom scheme. Let ZF−-extensionality be obtained from ZF by using intuitionistic logic instead of classical logic, and dropping the axiom of extensionality. We give a syntactic transformation of ZF into ZF−-extensionality.

Let CPC, HPC respectively be classical, intuitionistic predicate calculus without identity, whose only homological symbol is ∈. We use the ~ ~-translation, a basic tool in the metatheory of intuitionistic systems, which is defined by

The two fundamental lemmas about this ~ ~ -translation we will use are

For proofs, see Kleene [3, Lemma 43a, Theorem 60d].

This - would provide the desired syntactic transformation at least for ZF into ZF− with extensionality, if A− were provable in ZF− for each axiom A of ZF. Unfortunately, the ~ ~-translations of extensionality and power set appear not to be provable in ZF−. We therefore form an auxiliary classical theory S which has no extensionality and has a weakened power set axiom, and show in §2 that the ~ ~-translation of each axiom of Sis provable in ZF−-extensionality. §1 is devoted to the translation of ZF in S.
An axiomatization for a class of two-cardinal models
Authors: Schmerl James H.
Published: May 2006

In this note we give a simple recursive axiomatization for the class of structures of type (ℶω ℵ0). This solves a problem of Vaught which is Problem 13 in the book [1] of Chang and Keisler. The same technique is used to get a recursive axiomatization for the class of κ-like structures where κ is strongly ω-inaccessible.

Let us fix throughout some recursive first-order language L, and until further notice let us suppose that included in L is a distinguished unary predicate symbol U. For cardinals κ and λ with κ ≥ λ ≥ ℵ0, we say the structure has type (κ, λ) if card(A)= κ and card . Let K(κ, λ) be the class of all structures of type (κ, λ). For each ordinal α define 2ακby 20κ = κ, and 2ακ= ⋃ {2λ: λ = 2βκ for some β < α} when α > 0. Let

Vaught proved the following theorem in [7].

Theorem (Vaught). Suppose a is a sentence such that for each n < ω there are κ, λ with κ > 2λn and a model of σ of type (κ, λ). Then whenever κ ≥ λ ≥ ℵ0, the sentence σ has a model of type (κ, λ).
Fragments of first order logic, I: universal Horn logic
Authors: McNulty George F.
Published: May 2006

Let L be any finitary language. By restricting our attention to the universal Horn sentences of L and appealing to a semantical notion of logical consequence, we can formulate the universal Horn logic of L. The present paper provides some theorems about universal Horn logic that serve to distinguish it from the full first order predicate logic. Universal Horn equivalence between structures is characterized in two ways, one resembling Kochen's ultralimit theorem. A sharp version of Beth's definability theorem is established for universal Horn logic by means of a reduced product construction. The notion of a consistency property is relativized to universal Horn logic and the corresponding model existence theorem is proven. Using the model existence theorem another proof of the definability result is presented. The relativized consistency properties also suggest a syntactical notion of proof that lies entirely within the universal Horn logic. Finally, a decision problem in universal Horn logic is discussed. It is shown that the set of universal Horn sentences preserved under the formation of homomorphic images (or direct factors) is not recursive, provided the language has at least two unary function symbols or at least one function symbol of rank more than one.

This paper begins with a discussion of how algebraic relations between structures can be used to obtain fragments of a given logic. Only two such fragments seem to be under current investigation: equational logic and universal Horn logic. Other fragments which seem interesting are pointed out.
A new look at the interpolation problem
Authors: Stern Jacques
Published: May 2006

The original aim of this paper was to show that forcing provided a useful and unifying tool in the model theory of finite and admissible languages. Roughly speaking, any result obtained by a Henkin proof, by Makkai's method or by an omitting type argument can be given an alternative proof via forcing. Finally, instead of giving new proofs of a number of known theorems, we have chosen to focus on the interpolation theorem for many-sorted languages. The main result of this paper is thus a generalization of Feferman's theorems ([2], [3]) with a completely different proof; this was announced in [8] and [9].

For more on forcing techniques in model theory the reader should consult [4] as well as [5]. He should also compare forcing and boolean-valued models developed in [6] for the classical case and in [7] for admissible languages. Throughout the paper familiarity with the standard concepts of model theory is assumed.

The author wishes to express his gratitude to J. L. Krivine and K. McAloon for supervising his work. Thanks are also due to J. P. Ressayre for helpful suggestions and to R. L. Vaught for an interesting discussion on forcing in model theory. Finally, an interesting application has been pointed out by S. Feferman and has been included with his permission.
A large power set axiom
Authors: Cohen Paul E.
Published: May 2006

Takeuti [6] has suggested the need for higher axioms for set theory which are analogous to higher axioms of infinity, but which claim that power sets are in some sense large. In this paper we investigate a reflection axiom of this sort (Axiom T).

In §1, we introduce Axiom T and explore some related axioms. A technical lemma involving an elementary embedding is developed in §2 which allows us, in §3, to prove the relative consistency of Axiom T.

The reader is assumed to be familiar with ramified forcing languages and the usual techniques of forcing. A suitable treatment of these subjects is given by Takeuti and Zaring [7].

ZFC, GBC, ZF and GB are the set theories of Zermelo-Fraenkel and of Gödel-Bernays, with and without the axiom of choice (AC). CH is the continuum hypothesis.

For α an ordinal, define

For p1, p2 ∈ pα let p1 ≤ p2 mean that p1 ⊇ p2 (thus p1 is the stronger forcing condition). It is well known that Pα satisfies the countable chain condition [5].
A note on modal formulae and relational properties
Authors: van Benthem J. F. A. K.
Published: May 2006

Consider modal propositional formulae, constructed using proposition-letters, connectives and the modal operators □ and ⋄. The semantic structures are frames, i.e., pairs  with R ⊆ W2. Let F, V be variables ranging respectively over frames and functions from the set of proposition-letters into the powerset of W. Then the relation

may be defined, for arbitrary formulae α, following the Kripke truth-definition. From this relation we may further define

Now, to every modal formula α there corresponds some property Pα of R. A particular example is obtained by considering the well-known translation of modal formulae into formulae of monadic second-order logic with a single binary first-order predicate. For these particular Pα we have

for all F and w ∈ W. These formulae Pα are, however, rather intractable and more convenient ones can often be found. An especially interesting case occurs when Pα may be taken to be some first-order formula. For example, it can be seen that

for all F and w ∈ W. It is customary to talk about a related correspondence, namely when for all F we have

Note that this correspondence holds whenever the first one above holds.
Skolem functions and elementary embeddings
Authors: Knight Julia F.
Published: May 2006

Let L be an elementary first order language. Let be an L-structure, and let φ be an L-formula with free variables u1, …, un, and υ. A Skolem function for φ on is an n-ary operation f on such that for all . If is an elementary substructure of , then an n-ary operation f on is said to preserve the elementary embedding of into if f(x)∈ for all x ∈ n, and (, f ∣n) ≺ (, f). Keisler asked the following question:

Problem 1. If and are L-structures such that ≺ , and if φ (u, υ) is an L-formula (with appropriate free variables), must there be a Skolem function for φ on which preserves the elementary embedding?

Payne [6] gave a counterexample in which the language L is uncountable. In [3], [5], the author announced the existence of an example in which L is countable but the structures and are uncountable. The construction of the example will be given in this paper. Keisler's problem is still open in case both the language and the structures are required to be countable. Positive results for some special cases are given in [4].

The following variant of Keisler's question was brought to the author's attention by Peter Winkler:

Problem 2. If L is a countable language, a countable L-structure, and φ(u, υ) an L-formula, must there be a Skolem function f for φ on such that for every countable elementary extension of , there is an extension of f which preserves the elementary embedding of into ?
Σ1 compactness for next admissible sets
Authors: Green Judy
Published: May 2006

Let σ be any sequence B0, B1 …, Bn, … of transitive sets closed under pairs with for each n. In this paper we show that the smallest admissible set Aσ with σ ∈ Aσ is Σ1 compact. Thus we have an entirely new class of explicitly describable uncountable Σ1 compact sets.

The search for uncountable Σ1 compact languages goes back to Hanf's negative results on compact cardinals [7]. Barwise first showed that all countable admissible sets were Σ1 compact [1] and then went on to give a characterization of the Σ1 compact sets in terms of strict reflection [2]. While his characterization has been of interest in understanding the Σ1 compactness phenomenon it has led to the identification of only one class of uncountable Σ1 compact sets. In particular, Barwise showed [2], using the above notation, that if ⋃nBn is power set admissible it satisfies the strict reflection principle and hence is Σ1 compact. (This result was obtained independently by Karp using algebraic methods [9].)

In proving our compactness theorem we follow Makkai's approach to the Barwise Compactness Theorem [12] and use a modified version of Smullyan's abstract consistency property [14]. A direct generalization of Makkai's method to the cofinality ω case yields a proof of the Barwise-Karp result mentioned above [6]. In order to obtain our new result we depart from the usual definition of language and use instead the indexed languages of Karp [9] in which a conjunction is considered to operate on a function whose range is a set of formulas rather than on a set of formulas itself.
Turing machines and the spectra of first-order formulas
Authors: Jones Neil D. , Selman Alan L.
Published: May 2006

H. Scholz [11] defined the spectrum of a formula φ of first-order logic with equality to be the set of all natural numbers n for which φ has a model of cardinality n. He then asked for a characterization of spectra. Only partial progress has been made. Computational aspects of this problem have been worked on by Gunter Asser [1], A. Mostowski [9], and J. H. Bennett [2]. It is known that spectra include the Grzegorczyk class and are properly included in . However, no progress has been made toward establishing whether spectra properly include , or whether spectra are closed under complementation.

A possible connection with automata theory arises from the fact that contains just those sets which are accepted by deterministic linear-bounded Turing machines (Ritchie [10]). Another resemblance lies in the fact that the same two problems (closure under complement, and proper inclusion of ) have remained open for the class of context sensitive languages for several years.

In this paper we show that these similarities are not accidental—that spectra and context sensitive languages are closely related, and that their open questions are merely special cases of a family of open questions which relate to the difference (if any) between deterministic and nondeterministic time or space bounded Turing machines.

In particular we show that spectra are just those sets which are acceptable by nondeterministic Turing machines in time 2cx, where c is constant and x is the length of the input. Combining this result with results of Bennett [2], Ritchie [10], Kuroda [7], and Cook [3], we obtain the “hierarchy” of classes of sets shown in Figure 1. It is of interest to note that in all of these cases the amount of unrestricted read/write memory appears to be too small to allow diagonalization within the larger classes.
Minimum models of analysis
Authors: Shilleto J. R.
Published: May 2006

Although there is no smallest ω model [6], Putnam and Gandy independently proved about 1963 that the class of ramified analytical sets, as defined by Cohen [3], form the smallest β model of analysis [2], [8]. This paper will consider other restricted classes of models, namely the βn models for integers n > 1 [10], and prove under appropriate assumptions the existence of minimum such models. In fact we shall construct the minimum βn model in a fashion similar to the procedure yielding the class of ramified analytical sets, but adding at each stage a segment of the sets in those already obtained (for n a fixed integer > 1).

Roughly speaking a βn model is an ω model absolute for n-set-quantifier assertions about its subsets of natural numbers. A β model is simply a β1 model. See Enderton and Friedman [4] for a further investigation of βn models.
Nonrecursive combinatorial functions
Authors: Ellentuck Erik
Published: May 2006

In this paper we show how nonrecursive combinatorial functions can be used to obtain another proof of the compactness Theorem 3.1 of [6]. Our method is closely related to the argument used to show that a countable ultraproduct is ℵ1-saturated. What we do is to diagonalize in the most obvious way. The main difficulty with this approach is that the resulting diagonal function need not be recursive. Just to give an idea of how bad nonrecursive combinatorial functions are, we mention that by using frames (cf. [5]) they do not extend to Λ, and that by using normal combinatorial operators (cf. [4]) they do extend to Λ, map Λ into Λ, but in general, composition of such functions does not commute with their extension. We take care of this problem by constructing a large class of isols with respect to which the diagonal function is well behaved. The advantage of our method is that it provides the investigator with a natural and intuitive way of constructing counterexamples in his own research area.
Countable homogeneous relational structures and ℵ0-categorical theories
Authors: Henson C. Ward
Published: May 2006

A relational structure of cardinality ℵ0 is called homogeneous by Fraissé [1] if each isomorphism between finite substructures of can be extended to an automorphism of . In §1 of this paper it is shown that there are isomorphism types of such structures for the first order language L0 with a single (binary) relation symbol, answering a question raised by Fraissé. In fact, as is shown in §2, a family of nonisomorphic homogeneous structures for L0 can be constructed, each member of which satisfies the following conditions (where U is the homogeneous, ℵ0-universal graph, the structure of which is considered in [4]):

(i) The relation R of is asymmetric (R ∩ R−1 = ∅);

(ii) If A is the domain of and S is the symmetric relation R ∪ R−1, then (A, S) is isomorphic to U. That is, each may be regarded as the result of assigning a unique direction to each edge of the graph U.

Let T0 be the first order theory of all homogeneous structures for L0 which have cardinality ℵ0. In §3 (which can be read independently of §2) it is shown that T0 has complete extensions (in L0), each of which is ℵ0-categorical. Moreover, among the complete extensions of T0 are theories of arbitrary (preassigned) degree of unsolvability. In particular, there exists an undecidable, ℵ0-categorieal theory in L0, which answers a question raised by Grzegorczyk [2], [3].

It follows from Theorem 6 of [3] that there are ℵ0-categorical theories of partial orderings which have arbitrarily high degrees of unsolvability. This is in sharp contrast to the situation for linear orderings, which were the motivation for Fraissé's early work. Indeed, as is shown in [10], every ℵ0-categorical theory of a linear ordering is finitely axiomatizable. (W. Glassmire [12] has independently shown the existence of theories in L0 which are all ℵ0-categorical, and C. Ash [13] has independently shown that such theories exist with arbitrary degree of unsolvability.)
Decidability of the “almost all” theory of degrees
Authors: Stillwell John
Published: May 2006

Ever since Spector's brilliant application of measure theory to recursion theory in 1958 [6] it has been realized that measure theory promotes sweeping simplifications in the theory of degrees. Results previously thought to be pathological were shown by Spector, and later Sacks [4], [5], to hold for almost all degrees (“almost all” in the sense of Lebesgue measure), often with much simpler proofs. Good examples of this phenomenon are Spector's demonstration that almost all pairs of sets are of incomparable degree (as an immediate consequence of Fubini's theorem) and Sacks' exquisitely simple deduction from this result that almost every degree is the join of two incomparable degrees (for if a random sequence is decomposed into its even and odd parts, the result is a random pair).

The present paper attempts to vindicate the feeling that almost all degrees behave in a simple manner by showing that if the quantifier in the theory of degrees with ′(jump), ∪ (join) and ∩ (meet) is taken to be (almost ∀a) instead of (∀a) then the theory is decidable. We are able to use ∩ because it will be shown that if t1, t2 are any terms built from degree variables a1, …, am with ′ and ∪ then t1 ∩ t2 exists for almost all a1, …, am. Thus the “almost all” theory presents a sharp contrast to the standard theory, where ∩ is not always defined (Kleene-Post [1]) and which is known to be undecidable (Lachlan [2]).
An algebraic difference between isols and cosimple isols
Authors: Ellentuck Erik
Published: May 2006

There is a fairly simple algebraic property that distinguishes isols from cosimple isols.
Modal propositional logic on an orthomodular basis. I
Authors: Herman L. , Piziak R.
Published: May 2006

A common method of obtaining the classical modal logics, for example the Feys system T, the Lewis systems, the Brouwerian system etc., is to build on a basis for the propositional calculus by adjoining a new symbol L, specifying new axioms involving L and the symbols in the basis for PC, and imposing one or more additional transformation rules. In the jargon of algebraic logic, which is the point of view we shall adopt, the “necessity” symbol L may be interpreted as an operator on the Boolean algebra of propositions of PC. For example, the Lewis system S4 may be regarded as a Boolean algebra ℒ together with an operator L on ℒ having the properties: (1)Lp ≤ p for all p in ℒ, (2)L1 = 1, (3) L(p → q) ≤ Lp → Lq for all p, q in ℒ, and (4) Lp = L(Lp) for all p in ℒ. Here, of course, → denotes the material implication connective: p→q = p′ ∨ q. It is easy to verify that property (3) may be replaced by either (3′) L(p ∧ q) = Lp ∧ Lq for all p, q in ℒ, or by (3″) L(p → q) ∧ Lp ≤ Lq for all p, q in ℒ. In particular, it follows from (1) through (4) above that L is a decreasing, idempotent and isotone operator on ℒ. Such mappings are often called interior operators.

In a previous paper [5], we considered the problem of introducing an implication connective into a quantum logic. This is greatly complicated by the fact that the quantal propositions band together to form an orthocomplemented lattice which is only “locally” distributive. Such lattices are called orthomodular. For definitions and further discussion, the reader is referred to that paper. In it, we argued that the Sasaki implication connective ⊃ defined by p ⊃ q = p′ ∨ (p ∧ q) is a natural generalization of material implication when the lattice of propositions is ortho-modular. Indeed, if unrestricted distributivity were permitted, p ⊃ q would reduce to the classical material implication p → q. For this reason, we choose ⊃ to play the role of material implication in an orthomodular lattice. Further properties of ⊃ are enumerated in Example 2.2(1) and Corollary 2.4 below.
Almost local non-α-recursiveness
Authors: Chong Chi T.
Published: May 2006

§1. Let α be an admissible ordinal which is also a limit of admissible ordinals (e.g. take any α such that α = α*, its projectum [5]). For any admissible γ ≦ α, let [γ) denote the initial segment of ordinals less than γ. A very general question that one might ask is the following: What conditions should one put on γ so that a certain statement true in Lα is ‘reflected’ to be true in Lγ? We cite some examples: (a) If β < γ < α, then Lα ⊨ “β cardinal” is ‘reflected’ to Lγ ⊨ “ β cardinal” (⊨ is just the satisfaction relation). (b) If β < γ < α and γ is a cardinal in Lα (called α-cardinal for short), then Lα ⊨ “β is not a cardinal” is ‘reflected’ to Lγ ⊨ “β is not a cardinal” This fact is used in Gödel's proof that V = L implies the Generalized Continuum Hypothesis. Our objective in this paper is to study a ‘reflection’ property of the following sort: Let A ⊆ [α) be an α-recursively enumerable (α-r.e.), non-α-recursive set. Under what conditions will A restricted to a smaller admissible ordinal γ be γ-r.e. and not γ-recursive?

The notations used here are standard. Those that are not explained are adopted from the paper of Sacks and Simpson [5], to which we also refer the reader for background material.
A simplification of combinatory logic
Authors: Goodman Nicolas D.
Published: May 2006

The usual formulations of combinatory logic, as in Church [1] or Curry and Feys [2], have no straightforward semantics. This lack complicates the proofs of basic metasystematic results, prevents the perspicuous formalization of combinatory logic as a deductive theory, and makes the combinators unnecessarily difficult to apply to recursion theory or to the foundations of mathematics. In the present paper we shall give a new formulation of combinatory logic, thought of as an abstract theory of rules. At each stage in the development we shall give a precise semantic interpretation for our axioms. We begin with an abstract treatment of the syntax and semantics of a theory of rules. We then specialize to the theory of the combinators and prove a completeness theorem connecting our axioms with our semantics. On this basis we treat functional abstraction, truth-functions, and the representation of partial recursive functions. In the spirit of Church [1, pp. 62–71], we conclude by extending our methods to the treatment of intensional identity.

The theories developed here are part of a simplification of the theory of constructions described in [3]. Their semantics are motivated by the intended interpretation of the theory of constructions. The present paper is selfcontained and can be read without any familiarity with the theory of constructions, although the motivation of several of the notions considered here is given in [3]. In a future publication we will use the results of the present paper as the basis for a detailed study of a simplified form of the theory in [3].
Some model theory of abelian groups
Authors: Eklof Paul C.
Published: May 2006

We study the relations between abelian groups B and C that every universal (resp. universal-existential) sentence true in B is also true in C, and give algebraic criteria for these relations to hold. As a consequence we characterize the inductive complete theories of abelian groups and prove that they are exactly the model-complete theories.
General models, descriptions, and choice in type theory
Authors: Andrews Peter B.
Published: May 2006

In [4] Alonzo Church introduced an elegant and expressive formulation of type theory with λ-conversion. In [8] Henkin introduced the concept of a general model for this system, such that a sentence A is a theorem if and only if it is true in all general models. The crucial clause in Henkin's definition of a general model ℳ is that for each assignment φ of values in ℳ to variables and for each wff A, there must be an appropriate value of A in ℳ. Hintikka points out in [10, p. 3] that this constitutes a rather strong requirement concerning the structure of a general model. Henkin draws attention to the problem of constructing nonstandard models for the theory of types in [9, p. 324].

We shall use a simple idea of combinatory logic to find a characterization of general models which does not directly refer to wffs, and which is easier to work with in certain contexts. This characterization can be applied, with appropriate minor and obvious modifications, to a variety of formulations of type theory with λ-conversion. We shall be concerned with a language ℒ with extensionality in which there is no description or selection operator, and in which (for convenience) the sole primitive logical constants are the equality symbols Qoαα for each type α.
General models and extensionality
Authors: Andrews Peter B.
Published: May 2006

It is well known that equality is definable in type theory. Thus, in the language of [2], the equality relation between elements of type α is definable as , i.e., xα = yα iff every set which contains xα also contains yα. However, in a nonstandard model of type theory, the sets may be so sparse that the wff above does not denote the true equality relation. We shall use this observation to construct a general model in the sense of [2] in which the Axiom of Extensionality is not valid. Thus Theorem 2 of [2] is technically incorrect. However, it is easy to remedy the situation by slightly modifying the definition of general model.

Our construction will show that the Axiom Schema of Extensionality is independent even if one takes as an axiom schema.

We shall assume familiarity with, and use the notation of, [2] and §§2–3 of [1].
The decision problem for formulas with a small number of atomic subformulas
Authors: Lewis Harry R. , Goldfarb Warren D.
Published: May 2006

In this paper we consider classes of quantificational formulas specified by restrictions on the number of atomic subformulas appearing in a formula. Little seems to be known about the decision problem for such classes, except that the class whose members contain at most two distinct atomic subformulas is decidable [2]. (We use “decidable” and “undecidable” throughout with respect to satisfiability rather than validity. All undecidable problems to which we refer are of maximal r.e. degree.) The principal result of this paper is the undecidability of the class of those formulas containing five atomic subformulas and with prefixes of the form ∀∃∀…∀. In fact, we show the undecidability of two sub-classes of this class: one (Theorem 1) consists of formulas whose matrices are in disjunctive normal form with two disjuncts; the other (Corollary 1) consists of formulas whose matrices are in conjunctive normal form with three conjuncts. (Theorem 1 sharpens Orevkov's result [8] that the class of formulas in disjunctive normal form with two disjuncts is undecidable.) A second corollary of Theorem 1 shows the undecidability of the class of formulas with prefixes of the form ∀…∀∃, containing six atomic subformulas, and in conjunctive normal form with three conjuncts. These restrictions to prefixes ∀∃∀…∀ and ∀…∀∃ are optimal. For by a result of the first author [5], any class of prenex formulas obtained by restricting both the number of atomic formulas and the number of universal quantifiers is reducible to a finite class of formulas, and so each such class is decidable; and the class of formulas with prefixes ∃…∃∀…∀ is, of course, decidable.
Metamathematical problems
Authors: Robinson Abraham
Published: May 2006

When a logician approaches the world of mathematics, he may have in mind one or more of several purposes. He may try to find in mathematics a framework for formalizing commonly accepted laws of thought or perhaps laws of thought that are not commonly accepted. He may want to assist the mathematician by providing him with firm foundations for his theories. But it may also be the case that the logician wishes to use his own characteristic tools—formalized languages, explicit relations between symbols and objects, rigidly expressed and controlled rules of deduction—in order to gain a better understanding of the various and variegated kinds of structures, methods, theories and theorems that are to be found in mathematics. We may then expect him to adopt the attitude of the physicist or psychologist who (whatever his professed philosophy) feels that he deals with phenomena of the external world, whose rules cannot be imposed by him arbitrarily. He, or those that come after him, may indeed use the understanding thus gained in order to modify these phenomena, but as a scientist he would not regard this possibility as his only justification.

For many years now, I have concentrated on the third of the lines of approach sketched above, and it seemed natural that I should discuss it again on the present occasion. However, today I do not wish to emphasize past developments but, using some of them as a background, I propose to enumerate a number of open problems. These problems seemed to me of some interest not only for their own sake but also because their solution might well require weapons whose introduction would close definite gaps in our armory.
Constructible lattices of c-degrees
Authors: Farrington C.P.
Published: May 2006

This paper is devoted to the proof of the following theorem.

Theorem. Let M be a countable standard transitive model of ZF + V = L, and let ℒ Є M be a wellfounded lattice in M, with top and bottom. Let ∣ℒ∣M = λ, and suppose κ ≥ λ is a regular cardinal in M. Then there is a generic extension N of M such that

(i) N and M have the same cardinals, and κN ⊂ M;

(ii) the c-degrees of sets of ordinals of N form a pattern isomorphic to ℒ;

(iii) if A ⊂ On and A Є N, there is B Є P(κ+)N such that L(A) = L(B).

The proof proceeds by forcing with Souslin trees, and relies heavily on techniques developed by Jech. In [5] he uses these techniques to construct simple Boolean algebras in L, and in [6] he uses them to construct a model of set theory whose c-degrees have orderlype 1 + ω*.

The proof also draws on ideas of Adamovicz. In [1]–[3] she obtains consistency results concerning the possible patterns of c-degrees of sets of ordinals using perfect set forcing and symmetric models. These methods have the advantage of yielding real degrees, but involve greater combinatorial complexity, in particular the use of ‘sequential representations’ of lattices.

The advantage of the approach using Souslin trees is twofold: first, we can make use of ready-made combinatorial principles which hold in L, and secondly, the notion of genericity over a Souslin tree is particularly simple.
Partial degrees and the density problem
Authors: Cooper S. B.
Published: May 2006

A notion of relative reducibility for partial functions, which coincides with Turing reducibility on the total functions, was first given by S.C. Kleene in Introduction to metamathematics [4]. Following Myhill [7], this was made more explicit in Hartley Rogers, Jr., Theory of recursive functions and effective computability [8, pp. 146, 279], where some basic properties of the partial degrees or (equivalent, but notationally more convenient) the enumeration degrees, were derived. The question of density of this proper extension of the degrees of unsolvability was left open, although Medvedev's result [6] that there are quasi-minimal partial degrees (that is, nonrecursive partial degrees with no nonrecursive total predecessors) is proved.

In 1971, Sasso [9] introduced a finer notion of partial degree, which also contained the Turing degrees as a proper substructure (intuitively, Sasso's notion of reducibility between partial functions differed from Rogers' in that computations terminated when the oracle was asked for an undefined value, whereas a Rogers computation could be thought of as proceeding simultaneously along a number of different branches of a ‘consistent’ computation tree—cf. Sasso [10]). His construction of minimal ‘partial degrees’ [11], while of interest in itself, left open the analogous problem for the more standard partial degree structure.
Jumping through the transfinite: the master code hierarchy of Turing degrees
Authors: Hodes Harold T.
Published: May 2006

Where a is a Turing degree and ξ is an ordinal < (ℵ1)L1, the result of performing ξ jumps on a, a(ξ), is defined set-theoretically, using Jensen's fine-structure results. This operation appears to be the natural extension through (ℵ1)L1 of the ordinary jump operations. We describe this operation in more degree-theoretic terms, examine how much of it could be defined in degree-theoretic terms and compare it to the single jump operation.
On P-points over a measurable cardinal
Authors: Kanamori A.
Published: May 2006

This paper continues the study of κ-ultrafilters over a measurable cardinal κ, following the sequence of papers Ketonen [2], Kanamori [1] and Menas [4]. Much of the concern will be with p-point κ-ultrafilters, which have become a focus of attention because they epitomize situations of further complexity beyond the better understood cases, normal and product κ-ultrafilters.

For any κ-ultrafilter D, let iD: V → MD ≃ Vκ/D be the elementary embedding of the universe into the transitization of the ultrapower by D. Situations of U < RKD will be exhibited when iU(κ) < iD(κ), and when iU(κ) = iD(κ). The main result will then be that if the latter case obtains, then there is an inner model with two measurable cardinals. (As will be pointed out, this formulation is due to Kunen, and improves on an earlier version of the author.) Incidentally, a similar conclusion will also follow from the assertion that there is an ascending Rudin-Keisler chain of κ-ultrafilters of length ω + 1. The interest in these results lies in the derivability of a substantial large cardinal assertion from plausible hypotheses on κ-ultrafilters.
Son of George and V = L
Authors: Fleissner William G.
Published: May 2006

This paper has three parts. In this first part, we formulate and prove from V = L a new combinatorial principle, ⋄++. In the second part, we discuss the topological problem which led to the formulation of ⋄++. Finally, we use ⋄++ to construct a space solving the topological problem.
Omitting types, type spectrums, and decidability
Authors: Millar Terrence
Published: May 2006

Notations, conventions, and definitions. {μi∣i < ω} will be an effective enumeration of all partial recursive μi{ω → 2. A type of a theory T will be a set of formulas in the language of T, in finitely many free variables, which is consistent with T. A complete type is a maximal type in some fixed number of free variables. A type is recursive if, relative to some effective enumeration of the formulas of the language, the characteristic function for the type is recursive. A set ψ of recursive types has property P if some set of indices of characteristic functions for all the types in ψ has property P. So, for example, we might say that a set of recursive types is . If is an L-structure, then the type spectrum of , denoted ‘TySp()’, is the set of complete types realized in (we will assume that an n-type has formulas with free variables among {x1, …, xn}). A type spectrum for a theory T is a type spectrum of some model of T. ‘TySp0(T)’ will denote the set of principal types of T.

We will assume that the reader is familiar with Henkin constructions of models, and of passing from a maximal consistent set of sentences, with “Henkin constants”, to a model. In particular, for a theory T in L we will let {ai∣i < ω} be new distinct constant symbols, and {φi < ω} a list of all sentences in the expanded language. ‘ΔN’ will denote the elementary diagram constructed at stage N, and .
Two-dimensional partial orderings: Recursive model theory
Authors: Manaster Alfred B. , Rosenstein Joseph G.
Published: May 2006

In this paper and the companion paper [9] we describe a number of contrasts between the theory of linear orderings and the theory of two-dimensional partial orderings.

The notion of dimensionality for partial orderings was introduced by Dushnik and Miller [3], who defined a partial ordering 〈A, R〉 to be n-dimensional if there are n linear orderings of A, 〈A, L1〉, 〈A, L2〉 …, 〈A, Ln〉 such that R = L1 ∩ L2 ∩ … ∩ Ln. Thus, for example, if Q is the linear ordering of the rationals, then the (rational) plane Q × Q with the product ordering (〈x1, y1〉 ≤Q×Q 〈x2, y2, if and only if x1 ≤ x2 and y1 ≤ y2) is 2-dimensional, since ≤Q×Q is the intersection of the two lexicographic orderings of Q × Q. In fact, as shown by Dushnik and Miller, a countable partial ordering is n-dimensional if and only if it can be embedded as a subordering of Qn.

Two-dimensional partial orderings have attracted the attention of a number of combinatorialists in recent years. A basis result recently obtained, independently, by Kelly [7] and Trotter and Moore [10], describes explicitly a collection of finite partial orderings such that a partial ordering is a 2dpo if and only if it contains no element of as a subordering.
Recursively enumerable complexity sequences and measure independence
Authors: Bennison Victor L.
Published: May 2006

Though researchers in the field of abstract computational complexity theory have utilized many of the tools of recursive function theory in the development of their field, the early results obtained (e.g., see [8]) seemed to be rather independent of results in recursion theory (at least to the extent that the results were not uniformly interesting to both varieties of theorists). It seems to have been generally accepted, however, that strong parallels of one form or another must exist between the two fields. Indeed, recent results of Blum and Marques [7], Morris [13], Soare [15] and Bennison [1], [3] have revealed a striking correspondence between complexity theoretic properties and recursion theoretic properties. These results are not contrived, but rather link together interesting properties which had arisen naturally and independently in their respective fields. This paper presents the results of research aimed at finding a recursion theoretic characterization for a complexity theoretic property which had arisen from the study of the speed-up phenomenon.

In abstract computational complexity theory we are concerned with categorizing computable functions or sets according to their relative difficulty of computation. The phrase “difficult to compute” may take on different meanings depending on which criteria (complexity theoretic properties) we use to define what it means for a function or set to be hard to compute. In the abstract setting, however, such criteria should yield the same classes of functions or sets regardless of the underlying abstract complexity measure (in the sense of Blum [4], e.g., tape, time, etc.). In other words, such criteria should be measure-independent. In this paper we will be considering one way of defining “difficult to compute”. Namely, we shall say that a function or set is difficult to compute if it does not have a recursively enumerable complexity sequence as defined by Meyer and Fischer [12]. For a property to have a recursion theoretic characterization it must be measure-independent, for a recursion theoretic property is, by its very nature, measure-independent. It will not be immediately obvious whether or not the property of having an r.e. complexity sequence is measure-independent. We attack this question by first considering an alternative definition of an r.e. complexity sequence, one which is easily seen to be measure-independent.
Constructing pure injective hulls
Authors: Hodges Wilfrid
Published: May 2006

Let A be an abelian group and B a pure injective pure extension of A. Then there is a homomorphic image C of B over A which is a pure injective hull of A; C can be constructed by using Zorn's lemma to find a suitable congruence on B. In a paper [4] which greatly generalises this and related facts about pure injectives, Walter Taylor asks (Problem 1.5) whether one can find a “construction” of C which is more concrete than the one mentioned above; he asks also whether the points of C can be explicitly described. In this note I return the answer No.
Cardinalities of ultraproducts of finite sets
Authors: Koppelberg Sabine
Published: May 2006

Keisler, in [1], defined a set F(D) of infinite cardinals for every ultrafilter D on a set I, and, assuming GCH, gave a sufficient condition for a set C of infinite cardinals to have the form F(D) for suitable D and I. In this paper we prove a similar theorem (Theorem 1) under considerably weaker assumptions. Our main tool is a construction of elementary end extensions of Boolean ultrapowers of ω outlined by Shelah in [6, Exercise VI.3.35]. Hence this paper will mostly be concerned with Boolean ultrapowers of ω.
On the interpretation of combinators with weak reduction
Authors: Shabunin L.V.
Published: May 2006

In this paper some partial models for combinators with weak reduction are proposed. The underlying ideas are due to Church [1]. The results are extensions of the previous results of the author proved in [8].
Mapping a set of reals onto the reals
Authors: Miller Arnold W.
Published: May 2006

In this paper we show that it is consistent with ZFC that for any set of reals of cardinality the continuum, there is a continuous map from that set onto the closed unit interval. In fact, this holds in the iterated perfect set model. We also show that in this model every set of reals which is always of first category has cardinality less than or equal to ω1.
Additive structure in uncountable models for a fixed completion of P
Authors: Knight Julia F.
Published: May 2006

In [6], Nadel showed that if is a recursively saturated model of Pr = Th(ω, +) of power at most ℵ1, then there is a model such that ≡ ∞ω and can be expanded to a recursively saturated model of P. For a fixed completion T of P, can be chosen to have a recursively saturated expansion to a model of T just in case is recursive in T-saturated. (“Recursive in T-saturation” is defined just like recursive saturation except that the sets of formulas considered are those that are recursive in T.)

Nadel also showed in [6] that for a fixed completion T of P, a countable nonstandard model of Pr can be expanded to a model of T (not necessarily recursively saturated) iff satisfies a condition called “exp(T)-saturation.” This condition is stronger than recursive saturation but weaker than recursive in T-saturation. Nadel left open the problem of characterizing the models of Pr of power ℵ1 such that for some , ≣ ∞ω and can be expanded to a model of T. The present paper gives such a characterization. The condition on is that it is recursively saturated, and for each n ∈ ω, the set Tn of Πn-sentences of T is recursive in some type realized in .

This result can be interpreted in various ways, just as the results from [6] were interpreted in various ways in [4]. Friedman [2] introduced the notion of a “standard system.”