bluuebunny/crossref_metadata_2025 huggingface dataset:
A system of formal logic without an analogue to the curry W operator
Authors: Fitch Frederic Brenton
Published: May 2006

The system of formal logic to be presented in this paper has the following main properties:

(1). The Mengenlehre paradoxes do not arise in it.

(2). It seems to be free from other contradictions.

(3). It does not resort to a theory of types.

(4). It uses negation and material implication and does not weaken the principle of excluded middle.

(5). It contains no analogue to the Curry W operator; consequently, given a propositional function ϕ, a propositional function Ψ cannot always be found such that, for all x, ϕ(x, x) and Ψ(x) are equivalent propositions.

(6). It employs a universal quantifier, G, such that (x)f(x), (x)f(x, x), (x)f(x, x, x), …, would be respectively expressed thus, G(f, f), G(f, f, f), G(f, f, f, f), ….

(7). It employs Schönfinkel's functional notation, so that f(x1, x2, …, xn) will be written as (( … ((fx1)x2) …)xn) and abbreviated to (fx1x2… xn) and, when no ambiguity results, to fx1x2…xn.

(8). A theory of integers and real numbers cannot, apparently, be deduced from it.

(9). A form of the axiom of choice is provable in it.
Note on a system of myhill
Authors: Shepherdson J.C.
Published: May 2006

In [1] Myhill gave a system K in which much of the classical theory of rational and real numbers could be carried out but which was nevertheless complete; this was achieved by sacrificing the notions of negation and universal quantification and introducing instead the ancestral as a primitive idea. He mentioned two ways of dealing with real numbers in K; the first was to use the half-section corresponding to x, i.e. the class of rationals r satisfying r ≤, x; the second was to use the whole-section corresponding to x, i.e. the relation between rationals r, s which holds when r ≤ x and x ≤ s. In [2] he proved various theorems about the relation between these two forms of definition. In particular he proved that every bounded class of half-sections definable in K has a least bound definable in K. In a footnote he said, ‘This theorem risks triviality because it is doubtful whether there exists such a bounded class.’ We show in this note that this is the case; in fact there are not even any definable classes consisting entirely of classes of rationals. It is not difficult to see how this happens; since K has no negation, any statement matrix A (α) defining a class of classes of sequences is satisfied by α = V, where V is the class of all sequences. Thus there are no classes which consist entirely of half-sections. The same is true for whole-sections, showing that Conjecture I of [1], viz. ‘Not every bounded class of whole-sections definable in K has a least bound definable in K’, is trivially false. Since it may be of some intrinsic interest, we give below a more complete description of the classes of classes of sequences which are definable in K (or rather in K1 see below) than is necessary merely in order to prove the above assertion.
Einkleidung der Mathematik in Schröderschen Relativkalkul
Authors: Löwenheim Leopold
Published: May 2006

Bei dem Bestreben, die Mathematik zu logisieren, erschienen die von Russell u.a. entdeckten Paradoxieen als das größte Hindernis. Zu ihrer Überwindung wurde die Typentheorie von Russell aufgestellt, die aber auch in ihrer gemilderten Form die Mathematiker nicht befriedigt. Ich bin diesen Schwierigkeiten nie begegnet, und zwar deshalb nicht, weil logisieren für mich immer bedeutet hat: in Schröderschen Relativkalkul einkleiden.

Ich bedaure es aus mehr als einem Grunde schwer, daß man von dem eleganten Peirce-Schröderschen Kalkul abgewichen ist und die Peano-Russellschen Zeichen benutzt, in denen aus bestimmten (m.A.n. nicht stichhaltigen) Gründen die sonst selbstverständliche Harmonie und Schönheit der Mathematik preisgegeben wurde, wodurch die Forschung ziemlich einseitig in eine bestimmte Richtung gedrängt wurde (in der freilich Hochbedeutendes geleistet wurde) während beim Peirce-Schröderschen Kalkul auf Schönheit besonderer Wert gelegt und mit wunderbarer Instinktsicherheit gerade das mathematisch Bedeutsame und Fruchtbare getroffen wurde. Ich bin der Überzeugung, daß in Wissenschaft und Technik das Zweckmäßige immer auch zugleich das Schöne ist. Mit Russells Zeichen hätte ich manches nicht entdeckt, was ich gefunden habe, und besäße jedenfalls nicht meine grosse Kalkulfreudigkeit. Ungünstige Zeichen lähmen die Produktivität. Der heutige Logikkalkul entbehrt daher jeder Eleganz und Geschmeidigkeit, was ganz und gar nicht in der Natur der Sache liegt. Meine Bemühungen, bestimmte Teile des Kalkuls flüssiger, geschmeidiger zu handhaben, sind unbeachtet geblieben.
An axiomatic system for the first order language with an equi-cardinality quantifier
Authors: Yasuhara Mitsuru
Published: May 2006

The equi-cardinality quantifier1 to be used in this article, written as Qx, is characterised by the following semantical rule: A formula QxA(x) is true in a relational system exactly when the cardinality of the set consisting of these elements which make A(x) true is the same as that of the universe. For instance, QxN(x) is true in 〈Rt, N〉 but false in 〈Rl, N〉 where Rt, Rl, and N are the sets of rational numbers, real numbers, and natural numbers, respectively. We notice that in finite domains the equi-cardinality quantifier is the same as the universal quantifier. For this reason, all relational systems considered in the following are assumed infinite.
An application of nonstandard analysis to game theory
Authors: Wesley Eugene
Published: May 2006

