bluuebunny/crossref_metadata_2025_split huggingface dataset:
A note on two-place predicates and fitting sequences of measure functions
Authors: Rubin Herman , Suppes Patrick 
Published: May 2006

Carnap (in [1], p. 566) has remarked that his measure function m* is fitting for finite languages using a fixed number of one-place predicates, i.e., for any sentence i, m*(i) is the same in all such restricted finite languages in which i occurs. The main purpose of this brief note is to show by means of a counter-example that m* does not have the intuitively desirable property of fittingness when we consider languages using two-place predicates.We first state for finite languages a general theorem (related to the results in [2]) which guides the construction of large numbers of counter-examples.Theorem. Let be the symmetric group of n letters. In a language which consists of a finite number of predicates and n individual names, the number of state descriptions in a structure description is equal to the index of some subgroup G in .Proof. Let Σ be a structure description (of a language satisfying our hypothesis) and let S be an arbitrary state description in Σ. Let π be a permutation in , and let π*S be the state description which results from S by applying the permutation π to the individual names of . It is easily verified that for every π in π*S ∊ Σ. Also, for π, ψ in ,We define the set G of permutations as follows :.
Computational logic
Authors: Levin Nathan P. 
Published: May 2006

We make certain notational conventions. These are referred to as CL (Computational Logic). The relation of interchangeability is introduced as the basic connection between logical formulas. This approach lends perspicuity to the results of sentential calculus. With its technical devices CL is able to rephrase logical theorems in rather succinct manner. Our exposition tries to steer a middle course between informality and strict rigor.It is felt that the method of CL offers advantages for the teaching of logic. Proofs are algorithmic and resemble those of elementary algebra. All inferences are reversible and practically non-tentative.Sign is a primitive term of CL. Its denning property is a capacity for entering into binary combination with other signs, or with itself, according to this convention:x and y are signs if, and only if, (x y) is a sign. Bracketing is looked upon as an operation on signs in terms of which other operations are definable. The practice of some authors in classifying brackets under the heading of symbols, seems to us questionable; for unlike symbols or signs brackets are never used to denote anything. Brackets enter into the composition of signs, not to denote a grouping, but rather to exhibit it, in the manner of a diagram.An unending list of letters, with or without subscripts,serve to denote arbitrary signs. An arbitrary sign may or may not have other signs as parts. The numeral “2” is used as a constant. Bracketing abbreviation is as follows:and so on. Outermost brackets will ordinarily be omitted. This kind of bracketing may be termed left-associative. For convenience, these bracketing conventions are crystallized into a rule.
A problem in recursive function theory
Authors: Goodstein R. L. 
Published: May 2006

In a recent paper [4] on mean value theorems in recursive function theory we proved the theorem that(A) iff(n, x) is relatively differentiable with a relative derivative f1(n, x), for a ≤ x ≤ b, and if f(n, a) = f(n, b) = 0 relative to n,then there is a recursive function ck, a < ck < b, and a recursive R(k) such that f1(n, ck) = 0(k) for n ≥ R(k); and we showed further that the added condition(B) f(n, x) is either relatively variable or relatively constantsuffices to ensure that ck is uniformly contained in (a, b), i.e. that there exist α, β such thatA comparison with the conditions under which Rolle's theorem is established in classical analysis suggests that clause (A) itself might suffice to ensure that ck is uniformly contained in (a, b); for in the classical theory there is a single point c, a < c < b, for which lim f1(n, c) = 0, and therefore f1(n, c) = 0(k) for sufficiently great values of n, where of course c is independent of k.The object of the present note is to show that this is not in fact the case, and we shall construct a recursive function f(n, x) satisfying condition (A) in the interval (0, 1) and such that any sequence ck for which f1(n, ck) = 0(k) for large enough values of n is not uniformly contained in (0, 1).
New sets of postulates for combinatory logics
Authors: Rosser Barkley 
Published: May 2006

