bluuebunny/crossref_metadata_2025 huggingface dataset:
A complete theory of natural, rational, and real numbers
Authors: Myhill John R.
Published: May 2006

The purpose of the present paper is to construct a fragment of number theory not subject to Gödel incompletability. Originally the system was designed as a metalanguage for classical mathematics (see section 10); but it now appears to the author worthwhile to present it as a mathematical system in its own right, to serve however rather as an instrument of computation than of proof. Its resources in the latter respect seem very extensive, sufficient apparently for the systematic tabulation of every function used in any but the most recondite physics. The author intends to pursue this topic in a later paper; the present one will simply present the system, along with proofs of consistency and completeness and a few metatheorems which will be used as lemmas for future research.

Completeness is achieved by sacrificing the notions of negation and universal quantification customary in number-theoretic systems; the losses consequent upon this are made good in part by the use of the ancestral as a primitive idea. The general outlines of the system follow closely the pattern of Fitch's “basic logic”; however the latter system uses combinatory operators in place of the variables used in the present paper, and if variables are introduced into Fitch's system by definition their range of values will be found to be much more extensive than that of my variables. The present system K is thus a weaker form of Fitch's system.

It is apparently not known whether or not Fitch's system is complete.
Matrix development of the calculus of relations
Authors: Copilowish Irving M.
Published: May 2006

In his very interesting address On the calculus of refations, Professor Tarski discussed alternative bases for that calculus. He was there interested in “…different methods of setting up the foundations of this elementary calculus in a rigorously deductive way…” and so did not discuss the method of developing the calculus of relations with which this paper is concerned. Our purpose here is to show how the use of matrix notation for relations permits an algorithmic rather than a postulational-deductive development of the calculus of relations. One limitation of the present approach is to be admitted at the very outset: to enjoy the full benefits of the matrix approach, we are obliged to confine our investigations to Universes of Discourse which are finite. The reason for this restriction will become apparent presently.
A finitary metalanguage for extended basic logic
Authors: Myhill John
Published: May 2006

In a series of five papers, Fitch has constructed a system of combinatory logic K′ which is adequate for much of classical analysis, and is demonstrably consistent if we assume the validity of transfinite induction up to a certain ordinal (at present undetermined). The system has the following peculiarities:

1.1. It is non-finitary, i.e. the class of Gödel-numbers of its theorems does not form the range of values of any recursive function (nor, as a matter of fact, of any function definable in elementary number theory).

1.2. It does not permit quantification over real numbers; i.e. it contains no theorems of the form

1.3. Because of 1.1, we cannot, except in trivial cases, construct actual proofs in K′; we have to resort to a metalanguage (of undetermined strength) in order to show that certain formulae are theorems of K′. Also because of 1.2, many important theorems of classical mathematics are not forthcoming in K′ itself, but only in the aforementioned metalanguage, e.g. in the form

where ‘x’ is a syntactical rather than a numerical variable, a U-real is an expression of K′ rather than a number, and ‘ … x– – –’ ascribes a syntactical rather than a real number-theoretic property to x.

The purpose of this paper is to construct a finitary metalanguage for K′ in which all of Fitch's important theorems may be proved.
Some theorems on definability and decidability
Authors: Church Alonzo , Quine W. V.
Published: May 2006

In this paper a theorem about numerical relations will be established and shown to have certain consequences concerning decidability in quantification theory, as well as concerning the foundation of number theory. The theorem is that relations of natural numbers are reducible in elementary fashion to symmetric ones; i.e.:

Theorem I. For every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that R is definable in terms of H plus just truth-functions and quantification over natural numbers.

To state the matter more fully, there is a (well-formed) formula ϕ of pure quantification theory, or first-order functional calculus, which meets these conditions:

(a) ϕ has ‘x’ and ‘y’ as sole free individual variables;

(b) ϕ contains just one predicate letter, and it is dyadic;

(c) for every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that, when the predicate letter in ϕ is interpreted as expressing H, ϕ comes to agree in truth-value with ‘x bears R to y’ for all values of ‘x’ and ‘y’.
A note concerning the paradoxes of strict implication and Lewis's system SI
Authors: Halldén Sören
Published: May 2006

It has been shown by Lewis and Langford that the postulate B8,

is not deducible in SI. From this it follows that neither are the paradoxes of strict implication deducible in that system. However, the following weaker—but perhaps philosophically equally important—analogues are deducible:
A remark concerning decidability of complete theories
Authors: Janiczak Antoni
Published: May 2006

A formalized theory is called complete if for each sentence expressible in this theory either the sentence itself or its negation is provable.

A theory is called deciddble if there exists an effective procedure (called decision-procedure) which enables one to decide of each sentence, in a finite number of steps, whether or not it is provable in the theory.

It is known that there exist complete but undecidable theories. There exist, namely, the so called essentially undecidable theories, i.e. theories which are undecidable and remain so after an arbitrary consistent extension of the set of axioms. Using the well-known method of Lindenbaum we can therefore obtain from each such theory a complete and undecidable theory.

The aim of this paper is to prove a theorem which shows that complete theories satisfying certain very general conditions are always decidable. In somewhat loose formulation these conditions are: There exist four effective methods M1, M2, M3, M4, such that

