Some theorems on definability and decidability

1952 ◽  
Vol 17 (3) ◽  
pp. 179-187 ◽  
Author(s):  
Alonzo Church ◽  
W. V. Quine
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
Natural Numbers ◽  
Quantification Theory ◽  
First Order ◽  
Dyadic Relation ◽  
Truth Value ◽  
Individual Variables

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 derivation of number theory from ancestral theory

1952 ◽  
Vol 17 (3) ◽  
pp. 192-197 ◽  
Author(s):  
John Myhill
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
Natural Numbers ◽  
Class Inclusion ◽  
First Order ◽  
Free Variables

Martin has shown that the notions of ancestral and class-inclusion are sufficient to develop the theory of natural numbers in a system containing variables of only one type.The purpose of the present paper is to show that an analogous construction is possible in a system containing, beyond the quantificational level, only the ancestral and the ordered pair.The formulae of our system comprise quantificational schemata and anything which can be obtained therefrom by writing pairs (e.g. (x; y), ((x; y); (x; (y; y))) etc.) for free variables, or by writing ancestral abstracts (e.g. (*xyFxy) etc.) for schematic letters, or both.The ancestral abstract (*xyFxy) means what is usually meant by ; and the formula (*xyFxy)zw answers to Martin's (zw; xy)(Fxy).The system presupposes a non-simple applied functional calculus of the first order, with a rule of substitution for predicate letters; over and above this it has three axioms for the ancestral and two for the ordered pair.

A finite arithmetic

1973 ◽  
Vol 38 (2) ◽  
pp. 232-248 ◽  
Author(s):  
Philip T. Shepard
Keyword(s):  
Number Theory ◽  
Natural Number ◽  
Singular Term ◽  
New Method ◽  
Axiomatic System ◽  
Natural Numbers ◽  
Substantial Loss ◽  
First Order ◽  
Finite Arithmetic

In this paper I shall argue that the presumption of infinitude may be excised from the area of mathematics known as natural number theory with no substantial loss. Except for a few concluding remarks, I shall restrict my concern in here arguing the thesis to the business of constructing and developing a first-order axiomatic system for arithmetic (called ‘FA’ for finite arithmetic) that contains no theorem to the effect that there are infinitely many numbers.The paper will consist of five parts. Part I characterizes the underlying logic of FA. In part II ordering of natural numbers is developed from a restricted set of axioms, induction schemata are proved and a way of expressing finitude presented. A full set of axioms are used in part III to prove working theorems on comparison of size. In part IV an ordinal expression is defined and characteristic theorems proved. Theorems for addition and multiplication are derived in part V from definitions in terms of the ordinal expression of part IV. The crucial final constructions of part V present a new method of replacing recursive characterizations by strict definitions.In view of our resolution not to assume that there are infinitely many numbers, we shall have to deal with the situation where singular arithmetic terms of FA may fail to refer. For I know of no acceptable and systematic way of avoiding such situations. As a further result, singular-term instances of universal generalizations of FA are not to be inferred directly from the generalizations themselves. Nevertheless, (i) (x)(y)(x + y = y + x), for example, and all its instances are provable in FA.

On the definition of ‘formal deduction’

1956 ◽  
Vol 21 (2) ◽  
pp. 129-136 ◽  
Author(s):  
Richard Montague ◽  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Modus Ponens ◽  
Formal Proof ◽  
Axiom Schema ◽  
First Order ◽  
Individual Variable ◽  
Individual Variables ◽  
Definition Of ◽  
Formal Rules

The following remarks apply to many functional calculi, each of which can be variously axiomatized, but for clarity of exposition we shall confine our attention to one particular system Σ. This system is to have the usual primitive symbols and formation rules of the pure first-order functional calculus, and the following formal axiom schemata and formal rules of inference.Axiom schema 1. Any tautologous wff (well-formed formula).Axiom schema 2. (a) A ⊃ B, where A is any wff, a and b are any individual variables, and B arises from A by replacing all free occurrences of a by free occurrences of b.Axiom schema 3. (a)(A ⊃ B)⊃(A⊃ (a)B). where A and B are any wffs, and a is any individual variable not free in A.Rule of Modus Ponens: applies to wffs A and A ⊃ B, and yields B.Rule of Generalization: applies to a wff A and yields (a)A, where a is any individual variable.A formal proof in Σ is a finite column of wffs each of whose lines is a formal axiom or arises from two preceding lines by the Rule of Modus Ponens or arises from a single preceding line by the Rule of Generalization. A formal theorem of Σ is a wff which occurs as the last line of some formal proof.