Sets of postulates for at least three different combinatory logics have been given ([2], [3], [4], [5], [6], [7]). The logics and their sets of postulates are quite similar. In all cases it is the proof of the completeness of the set of postulates which causes the difficulty and makes the main papers so long ([3], [7]). It is the purpose of this paper to present a method of writing down sets of postulates for combinatory logics for which the proof of completeness will be fairly simple. We assume acquaintance with certain descriptive portions of [1], namely sections 1–6, 12, 13, 15. Otherwise the present paper is self-contained.We first solve our problem for the particular logic studied by Rosser ([7]) and then indicate how the method would apply to other logics.We start with a set, s, of primitive terms. We define s-combination as in [1], p. 43. The precise contents of s need not concern us. It suffices that there be s-combinations I, J, and Q, with no variables in them, and having properties as described below. I and J are to have the same meaning as in [1], p. 43, namely IA is the same as A and JABCD is the same as AB(ADC). QAB is to have the meaning that A and B, considered as functions, are the same.
A formal theorem in Church's theory of types
Authors: Newman M. H. A. , Turing A. M. 
Published: May 2006

This note is concerned with the logical formalism with types recently introduced by Church [1] (and called (C) in this note) It was shewn in his paper (Theorem 26α) that if Yα stands for(a form of the “axiom of infinity” for the type α), Yα can be proved formally, from Yι and the axioms 1 to 7, for all types α of the forms ι′, ι″, …. For other types the question was left open, but for the purposes of an intrinsic characterisation of the Church type-stratification given by one of us, it is desirable to have the remaining cases cleared up. A formal proof of Yα is now given for all types α containing ι, but the proof uses, in addition to Axioms 1 to 7 and Yι, also Axiom 9 (in connection with Def. 4), and Axiom 10 (in Theorem 9).
A system of completely independent axioms for the sequence of natural numbers
Authors: Wang Shianghaw 
Published: May 2006

Peano's five axioms for the sequence of natural numbers run as follows: (1) 1 is a number, (2) Any number α has a unique sequent a′ (3) Different numbers have different sequents, (4) 1 is not a sequent, and (5) The principle of mathematical induction.Now, in a system of axioms, it seems desirable, in the first place, to avoid symbols for particular individuals and symbols for functions, and, secondly, to secure the property of complete independence. In fact, Peano's system can be replaced by an equivalent one which fulfills both requirements. In such a system, the symbol “1” and the function “sequent” will not appear, although they may be introduced afresh through definitions. Besides, the principle of mathematical induction will no more play the rôle of an axiom, because, under the second requirement, it can hardly be stated in a simple and elegant form.
Remark on Nicod's reduction of Principia mathematica
Authors: Bernstein B. A. 
Published: May 2006

The object of this note is to close a slight gap, hitherto seemingly over-looked, in Nicod's derivation from his postulates of the primitives of Principia mathematica. The gap consists in this: Nicod's propositions corresponding to *1·1−*1·6 of the Principia, though they bear the same names and have the same symbol-forms as the Principia propositions, are not precisely *1·1−1·6. Indeed, if we denote Nicod's “p ⊃ q” and “p · q” by “p < q” and “pq” respectively, and if we write p′ for p∣p and p″ for (p′)′ then in terms of the “stroke,” we haveBut p ⊃ q and p · q of the Principia areAccordingly, the Nicod-Principia propositions are not *1·1−*1·6. They are *1·1−*1·6 in which < takes the place of ⊃, and Nicod has not shown us explicitly how to pass from < to ⊃.It is true that Nicod also proves the following:i.e.,This yields: If ⊢· p < q then ⊢· p ⊃ q, and conversely. This would seem to allow passing from < to ⊃ throughout a proposition. But, it is clear, T1 permits this change only in the case of the principal <. The change in the case of a minor < still has to be justified.
A new approach to semantics – Part I
Authors: Kemeny John G. 
Published: May 2006

This is the first in a series of articles outlining a new approach to Semantics. The novelty in the approach is that the concept of an interpretation of a logical system is taken as the central concept of Semantics. I hope to show that by means of this approach a satisfactory definition can be given for such controversial concepts as analyticity, and at the same time the approach leads to a unified foundation for formalized Semantics.As the possibility of such definitions has been questioned in recent years, it is an important task to try to give precise definitions. Clearly, this is the task of those philosophers who believe that concepts like analyticity should play a fundamental role in Semantics. On the other hand, the philosophers who have criticized these concepts will now be able to tell just exactly why these definitions are unacceptable to them — instead of being forced to talk in generalities. It seems to me that no further progress is possible until we have precise definitions available for discussion.The fundamental semantic concepts fall into two classes: those, like truth, for which Tarski has offered definitions; and those additional ones, like analytic truth, for which we have Carnap's proposed definitions.
Ideographic computation in the propositional calculus
Authors: Standley Gerald B. 
Published: May 2006