In this article an application of extended fields of real numbers to the proof of theorems in the theory of cooperative games will be presented. The proofs set forth below involve the use of A. Robinson's theory of nonstandard analysis and are metamathematical in character. Alternative proofs utilizing ordinary topological methods can in fact be carried out quite briefly. However, attempts to apply nonstandard analysis to game theory are relatively novel. For this reason these results may be of interest not only insofar as they present new information on the theory of the kernel of a cooperative game, but also in that they serve to demonstrate the possibility of effectively exploiting nonstandard analysis as a tool for future investigation in this area. It may well turn out that nonstandard analysis could serve as the most natural vehicle through which concepts defined for games with a finite number of players might be extended to games with a continuum of players.
Existence and feasibility in arithmetic
Authors: Parikh Rohit
Published: May 2006

“From two integers k, l one passes immediately to kl; this process leads in a few steps to numbers which are far larger than any occurring in experience, e.g., 67(257729).

Intuitionism, like ordinary mathematics, claims that this number can be represented by an arabic numeral. Could not one press further the criticism which intuitionism makes of existential assertions and raise the question: What does it mean to claim the existence of an arabic numeral for the foregoing number, since in practice we are not in a position to obtain it?
On the strong semantical completeness of the intuitionistic predicate calculus
Authors: Thomason Richmond H.
Published: May 2006

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.
Functional completeness in one variable
Authors: Rosenberg James
Published: May 2006

It is extremely difficult to make general statements about functional completeness. (For the main reference on the subject see Post [2].) In this paper we restrict ourselves to the case of unary functions in a finite valued logic, and prove a result concerning minimal functionally complete sets, along with a necessary and sufficient condition for completeness. A basic familiarity with group theory would be helpful.
The substitution method
Authors: Tait W. W.
Published: May 2006

This paper deals with Hilbert's substitution method for eliminating bound variables from first order proofs. With a first order system S framed in the ε-calculus [2] the problem is to associate a system S' without bound variables and an effective procedure for transforming derivations in S into derivations in S′. The transform of a formula A derived in S is to be an “ε-substitution instance” of A, i.e. it is obtained by replacing terms εxB(x) in A by terms of S′. In general the choice of these terms will depend on the particular derivation of A, and not on A alone. Cf. [4]. The present formulation sharpens Hilbert's original statement of the problem, i.e. that the transform of A should be finitistically verifiable, by making explicit the methods of verification used, namely those formalized in S′; on the other hand, it generalizes Hilbert's formulation since S′ need not be restricted to finitist systems.

The bound variable elimination procedure can always be taken to be primitive recursive in (the Gödel number of) the derivation of A. Constructions which transcend primitive recursion can simply be built into S′.

In this paper we show that if S′ is taken to be a second order system with constants for functionals, then the existence of suitable ε-substitution instances can be expressed by the solvability of certain functional equations in S′. We deal with two cases here. If S is number theory without induction, i.e. essentially predicate calculus with identity, then we can solve the equations in question by taking for S′ the free variable part S* of S with an added rule of definition of functionals by cases (recursive definition on finite ordinals), which is a conservative extension of S*.
Infinitary analogs of theorems from first order model theory
Authors: Malitz Jerome
Published: May 2006

The material presented here belongs to the model theory of the Lκ, λ languages. Our results are either infinitary analogs of important theorems in finitary model theory, or else show that such analogs do not exist.

For example, it is well known that whenever i, and , have the same true Lω, ω sentences (i.e., are elementarily equivalent) for i = 1, 2, then the cardinal sums 1 + 2 and + have the same true Lω, ω sentences, and the direct products 1 · 2 and · have the same true Lω, ω sentences [3]. We show that this is true when ‘Lω, ω’ is replaced by ‘Lκ, λ’ if and only if κ is strongly inaccessible. For Lω1, ω this settles a question, posed by Lopez-Escobar [7].

In §3 we give a complete description of the expressive power of those sentences of Lκ, λ in which the identity symbol is the only relation symbol which occurs. This extends a result by Hanf [4].
A survey of proof theory
Authors: Kreisel G.
Published: May 2006