Prerequisites

1993 ◽  
Author(s):  
Raymond M. Smullyan
Keyword(s):  
Completeness Theorem ◽  
Order Logic ◽  
First Order Logic ◽  
Natural Numbers ◽  
Logical Validity ◽  
First Order ◽  
Gödel’S Completeness Theorem ◽  
Logical Connectives ◽  
Incompleteness Theorems ◽  
Individual Variables

As we remarked in the preface, although this volume is a sequel to our earlier volume G.I.T. (Gödel’s Incompleteness Theorems), it can be read independently by those readers familiar with at least one proof of Gödel’s first incompleteness theorem. In this chapter we give the notation, terminology and main results of G.I.T. that are needed for this volume. Readers familiar with G.I.T. can skip this chapter or perhaps glance through it briefly as a refresher. §0. Preliminaries. we assume the reader to be familiar with the basic notions of first-order logic—the logical connectives, quantifiers, terms, formulas, free and bound occurrences of variables, the notion of interpretations (or models), truth under an interpretation, logical validity (truth under all interpretations), provability (in some complete system of first-order logic with identity) and its equivalence to logical validity (Gödel’s completeness theorem). we let S be a system (theory) couched in the language of first-order logic with identity and with predicate and/or function symbols and with names for the natural numbers. A system S is usually presented by taking some standard axiomatization of first-order logic with identity and adding other axioms called the non-logical axioms of S.we associate with each natural number n an expression n̅ of S called the numeral designating n (or the name of n).we could, for example, take 0̅,1̅,2̅, . . . ,to be the expressions 0,0', 0",..., as we did in G.I.T. we have our individual variables arranged in some fixed infinite sequence v1, v2,..., vn , . . . . By F(v1, ..., vn) we mean any formula whose free variables are all among v1,... ,vn, and for any (natural) numbers k1,...,kn by F(к̅1 ,... к̅n), we mean the result of substituting the numerals к̅1 ,... к̅n, for all free occurrences of v1,... ,vn in F respectively.

A note on direct products

1958 ◽  
Vol 23 (1) ◽  
pp. 1-6 ◽  
Author(s):  
L. Novak Gál
Keyword(s):  
Binary Relation ◽  
Direct Product ◽  
Functional Calculus ◽  
Ordered Set ◽  
Infinite Sequence ◽  
Direct Products ◽  
First Order ◽  
Individual Variables ◽  
The Individual ◽  
Infinite Sequences

By an algebra is meant an ordered set Γ = 〈V,R1, …, Rn, O1, …, Om〉, where V is a class, Ri (1 ≤ i ≤, n) is a relation on nj elements of V (i.e. Ri ⊆ Vni), and Oj (1 ≤ i ≤ n) is an operation on elements of V such that Oj(x1, … xmj) ∈ V) for all x1, …, xmj ∈ V). A sentence S of the first-order functional calculus is valid in Γ, if it contains just individual variables x1, x2, …, relation variables ϱ1, …,ϱn, where ϱi,- is nj-ary (1 ≤ i ≤ n), and operation variables σ1, …, σm, where σj is mj-ary (1 ≤, j ≤ m), and S holds if the individual variables are interpreted as ranging over V, ϱi is interpreted as Ri, and σi as Oj. If {Γi}i≤α is a (finite or infinite) sequence of algebras Γi, where Γi = 〈Vi, Ri〉 and Ri, is a binary relation, then by the direct productΓ = Πi<αΓi is meant the algebra Γ = 〈V, R〉, where V consists of all (finite or infinite) sequences x = 〈x1, x2, …, xi, …〉 with Xi ∈ Vi and where R is a binary relation such that two elements x and y of V are in the relation R if and only if xi and yi- are in the relation Ri for each i < α.

Incompleteness along paths in progressions of theories

