Special Cases of the Decision Problem - article ; n°22 ; vol.49, pg 203-221

-

English
20 Pages
Read an excerpt
Gain access to the library to view online
Learn more

Description

Revue Philosophique de Louvain - Année 1951 - Volume 49 - Numéro 22 - Pages 203-221
19 pages

Subjects

Informations

Published by
Published 01 January 1951
Reads 15
Language English
Document size 1 MB
Report a problem

Alonzo Church
Special Cases of the Decision Problem
In: Revue Philosophique de Louvain. Troisième série, Tome 49, N°22, 1951. pp. 203-221.
Citer ce document / Cite this document :
Church Alonzo. Special Cases of the Decision Problem. In: Revue Philosophique de Louvain. Troisième série, Tome 49, N°22,
1951. pp. 203-221.
http://www.persee.fr/web/revues/home/prescript/article/phlou_0035-3841_1951_num_49_22_4341Special Cases of the Decision Problem
the Functional decision problem, calculus. we To shall facilitate adopt the a statement particular of formulation results about of
the pure functional calculus of first order, as follows. (All of the
results treated, however, may easily be restated so as to apply to
other formulations.)
There is one primitive propositional constant / (falsehood), one
primitive sentence connective D (material implication), and two quantifiers, the universal and the existential quantifier (1>. •
As individual variables we use x, y, z, x0, ... ; as propositional
variables, p, q, r, p0, ... ; and as n-ary functional variables, F", G",
Hn, Fo, .... The superscript n after a variable may, howe
ver, usually be omitted without any danger of misunderstanding.
Where a is any individual variable, we use (a) as universal
quantifier and (Ea) as existential quantifier.
An elementary well-formed formula either consists of the pro-
positional constant / standing alone, or consists of a propositional
variable alone, or has the form f(alf a3, ...» an), where f is an
n-ary functional variable, and alf a2, .... an are individual variables
(not necessarily all distinct). A well-formed formula is an expression
built up in the usual way by means of the connective D and the
quantifiers from elementary formulas. And the el
ementary well-formed formulas thus used in building up a well-
formed formula are called its elementary parts.
Hereafter we shall use the abbreviations, « wff » for « well-
formed formula », and « wf » for « well-formed ».
As already illustrated, we use bold letters in the rôle of syn
tactical variables, bold small letters (as a, b) standing for variables
of the object language, and bold capital letters (as A, B) for wffs.
If (a)A or (Ea)A occurs as a wf part of a wff L, then that
<*> For our present purpose it is more convenient to treat both quantifiers
as primitive. 204 Alonzo Church
particular occurrence of the wff A in L is called the scope of that of the quantifier (a) or (Ea). All occurrences
of an individual variable a in a wf part (a)A of (£a)A of a wff L
are called bound occurrences of a in L ; and all other
of a in L are called jree occurrences. All occurrences of proposi-
tional and functional variables are free occurrences. The bound
variables of L are those (individual) variables which have
occurrences in L, and the jree variables of L are those variables
which have free occurrences in L.
A particular occurrence of a wff P as a wf part of a wff L is
called an occurrence as a P-constituent in L if it is not within the
scope of any quantifier in L, and P does not have the form, either
of an implication [A D B]or of the constant / standing alone. And
the P'Constituents of L are those wffs which have occurrences as
P-constituents in L <2).
We shall speak in the usual sense of validity and satisfiability
of wffs. These notions are capable of a precise syntactical definition,
by a method due to Tarski <8). But we content ourselves here with
the following brief statement. If a particular non-empty domain D
is taken as the range of the individual variables, then the range
of the n-ary functional variables is to consist of all n-ary propo-
sitional functions over this domain, and the range of the variables is to consist of the two truth-values, truth and
falsehood. (The value of the constant / is always to be the truth-
value falsehood.) Upon taking the ranges of the variables in this
way, a wff is said to be valid in the domain D if it has the value
truth for every system of values of its free variables, satisfiable in
the domain D if it has the value truth for at least one system of
values of its free variables. A wff is said to be valid if it is valid in
every non-empty domain, satisfiable if it is satisfiable in some non
empty domain.
We require axioms and rules of inference for the functional
calculus of first order satisfying the two conditions, that every
<2> Thus every P-constituent of a wff either is an elementary part (other
than f) or else begins with a quantifier and consists of the quantifier together
with its scope. And every wff can be thought of as obtained from a wff of the
propositional calculus by substituting various P-constituents for the propositional
variables.
(*> Alfred TARSKI, Der Wahrheitabegriff in den formalisierten Sprachen, Studia
Philosophica, I (1936). - . - The Decision Problem 205
theorem of the calculus is a valid wff, and every valid wff is a of the calculus. As is well known, this may be accomp
lished in various ways. And since the particular choice of axioms
and rules is not important for our present purpose, we shall not
take the space to list them, but shall simply assume the proofs of
familiar theorems of the calculus as these are needed.
Merely as a matter of convenience in the metatheoretic pre
sentation, we shall use the following abbreviations of wffs :
~A as an abbreviation of [A D /].
[A v B] as an of [~B DA].
[AB] as an of ~[B D "^ A].
[A = B] as an abbreviation of [ [A D B] [B D A] ] .
We shall also abbreviate by omitting brackets under the con
vention of association to the left — so that, e. g., F(x) D G{y) D
H{x,y) is an abbreviation of [ [F(x) D G{y)] O H(x,y)] , and p v q v
[rt D r2] is an of [ [p v q] v [rx D r2] ] . And a bold
dot will be used to stand for a pair of brackets, one at the position
of the dot, and the other, either at the end of the wff or otherwise
at the latest position which is consistent with the formula's being wf
— so that, e. g., F{x) D G(y) O . H(x,y) D H{y,x) is an abbrev
iation of [[F{x) D G{y)) D [H(x,y) D H(y,x)]], and [p D . q
ID . rx O r2] O r is an abbreviation of [ [p D [qO [r2 Dr2]j] Dr].
A wff A! v A2 v ... v Ajt will be called a disjunction, and
A,, A2, ..», A|t will be called its terms (4\ Similarly, AjA2 ... Ajj,
is a conjunction, and Alt A2, ...» A^ are its terms ; A D B -is an
implication, A is its antecedent, and B is its consequent ; A = B
is an equivalence, and A and B are its sides. Also a wff • — A will
be called the negation of A.
We shall say that two wffs A and B are equivalent if the wff
A = B is a theorem (of the pure functional calculus of first order).
And we shall assume the following metatheorems : If in any theorem
a wf part is replaced by an equivalent wf part, the wff so obtained
is also a theorem. Hence in particular, if two wffs are equivalent,
and if either is a theorem, then the other is a theorem.
In order to provide a convenient syntactical notation for the
operation of substitution, we shall often write M(a!a2 ... av) instead
<4> As a particular case, n may be I ; i. e., an arbitrary wff At may be con
sidered as a disjunction having a single term; or also as a conjunction having
a single term. . Alonzo Church 206
of merely M, as a notation for a wff having no other free individual
variables than alt a2 av. Then M(bjb3 ... bv) will be used as
a notation for the result of substituting blf b2, ... bv for free occur
rences of alt a2, ..., av respectively, simultaneously throughout
M(a,a3 ... av).
We shall also sometimes make use of the notation (M) £ for
the result of substituting b for all free occurrences of a in M . (Notice
that the use of this notation for substitution does not imply but
what M may contain other free individual variables than a.)
Tautology. We shall call a wff tautologous if it has the value
truth for every system of truth-values of its P-constituents. Assumi
ng this -notion to be familiar, we recall only that there is an
effective test, the truth-table decision procedure, by which to
recognize whether a given wff is tautologous. Evidently, every tauto
logous wff is valid, but not conversely.
If a wff Lis not tautologous, there exist one or more falsifying
systems of truth-values of its P-constituents — i. e., systems of truth-
values of the P-constituents .for which the value of L is falsehood.
Let the (distinct) of L be P1( P2, .... Pfi ; and let the
complete list of falsifying systems of truth-values of these P-constit
uents consist in the of values x\, x\ t^, where
i = 1,2, ..., V. Let P'. be P/ or ~Py- according as the corresponding
truth- value z1'. is truth or falsehood. Then the wff
L = [P] D . ?\O . ... Pj O f] [P? D . Pi D . ?l D /]
... [p; d . ?i d . p; d /]
is tautologous, and therefore a theorem. The right-hand side of
this equivalence we shall here call the conjunctive normal form of L
(as is only a minor deviation from standard terminology). The sepa
rate terms P\ O . P'2 D . ... P^ D / we call the terms of the con
junctive normal form.
If L is tautologous, then ji = 0, and there is no conjunctive
normal form of L. In this case, the terms of the conjunctive normal
form of L shall be understood to be the null set.
Prenex normal form. An occurrence of a quantifier, (a) or (£a),
in a wff L is said to be vacuous if a is not a free variable of A,
where A is the scope.
An occurrence of a quantifier in a wff L is said to be initially Decision Problem 207 The
placed if it is at the beginning of L or is preceded in L only by
other quantifiers, and if at the same time its scope extends to the
end of L. Thus, e. g., in (x)(y) . {z)F{x,z) D F(x,y), the quantif
iers (x) and (y) are initially placed, but not the quantifier (z).
A wff is said to be in prenex normal form if all its quantifiers
are initially placed and none of them are vacuous.
Thus a wff in prenex normal form may be thought of as cons
isting of two parts ; the matrix, which is a quantifier-free wff,
preceded by the prefix, which is composed entirely of a number
of quantifiers (0 or more) each with its own variable. The variables
in the prefix must be all different and must all occur in the matrix.
According to a familiar metatheorem, every wff can be reduced
to prenex normal form. More explicitly, given any wff L, an equiv
alent wff L* in prenex normal form can be obtained from L by
applying the following reduction steps (l)-(4) a finite number of
times :
(1) To delete a vacuous occurrence of a Quantifier .
(2) b being an individual variable which does not otherwise
occur, to replace a wf part Ci D . Ca 3 . ... CL D D by
' D D' ; where, in case D has the form (Eb) . G| O . C'2 ^ . ... C
(Ea)B, D' is (B)g, and otherwise D' is D ; and where (for
i=l,2, .... jx), in case C/ has the form (a/) A/, C/ is (A/)b\ and
otherwise C^. is C. ; but provided, finally, that Ji > 0 and that the
quantifier (Eb) so introduced is not vacuous.
(3) b being an individual variable which does not otherwise
occur, to replace a wf part C D (a)B by (b) . C O (B)b-
(4) b being an variable which does not
occur, to replace a wf part (Ea)A D D by (b) . (A)b O D.
The observation is due to Behmann (1922) and more recently
to Quine that, in connection with certain cases of the decision prob
lem, it may be useful to apply also what we shall call the inverse
of reduction to prenex normal form. This process consists in the
following reduction steps (i) - (vii) to be applied any number of
times in succession :
(i) To delete a vacuous occurrence of a quantifier.
(ii) To replace a wf part (Ea) . A, D . A2 D . ... AjtD B by
(a)A, D . (a)A2 D . ... (a)A^ D (£a)B, if ji > 0.
(iii) To replace a wf part (a)B by [(a)Bi D . (a)Ba D . ...
(a)B(i O f] O f, where Blt B2, .... Bjx are the terms of the con
junctive normal form of B, and where ji > 1, 208 Alonzo Church
(iv) To replace a wf part (a)B by (a)Bjf if B is not in con
junctive normal form, and the conjunctive normal form of B has a
single term Bi.
(v) To replace a wf part (a)B by / D / if B is tautologous. •
(vi) To a wf part (a) , A, D. A2 D . ... Api D, C DB
by C D (a) . Aj D . A2 D . ... Aj* D B, if a is not a free variable
of C, and ji ^ 0.
(vii) To replace a wf part (a) . A O D by (Ea)A D D, if a is
not a free variable of D.
Starting with a given wfî L and applying steps (i) - (vii) repeat
edly until the process is blocked, we obtain an equivalent wff L*
which is in a certain sense as far removed as possible from the
prenex normal form of L.
In connection with the process of reduction of L to prenex
normal form and the inverse process, it is possible to give effective
instructions for building up proofs of the equivalences L = L* and
L EE L# as theorems of the functional calculus. We here leave it
to the reader to supply these.
Decision problem. By a solution of a special case of the decision
problem of the pare functional calculus of first order (or briefly,
of the decision problem) we mean that there shall be given a
special class of wffs, an effective test for recognizing whether a wff
belongs to this class, an procedure (the decision procedure)
for determining whether a wff L of this class is a theorem, and
finally an effective method of finding a proof of a wff thus dete
rmined to be a theorem.
In calling a procedure or a method effective we mean, roughly
speaking, that there is assurance of reaching the desired result in
every particular case by a faithful and purely mechanical following
of fixed instructions, without the need for exercise of ingenuity.
We forgo a more exact definition here, because it is believed that
in the cases treated below there can hardly be doubt of the effec
tiveness of the particular procedures introduced (5>.
The purpose of this note is to outline briefly the important
special cases of the decision problem for which solutions either
<s> Representing formulas by Gôdel numbers in a straightforward manner,
we find in fact that all the procedures introduced are represented by primitive
recursive functions — which is surely sufficient. The Decision Problem 209
exist explicitly or are easily obtained as corollaries of methods
found in the literature. The actual decision procedures will be given
only in the simpler cases (the reader being referred to the original
papers for the rest), and their proofs will be at best roughly
indicated.
For purposes of exposition it will be convenient to divide exis
ting solutions of special cases of the decision problem into two
types, namely (1) those in which the special class of wffs is charac
terized by conditions on the prefix and the matrix of a wff L in
prenex normal form and the decision procedure is applied to L
directly in this prenex normal form, and (II) those in which the
decision procedure is indirect, the decision problem for a given
wff L being reduced to the decision problem for one or more wffs
which fall under special cases of type I.
In stating cases of type I, we shall assume that the
given wff L is in prenex normal form and without free individual
variables. The latter condition involves no loss of generality, since
LCa^-.-av) is a theorem if and only if (a1)(a2)...(av)L(a1a2...av)
is a theorem.
For special cases of type II, on the other hand, free individual
variables are to be allowed ; and indeed it may happen that a
particular wff is recognized as falling under one of these cases only
after dropping one or more initially placed universal quantifiers
from the beginning.
But in stating special cases of type II we shall assume, for
convenience, that every P-constituent is in prenex normal form.
Type I. Solutions exist of the following special cases (6) :
Case I (7). Prefix («1X«f).,.(«/XEb1)(Eb,)...(EbIB). 2 (8>. (•1K«I)...(ai)(Eb)(c1Kc1)...(cJi).
(S) In each case, it is not excluded that /, m, n may some or all of them be 0.
(r> Paul BERNAYS and Moses ScHONFINKEL, Zum Entscheidungsproblem der
Mathematiachen Logik, Mathematische Annalen, 99 (1928). The subcase / =0,
n = I of Case 2 is also treated by Bernays and Schônfinkel in this paper.
<"' Wilhelm ACKERMANN, Ueber die Erfiillbarkeit getoisser Zahlausdrucke,
Mathematische Annalen, 100 (1928); Thoralf SKOLEM, Ueber die Mathematische
Logik, Norsk Matematisk Tidsskrift, 10 (1928); Jacques HERBRAND, Sur le Problème
Fondamental de la Logique Mathématique, Comptes Rendus des séances de la
Société des Sciences et des Lettres de Varsovie, Classe III, 24 (1931). In some
of these papers it is the decision problem for satisfiability which is treated 210 Alonzo Church
Case 3 <•>. Prefix (a1)(a2)...(a/)(Eb1)(£b2)(c1)(c2)...(c/1). 4 <10>. (a1)(a2)...(ay)(£b1)(£b2)...(Ebm)(c1)(c2)...(cil), and
a matrix in which every elementary part that contains individual
variables other than a1>a2,...,a/ contains either all of the variables
bllb2,...,bn) or at least one of the variables cltc2,...,cn.
CASE 5 (10). Prefix beginning with (a1)(a2)...(ay) and ending with
(ci)(c2).».(cn). and a matrix in which every elementary part that con
tains individual variables other than a,,a2,...,a/ contains at least one
of the variables Ci,c2...,cn.
Case 6 <u). There is at most one falsifying system of truth-values
of the P-constituents of the matrix.
Case 7 (12). Prefix {Eb1){Eb2)...(Ebm)(c), where m <;4. and a
matrix of the form N D fflbx.c), where c does not occur in N.
directly, i. e., the problem to find an effective procedure to determine whether
wffs are satisfiable. But we have here modified and restated their results so as
to apply to the decision problem in the sense in which we are using the term.
(Compare the discussion of Bernays and Schonfinkel regarding the relationship
of the two decision problems.)
<•' Kurt GÔDEL, Ein Spezialfall des Entscheidungsproblems der Theoretischen
Logi\, Ergebnisse eines Mathematischen (Colloquiums, 2 (1932); Lâszlo KALMÀR,
Ueber die Erfullbarkeit derjenigen Zâhlausdriickc, welche in der Normalform
zwei Benachbarte Allzeichen Enthalten, Mathematische Annalen, 108 (1933);
Kurt GÔDEL, Zum Entscheidungsproblem des Logischen Funkjtionenkfllhuh, Mo-
natshefte fur Mathematik und Physik, 40 (1933); Kurt SCHUTTE, Untersachungen
zum Entscheidungsproblem der Mathematischen Logikt Mathematische Annalen,
109 (1934).
<10> Cf. Skolem, Joe. cit.
(11) HERBRAND, loc. cit. Another way of stating the condition which charac
terizes this case is that the matrix is a disjunction of elementary parts and negations
of elementary parts, or equivalent to such a disjunction. But if the prefix begins
with the universal quantifiers (a1)(a2)...(a,) (I ^> 0), a somewhat weaker condition
is actually sufficient, namely that the matrix "shall be or be equivalent to a dis
junction in which each term is a conjunction of elementary parts and negations
of elementary parts, at most one of the terms of each such conjunction containing
individual variables other than B.l,ai2,...,a.j. For the method of solution of Case 6
which is indicated below may readily be extended to solve this more general case.
(") Wilhelm AcKERMANN, Beitrage zum Entscheidungsproblem der Mathemat
ischen Logik, Mathematische Annalen, 112 (1936); I. GÉGALKINE, Sur VEntschei-
dungsproblem, Recueil Mathématique, 6 (1939). In spite of the rather special
appearance of the condition which characterizes it, this case has some considerable
interest because it is here the only case that includes examples of wffs which,
though valid in every finite domain, are not valid in an infinite domain. Moreover,
as Ackermann points out, there follows as an immediate corollary a solution of
the decision problem for wffs with prefix (£a)(b)(£c) or (£a)(b)(£c)(£d) ; for a The Decision Problem 211
The treatment of some of these cases may be unified by means
of the following metatheorem. Let the ordered m-tuples of natural
numbers be enumerated in such a way that one m-tuple comes later
in the enumeration than another if it contains as member a natural
number greater than the greatest natural number contained in the
other, and the m-tuples having the same greatest natural number
are arranged among themselves in lexicographic order. For the
ith member of the fcth m-tuple in this enumeration, use the nota
tion [mfcij. Let M(a1a2...ayb1b2...b/nCiC2...c/1) be any quantifier-free
wff, let Mjt be
let D* be the disjunction Mx v M3 v ... v M#, and let L be
(a1)(a2)...(a/)(£b,)(Eb2)...(£bm)(c1)(c2)...(c/1)M(a1a2...a/b1b2...bmc1c2...
C/i ) . Then L is a theorem if and only if D# is tautologous for some k..
This metatheorem is, in. fact, a corollary of Gôdel's proof (13)
of the completeness of the functional calculus of first order.
Moreover, if a particular D# has been found which is tautol
ogous, it is well known how (by methods belonging essentially to
propositional calculus) to find a proof of D*. Then to go on from
a proof of D£ to a proof of L is a matter of using familiar laws of
quantifiers (it is suggested that the reader carry this out in a repre
sentative particular case — say the case that / = 1, m = 2, n = 1,
k = 7). Thus an effective method may be provided, to find a proof
of L when a number k is given such that D& is tautologous.
For a class of wffs in prenex normal form, if all the prefixes
are of the form given above (i. e., if no universal quantifiers occur
between existential quantifiers) it will therefore constitute a solution
of the decision problem to find a particular value K of fc, depending
in an effective way on the given wff L, such that either D# is tau
tologous or none of the wffs D* is tautologous. And we may state
the solution just by giving this number K.
To illustrate the method, consider a wff L falling under Case 2
with / = 0 and n = I, and suppose that the matrix M (be) of L
contains no propositional variables, and no functional variables but
one binary functional variable f. Taking the domain of natural
wff with either of these prefixes is reduced to Case 7 by the usual process for
reduction to Skolem normal form.
<") Kiirt GÔDEL, Die Vollstandigkeit der Axiome des Logischen Funkjtionen-
kalkHls, Monatshefte fur Mathematik und Physik, 37 (1930).