One might fairly say that the very meaning of our subject has changed since Hilbert introduced it under the name Beweistheorie (it was meant to be the principal tool for formulating Hubert's general conception of how to analyze mathematical reasoning). Specifically, the roles of the two principal elements of proof theory, namely the intuitive proofs accepted and the formal proofs (or derivations) studied, have turned out to be quite different from what Hilbert thought. In his view the hard work had been done in the discovery of formalization, and what remained was the study of certain given formal systems.
A note on Quine's treatment of transfinite recursion
Authors: Parsons Charles
Published: May 2006

In this note we point out a limitation of the treatment of transfinite recursion in Quine's Set Theory and its Logic2 and develop a method for overcoming it. We shall also mention and indicate how to overcome a second more trivial limitation. We assume familiarity with Set Theory and its Logic and use its notation and terminology. Numbered references are to Quine's numbered formulae. In our work we continue the numbering of § 26.

The first difficulty is that the theorems which show that his device for defining functions by transfinite recursion (§ 25) accomplishes its purpose do not apply to functions defined by recursion over all the ordinals. Let γ be the function which gives the value of the function we want for an ordinal y from the sequence of its values for ordinals less than y.
A supplement to Herbrand
Authors: Dreben Burton , Denton John
Published: May 2006

In [5] it was shown that to complete Herbrand's argument for his Fundamental Theorem (see [6]) a weak analyzing function for certain applications of the rules of passage is needed. The following theorem describes such a function. (We use the terminology and notation of [5] except that, for each schema S and each p ≧ 1, we shall write D(S,p) rather than DSp for the domain of order p generated by S. In addition, we shall say that an element of D(S, p) is of order k, 1 ≦ k ≦ p, if it belongs to D(S, k) but not to D(S,k—1).)
Connexive implication
Authors: Mccall Storrs
Published: May 2006

This paper contains a rigorous treatment of the species of implication described in [8] and [9], where it was given the name of connexive implication. A brief historical survey will lay bare its roots in antiquity, and it will be shown that none of the well-known systems of propositional logic serves to formalize it.1 In this paper a new system of ‘connexive’ logic will be presented, the system being shown to be (a) consistent, (b) independent of two-valued logic, (c) Post-complete.
Modus ponens under hypotheses
Authors: Bausch A. F.
Published: May 2006

The Stoic “indemonstrables” were inference rules; a rule about rules was the synthetic theorem: if from certain premisses a conclusion follows and from that conclusion and certain further premisses a second conclusion follows, then the second conclusion follows from all the premisses together. Similar things occur as medieval “rules of consequence”, although not usually on a metametalevel; and (with the same proviso) the following might be deemed a contemporary avatar of that Stoic theorem.

If every formula which occurs once or more often in the list A1, A2, …, An, B1, B2, …, Bm occurs also at least once in the list C1, C2, …, Cr then:

This rule [Church: Introduction to Mathematical Logic, 1956, pp. 94, 165], which may be called the rule of modus ponens under hypotheses (MPH), is worthy of attention for the following reasons:

A. MPH and the axioms A ⊃ A yield precisely the positive implicative calculus (and very easily, too).

B. MPH and the axioms A ⊃ f ⊃ f ⊃ A yield a new formulation of the full classical propositional calculus (in terms of f and ⊃).

C. MPH and the axioms ∼A ⊃ A ⊃ A and A ⊃. ∼A ⊃ B yield the classical calculus in terms of ∼ and ⊃.
Extensional interpretations of modal logics
Authors: Löb M. H.
Published: May 2006

By ΡL we shall mean the first order predicate logic based on S4. More explicitly: Let Ρ0 stand for the first order predicate calculus. The formalisation of Ρ0 used in the present paper will be given later. ΡL is obtained from Ρ0 by adding the rules the propositional constant □ and
An introduction to hyperarithmetical functions
Authors: Robinson Julia
Published: May 2006

By functional equation we mean an equation of the form

(1) A1 … Aκ = B1 … B1.

Here the A's and B's are functions of one variable from and to the natural numbers and FG is the function obtained from F and G by composition, i.e. FG(x) = F(G(x)) for all natural numbers x. We wish to investigate finite systems of functional equations. Now if all the A's and B's of (1) are equal to the identity function I (or all equal to the zero function O), then the equation (1) is satisfied trivially. Thus, in order to make the problem of solvability of systems of equations interesting, we must have some function given which will be held fixed throughout. We take the successor function S to be this given function.
All or none; A novel choice of primitives for elementary logic
Authors: Thomason R. H. , Leblanc H.
Published: May 2006

In [1] Ludwik Borkowski takes a quantifier symbol ‘Q1’ (e.g., the familiar ‘∀’) to permit definition of another quantifier symbol ‘Q1’ if, where ‘f’ is a singulary predicate variable, there exists a formula A of QC1—a first-order quantificational calculus (without identity and individual constants) having ‘Q1’ as its one primitive quantifier symbol—such that: (1) under the intended interpretations of ‘Q1’ and ‘Q1’ the biconditional (Q1X)f(X) = A is valid, (2) no individual variable occurs free in A, and (3) A contains no propositional variable, and no predicate variable other than ‘f.’
Basic modal logic
Authors: Pollock John L.
Published: May 2006

As anyone who is familiar with the literature knows, there is a great deal of controversy concerning which, if any, of the extant theories of propositional modal logic correctly formalizes the logic of certain logical concepts such as analyticity and logical necessity. Most of the controversy concerns certain principles that involve iterated modalities (where one modal operator occurs within the scope of another). For example, there is considerable disagreement about whether the principle(□p⊃□□p)should be considered valid. However, when philosophers and logiciansapplymodal logic to concrete problems, they rarely need principles which involve iterated modalities. For most practical purposes, principles involving only one layer of modalities are all that are needed. This suggests that if we try to construct a theory of modal logic in which there are no iterated modalities, we can avoid most of the controversy and still have a theory that is strong enough for all of the normal uses to which modal logic is put.
Abstract Computability and Invariant Definability
Authors: Moschovakis Yiannis N.
Published: May 2006

By language we understand a lower predicate calculus with identity and (perhaps) relation and function symbols. It is convenient to allow for more than one sort of variable. Now each individual constant (if there are any) is of a specified sort, the formal expressions R(t1, … tn), f(t1,…, tn) are well formed only if the terms t1, …, tn are of specified sorts determined by the relation symbol R and the function symbol f, and the term f(t1, …, tn) (if well formed) is of a sort determined by f. We admit s = t as well formed, no matter what the sorts of s and t.
On the simplicity of ideas
Authors: Goodman Nelson
Published: May 2006

The motives for seeking economy in the basis of a system are much the same as the motives for constructing the system itself. A given idea A need be left as primitive in a system only so long as we have discovered between A and the other primitives no relationship intimate enough to permit defining A in terms of them; hence the more the set of primitives can be reduced without becoming inadequate, the more comprehensively will the system exhibit the network of interrelationships that comprise its subject-matter. Of course we are often concerned less with an explicit effort to reduce our basis than with particular problems as to how to define certain ideas from others. But such special problems of derivation, such problems of rendering certain ideas eliminable in favor of others, are merely instances of the general problem of economy. Thus it is quite wrong to think of the search for economy as a sort of game, inspired by an abnormal love of superficial neatness. Some economies may be relatively unimportant, but the inevitable result of regarding all economy as trivial would be a willingness to accept all ideas as primitive at the outset, making a system both unnecessary and impossible.
An extension of the Craig-Lyndon interpolation theorem
Authors: Henkin Leon
Published: May 2006

In a work widely quoted and applied,3 Craig has shown that if A and C are any formulas of predicate logic such that A├C, then there is a formula B such that (i) A├B and B├C, and (ii) each predicate symbol occurring in B occurs both in A and in C.4 If, in this theorem, we replace the syntactic notion of derivability, ├, by the semantical notion of consequence, ╞, the resulting proposition is of course equally valid, for by the (strong) completeness theorem of predicate logic5 the relations ├ and ╞ coincide in extension.
The number of countable models
Authors: Morley Michael
Published: May 2006

A theory formulated in a countable predicate calculus can have at most nonisomorphic countable models. It has been conjected (e.g., in [4]) that if it has an uncountable number of such models then it has exactly such. Of course, this would follow immediately if one assumed the continuum hypothesis.

In this paper we show that if a theory has more than ℵ1 (i.e., at least ℵ2) isomorphism types of countable models then it has exactly . Our results generalize immediately to theories in Lω1ω and even to pseudo-axiomatic classes in Lω1ω. In this last case, a result of H. Friedman shows that it is the best possible result.
A theorem on initial segments of degrees
Authors: Thomason S. K.
Published: May 2006

A set S of degrees is said to be an initial segment if c ≤ d ∈ S→-c∈S. Shoenfield has shown that if P is the lattice of all subsets of a finite set then there is an initial segment of degrees isomorphic to P. Rosenstein [2] (independently) proved the same to hold of the lattice of all finite subsets of a countable set. We shall show that “countable set” may be replaced by “set of cardinality at most that of the continuum.” This result is also an extension of [3, Corollary 2 to Theorem 15], which states that there is a sublattice of degrees isomorphic to the lattice of all finite subsets of 2N. (A sublattice of degrees is a subset closed under ∪ and ∩; an initial segment closed under ∪ is necessarily a sublattice, but not conversely.)

It seems worth noting that the proof of the present result was preceded in time by our proof [4] of the analogous theorem for hyperdegrees, and is in fact an adaptation of that proof. Thus the present work has been influenced much more directly by the Gandy-Sacks forcing construction of a minimal hyperdegree [1] than by previous work on initial segments of degrees.
Every analytic set is Ramsey
Authors: Silver Jack
Published: May 2006

If X is a set, [Χ]ω will denote the set of countably infinite subsets of X. ω is the set of natural numbers. If S is a subset of [ω]ω, we shall say that S is Ramsey if there is some infinite subset X of ω such that either [Χ]ω ⊆ S or [Χ]ω ∩ S = 0. Dana Scott (unpublished) has asked which sets, in terms of logical complexity, are Ramsey.

The principal theorem of this paper is: Every Σ11 (i.e., analytic) subset of [ω]ω is Ramsey (for the Σ, Π notations, see Addison [1]). This improves a result of Galvin-Prikry [2] to the effect that every Borel set is Ramsey. Our theorem is essentially optimal because, if the axiom of constructibility is true, then Gödel's Σ21 Π21 well-ordering of the set of reals [3], having the convenient property that the set of ω-sequences of reals enumerating initial segments is also Σ21 ∩ Π21, rather directly gives a Σ21 ∩ Π21 set which is not Ramsey. On the other hand, from the assumption that there is a measurable cardinal we shall derive the conclusion that every Σ21 (i.e., PCA) is Ramsey. Also, we shall explore the connection between Martin's axiom and the Ramsey property.
Tense logic for discrete future time
Authors: Schindler Patrick
Published: May 2006

Prior has conjectured that the tense-logical system Gli obtained by adding to a complete basis for the classical propositional calculus the primitive symbol G, the definitions

Df. F: Fα = NGNα

Df. L: Lα = KαGα,

and the postulates

is complete for the logic of linear, infinite, transitive, discrete future time. In this paper it is demonstrated that that conjecture is correct and it is shown that Gli has the finite model property: see [4]. The techniques used are in part suggested by those used in Bull [2] and [3]:

Gli can be shown to be complete for the logic of linear, infinite, transitive, discrete future time in the sense that every formula of Gli which is true of such time can be proved as a theorem of Gli. For this purpose the notion of truth needs to be formalized. This formalization is effected by the construction of a model for linear, infinite, transitive, discrete future time.
Persistence and Herbrand expansions
Authors: Wholey Joseph S.
Published: May 2006

Following Robinson [3], we say that a first-order sentence S is persistent with respect to a set of sentences K if, whenever S is true in a model M of K, then S is true in every extension of M that is also a model of K. Robinson proved in [3] that:

(T) In order that the sentence S be persistent with respect to the set K it is necessary and sufficient that there be some existential sentence Y such that the sentence S↔Y is deducible from K.
Topological Logic
Authors: Rescher Nicholas , Garson James
Published: May 2006

The purpose of this paper is to present a very versatile family of logical systems ofpositionalortopologicallogic. These systems—obtained by generalizing the existing systems of chronological logic—are to have a very general nature, capable of reflecting the characteristics of a wide range of logical systems, including not only chronological (alsotemporalortense) logic, but also what we may call locative or place logic, and even a logic of “possible worlds”.
An embedding of classical logic in S4
Authors: Fitting Melvin
Published: May 2006

There are well-known embeddings of intuitionistic logic into S4 and of classical logic into S5. In this paper we give a related embedding of (first order) classical logic directly into (first order) S4, with or without the Barcan formula. If one reads the necessity operator of S4 as ‘provable’, the translation may be roughly stated as: truth may be replaced by provable consistency. A proper statement will be found below. The proof is based ultimately on the notion of complete sequences used in Cohen's technique of forcing [1], and is given in terms of Kripke's model theory [3], [4].
ω-homomorphisms and ω-groups
Authors: Applebaum C. H.
Published: May 2006

Let ε stand for the set of nonnegative integers (numbers), V for the class of all subcollections of ε (sets), Λ for the set of isols, and for the set of mappings from a subset of ε into ε (functions). I f is a function we write δf and ρf for its domain and range respectively. The relation of inclusion is denoted by ⊂ and that of proper inclusion by ⊊. The sets α and β are recursively equivalent [written: α ≃ β], if δf = α and ρf = β for some function f with a one-to-one partial recursive extension f. We denote the recursive equivalence type of α, {σ ∈ V ∣ ≃ α}, by Req(α). Also R stands for Req(ε), while ΛR denotes the collection of all regressive isols. The reader is assumed to be familiar with the contents of [1] and [6].
On the undecidability of finite planar graphs
Authors: Garfunkel Solomon , Shank Herbert
Published: May 2006

In this paper we demonstrate the hereditary undecidability of finite planar graphs. In §2 we introduce the preliminary logical notions used and outline the Rabin–Scott method of semantic embedding. This method is illustrated in §3 by proving the undecidability of the theory of two finite equivalence relations of a special type. In §4 we give a proof of the main theorem by embedding these equivalence relations into finite planar graphs.

The basic idea is first to form a graph which codes a pair of these relations and then to take a representative of it and “squish” it to the plane. This “squishing” requires the introduction of crossings; and edges of the original graph become paths in the new one. To distinguish the original edges we place two different types of “diamonds” about crossing points. We can then uncode our new graphs to recover the equivalence relations by means of simple first-order incidence properties.
On many-one degrees
Authors: Liu Shih-Chao
Published: May 2006

Two questions were left open in [1]. 1) Do W(σ) and W(r) have the same many-one degree for any σ, τ such that ωη+1.2 ≤ σ < τ < ωη+2? 2) Is W(σ) many-one reducible to W(r) for any σ, τ such that ωη+1.2 ≤ σ < τ < ωη+2? We answered the second question affirmatively in [2]. In this paper we answer the first question in the negative. From the results of [1] [2] and this paper we have a complete picture of the many-one degrees of the predicates e ∈ W(σ)
Some theorems on extensions of arithmetic1
Authors: Di Paola Robert A.
Published: May 2006

