bluuebunny/crossref_metadata_2025_split huggingface dataset:
A formulation of the simple theory of types
Authors: Church Alonzo 
Published: May 2006

The purpose of the present paper is to give a formulation of the simple theory of types which incorporates certain features of the calculus of λ-conversion. A complete incorporation of the calculus of λ-conversion into the theory of types is impossible if we require that λx and juxtaposition shall retain their respective meanings as an abstraction operator and as denoting the application of function to argument. But the present partial incorporation has certain advantages from the point of view of type theory and is offered as being of interest on this basis (whatever may be thought of the finally satisfactory character of the theory of types as a foundation for logic and mathematics).For features of the formulation which are not immediately connected with the incorporation of λ-conversion, we are heavily indebted to Whitehead and Russell, Hilbert and Ackermann, Hilbert and Bernays, and to forerunners of these, as the reader familiar with the works in question will recognize.The class of type symbols is described by the rules that ı and o are each type symbols and that if α and β are type symbols then (αβ) is a type symbol: it is the least class of symbols which contains the symbols ı and o and is closed under the operation of forming the symbol (αβ) from the symbols α and β.
On the definition of negation by a fixed proposition in inferential calculus
Authors: Curry Haskell B. 
Published: May 2006

It is well known that negation can be defined by postulating a fixed proposition F and specifying thatwhere “≡” indicates identity by definition. I propose to discuss this way of introducing negation in relation to the inferential systems of my Notre Dame lectures of 1948. Acquaintance with these lectures is presupposed; they will be referred to as TFD. The definition (1) was used there, essentially, in connection with the T-systems; but it was not used in connection with the L-systems because of a certain difficulty which I was not able to overcome at that time. This paper contains proofs of results concerning L-systems which have been announced elsewhere.
Arithmetical problems and recursively enumerable predicates
Authors: Davis Martin 
Published: May 2006

It is an immediate consequence of results of Church and Gödel that there exist arithmetical recursively unsolvable problems, that is, recursively unsolvable problems of the form [M](P = Q) where P and Q are polynomials and [M] is some finite sequence of existential and universal quantifiers. A question which is immediately raised by this result is whether there exist unsolvable problems of this form where [M] is some finite sequence of existential quantifiers only. As a matter of fact this question is easily seen to be closely related to the tenth problem in the famous list proposed by Hilbert in 1900.In this paper, we prove the existence of recursively unsolvable problems of the formwhere P and Q are polynomials with non-negative integral coefficients. As a matter of fact we show that every recursively enumerable predicate is of the form (1), and conversely that every predicate of the form (1) is recursively enumerable. While our result does not yield the recursive unsolvability of Hilbert's tenth problem, it is easily seen that any considerable improvement of our result would yield this unsolvability.The author wishes to take this opportunity to express his gratitude to Professors Alonzo Church and E. L. Post with whom he has had the privilege of discussing some of the questions involved in this paper. He also wishes to thank his friends Melvin Hausner and Jacob Schwartz who have made valuable suggestions.
On the rules of proof in the pure functional calculus of the first order
Authors: Mostowski Andrzej 
Published: May 2006

We consider here the pure functional calculus of first order as formulated by Church.Church, l.c., p. 79, gives the definition of the validity of a formula in a given set I of individuals and shows that a formula is provable in if and only if it is valid in every non-empty set I. The definition of validity is preceded by the definition of a value of a formula; the notion of a value is the basic “semantical” notion in terms of which all other semantical notions are definable.The notion of a value of a formula retains its meaning also in the case when the set I is empty. We have only to remember that if I is empty, then an m-ary propositional function (i.e. a function from the m-th cartesian power Im to the set {f, t}) is the empty set. It then follows easily that the value of each well-formed formula with free individual variables is the empty set. The values of wffs without free variables are on the contrary either f or t. Indeed, if B has the unique free variable c and ϕ is the value of B, then the value of (c)B according to the definition given by Church is the propositional constant f or t according as ϕ(j) is f for at least one j in I or not. Since, however, there is no j in I, the condition ϕ(j) = t for all j in I is vacuously satisfied and hence the value of (c)B is t.
On the paradox of grounded classes
Authors: Montague Richard 
Published: May 2006