(a) M1 enables us to decide in each case whether or not any given formula is a sentence of the theory;

(b) M2 gives an enumeration of all axioms of the theory;

(c) the rules of inference can be arranged in a sequence R1, R2, … such that if p1, … pk, r are arbitrary sentences of the theory, we can decide by M3 whether or not r results from p1, … pk, by the n-th rule;

(d) M4 enables us to construct effectively the negation of each effectively given sentence.

In order to express these conditions more precisely we shall make use of an arithmetization of the considered theory .
The independence of a weak axiom of choice
Authors: Mendelson Elliott
Published: May 2006

1. The purpose of this paper is to show that, if the axioms of a system G of set theory are consistent, then it is impossible to prove from them the following weak form of the axiom of choice: (H1) For every denumerable set x of disjoint two-element sets, there is a set y, called a choice set for x, which contains exactly one element in common with each element of x. Among the axioms of the system G, we take, with minor modifications, Axioms A, B, C of Gödel [6]. Clearly, the independence of H1 implies that of all stronger propositions, including the general axiom of choice and the generalized continuum hypothesis.

The proof depends upon ideas of Fraenkel and Mostowski, and proceeds in the following manner. Let a be a denumerable set of objects Δ0, Δ1, Δ2, …, the exact nature of which will be specified later. Let μj = {Δ2j, Δ2j+1} for each j, c = {μ0, μ1, μ2, …}, and b = [the sum set of a]. By transfinite induction, construct the class Vc which is the closure of b under the power-set operation. For each j, it is possible to define a 1–1 mapping of Vc onto itself with the following properties. The mapping preserves the ε-relation, or, more precisely, .
The independence of Quine's axioms *200 and *201
Authors: Rosser Barkley
Published: May 2006

We refer to the axioms in Quine's book, Mathematical logic, New York, 1940.

To prove the independence of *200, give xϵ α the truth value F in all cases and give (x)ϕ the same truth value as ϕ. Then clearly all formulas derivable from the other axioms besides *200 have the value T, whereas from *200 one can derive (∃x)(∃α)(xϵ α) which has the value F. This method of proving independence amounts to taking for a model a universe consisting of the single object Λ.

For *201 we prove a contingent independence. That is, we prove that if Quine's system is consistent, then *201 is independent. The line of argument is the following. Suppose *201 can be derived from the other axioms. Let us replace xϵ α by throughout all the axioms. Then what *201 becomes can be derived from what the other axioms become. However what *201 becomes will lead to a contradiction in Quine's system whereas the rules which the other axioms become are valid in Quine's system.

We now get down to technical details. Let us refer to the replacement of xϵ α by throughout an expression as an r replacement. Denote the result of performing an r replacement on ϕ by ϕr. Let Wα denote

Then

Note that if x and y are variables, then by D10,
The representations of S5
Authors: Bergmann Gustav
Published: May 2006

According to McKinsey and Tarski [3], who introduced the notion, a closure algebra Γ = (K, ∪, ∩, –, C) is a Boolean algebra (K, ∪, ∩, –) with an additional unary operator C, closed in K, such that, for every x, y ϵ K, x ⊆ Cx, CCx = Cx, C(x∪y) = Cx∪Cy, CΛ = Λ. McKinsey [2] has proved that a matrix Γ = (K, D, ∪, ∩, –, C) is a representation (normal matrix) of S4, if and only if (1) (K, ∪, ∩, –, C) is a closure algebra, (2) D is an additive ideal of K, (3) if – Cx ϵ D then x = Λ, D being the distinguished proper subset of K and ∪, ∩, –, C having been made to correspond to ∨, ·, ∼, ◊, respectively. Following McKinsey, one proves immediately

Theorem 1. A matrix Γ is a representation of S5, if and only if it is a closure algebra and

(α) for every x ϵ K, –C–Cx = Cx, and

(β) D is an additive ideal of K such that, for every x ϵ D, Cx = V.

This raises the question of alternative characterizations of S5. Because of (β), one may without substantial loss of generality put D = {V}. The question then becomes one for conditions that are in closure algebras equivalent to (α). One such characterization has been given by McKinsey and Tarski [4]. Defining x∸y = C(x∩–y) and ¬x = V∸x, these authors have shown that the closed elements K* of a closure algebra Γ form a Brouwerian algebra Γ* = (K*, ∪, ∩, ∸), and furthermore that Γ* is a Boolean algebra under ∪, ∩, ¬, if and only if, for every x ϵ K*,
Unification of universes in set theory
Authors: Quine W. V.
Published: May 2006

The logic of quantification is conveniently developed in terms of the so-calledquantificational schemata. The atomic quantificational schemata consist each of a schematic predicate letter (‘F’, ‘G’, etc.) attached to one or more quantifiable variables (‘x’, ‘y’, etc.). Compound quantificational schemata are built up of these atomic ones by means of truth functions and quantifiers. The business of the logic of quantification then becomes that of spotting thevalidschemata: the ones that are true under all interpretations.