In this paper we study some of the consequences of adding as new axioms to consistent re (recursively enumerable) extensions T of Peano arithmetic P sentences undecidable in T of the Π10 variety, as are those one naturally comes upon. The question arises: how much can two extensions “differ” when each is obtained by adding just once distinct Π10 sentences undecidable in T? We shall show that if T is as stated above, we can find extensions T1 and T2, constructed very simply from T, having the property that if (A, B) is any pair of re sets with recursive intersection, there can be found a Π10 formula of P which represents A in T1 and B in T2.
Maximal vector spaces under automorphisms of the lattice of recursively enumerable vector spaces
Authors: Kalantari Iraj , Retzlaff Allen
Published: May 2006

The area of interest of this paper is recursively enumerable vector spaces; its origins lie in the works of Rabin [16], Dekker [4], [5], Crossley and Nerode [3], and Metakides and Nerode [14]. We concern ourselves here with questions about maximal vector spaces, a notion introduced by Metakides and Nerode in [14]. The domain of discourse is V∞ a fully effective, countably infinite dimensional vector space over a recursive infinite field F.

By fully effective we mean that V∞, under a fixed Gödel numbering, has the following properties:

(i) The operations of vector addition and scalar multiplication on V∞ are represented by recursive functions.

(ii) There is a uniform effective procedure which, given n vectors, determines whether or not they are linearly dependent (the procedure is called a dependence algorithm).