1962 ◽  
Vol 27 (4) ◽  
pp. 383-390 ◽  
Author(s):  
S. Feferman ◽  
C. Spector
Keyword(s):  
Number Theory ◽  
Recursive Function ◽  
Order Number ◽  
Basic Logic ◽  
Natural Numbers ◽  
Logical Deduction ◽  
First Order ◽  
Primitive Recursive Function ◽  
Primitive Recursive ◽  
Recursive Definitions

We deal in the following with certain theories S, by which we mean sets of sentences closed under logical deduction. The basic logic is understood to be the classical one, but we place no restriction on the orders of the variables to be used. However, we do assume that we can at least express certain notions from classical first-order number theory within these theories. In particular, there should correspond to each primitive recursive function ξ a formula φ(χ), where ‘x’ is a variable ranging over natural numbers, such that for each numeral ñ, φ(ñ) expresses in the language of S that ξ(η) = 0. Such formulas, when obtained say by the Gödel method of eliminating primitive recursive definitions in favor of arithmetical definitions in +. ·. are called PR-formulas (cf. [1] §2 (C)).

On the rules of proof in the pure functional calculus of the first order

1951 ◽  
Vol 16 (2) ◽  
pp. 107-111 ◽  
Author(s):  
Andrzej Mostowski
Keyword(s):  
Functional Calculus ◽  
Free Variable ◽  
Propositional Function ◽  
Cartesian Power ◽  
First Order ◽  
A Value ◽  
Free Variables ◽  
Individual Variables ◽  
Definition Of

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.

Some formal relative consistency proofs

1953 ◽  
Vol 18 (2) ◽  
pp. 136-144 ◽  
Author(s):  
Robert McNaughton
Keyword(s):  
Number Theory ◽  
Natural Number ◽  
Natural Numbers ◽  
Quantification Theory ◽  
Usual Manner ◽  
Function Calculus ◽  
Image Position ◽  
Positive Integers

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:

Quantification theory and empty individual-domains

1953 ◽  
Vol 18 (3) ◽  
pp. 197-200 ◽  
Author(s):  
Theodore Hailperin
Keyword(s):  
Functional Calculus ◽  
Modus Ponens ◽  
Quantification Theory ◽  
First Order ◽  
Complete Set ◽  
Universal Quantification

In a recent paper by Mostowski [1] we find an investigation of those formulas of quantification theory which are valid in all domains of individuals, including the empty domain. Mostowski gives a complete set of axioms for such a first order functional calculus (the system is called “”) and a comparison is made with a form of the usual calculus, Church's in [2]. It is pointed out that is much less elegant; in particular, the distributivity laws for quantifiers (e.g., (x){A . B) .{x)A . (x)B) do not hold in general, and likewise the rule of modus ponens does not preserve validity in all cases.In this paper we show that a not inelegant system is obtained if one modifies Mostowski's approach in two respects; and once this is done a somewhat neater proof of completeness can be given.The first respect in which we diverge from Mostowski is in the treatment of vacuous quantifiers. For him if p has no free x, then (x)p and (∃x)p are both to have the same value (interpretation) as p1. But this is not the only way to assign values to vacuous quantifications. For when universal quantification is viewed as a generalized conjunction, the formula (x)Fx has the significance of Fa . Fb…. for as many conjunctands as there are individuals in the domain, and if Fx should have the “constant” value p, then (x)p is to mean the conjunction of p with itself for as many times as there are individuals in the domain (compare the arithmetical ).

Transfinite recursive progressions of axiomatic theories

1962 ◽  
Vol 27 (3) ◽  
pp. 259-316 ◽  
Author(s):  
Solomon Feferman
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
Higher Order ◽  
Order Number ◽  
First Order ◽  
Definable Set ◽  
Recursively Enumerable

The theories considered here are based on the classical functional calculus (possibly of higher order) together with a set A of non-logical axioms; they are also assumed to contain classical first-order number theory. In foundational investigations it is customary to further restrict attention to the case that A is recursive, or at least recursively enumerable (an equivalent restriction, by [1]). For such axiomatic theories we have the well-known incompleteness phenomena discovered by Godei [6]. Quite far removed from such theories are those based on non-constructive sets of axioms, for example the set of all true sentences of first-order number theory. According to Tarski's theorem, there is not even an arithmetically definable set of axioms A which will give the same result (cf. [18] for exposition).

Sign in / Sign up

Export Citation Format

Share Document