Mr. Shen Yuting, in this Journal, vol. 18, no. 2 (June, 1953), stated a new paradox of intuitive set-theory. This paradox involves what Mr. Yuting calls the class of all grounded classes, that is, the family of all classes a for which there is no infinite sequence b such that … ϵ bn ϵ … ϵ b2ϵb1 ϵ a.Now it is possible to state this paradox without employing any complex set-theoretical notions (like those of a natural number or an infinite sequence). For let a class x be called regular if and only if (k)(x ϵ k ⊃ (∃y)(y ϵ k · ~(∃z)(z ϵ k · z ϵ y))). Let Reg be the class of all regular classes. I shall show that Reg is neither regular nor non-regular.Suppose, on the one hand, that Reg is regular. Then Reg ϵ Reg. Now Reg ϵ ẑ(z = Reg). Therefore, since Reg is regular, there is a y such that y ϵ ẑ(z = Reg) · ~(∃z)(z ϵ z(z = Reg) · z ϵ y). Hence ~(∃z)(z ϵ ẑ(z = Reg) · z ϵ Reg). But there is a z (namely Reg) such that z ϵ ẑ(z = Reg) · z ϵ Reg.On the other hand, suppose that Reg is not regular. Then, for some k, Reg ϵ k · [1] (y)(y ϵ k ⊃ (∃z)(z ϵ k · z ϵ y)). It follows that, for some z, z ϵ k · z ϵ Reg. But this implies that (ϵy)(y ϵ k · ~(ϵw)(w ϵ k · w ϵ y)), which contradicts [1].It can easily be shown, with the aid of the axiom of choice, that the regular classes are just Mr. Yuting's grounded classes.
Closure and Quine's *101
Authors: Fitch Frederic B. 
Published: May 2006