We denote the Gödel number of x by ⌈x⌉ By taking {εn ∣ n > 0} to be a fixed recursive basis for V∞, we may effectively represent elements of V∞ in terms of this basis. Each element of V∞ may be identified uniquely by a finitely-nonzero sequence from F Under this identification, εn corresponds to the sequence whose n th entry is 1 and all other entries are 0. A recursively enumerable (r.e.) space is a subspace of V∞ which is an r.e. set of integers, ℒ(V∞) denotes the lattice of all r.e. spaces under the operations of intersection and weak sum. For V, W ∈ ℒ(V∞), let V mod W denote the quotient space. Metakides and Nerode define an r.e. space M to be maximal if V∞ mod M is infinite dimensional and for all V ∈ ℒ(V∞), if V ⊇ M then either V mod M or V∞ mod V is finite dimensional. That is, M has a very simple lattice of r.e. superspaces.
ℵ0-categorical modules
Authors: Baur Walter
Published: May 2006

It is shown that the first-order theory ThR(A) of a countable module over an arbitrary countable ring R is ℵ0-categorical if and only if Ai finite, n ∈ ω, κi ≤ ω. Furthermore, ThR(A) is ℵ0-categorical for all R-modules A if and only if R is finite and there exist only finitely many isomorphism classes of indecomposable R-modules.
Prefix classes of Krom formulas
Authors: Aanderaa Stål O. , Lewis Harry R.
Published: May 2006