This paper will be concerned with an adaptation of Parry's trapezoid symbolism to the solving of problems.In Parry's notation ‘pq’, in particular, sets forth the relationship that obtains when p is true, whether q be true or false. The symbol may also be regarded as manifesting the matrix analysis of p. It is this aspect which offers promise for manipulation. We propose to write the symbol ‘’ for p itself. It is to be kept in mind, however, that ‘’ is the symbol of p when there are but two variables. How to proceed when there are more than two will be seen later.The symbol for q will in like manner be ‘⌋’.Let ‘’ and ‘’, then, be regarded as elemental symbols setting forth the matrix analysis of the variables. Suppose further that in transcribing from conventional to the trapezoid symbolism we substitute for the variables only, retaining the constants (antithetically to Parry's procedure). Thus ‘p ∨ q’ becomes, not ‘pq’ as with Parry, but ‘ ∨ ’. Problem-solving consists of merging the trapezoidal symbols according to procedures specified by the constants. As symbols are merged, the constants are eliminated.The resultant symbol constitutes the solution.The rules for merging symbols are derived from the elementary processes of forming truth-tables:Disjunction of two symbols consists of superimposing them.Conjunction consists of preserving only such sides as are common to both the conjoined symbols.
Some formal relative consistency proofs
Authors: McNaughton Robert 
Published: May 2006

These systems are roughly natural number theory in, respectively, nth order function calculus, for all positive integers n. Each of these systems is expressed in the notation of the theory of types, having variables with type subscripts from 1 to n. Variables of type 1 stand for natural numbers, variables of type 2 stand for classes of natural numbers, etc. Primitive atomic wff's (well-formed formulas) of Tn are those of number theory in variables of type 1, and of the following kind for n > 1: xi ϵ yi+1. Other wff's are formed by truth functions and quantifiers in the usual manner. Quantification theory holds for all the variables of Tn. Tn has the axioms Z1 to Z9, which are, respectively, the nine axioms and axiom schemata for the system Z (natural number theory) on p. 371 of [1]. These axioms and axiom schemata contain only variables of type 1, except for the schemata Z2 and Z9, which are as follows:where ‘F(x1)’ can be any wff of Tn. Identity is primitive for variables of type 1; for variables of other types it is defined as follows:
A theorem on deducibility for second-order functions
Authors: Langford C. H. 
Published: May 2006

It is known that the usual definition of a dense series without extreme elements is complete with respect to first-order functions, in the sense that any first-order function on the base of a set of postulates defining such a series either is implied by the postulates or is inconsistent with them. It is here understood, in accordance with the usual convention, that when we speak of a function on the base , the function shall be such as to place restrictions only upon elements belonging to the class determined by f; or, more exactly, every variable with a universal prefix shall occur under the hypothesis that its values satisfy f, while every variable with an existential prefix shall have this condition categorically imposed upon it.Consider a set of postulates defining a dense series without extreme elements, and add to this set the condition of Dedekind section, to be formulated as follows. Let the conjunction of the three functions,be written H(ϕ), where the free variables f and g, being parameters throughout, are suppressed. This is the hypothesis of Dedekind's condition, and the conclusion iswhich may be written C(ϕ).
Definition by induction in quine's new foundations for mathematical logic
Authors: Bosser Barkley 
Published: May 2006

In Quine's New foundations the axiom of infinity does not appear to be provable. In a certain stronger system, very closely related to Quine's New foundations, the axiom of infinity is provable. One of the peculiarities of this latter system is that even unstratified propositions can be proved by induction (this is used in the proof of the axiom of infinity). It would seem that definition by induction should also be possible quite irrespective of any conditions of stratification in this latter system. In this paper it is shown that such is the case.Theorem. If α, α1, α2, …, αs are any classes, and if there is no confusion of bound variables in {Sxp}(v) or {Sxq}(v) and neither z nor v occurs free in p or q, and if⊦ (y1, y1, … ys):. y1ϵα1 . y2ϵα2 . … . ysϵαs : ⊃ : (Ez) : zϵα : (v) : v . ≡ . {Sxp}(v),⊦ (y, n, y1, y2, …, ys) :. yϵα . n ϵ Fin . y1ϵα1 . y2ϵα2. … . ysϵαs : ⊃ : (Ex) :zxα : (v) : v=z . ≡ . {Sxq}(v),then there is an r such thai there is no confusion of bound variables in {Sxr}(v) and neither z nor v occurs free in r, and⊦ (n, y1, y2, …, ys) :. nϵ Fin . y1ϵα1 . y2ϵα2 . … . ysϵαs : ⊃ : (Ez) : zϵα : (v) : v=z . ≡ . {Sxr}(v),⊦ (y1, y2, …, ys) : y1ϵα1 . y2ϵα2 . … . ysϵαs . ⊃ . ιx{Snr}(0) = ιxp,⊦ (n, y1, y2, …, ys) : nϵ Fin . y1ϵα1 . y2ϵα2 . … . ysϵαs . ⊃ . ιx{Snr}(n+1) = ιx{Syq}(ιxr).
Independent axiom schemata for S5
Authors: Anderson Alan Ross 
Published: May 2006

Leo Simons has shown that H1—H6 below constitute a set of independent axiom schemata for S3, with detachment for material implication “→” as the only primitive rule. He also showed that addition of the scheme (◇ ◇ α ⥽ ◇ α) yields S4, and that these schemata for S4 are independent. The question for S5 was left open. We shall show (presupposing familiarity with Simons' paper) that H1—H6 and S, below, constitute a set of independent axiom schemata for S5, with detachment for material implication as the only primitive rule.Let S5′ be the system generated from H1—H6 and S with the help of the primitive rule. It is easy to see that Simons' derivations of the rules (a) adjunction, (b) detachment for strict implication, and (c) intersubstitutability of strict equivalents, may be carried out for S5′. We know that (1) (∼ ◇ ∼ α ⥽ ◇ α) is provable in S2, hence also in S3 and S5′; and (1) and S yield (2) (α ⥽ ∼ ◇ ∼ ◇ α). Perry has shown that addition of (2) to S3 yields S5, so S5 is a subsystem of S5′. And it is easy to prove S in S5; hence the systems are equivalent.
Some applications of infinitely long formulas
Authors: Keisler H. Jerome 
Published: May 2006

Introduction. This paper is a sequel to our paper [3]. In that paper we introduced the notion of a finite approximation to an infinitely long formula, in a language L with infinitely long expressions of the type considered by Henkin in [2]. The results of the paper [3] show relationships between the models of an infinitely long sentence and the models of its finite approximations. In the present paper we shall apply the main result of [3] to prove a number of theorems about ordinary finitely long sentences; these theorems are of a type which one might call “preservation theorems”. The following two known results are typical preservation theorems: A sentence φ is preserved under substructures if and only if φ is (logically) equivalent to some universal sentence (Łoś [7] and Tarski [11]); φ is preserved under homomorphic images if and only if φ is equivalent to some positive sentence (Lyndon [8]). An expository account of preservation theorems may be found in Lyndon [9].We shall use freely all of the notation introduced in [3], and shall not attempt to make this paper selfcontained. However, the reader should have no difficulty following this paper after he has read [3]. In § 1 we cover some preliminary topics. In § 2 and § 3 we shall illustrate our method in familiar situations by proving anew the two preservation theorems mentioned above. We shall then obtain four new preservation theorems in §§ 4, 5, and 6, involving respectively direct powers and roots, strong homomorphisms and retracts, and direct factors. The result in § 6 was stated in the abstract [4], while the results in § 5 were stated in the abstract [5].
Constructive order types, II
Authors: Crossley John N. 
Published: May 2006

In this paper we continue the investigations begun in [2] of equivalence classes of (denumerable) well-orderings under one-one partial recursive, order-preserving maps (recursive isotonisms). The numbering and notation are continued from [2] except that we now use lower case Greek letters for classical ordinals and upper case Roman letters for sets and we slightly modify the definition of (see §IX.3).In section IX, after proving some lemmata which we use repeatedly in this paper, we establish the existence of Cantor Normal Forms for all co-ordinals less than a co-ordinal of the form WA (a fortiori for all co-ordinals less than a principal number for exponentiation).
On the completeness of some transfinite recursive progressions of axiomatic theories
Authors: Erik Fenstad Jens 
Published: May 2006

The well-known incompleteness results of Gödel assert that there is no recursively enumerable set of sentences of formalized first order arithmetic which entails all true statements of that theory. It is equally well known that by introducing sufficiently nonconstructive rules, such as the ω-rule of induction, completeness can be re-established.Starting from the work of Turing [4] Feferman in [1] developed another method, viz. the study of transfinite recursive progressions of theories, for closing the gap between Gödel (recursively enumerable sets of axioms yield incompleteness) and Tarski (number-theoretic truth is not arithmetically definable).
Comments on a variant form of natural deduction
Authors: Parry William Tuthill 
Published: May 2006

This note shows that the system of natural deduction proposed by Copi in this Journal (1956), made by varying one restriction on Universal Generalization (UG) of the system of his Symbolic logic (1954), is incorrect. The original Symbolic logic system, also incorrect, was corrected in the third printing (1958) by modification of another restriction on UG; but combining this modification with that of the Journal article does not give a correct system.1. In Symbolic logic — cited as SL (or as SL54 to indicate the first printing) — Copi precedes his formal statement of the quantification rules by a set of conventions applying to all the rules.The expression ‘Φμ’ will denote any propositional function in which there is at least one free occurrence of the variable denoted by ‘μ’. The expression ‘Φν’ will denote the result of replacing all free occurrences of μ in Φμ by ν, with the added provision that [a] when ν is a variable it must occur free in Φν at all places at which μ occurs free in Φμ.The italicized provision we call Restriction a. In the third printing of Symbolic logic — cited as SL58 — Restriction a appears explicitly as part of each of the four quantification rules.
Recursively enumerable sets which are uniform for finite extensions
Authors: Alton Donald A. 
Published: May 2006

Let W0, W1 … be one of the usual enumerations of recursively enumerable (r.e.) subsets of the set N of nonnegative integers. (Background information will be given later.) Suggestions of Anil Nerode led to the followingDefinitions. Let B be a subset of N and let ψ be a partial recursive function.
A model theoretic characterization of effective operations
Authors: Löb M. H. 
Published: May 2006

Let be a standard formalization of type theory. In [6] Kreisel introduced N-models for . These are general models in the sense of [1] in which the numerals have their standard denotations.If ξ is a closed term of we shall denote the object denoted by ξ in the N-model M by ξM. In particular, ξ* is the object denoted by ξ in the standard model of .
On the logic of incomplete answers
Authors: Cresswell M. J. 
Published: May 2006

I have argued in [1] that a concept bearing some resemblance to ‘p is the answer to d’ (p a proposition and d a question) can be defined wherever d has the form,‘For which a's is it the case that A (a)?’ (Qa)A(a)where a is a variable and A a wff containing a. To say that p is the true and complete answer to (Qa)A(a) is expressed as saying that p is logically equivalent to the true conjunction of A(a) or ~A(a) for each a. It is defined as;Such a concept of answer is like Belnap's [2] direct true answer to a complete list question, or like Harrah's use [3] (p. 43) of the notion of a state description. The main difference between my approach and that of Belnap and Harrah is that while they are concerned to develop a formal metalanguage for discussion of questions and answers I am concerned to express, as far as possible in existing systems, certain interrogative statements; in particular statements of the form ‘— is the (an) answer to —’.While the account in [1] does give a formal analysis of one ‘answer’ concept there are respects in which it is inadequate.1. Since it uses entailment (or strict implication) to define the relation between p the answer and d the question we can shew that if p is the answer to d and q is logically equivalent to p then q is the answer to d.
There exist two regressive sets whose intersection is not regressive
Authors: Appel K. I. 
Published: May 2006

§1. In [2], as part of an analogy between the concepts of recursive emimerability and regressiveness, Dekker showed that the intersection of any two regressive sets which are recursively equivalent is a regressive set. In [1], McLaughlin and the author showed that the intersection of two regressive sets, if infinite, has an infinite regressive subset. However, the following theorem shows that the analogy is not complete in this instance.Theorem. There exist two regressive sets whose intersection is not regressive.