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).