In this paper we consider decision problems for subclasses of Kr, the class of those formulas of pure quantification theory whose matrices are conjunctions of binary disjunctions of signed atomic formulas. If each of Q1, …, Qn is an ∀ or an ∃, then let Q1 … Qn be the class of those closed prenex formulas with prefixes of the form (Q1x1)… (Qnxn). Our results may then be stated as follows:

Theorem 1. The decision problem for satisfiability is solvable for the class ∀∃∀ ∩ Kr.

Theorem 2. The classes ∀∃∀∀ ∩ Kr and ∀∀∃∀ ∩ Kr are reduction classes for satisfiability.

Maslov [11] showed that the class ∃…∃∀…∀∃…∃ ∩ Kr is solvable, while the first author [1, Corollary 4] showed ∃∀∃∀ ∩ Kr and ∀∃∃∀ ∩ Kr to be reduction classes. Thus the only prefix subclass of Kr for which the decision problem remains open is ∀∃∀∃…∃∩ Kr.

The class ∀∃∀ ∩ Kr, though solvable, contains formulas whose only models are infinite (e.g., (∀x)(∃u)(∀y)[(Pxy ∨ Pyx) ∧ (¬ Pxy ∨ ¬Pyu)], which can be satisfied over the integers by taking P to be ≥). This is not the case for Maslov's class ∃…∃∀…∀∃…∃ ∩ Kr, which contains no formula whose only models are infinite ([2] [5]).

Theorem 1 was announced in [1, Theorem 4], but the proof sketched there is defective: Lemma 4 (p. 17) is incorrectly stated. Theorem 2 was announced in [9].
On the complexity of the theories of weak direct powers
Authors: Rackoff Charles
Published: May 2006

Mostowski [11] shows that if a structure has a decidable theory, then its weak direct power has one as well; his proof however never produces decision procedures which are elementary recursive.

Some very general results are obtained here about the nature of the weak direct power of a structure, which in most cases lead to elementary recursive decision procedures for weak direct powers of structures which themselves have elementary recursive procedures.

In particular, it is shown that 〈N*, +〉, the weak direct power of 〈N, +〉, can be decided in space

for some constant c. As corollaries, the same upper bound is obtained for the theory of the structure 〈N+, ·〉 of positive integers under multiplication, and for the theory of finite abelian groups. Fischer and Rabin [7] have shown that the theory of 〈N,* +〉 requires time

even on nondeterministic Turing machines.
Hanf numbers for omitting types over particular theories
Authors: Knight Julia F.
Published: May 2006

The main result of this paper is the fact that for T a complete extension of either P or ZF + V = L, with no new symbols, there is a type which is omitted in a model of T of power ℵ1 but which is realized in all models of higher power. Therefore, the “Hanf number” for omitting types over T is greater than ℵ2.

The present section contains some basic definitions and a discussion of related results. §1 discusses generic relations on models of P and ZFC, and describes a special forcing technique due to Addison. In §2, this technique is used to obtain the main result.

The use of forcing is not essential. Those who do not wish to read a forcing argument may skip §1. At the point in §2 where forcing is used, a proof without forcing is sketched. This proof was obtained only after a careful study of the forcing argument. The forcing argument is given because it is simple, and because the technique of forcing makes intuitively clear why this and other similar results should be true.

All theories in the paper are assumed to be countable and to have infinite models. Let T be a complete theory in a language L. The Hanf number for omitting types over T, denoted by H(T), is the first infinite cardinal κ such that for all L-types, Σ, if T has models omitting Σ in all infinite powers less than κ, then T has models omitting Σ in all infinite powers.
Co-hypersimple structures
Authors: Remmel J. B.
Published: May 2006