The logic of quantification is well understood and well behaved. Proof procedures in this domain are known, thanks to Gödel, to be complete. If decision procedures are not known for the whole of this part of logic, still we do know, thanks to Church, that they cannot exist. And we know how to streamline our proof procedure for quick success in the average case where proof is possible. Because of all this, there is a premium on adapting special theories, of special subject matters, to this general mold. This means representing the truths of the special theory as a class of quantificational schemata with interpreted predicate letters and a chosen universe of discourse. Once a theory has been thus regimented, it is astandardtheory (in approximately Tarski's sense of the term).
Some structure results for propositional calculi
Authors: Harrop Ronald
Published: May 2006

1. Introduction. Since this paper is a written version of one presented as a survey lecture at a meeting of the Association for Symbolic Logic, its form and content have been essentially determined by the form and content of that lecture, and these latter were themselves considerably influenced by a deliberate attempt to avoid the lecture consisting essentially either of a catalogue of results in some fairly wide field or of the presentation of detailed proofs of a few particular results in a very limited field, with, in either case, a consequential serious limitation of the time available for discussion of the motivation for the results and of the connections between them. There is thus no attempt to cover, even in outline, the full range of topics which could reasonably fall within the scope of its title.

The paper consists mainly of a general discussion of some results concerned with finite models of axiomatically defined calculi of propositional form, with particular reference to the occurrence of such models in proofs that certain propositional calculi are decidable. In addition, there is an account of some results concerned with the existence of undecidable propositional calculi and of others connected with the decidability or undecidability of certain structure problems which relate either to sets of propositional calculi or to different presentations of the same calculus.
A theorem on minimal degrees
Authors: Shoenfield J. R.
Published: May 2006

In their original paper on degrees [3], Kleene and Post showed that there is a degree between 0 and 0′. Later, Friedberg [1] and Muchnik [4] showed that there is a recursively enumerable degree between 0 and 0′. Since then, this phenomenon has been repeated several times: a result has been proved for degrees, and then, after considerable additional effort, it has been proved for recursively enumerable degrees.

There are some obvious respects in which that set of all degrees differs from the set of recursively enumerable degrees; e.g., the former is uncountable and has no largest member.
Functions of Propositions
Authors: Cresswell M. J.
Published: May 2006

In [1] (p. 131 et seq) Professor A. N. Prior suggests a calculus of functions of propositions in which the range of the function variables is not restricted to truth functions.1 If f, g, … etc. represent such variables and we have quantification over all variables we can introduce propositional identity by definition as (ƒ)(ƒp ⊃ ƒq) Alternatively identity may be primitive with the usual axioms and schemata (v.e.g. [4] p. 190 et seq). We shall refer to such systems as ‘functorial calculi’2 (abbreviated as FC).
Some results for implicational calculi
Authors: Bull R. A.
Published: May 2006

I shall refer to the implicational fragment of intuitionist logic, and its extension with the further axiom

CCCCpqqrCCCpqrr

as IIC and OIC, respectively. The purpose of this paper is to apply a result due to Garrett Birkhoff to the extensions of IIC, and to the extensions of OIC in particular. The main result obtained is that every extension of OIC is characterised by finite models.
Independence of two nice sets of axioms for the propositional calculus
Authors: Thacher Robinson T.
Published: May 2006

Kanger [4] gives a set of twelve axioms for the classical prepositional calculus which, together with modus ponens and substitution, have the following nice properties:

(0.1) Each axiom contains =⊃, and no axiom contains more than two different connectives.

(0.2) Deletions of certain of the axioms yield the intuitionistic, minimal, and classical refutability1 subsystems of propositional calculus.
ℵ0-Complete cardinals and transcendency of cardinals
Authors: Namba Kanji
Published: May 2006

In this paper, we shall state some results concerning ℵ0-complete cardinals and the transcendency of cardinals which is proposed by G. Takeuti [6]. The main purpose of this paper is to prove the following theorems.

Theorem 1. Let ℵ1, be the first ℵ0-complete cardinal number. Then the transcendency of cardinals holds for Δ11-functions of ℵ1-language.
On large cardinals and partition relations
Authors: Kleinberg E. M. , Shore R. A.
Published: May 2006

A significant portion of the study of large cardinals in set theory centers around the concept of “partition relation”. To best capture the basic idea here, we introduce the following notation: for x and y sets, κ an infinite cardinal, and γ an ordinal less than κ, we let [x]γ denote the collection of subsets of x of order-type γ and abbreviate with the partition relation for each function F frominto y there exists a subset C of κ of cardinality κ such that (such that for each α < γ) the range of F on [С]γ ([С]α) has cardinality 1. Now although each infinite cardinal κ satisfies the relation for each n and m in ω (F. P. Ramsey [8]), a connection with large cardinals arises when one asks, “For which uncountable κ do we have κ → (κ)2?” Indeed, any uncountable cardinal κ which satisfies κ → (κ)2 is strongly inaccessible and weakly compact (see [9]). As another example one can look at the improvements of Scott's original result to the effect that if there exists a measurable cardinal then there exists a nonconstructible set. Indeed, if κ is a measurable cardinal then κ → (κ)< ω, and as Solovay [11] has shown, if there exists a cardinal κ such that κ → (κ)< ω3 (κ → (ℵ1)< ω, even) then there exists a nonconstructible set of integers.
Effective operations in a general setting
Authors: Lachlan A. H.
Published: May 2006

There are essentially two ‘positive’ results concerning the extension of effective operations to partial recursive functionals. The first proved by Myhill and Shepherdson in [9] states that any effective operation whose domain is the set of all partial recursive (p.r.) functions is potentially p.r. The second proved originally by Kreisel, Lacombe, and Shoenfield in [5] states: Let F be an effective operation mapping a set of recursive functions into the natural numbers; if has a recursively dense base, then F is potentially p.r. The main objective of this paper is to present these two theorems in a general setting.
An incorrect theorem
Authors: Hailperin Theodore
Published: May 2006

In the fourth edition of Hilbert-Ackermann's Grundzüge der Theoretischen Logik (Springer-Verlag: Berlin-Göttingen-Heidelberg 1959) the following assertion is “proved” (p. 131):

Ein Ausdruck, der keine freien Individuenvariablen enthält, ist dann und nur dann allgemeingültig, wenn allgemeingültig ist. Die Ausdrücke, die die Identität enthalten, sind dabei eingeschlossen.

As a counter example one can cite: ∃x(¬∃xFx ∨ Fx), which is universally valid yet the generalized form: ∀x(¬∃xFx ∨ Fx) is not (e.g. let the domain of individuals be the natural numbers and let ‘Fx’ be ‘x is factorable’).

It may be of interest to see where the alleged proof went astray. It is argued (correctly) that any expression can only be derived by the given rules from a formula , or from this formula with any other variable in place of y. Moreover (still correctly) any upper formula of such a formula is of the form (“Upper formula” in the transitive sense of an upper formula of an upper formula being an upper formula). But then it is stated (incorrectly) that if is an upper formula of , then is an upper formula of . To show that this is incorrect we here append a proof of the universally valid formula mentioned above:
A coding theorem for isols
Authors: Ellentuck Erik
Published: May 2006

In [1] it is shown that for every sequence x = 〈xn : n ∈ ω〉 ∈ Xω Λ there is an isol xω (essentially an immunized product) such that

Here we have used the notation: Λ = the isols, ω = the nonnegative integers, pn is the nth prime rational integer starting with p0 = 2, ∣ denotes divisibility and ∤ its negation. If p is an arbitrary prime, py ∣ x, pz ∣ x, and y < z then py+1 ∣ x. In particular since y ∈ ω is comparable with every element of Λ, the conditions py ∣ x and py+1 ∤ x uniquely determine y. Thus every sequence x ∈ Xωω is uniquely determined by an xω satisfying (1) and consequently may be used as a “code” for that sequence. In Theorem 1 it is shown that (1) does not uniquely determine the values of an arbitrary sequence x ∈ XωΛ, however in Theorem 3 we find a different scheme which does. At the very end of the paper we give some reasons why coding theorems are useful. It should also be mentioned that for a coding theorem to be meaningful it is necessary to restrict the operations by which a sequence can be recaptured from its code. Otherwise a triviality results. Our coding theorem will allow all operations which are first order definable in Λ with respect to addition, multiplication, and exponentiation. We conjecture that the latter operation is really necessary.
Correction to a paper on definability of ordinals in infinite logic
Authors: Kino Akiko
Published: May 2006

We wish to make a correction to our paper On definability of ordinals in logic with infinitely long expressions (this journal, vol. 31 (1966), pp. 365–375). Let Ω be an infinite singular cardinal and Ω+ the smallest cardinal >Ω. For the proof of the second half of Theorem 3, we incorrectly assumed that an ordinal γ is not definable in LΩ, if γ is not cofinal with any ordinal ≤Ω. However, Ω+ is indeed definable in LΩ and Theorem 3 should read:

If Ω singular, then an ordinal α is definable in Lα, if and only if σ ≤ exp(Ω+, Ω+), where exp (β,γ) denotes ordinal exponentiation βγ.
A note on finite axiomatization of partial propositional calculi
Authors: Singletary W. E.
Published: May 2006

At the Princeton Bicentennial in 1946 Tarski posed the question as to whether or not certain problems connected with partial propositional calculi were recursively solvable. Since that time the specific problems mentioned by Tarski as well as a number of related problems have been shown to be recursively unsolvable. Such results are due to Post and Linial [5], Yntema [9], Gladstone [2], Ihrig [3] and Singletary [7], [8].
Nonaxiomatizability results for infinitary systems
Authors: Karp Carol
Published: May 2006

Methods are being developed for treating questions of decidability in fewer than Ω steps, Ω being a regular nondenumerable cardinal. In this paper we consider the set-theoretical predicate Taut(x), “x is a tautology,” taken in the infinitary sense. In case x is hereditarily finite there is no question that it is decidable in finitely many steps. But what if x is infinite? We are not assuming that x is in any way constructive or even that the propositional formulas can be well-ordered, so it is not appropriate to treat this predicate as one of natural numbers or even as one of ordinals.
On primitive recursive permutations and their inverses
Authors: Cannonito Frank B. , Finkelstein Mark
Published: May 2006

It has been known for some time that there is a primitive recursive permutation of the nonnegative integers whose inverse is recursive but not primitive recursive. For example one has this result apparently for the first time in Kuznecov [1] and implicitly in Kent [2] or J. Robinson [3], who shows that every singularly recursive function ƒ is representable as

where A, B, C are primitive recursive and B is a permutation.
A simple solution of the uniform halting problem
Authors: Herman Gabor T.
Published: May 2006

The uniform halting problem (UH) can be stated as follows.

Give a decision procedure which for any given Turing machine (TM) will decide whether or not it has an immortal instantaneous description (ID).

An ID is called immortal if it has no terminal successor. As it is generally the case in the literature (see e.g. Minsky [3, p. 118]) we assume that in an ID the tape must be blank except for some finite numbers of squares. If we remove this restriction the UH becomes the immortality problem (IP). The UH should not be confused with the initialised uniform halting problem (whether or not a TM has an immortal ID when started in a specified state) which can easily be shown to be undecidable (see e.g. Minsky [3, p. 151]).
The elimination of De Re modalities
Authors: Cresswell M. J.
Published: May 2006

A formula α of modal LPC is a de re modality iff it contains a free individual variable within the scope of a modal operator; otherwise α is de dicto.1 We shall say that de re modalities are eliminable in a system S of modal LPC iff there is a transformation R on wffs of S such that R(α) is de dicto and ├sα ≡ R(α). We shall show that where S is LPC + S5 + Pr2 then de re modalities are not eliminable in S.
A purely syntactical definition of confirmation
Authors: Hempel Carl G.
Published: May 2006

The concept of confirmation occupies a central position in the methodology of empirical science. For it is the distinctive characteristic of an empirical hypothesis to be amenable, at least in principle, to a test based on suitable observations or experiments; the empirical data obtained in a test—or, as we shall prefer to say, the observation sentences describing those data—may then either confirm or disconfirm the given hypothesis, or they may be neutral with respect to it. To say that certain observation sentences confirm or disconfirm a hypothesis, does not, of course, generally mean that those observation sentences suffice strictly to prove or to refute the hypothesis in question, but rather that they constitute favorable, or unfavorable, evidence for it; and the term “neutral” is to indicate that the observation sentences are either entirely irrelevant to the hypothesis, or at least insufficient to strengthen or weaken it.
A Gentzen-type calculus of sequents for single-operator propositional logic
Authors: Riser John
Published: May 2006

The following describes a calculus of sequents (SLK) patterned after the calculus LK of Gentzen in [1] but restricted to the formulas of propositional logic and modified so that the only connective is the Sheffer stroke. The ‘elimination theorem’ (Hauptsatz) is proved for SLK and a decision procedure is specified for determining whether a given formula in stroke notation is tautologous. In addition, SLK is proved consistent and complete. Subsequent remarks indicate briefly how the calculus can be modified so as to employ the dagger as the only connective.
A note on existential instantiation
Authors: Prawitz Dag
Published: May 2006

The presence of a rule for existential instantiation (EI) in a system of natural deduction often causes some difficulties, in particular, when it comes to formulate necessary restrictions on the rule for universal generalization (UG). A system containing rules for EI and UG that avoided Quine's rather cumbersome restrictions on these rules was formulated by Copi [2], but the system was found to be inconveniently restrictive. A less restrictive system was therefore suggested by Copi [3]. Also that system forces some deductions to be unnecessarily long as is shown in Prawitz [5, Appendix C, p. 104], where a way to liberalize Copi's restriction on UG is suggested (p. 105). However, the system suggested by Copi [3] is also incorrect (i.e. unsound) as has recently been shown by Parry [4] in this Journal.
Uniformly introreducible sets
Authors: Jockusch Carl G.
Published: May 2006

Retraceable sets were denned in Dekker and Myhill [5]. In that paper it was pointed out that if A is a retraceable set, then A is recursive in each of its infinite subsets, i.e. A is introreducible. We would like to know to what extent theorems on retraceable sets also hold for introreducible sets; however, we have made very little progress in this direction. On the other hand, “uniformly introreducible” sets (which will be defined in §2) are more tractable, and it turns out that some results on retraceable sets extend to uniformly introreducible sets while others fail.
Uniform Gentzen systems
Authors: Smullyan Raymond M.
Published: May 2006

Generally speaking, it appears correct to say that in a formulation of first order logic in which a large number of connectives are taken as primitive (e.g. ∼, Λ, ∨, ⊃, ∀, ∃ as opposed to ∼, ⊃, ∀, or still more economically, ↓, ∀ proofs within the formal system tend to be smoother and more natural, but the metatheory tends to be that much more elaborate. In [1] we introduced a unifying ‘α, β, γ, δ” notation (which we also used in [2]–[7] and which we briefly review in this paper) which allows us to have our cake and eat it too.
Partial recursive functions and ω-functions
Authors: Applebaum C. H. , Dekker J. C. E.
Published: May 2006

Let ε stand for the set of all numbers (i.e., nonnegative integers), V for the class of all sets (i.e., subcollections of ε) and for the family of all functions (i.e., mappings from a subset of ε into ε). If ƒ is a function, we write δƒ and ρƒ for its domain and range respectively. The relation of inclusion is denoted by ⊂ and that of proper inclusion by ⊆.
On n-adic representation of numbers
Authors: Patton Thomas E.
Published: May 2006

In Smullyan [1], where recursive enumerability is defined in terms of elementary dyadic arithmetics (dyadic EA's), it is shown that for any number n, the parallel definition in terms of n-adic EA′s is equivalent. This proof at one stage uses the deep result of Godei that plus and times form a sub-basis for the recursively enumerable attributes (sets and relations)2. The aim of this note is to prove this equivalence in more pedestrian fashion.
Type-raising operations on cardinal and ordinal numbers in Quine's “New foundations”
Authors: Henson C. Ward
Published: May 2006

In this paper we develop certain methods of proof in Quine's set theory NF which have no counterparts elsewhere. These ideas were first used by Specker [5] in his disproof of the Axiom of Choice in NF. They depend on the properties of two related operations, T(n) on cardinal numbers and U(α) on ordinal numbers, which are defined by the equations

for each set x and well ordering R. (Here and below we use Rosser's notation [3].) The definitions insure that the formulas T(x) = y and U(x) = y are stratified when y is assigned a type one higher than x. The importance of T and U stems from the following facts: (i) each of T and U is a 1-1, order preserving operation from its domain onto a proper initial section of its domain; (ii) Tand U commute with most of the standard operations on cardinal and ordinal numbers.

These basic facts are discussed in §1. In §2 we prove in NF that the exponential function 2n is not 1-1. Indeed, there exist cardinal numbers m and n which satisfy

In §3 we prove the following technical result, which has many important applications. Suppose f is an increasing function from an initial segment S of the set NO of ordinal numbers into NO and that f commutes with U.
Measurable cardinals and a combinatorial principle of Jensen
Authors: Devlin Keith J.
Published: May 2006

At the end of his paper [2], Silver shows how methods developed by Jensen and Solovay in order to prove results about the constructible universe L may be adapted to prove corresponding results for the universe L[μ], where μ is a normal measure on some uncountable cardinal ρ. In this paper we pursue this in greater depth. Jensen proved, in fact, much stronger results than those considered in [2], and we shall show that all of these carry over from L to L[μ], More precisely, we show that if V = L[μ] is assumed, then for any regular uncountable cardinal κ and any uncountable λ < κ, + (κ, λ) holds, and that + (κ, κ) holds just in the case κ is not ineffable. This result was proved to hold in L by Jensen, who first formulated the principles + (κ, λ).

Our proof differs in detail from Jensen's, and at one point (in choosing the set B of + ) differs fundamentally from his argument. However, the fact remains that our argument is modelled closely upon Jensen's, and it should be made clear that in many parts it is a straightforward adaption of his proof to the L[μ] situation. It is regrettable that, at the time of our writing this, Jensen's proof still only exists in the rough, handwritten form of [1]; so we shall give our argument in some detail, even those parts which are merely “translations” of Jensen's original arguments.
On splitting stationary subsets of large cardinals
Authors: Baumgartner James E. , Taylor Alan D. , Wagon Stanley
Published: May 2006

Let κ denote a regular uncountable cardinal and NS the normal ideal of nonstationary subsets of κ. Our results concern the well-known open question whether NS fails to be κ+-saturated, i.e., are there κ+ stationary subsets of κ with pairwise intersections nonstationary? Our first observation is:

Theorem. NS isκ+-saturated iff for every normal ideal J on κ there is a stationary set A ⊆ κsuch that J = NS∣A = {X ⊆ κ: X ∩ A ∈ NS}.

Turning our attention to large cardinals, we extend the usual (weak) Mahlo hierarchy to define “greatly Mahlo” cardinals and obtain the following:

Theorem. If κ is greatly Mahlo then NS is notκ+-saturated.

Theorem. If κ is ordinal Π11-indescribable (e.g., weakly compact), ethereal (e.g., subtle), or carries aκ-saturated ideal, thenκis greatly Mahlo. Moreover, there is a stationary set of greatly Mahlo cardinals below any ordinal Π11-indescribable cardinal.

These methods apply to other normal ideals as well; e.g., the subtle ideal on an ineffable cardinal κ is not κ+-saturated.
Complete theories with countably many rigid nonisomorphic models
Authors: Malitz Jerome
Published: May 2006

Here we prove the following:

Theorem. For every N ≤ ω there is a complete theory Tn having exactly n nonisomorphic rigid models and no uncountable rigid models. Moreover, each non-rigid model admits a nontrivial automorphism.

The Tn are theories in the first-order predicate calculus and a rigid structure is a structure with no nontrivial endomorphisms, i.e., the only endomorphism of the structure into itself is the identity. The theorem answers a question of A. Ehrenfeucht.

For the most part we use standard model theoretic notation with Th denoting the set of sentences true in and meaning . A complete set of sentences is one of the form Th for some . The universe of a structure may be denoted by ∣∣. An n-ary relation on X is a set of n tuples (x0, …, xn−1) with each xi ∈ X. All the structures encounted here will be relational. If P is an n-ary relation then P ↾ Y, the restriction of P to Y, is {(x0, …, xn−1): (x0, …, xn−1) ∈ P and x0, …, xn−1Y}.
On models of arithmetic—Answers to two problems raised by H. Gaifman
Authors: Wilkie Alex
Published: May 2006

In a recent paper [3] H. Gaifman investigated some model theoretic consequences of Matijasevič's theorem [5], and posed some further problems which naturally arise. We provide here partial answers to two of these problems, the results having been previously announced in the postscript of [3].

Firstly, it is shown in [3] that if M1 and M2 are models of the Peano axioms P and M1 ⊆ M2, then M1 is closed under the recursive functions of M2. The converse of this statement is false. Moreover, Gaifman asks: Is every initial segment of a model M of P which is closed under the recursive functions of M (or the ∑n-definable functions) also a model of P? We show that this is false and our method gives, en route, another proof of a theorem of Rabin [7] stating the P is not implied by any consistent set of ∑n sentences for any n.

Secondly, we partially answer a question posed on p. 129 of [3] by proving (some-what more than) every countable nonstandard model of P has an end extension in which a diophantine equation, not solvable in the original model, has a solution. We can, in fact, take the new model to be isomorphic to the original one. This generalises (apart from the countability restriction) a theorem of Rabin [6].
Transfinite extensions of Friedberg's completeness criterion
Authors: Macintyre John M.
Published: May 2006

In [3] Friedberg showed that every Turing degree ≥ 0′ is the jump of some degree. Using the relativized version of this theorem it can be shown by finite induction that if a ≥ 0(n)0(n) then there is a b such that b(n) = a (our notation is defined in §1). It is natural to ask whether these results can be extended into the transfinite. Is it true for example, that whenever a ≥ 0(ω) there is a b such that = b(ω)= a? In §2 we use forcing to prove this result. (The usefulness of forcing in answering questions involving the jump operation on degrees of unsolvability has been previously demonstrated in Selman [5] where, for example, forcing was used to construct degrees a and b such that a(ω) = b(ω) = a ∪ b = 0(ω).) In §3 we generalize the methods of §2 to show that if α is a recursive ordinal and a ≥ 0(α) then there is a bsuch that b(α) = a, i.e. the Friedberg result can be extended to all recursive ordinal levels.

Thomason [6] used a forcing argument to show: If (the Kleene set of notations for the recursive ordinals) then there is a B such that (the set of notations for ordinals recursive in B). In §4 we show this result holds when hyperarithmetic reducibility is replaced by Turing reducibility: If then there is a B such that .
On generalized computational complexity
Authors: Jacobs Barry E.
Published: May 2006

If one regards an ordinal number as a generalization of a counting number, then it is natural to begin thinking in terms of computations on sets of ordinal numbers. This is precisely what Takeuti [22] had in mind when he initiated the study of recursive functions on ordinals. Kreisel and Sacks [9] too developed an ordinal recursion theory, called metarecursion theory, which specialized to the initial segment of the ordinals bounded by(the first nonconstructive ordinal).

The notion of admissibility was introduced by Kripke [11] and Platek [14] and served to generalize metarecursion theory. Kripke called ordinal α admissible if it satisfied certain closure properties of infinitary computations. It was shown that admissibility could be equivalently formulated in terms of the replacement schema of ZF set theory and that α =is an admissible ordinal. The study of a recursion theory on an initial segment of the ordinals bounded by some arbitrary admissible α became known as α-recursion theory.

Kripke [10] employed a Gödel numbering scheme to perform an arithmetiza-tion of α -recursion theory and created an analogue to Kleene'sT-predicate (cf. [8]) of ordinary recursion theory (o.r.t.). TheT-predicate then served as the basis for showing that analogues of the major results of unrelativized o.r.t. held in α-recursion theory; namely, the α-Enumeration Theorem,T Theorem, α-Recursion Theorem, and α-Universal Function Theorem.
A hierarchy for the 1-section of any type two object
Authors: Wainer S. S.
Published: May 2006

Shoenfield [6] constructed a hierarchy for any type two object F in which 2E is recursive by generalizing the hyperarithmetical hierarchy, using a jump operation jF defined by

(A similar hierarchy was constructed independently by Hinman [3].) In order to construct a hierarchy for an arbitrary type two F we must first associate with F an operator which, on one hand will always be recursive in F, and on the other hand will generate all the functions recursive in F when iterated over a simultaneously generated set of ordinal notations OF. Clearly the use of 2E in the above definition of jF(f) can be avoided if, instead of diagonalizing F over all functions recursive in f, we only diagonalize F over, say, the functions primitive recursive in f. If furthermore we code in a function which enumerates all functions primitive recursive in f then the resulting operation will certainly generate a primitive recursively expanding hierarchy of functions recursive in F. The problem that remains is whether this hierarchy will exhaust the 1-section of F. But this reduces to an effectiyized version of the following problem: If g is recursive in some level of the hierarchy, is g primitive recursive in some higher level ? An affirmative answer is suggested by the completeness results of Feferman [2], and our main theorem below will be proved by combining his ideas with those of Shoenfield [6]. The result is a hierarchy which applies to all type two objects, and which replaces the notion of recursion in F by the simpler notion of primitive recursion in certain functions generated by F. Unfortunately, in contrast with the Shoenfield hierarchy, the hierarchy developed here cannot always be expected to have the uniqueness property (even w.r.t. ≤T), and for this reason the proof of our main theorem is rather more complicated than the corresponding proof in [6].
Projective model completeness
Authors: Sacerdote George S.
Published: May 2006

The concept of model completeness has been very useful in model theory. In this article we obtain a new model theoretic tool by “reversing the arrows.” Specifically, model completeness deals with the relations between a model of a theory and its extensions; in this paper we shall be concerned with the relation between a model of a theory and its homomorphic pre-images.

This work is based on the intuitive principle that metamathematical theorems about universal sentences of the lower predicate calculus and substructures can be translated in a truth-preserving way to theorems about positive sentences and homomorphic images. From model completeness and the completeness theorems which depend on it, this translation gives new criteria for completeness.

Special thanks are due to Professor A. Robinson whose encouragement and suggestions have contributed much to these results.
Noncompactness in propositional modal logic
Authors: Thomason S. K.
Published: May 2006

We have come to believe that propositional modal logic (with the usual relational semantics) must be understood as a rather strong fragment of classical second-order predicate logic. (The interpretation of propositional modal logic in second-order predicate logic is well known; see e.g. [2, §1].) “Strong” refers of course to the expressive power of the languages, not to the deductive power of formal systems. By “rather strong” we mean sufficiently strong that theorems about first-order logic which fail for second-order logic usually fail even for propositional modal logic. Some evidence for this belief is contained in [2] and [3]. In the former is exhibited a finitely axiomatized consistent tense logic having no relational models, and the latter presents a finitely axiomatized modal logic between T and S4, such that □p → □2p is valid in all relational models of the logic but is not a thesis of the logic. The result of [2] is strong evidence that bimodal logic is essentially second-order, but that of [3] does not eliminate the possibility that unimodal logic only appears to be incomplete because we have not adopted sufficiently powerful rules of inference. In the present paper we present stronger evidence of the essentially second-order nature of unimodal logic.
Products of two-sorted structures
Authors: Olin Philip
Published: May 2006

First order properties of direct products and direct sums (weak direct products) of relational systems have been studied extensively. For example, in Feferman and Vaught [3] an effective procedure is given for reducing such properties of the product to properties of the factors, and thus in particular elementary equivalence is preserved. We consider here two-sorted relational systems, with the direct product and sum operations keeping one of the sorts stationary. (See Feferman [4] for a similar definition of extensions.)

These considerations are motivated by the example of direct products and sums of modules [8], [9]. In [9] examples are given to show that the direct product of two modules (even having only a finite number of module elements) does not preserve two-sorted (even universal) equivalence for any finite or infinitary language Lκ, λ. So we restrict attention here to direct powers and multiples (many copies of one structure). Also in [9] it is shown (for modules, but the proofs generalize immediately to two-sorted structures with a finite number of relations) that the direct multiple operation preserves first order ∀E-equivalence and the direct power operation preserves first order ∀-equivalence. We show here that these results for general two-sorted structures in a finite first order language are, in a sense, best-possible. Examples are given to show that does not imply , and that does not imply .
Applications of trees to intermediate logics
Authors: Gabbay Dov M.
Published: May 2006

We investigate extensions of Heyting's predicate calculus (HPC). We relate geometric properties of the trees of Kripke models (see [2]) with schemas of HPC and thus obtain completeness theorems for several intermediate logics defined by schemas. Our main results are:

(a) ∼(∀x ∼ ∼ϕ(x) Λ ∼∀xϕ(x)) is characterized by all Kripke models with trees T with the property that every point is below an endpoint. (From this we shall deduce Glivenko type theorems for this extension.)

(b) The fragment of HPC without ∨ and ∃ is complete for all Kripke models with constant domains.

We assume familiarity with Kripke [2]. Our notation is different from his since we want to stress properties of the trees. A Kripke model will be denoted by (Aα, ≤ 0), α ∈ T where (T, ≤, 0) is the tree with the least member 0 ∈ T and Aα, α ∈ T, is the model standing at the node α. The truth value at α of a formula ϕ(a1 … an) under the indicated assignment at α is denoted by [ϕ(a1 … an)]α.

A Kripke model is said to be of constant domains if all the models Aα, α ∈ T, have the same domain.
On existence proofs of Hanf numbers
Authors: Friedman Harvey
Published: May 2006

This paper refines some results of Barwise [1] as well as answering the open question posed at the end of [1] about the Hanf number of positively. We conclude by showing that the existence of a Hanf bound for cannot be proved in the natural formally intuitionistic set theories with bounded predicates decidable of [3], [4] and [5].

All notation not explained below is taken from [1]. In the Appendix, we give the axioms of ZF0, ZF1, and T in full. We remark that an important point about the axiom of foundation was not emphasized in [1]. This axiom was intended to be the axiom scheme (∀x)((∀y ∈ x)(A(y)) → A(x)) → (∀x)(A(x)), where y does not occur in A = A(x), instead of the more customary (∀x)(∀y)(y ∈ x → (∃z ∈ x)(∀w ∈ z) (w ∉ x)). This is of no consequence in the presence of full separation, but is vital when considering ZF0 and the T below, for with the customary form of foundation, these cannot even prove the existence of Rω+ω.

In [1], a proof of the following is sketched.