The purpose of this paper is to suggest two alternatives to Quine's definition of closure. These new definitions have two advantages over Quine's definition, and they probably are the simplest definitions having both advantages. The two advantages are:(1). Principle *101 becomes superfluous and may be dropped from Quine's set of principles for quantification. (In the case of my second definition, however, the dropping of *101 must be balanced by a slight change in *104.)(2). Closure is made independent of the alphabetical order of variables.The second of these advantages turns on the fact that the “alphabetical order” possessed by variables in virtue of their respective positions in the alphabet (or arbitrarily assigned to them) is a mere convention and not of genuine logical significance. It seems therefore desirable to consider some alternatives to Quine's definition of closure, since according to his definition the closure of a given formula will be one statement or another, depending upon whether or not one letter of the alphabet is alphabetically prior to a certain other letter. It is interesting that the removal of this minor artificiality also enables us to dispense with *101.According to Quine, the closure of a formula containing n free variables is obtained by prefixing to it in alphabetical order the n universal quantifiers formed from these variables by enclosing each in a pair of parentheses. (If n = 0 the formula is its own closure and is a “statement” rather than a “matrix.”) Thus the statement ‘(x)(y)(z)(xϵy ▪ yϵz)’ would be the closure of ‘xϵy ▪ yϵz’, but ‘(z)(x)(y)(xϵy ▪ yϵz)’ would not be its closure. Now there is no reason why ‘(z)(x)(y)(xϵy ▪ yϵz)’ or (y)(z)(x)(xϵy ▪ yϵz) and so on, could not just as well be regarded as “the” closure of ‘(xϵy ▪ yϵz’ as ‘(x)(y)(z)(xϵy ▪ yϵz)’. I therefore propose to allow to each formula not merely one closure, but as many closures as can be obtained by permuting in various ways the n prefixed universal quantifiers. In this way alphabetical order becomes irrelevant and no preference is given to one order of prefixed quantifiers in contrast to other orders which seem equally good. This constitutes my first redefinition of closure.
Undecidable sentences generated by semantic paradoxes
Authors: Wang Hao 
Published: May 2006

In applying the method of arithmetization to a proof of the completeness of the predicate calculus, Bernays has obtained a result which, when applied to set theories formulated in the predicate calculus, may be stated thus.1.1. By adding an arithmetic sentence Con(S) (expressing the consistency of a set theory S) as a new axiom to the elementary number theory Zμ (HB II, p. 293), we can prove in the resulting system arithmetic translations of all theorems of S.It then follows that things definable or expressible in S have images in a simple extension of Zμ, if S is consistent. Since S can be a “strong” system, this fact has interesting consequences. Some of these are discussed by me and some are discussed by Kreisel. Kreisel finds an undecidable sentence of set theory by combining 1.1 and the Cantor diagonal argument. I shall prove below, using similar methods, a few further results, concerned with the notions of truth and designation. The method of numbering sets which I use (see 3.1 below) is different from Kreisel's. While the method used here is formally more elegant, Kreisel's method is much more efficient if we wish actually to calculate the numerical values.
The use of dots as brackets in Church's system
Authors: Turing A. M. 
Published: May 2006

Any logical system, if its use is to be carried beyond a rather elementary stage, needs powerful conventions about abbreviations: in particular one usually wants to modify the bracketing so as to make the formulae more readable, and also possibly shorter. The present note has been written in the belief that Church's formulation of the simple theory of types is particularly suitable as a basis for work on that theory, and that it is therefore worth while introducing special conventions which take into account the needs of this particular system. The conventions which I shall describe are ones which I have used a good deal myself, and have always found adequate. I intend to make use of them in forthcoming papers. They may be regarded as an extension of Curry's conventions.I shall begin with a general discussion of punctuation by means of groups of dots. This general theory is applicable, with some modifications, to Russell's, Quine's, and Curry's bracketing systems as well as to the present one.
Logic based on inclusion and abstraction
Authors: Quine W. V. 
Published: May 2006

All notions of mathematical logic, as measured e.g. by Principia mathematica, can be constructed from a basis which embraces variables and just two further primitives: the familiar notions of inclusion and abstraction. Inclusion will be expressed by the usual form of notation “(x⊂y)”, which may be read “x is included in y.” Abstraction will be expressed by the form of notation “x3 …” as with Peano, the blank being filled by any formula (statement or statement form); the whole may be read “the class of all objects x such that ….”A system of logic based on these primitives will be presented in this paper. The system involves the familiar theory of class types, which, for metamathematical convenience, will be recorded in the system by use of distinctive styles of variables; thus the variables “x”, “y”, and “z”, also with subscripts when further variety is needed, will take individuals as values; the variables “x′”, “y′”, and “z′”, also with subscripts, will take classes of individuals as values; the variables “x″”, “y″”, and “z″”, also with subscripts, will take classes of classes of individuals as values; and so on. The metamathematical notion of term, covering all variables and also all expressions of abstraction, is now describable recursively thus: a variable is a term, and the number of accents which it bears is called its rank; and if terms of equal rank are put for “ζ” and “η” and a variable of rank n is put for “α” in “α3(ζ ⊂ η)”, the result is a term of rank n+1. A formula finally, is any result of putting terms of equal rank for “ζ” and “η” in “(ζ ⊂ η)”.
Formal systems of constructive mathematics
Authors: Löb M. H. 
Published: May 2006

In the present paper we investigate in some detail two systems closely related to those contained in [4]. The system K1 of [4] is simplified by eliminating conjunction and disjunction, giving rise to a system Σ whose primitives are two individuals, concatenation, identity, existential and limited universal quantification. Any relation expressible in Σ may be expressed in the form (Eα1)(β)α1(Eα2)…(Eαn)(γ = δ). A further reduction of primitives leads to a system Σμ, which differs from Σ by containing the operator μ (i.e. “the first string, such that” with respect to a certain ordering) in place of the quantifiers. Reasons are given for restricting Myhill's definition of constructive ideas to those expressible in Σμ.Acquaintance with [4], [5], [6] is assumed. We deviate from [4] by dropping concatenation-signs and parentheses in chain matrices from the official notation, and, furthermore, by using Greek and German letters as metalinguistic variables standing for chain matrices and chains, respectively, while retaining small Roman letters (excluding a, b) for use as variables of the systems.
A theorem about infinite-valued sentential logic
Authors: McNaughton Robert 
Published: May 2006

In this paper we shall use a logic with truth values ranging over all the real numbers x such that 0 ≦ x ≦ 1.1 will be “complete truth” and 0 will be “complete falsity.” The primitive sentential connectives are ‘⊃’ and ‘∼’; other connectives are ‘∨’ and ‘·’. Assume that ‘p’ and ‘q’ are sentential variables, whose truth values are respectively x and y. Then1.1. ‘p ⊃ q’ has the value min(1 − x + y, 1),1.2. ‘∼p’ has the value 1 − x,1.3. ‘p∨q’ has the value max(x, y), and1.4. ‘p·q’ has the value min (x, y).‘∨’ and ‘·’ can be defined as follows:It is the purpose of this paper to prove a theorem which will be stated in the next section. The following symbolism and convention will be used throughout the paper:S is a logical formula.ν (S) is the value of S.‘p’, ‘pi1, ’p2, …, ‘q’, are sentential variables.ν(p) = x and ν(x1) = x1, etc.ν(S) = σ and ν(S1) = σ1, etc.If S contains the sentential variables ‘p1’, ‘p2’, …, then we write for S, S(p1, P2, …). Also ν{S(p1, p2, …)) = σ(x1, x2, …).A logical formula is defined in the usual manner. 1. A sentential variable is a logical formula; 2. if S is a logical formula then ·S is a logical formula; and 3. if S and S′ are logical formulae then (S ⊃ S′) is a logical formula.
Symbols, signs, and signals
Authors: Ducasse C. J. 
Published: May 2006

In this address, no attempt to deal with any problem of symbolic technique will be made, for even if a problem of this kind should be found that was suitable to the present occasion, I should probably lack sufficient competence in the handling of symbols to deal with it satisfactorily. It occurred to me, however, that it might be interesting to consider the nature of symbols in general, to point out certain characteristics peculiar to the symbols used by logicians and mathematicians, and to say something concerning the relations of these symbols to the knowledge of Nature. Although developments in the science of logic are not dependent on such an inquiry, it yet provides us with a perspective on the nature and importance of that science which we cannot gain so long as we attend only to the problems arising inside its field.The symbolic relation. Our attempt to gain this perspective may well begin with the trite remark that nothing is intrinsically a symbol, but that anything is a symbol if and only if it symbolizes. Moreover, the relation called symbolizing is not a dyadic but rather a tetradic relation. That is, in order for something A to be a symbol of something B, there must be in addition C, a mind trained in a special way, and D, a certain manner in which that mind is occupied at the time. For although we do say, for instance, that a mark consisting of a little cross is the symbol of addition, the fact is of course that at times when that mark is not present to a mind, it does not symbolize addition or anything else. Moreover, even when it is present to a mind, it does not symbolize addition unless that mind has been trained in a certain manner; for obviously such a mark does not symbolize addition to the mind of a Hottentot or other wholly illiterate person.
A basic logic
Authors: Fitch Frederic B. 
Published: May 2006

This paper is concerned with finding a fairly simple system of logic which is “basic” in the sense that every system of logic is definable in it. If a “system”is regarded as being a class of propositions, rather than a class of sentences, then every class of propositions which is a system should be definable in the basic logic. The system of logic proposed in this paper will not be proved to be a basic logic, but strong evidence that it is basic will be given at the end of the paper. Evidence will also be given that the class of propositions which are not provable in the system is not definable in any system of logic. It will be established that the decision problem is unsolvable for the system. Notable characteristics of the system are its lack of negation and universal quantification, and its similarity to systems proposed by Church, Curry, and Rosser.By a “system” will be meant a class of propositions the membership of which can be specified by ordinary recursive methods, so that if the membership of a given proposition in the class can be established at all, such membership can be established in a finite number of steps. (This is not the same as demanding that a criterion must exist for determining, in a finite number of steps, whether or not some given proposition is a member of the class. Such a demand would require a solution of the decision problem for every system.)
Two additions to positive implication
Authors: Prior A. N. 
Published: May 2006

Let LIC be the implicational fragment of Dummett's LC, axiomatised by Bull in [1] by adding the axiom (L) CCCpqrCCCqprr to positive implication. The system which Bull in [2] calls OIC, i.e. positive implication plus (0) CCCCpqqrCCCpqrr, is contained in LIC (it is thesis 34 in [1], p. 193); but it does not contain it, as the following matrix (due to Bull)
verifies OIC but not (L) (CCC342CCC4322 = 2). Nor is (L) deducible in OIC supplemented by intuitionist axioms for negation, since the latter are all verified by the above matrix with Cp5 for Np.
A minimal pair of recursively enumerable degrees
Authors: Yates C. E. M. 
Published: May 2006

Our principal result is that there exist two incomparable recursively enumerable degrees whose greatest lower bound in the upper semilattice of degrees is 0. This was conjectured by Sacks [5]. As a secondary result, we prove that on the other hand there exists a recursively enumerable degree a < 0(1) such that for no non-zero recursively enumerable degree b is 0 the greatest lower bound of a and b.The proof of the main theorem involves a method that we have developed elsewhere [8] to deal with situations in which a partial recursive functional may interfere infinitely often with an opposed requirement of lower priority.
Nonstandard logic
Authors: Geiser James R. 
Published: May 2006

This paper is an exposition of the author's [2] investigations of a class of infinitary first order logics. These logics are sometimes characterized by saying that the syntactical role played by the positive integers in first order predicate logic is taken over by a nonstandard model of arithmetic. The result is then called a nonstandard logic.1 In particular the operations of conjunction, disjunction and quantification may be iterated infinitely (nonstandard finitely) often.When the nonstandard model of arithmetic is an ultra power, the natural class of structures in which to interpret the nonstandard wffs is a class of ultra products. Within this framework, many model-theoretic properties of ultra products become manifest in the logical structure of the nonstandard language.
There are infinitely many Diodorean modal functions
Authors: Makinson D. C 
Published: May 2006

It is well known that the modal calculus S4 has infinitely many non-equivalent formulae in a single proposition letter (in standard terminology, infinitely many modal functions), whilst S5 has only finitely many. However, the situation regarding the intermediate modal calculi S4.2, S4.3, and Prior's Diodorean tense-logic D does not seem to have been settled. In this note we show that each of these systems, together with a certain proper supersystem D* of D, has infinitely many modal functions.This is in contrast with the fact that in the intermediate propositional logics KC and LC, which correspond under the McKinsey-Tarski translations to S4.2 and S4.3, there are only finitely many non-equivalent formulae in a single proposition letter.2
On the notational independence of various hierarchies of degrees of unsolvability
Authors: Hensel Gustav , Putnam Hilary 
Published: May 2006

From the work of Kleene, Post and Davis it is well-known that the arithmetic sets can be characterized as those sets recursive in∅(n)for some natural numbern, where∅(0)=∅and. Actually the arithmetic sets which can be expressed in prenex form withnalternating quantifiers (applied to recursive predicates) are recursive in∅(n). Hence, starting with∅, the “jump operation”, which takes a set A into the set, serves to increase the “complexity” of sets in a uniform way.As far as extending the ω-sequence of degrees of unsolvability (i.e. the degrees represented by the∅(n)) into the 2nd number class, there is an immediate problem. One knows from Spector [17], corollary 2, p. 585, that there is no l.u.b. for the ω-sequence. So, at ω one must pick a degree in some other “natural” way. Unfortunately, what has seemed “natural” to some mathematicians has not seemed natural to others. Kleene and Davis (cf. [10] and [3] respectively) extended this arithmetic hierarchy of degrees of unsolvability by making use of natural number notations for a certain segment of ordinals of the 1st and 2nd number classes, the “constructive” ordinals. Using the Church-Kleene system S3, one can “sum up” previously obtained sets at the limit notations in a way that is certainly natural from a notational point of view.
A system of axiomatic set theory. Part V. General set theory (continued)
Authors: Bernays Paul 
Published: May 2006

We have still to consider the extension of the methods of number theory to infinite ordinals—or to transfinite numbers as they may also, as usual, be called.The means for establishing number theory are, as we know, recursive definition, complete induction, and the “principle of the least number.” The last of these applies to arbitrary ordinals as well as to finite ordinals, since every nonempty class of ordinals has a lowest element. Hence immediately results also the following generalization of complete induction, called transfinite induction: If A is a class of ordinals such that (1) ΟηA, and (2) αηA → α′ηA, and (3) for every limiting number l, (x)(xεl → xηA) → lηA, then every ordinal belongs to A.