Priority arguments have been used to produce r.e. sets whose complements have various properties (e.g., maximal sets, hyperhypersimple sets, etc.). In this paper we use the priority method in the context of certain recursively presented models (e.g., dense unbordered linear orderings, countable atomless Boolean algebras, infinite dimensional vector spaces over a finite field) to produce hypersimple subsets of these models whose complements are closed under algebraic operations and/or whose complements are elementarily isomorphic to certain algebraic substructures. For example, it follows from the results of §3 that there are hypersimple subsets of a countable atomless Boolean algebra (of an infinite dimensional vector space over a finite field) in every nonzero r.e. degree whose complement is a subalgebra (subspace). Also, it follows from the same result that, given any subset P of the rationals Q, there is a hypersimple subset of Q whose complement is order isomorphic to P.

A model M of a theory T in a countable language L is said to be recursively presented if the universe ∣M∣ of M is an initial segment of the natural numbers and the satisfaction relation “a satisfies Φ in M” is recursive (where a is a finite sequence of elements of ∣M∣ and Φ is a formula in L).
Noncomplex sequences: characterizations and examples
Authors: Daley Robert P.
Published: May 2006

We are concerned in this paper with infinite binary sequences which are noncomplex in the sense that their minimal-program complexity (i.e., the lengths of shortest programs for computing their finite initial segments), as a function of the lengths of their initial segments, grows arbitrarily (in an effective sense) slowly. Indeed, the existence of such sequences which are also nonrecursive raises some interesting questions concerning the notion of computability itself. Our first task is to give a characterization of these sequences which does not directly involve the notions of complexity theory. Although these characterizations do involve the primitives of recursive function theory, they do not involve the types of properties which one usually encounters there. While a closer connection is still hoped for, the lack of one is not entirely unexpected. For example, except for the trivial case of degree 0, there is no general correlation between program complexity and degrees of unsolvability. The reason, roughly, is this: even though the inequality deg (f) ≤ deg (g) expresses the relative information between f and g (in the sense that if one knows g then one can compute f), it is a qualitative sort of information. The minimal-program complexity is used as a measure of algorithmic information content and as such is quantitative.

The second task of this paper is to present an example of one of these sequences which to its credit possesses a fairly long list of interesting properties, not the least attractive of which is that, though nonrecursive, it is very simple to describe. In fact this sequence has occurred previously in the literature. It is the characteristic sequence of the set of busy beaver numbers first studied by T. Rado [13]. Of particular interest to the discussion in the last section of this paper concerning the notion of computability is the fact that all the initial segments of this sequence are computable by arbitrarily short programs each of which is defined on all inputs and runs very quickly.
Categoricity regained
Authors: Ellentuck Erik
Published: May 2006

One of the earliest goals of modern logic was to characterize familiar mathematical structures up to isomorphism by means of properties expressed in a first order language. This hope was dashed by Skolem's discovery (cf. [6]) of a nonstandard model of first order arithmetic. A theory T such that any two of its models are isomorphic is called categorical. It is well known that if T has any infinite models then T is not categorical. We shall regain categoricity by

(i) enlarging our language so as to allow expressions of infinite length, and

(ii) enlarging our class of isomorphisms so as to allow isomorphisms existing in some Boolean valued extension of the universe of sets.
Another intuitionistic completeness proof
Authors: De Swart H.
Published: May 2006

In March 1973, W. Veldman [1] discovered that, by a slight modification of a Kripke-model, it was possible to give an intuitionistic proof of the completeness-theorem for the intuitionistic predicate calculus (IPC) with respect to modified Kripke models. The modification was the following: Let f represent absurdity, then we allow the possibility that and we agree that, for all sentences ϕ, , if . Just one modified Kripke model is constructed such that validity in implies derivability in IPC. While usually one thinks of as some subset of ⋃nNatn and of as the discrete natural ordering in ⋃nNatn, in Veldman's model , is a spread and , where Γα and Γβ are sets of sentences associated with α, resp. β, is a nondiscrete ordering.

In the completeness-proofs, both for Beth and for Kripke models that we present here, we consider only models over ⋃nNatn, with the natural discrete ordering and we need validity in all models, not just in one, to get derivability in IPC. Also we have to modify the definition of a model in a somewhat different way than Veldman did. We agree that if ∨s[M⊨sf], then M⊨sϕ for each s ∈ ⋃nNatn and for each sentence ϕ.

One can view a single model of the type constructed in [1] as the result of throwing together all the models of (the type constructed in) this paper into one big model, which has the somewhat strange properties mentioned above.
Higher Souslin trees and the generalized continuum hypothesis
Authors: Gregory John
Published: May 2006

The existence of an ω2-Souslin tree will be proved (Theorem 2.2 or §3) from the Generalized Continuum Hypothesis (GCH) plus Jensen's combinatorial principle □ω1. Thus, it follows from Jensen's 1.4(2) that the consistency of the formal theory T given by ZFC + GCH + “ω2-Souslin Hypothesis” implies the consistency of ZFC + “there exists a Mahlo cardinal.” So one does not hope to prove the consistency of this T relative to the consistency of ZFC + “there is an inaccessible cardinal, hence there are transitive models of ZFC.”

Silver [5, Theorem 5.8] has shown that the consistency of ZFC + “there is a weakly compact cardinal” implies the consistency of ZFC + not GCH + “there is no ω2-Aronszajn tree, hence no ω2-Souslin tree”; this is one reason why we deal with GCH here. Jensen has shown that the consistency of ZFC implies the consistency of ZFC +GCH + “ω1-Souslin Hypothesis.”

