bluuebunny/crossref_metadata_2025_split huggingface dataset:
A revision of the fundamental rules of combinatory logic
Authors: Curry Haskell B. 
Published: May 2006

The purpose of this paper is to put on record some theorems relating to improvements in the primitive frame of combinatory logic. These improvements were, for the most part, suggested by the work of Rosser, who formulated a weakened system of combinatory logic in which the rules had a simple character not possessed by those of the original system. In the latter the rules B, C, W, K were in reality axiom-schemes, and their postulation amounted to assuming infinitely many axioms. Rosser had rules of procedure such that no propositions were deducible from them except in combination with axioms (or previously proved propositions); moreover, the conclusion of each rule was uniquely determined by the premises. He also eliminated equality as a primitive term, defining it (essentially) according to the traditional method. This paper shows that these and related advantages apply to certain formulations of the full system of combinatory logic, so far as it concerns the theory of combinators.The method of procedure is as follows. Instead of setting up a primitive frame at the start and then deriving its properties, I begin (after some preliminary explanations in §2) by stating in §3 the properties which it is desired to establish. The next few sections are devoted to the formulation and proof of certain general theorems concerning possible bases for the system of §3. These theorems are, perhaps, more general than is necessary for the immediate purpose, but they are of some interest on their own account. A formulation in terms of the primitives of original system (i.e., B, C, W, and K), which is of the same general type as Rosser's formulation, is obtained at the end of §6. In §7 are discussed the changes in this formulation which are sufficient in order to base it on the primitive combinators S and K of Schönfinkel.
Consistency and completeness of the theory of combinators
Authors: Curry Haskell B. 
Published: May 2006

The consistency of the theory of combinators, when based on the combinatory axioms, the rules of equality, and the equationswas proved in my thesis; likewise some theorems expressing certain completeness properties of this theory of combinatory equivalence formed the principal subject of that thesis and a succeeding paper. Further theorems of this sort were later demonstrated by Rosser; his theorems are, in some cases, more powerful than those just mentioned, but they apply to a weakened system. The purpose of this note is to discuss the extension of these theorems to the case where the whole of the theory of combinators is taken into account, and the rules for equality are derived from more fundamental considerations.The paper is based on a formulation of the theory of combinators contained in a previous paper, acquaintance with which is presupposed.A key theorem in investigations of this character is a theorem proved in 1936 by Church and Rosser. It is necessary to give a brief account of this theorem together with a generalization of it.The theorem concerns a certain formalism, which I shall here call the λ-formalism. The terms of this formalism, which I shall call λ-terms, are constituted as follows. For primitive terms we have an infinite set of variables, together with certain constants, the nature of which is arbitrary. Further terms are formed by two operations: a binary operation (analogous to application in the theory of combinators) which combines two λ-terms and to form a new λ-term here symbolized by ; and another binary operation combining a variable x and a term containing x as free variable to form a term .
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.
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 form1.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 formwhere ‘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α denoteThenNote 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 immediatelyTheorem 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.
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 axiomCCCCpqqrCCCpqrras 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.
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 thatHere 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 βγ.
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 aswhere 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]).