In the preliminary §1, we state some definitions and known results about trees and some of Jensen's combinatorial principles, including □ and ◇*(E).

Our main Lemma 2.1 states (a fortiori) that GCH implies ◇* at ω-cofinal elements of ω2 (i.e., in our notation, ◇*(E(ω) ∩ ω2)). From Lemma 2.1 and the known facts of §1, it is proved (2.5) that if □k, the cofinality cf(k)> ω, and GCH, then there is a k+-Souslin tree. For k = ω1, this implies the result mentioned above for ω2-Souslin trees.
A note on countable complete theories having three isomorphism types of countable models
Authors: Woodrow Robert E.
Published: May 2006

With quantifier elimination and restriction of language to a binary relation symbol and constant symbols it is shown that countable complete theories having three isomorphism types of countable models are “essentially” the Ehrenfeucht example [4, §6].
The consistency problem for NF
Authors: Boffa M.
Published: May 2006

Although this problem is still open, there are a few related results concerning (i) theories equiconsistent with NF and (ii) consistent fragments of NF. Concerning (i) we will discuss the following results

(1) Specker's result about the equiconsistency of NF with an extension of the theory of types [16],

(2) the equiconsistency of NF with fragments of NF containing NFU [2], [10],

and a new one about

(3) the equiconsistency of NF with an extension of Zermelo's set theory with the axiom of comprehension restricted to bounded formulas.

Concerning (ii) we will give a simplified proof and a generalization of (4) Jensen's result about the consistency of NFU [13].

Only a few words will be devoted to

(5) Grishin's results and refinements [4], [5], [8], [9], treated with more details in [4].

The reader who is unfamiliar with NF or who has a natural repulsion for this system is first invited to read the excellent account contained in [7, Chapter III, §3].
A theorem on shortening the length of proof in formal systems of arithmetic
Authors: di Paola Robert A.
Published: May 2006

This note is concerned with an aspect of the length of proof of formulas in recursively enumerable theories T adequate for recursive arithmetic. In particular, we consider the relative length of proof of formulas in the theories T and T(S), where F represents an r.e. set A in T and T(S) is the theory obtained from T by adjunction, as a new axiom, of a sentence S undecidable in T.

Throughout the sequel T is a consistent, r.e. theory with standard formalization [7] in which all recursive functions of one variable are definable, and in which there is a binary formula x ≤ satisfying the well-known conditions [7]:

Here is the constant term corresponding to the natural number n. Wn is the nth r.e. set in a standard enumeration of the r.e. sets. Also, we assume an a priori Gödel numbering of our formalism satisfying the usual conditions, so that all formulas are numbers ab initio.

In the more common applications of the theorem below, if F is a k-ary formula of T, is a natural number that measures in some way the length of the shortest proof of in T.
On finite lattices of degrees of constructibility of reals
Authors: Adamowicz Zofia
Published: May 2006

Theorem. Assume that there exists a standard model of ZFC + V = L. Then there is a model of ZFC in which the partial ordering of the degrees of constructibility of reals is isomorphic with a given finite lattice.

The proof of the theorem uses forcing. The definition of the forcing conditions and the proofs of some of the lemmas are connected with Lerman's paper on initial segments of the upper semilattice of the Turing degrees [2]. As an auxiliary notion we shall introduce the notion of a sequential representation of a lattice, which slightly differs from Lerman's representation.

Let K be a given finite lattice. Assume that the universe of K is an integer l. Let ≤K be the ordering in K. A sequential representation of K is a sequence Ui ⊆ Ui+1 of finite subsets of ωi such that the following holds:

(1) For any s, s′ Є Ui, i Є ω, k, m Є l, k ≤Km & s(m) = s′(m) → s(k) = s′(k).

(2) For any s Є Ui, i Є ω, s(0) = 0 where 0 is the least element of K.

(3) For any s, s′ Є i Є ω, k,j Є l, if k y Kj = m and s(k) = s′(k) & s(j) = s′(j) → s(m) = s′(m), where vK denotes the join in K.
Noncharacterizability of the syntax set
Authors: Paulos John
Published: May 2006

Craig showed in [3] that Beth's theorem fails for 2nd order logic. This is so since the syntax for 2nd order logic can be represented in the structure of natural numbers and itself can be characterized in 2nd order logic. Thus the satisfaction relation S is implicitly definable yet not explicitly definable (by a Tarski diagonal argument) and Beth fails. Kreisel pointed out in a review of Craig's paper that a similar argument shows that Beth's theorem fails for ω-logic or for any logic whose syntax can be represented in and in which can be characterized. In this paper we use the abstract model-theoretic notions of truth adequacy, truth-maximality and truth-completeness developed by Feferman in [4] to prove the following generalization of Craig's result: If L is a truth-complete logic, then no structure in which the syntax is represented is L-characterizable. This is applied via a corollary to give new examples of failures of Beth's theorem. Another way to construe this result is that truth-complete logics L have the desirable model-theoretic property (see [5]) that the structure in which the syntax is represented is not generalized finite (interpreting generalized finite as L-characterizability).

Since the basic notions of [4] are defined in terms of many-sorted logics, we will consider all our logics to be many-sorted.