Leon Gumański

Leon Gumański

The Decidability of The First–Order
Functional Calculus

Abstract. Confining considerations to expressions in the prenex normal form and to economic proofs (i. e. without superfluous transformations) constructed according to the method of semantic tableaux, certain conditions and negative criterions of provability are stated at first. Next some solutions of decision procedure for special cases are pointed out. Then a test is described for an arbitrary expression t whether there exists its proof having length k. Finally a bound for k is established beyond which further quest of a proof is useless as no proof of t can exist.
1. Introduction and preliminaries
In our paper [9] we have pointed out to an error in Church’s proof that the first–order functional calculus is undecidable. Now the aim of the present paper is to show that his theorem is erroneous, too. As a matter of fact we have already devoted two former papers to the same problem. Our first proof of the decidability of the first–order functional calculus presented in [6] was based on a system, called “S_A”, of the calculus. The system was a modification of the axiomatic system described in [3]. Some readers of [6] suspected (wrongly) that S_A was not a correct system of the calculus. So in [7] it was shown that the same result could be grounded on Beth’s method of semantic tableaux (Cf. e. g. [2]). On the other hand, both papers, [6] and [7], made use of a reduction theorem proved by L. Kalmár and I. Surányi in [4]. However, again, certain readers of the paper were inclined to believe that there must be an error in the reduction theorem. That is why the theorem will be left out of account in the present paper. Besides, in order to simplify considerations the so–called o–variables and control tables – a technical device applied in [6] and [7] – will be dispensed with. More emphasis will be laid on explanations and illustrations here.

The paper is arranged as follows. After preliminaries Section II shows certain peculiarities of proofs by Beth’s method of semantic tableaux. One indicates the possibility to characterize and to investigate tableaux by means of an analysis of atomic expressions which occur in tableaux. Notions useful for such investigations are defined. Section III deals with conditions of closing tableaux and with negative criterions of existence of proofs. Section IV explains how to determine whether a tableau–construction of a given length can be closed. The final Section V gives the proof that the calculus is decidable, after discerning and examining three forms of prefix.

Now for a start let us explain some terms applied in the present paper in order to distinguish some types of utterance.

Assumptions – arrangements introduced with the aim to regulate and make perspicuous the form of proofs constructed according to the method of semantic tableaux. They do not change the set of theorems of the calculus.

Conventions – settlements which refer to terms or symbols but do not have the character of definition.

Observations – claims that need not be proved for they are obvious.

Remarks – comments drawing attention to something worthy of notice.

Besides, in what follows we shall make use, among others, of the following terms and symbols:

CONVENTION 1.1. The word “calculus” means always here the same as “first–order functional calculus”. The word “expression” denotes any well–formed formula of the calculus. An expression is fully open if and only if it does not contain any quantifiers.

CONVENTION 1.2. Using the term “atomic expression” we shall usually mean atomic expressions standing separately but sometimes we shall also apply the term to such atomic expressions which are a part of some compound expression. In the latter case – in order to avoid ambiguity – the words “not separate” will be added in parantheses.

CONVENTION 1.3. The letters “a”, “b”, “c” (with indices or not) stand for individual variables. The letters “t”, “u”, “v”, “w” (with indices or not) represent any expression. The symbol “u[a]” indicates any expression u which contains an individual free variable a (u may contain other variables as well). The symbol “u[a/b]” denotes an expression obtained from u by substitution of a variable b for the variable a. We shall distinguish between bound individual variables x₁, x₂,…(called “x–variables”) and free individual variables y₁, y₂,…(called “y–variables”). The notation “(x₁)”, “(x₂)”,… will be used for universal quantifiers and “(Ex₁)”, “(Ex₂)”,… for existential quantifiers. The symbols “(a)”, “(Ea)” denote any universal, existential quantifier respectively.

Other terms and symbols will be introduced later on.

ASSUMPTION 1.1. Let us consider any expression t. However, without loss of generality we shall assume that t fulfils the following conditions:

1^° t does not contain any free individual variables,

2^° t does not contain any sentential variables,

3^° t does not contain truth–functors other than “–” (the sign of negation) and “” (the sign of conjunction),

4^° t is in a prenex normal form,

5^° no quantifier bounds vacuously in t.

This assumption can be accepted here because it is possible to transform any expression into an equivalent one that fulfils all the conditions 1⁰ – 5^{0 1}.
2. Semantic tableaux
Of special interest for us the problem will be whether t is a theorem of the calculus (i. e. if t is universally valid). We shall identify the problem with the question if t can be proved by the method of semantic tableaux². The reader is supposed to be familiar with the method which in fact is nothing but a certain way of writing down indirect proofs. Nevertheless, some details will be recalled here with the aim of facilitating comprehension and making some terms more explicit.

DEFINITION 2.1. A construction built of all tableaux that have a common initial part with the expression t at the beginning of the right column of this part will be called “a tableau–construction of t”.

For instance, Tab. 1 below represents a tableau–construction of the expression:
W (Ex₁) (x₂)–[fx₂–(fx₁fx₂)]
In particular a tableau–construction of t may consist of one single tableau (as in Tab. 3 below).

RULES OF INFERENCE. In the light of Assumption 1.1 it should be clear that only the following six rules (reduction schemata) can be employed in a tableau–construction of t:

	True	False		True		False			True	False
	K1	K2		K1		K2			K1	K2
TN	–w		TC	u  w				F(a)		(a)w
		W		u w						w[a/b]
	True	False		True		False			True	False
	K1	K2		K1		K2			K1	K2
FN		–w	FC			u  w		F(Ea)		(Ea)w
	w			^1	^2	^1u	^2w			w[a/b]

K1, K2 are sets of expressions (may be empty) here and the y–variable b in F(a) should always be “new” (i. e. such that it does not yet occur in the tableau) whereas the y–variable b in F(Ea) can be “new” if and only if no y–variables are present in the tableau yet, so if there are some y–variables, b should be (freely) chosen from among them³.

Besides the closure rule states that a tableau is closed if and only if one and the same atomic expression occurs in both columns of the tableau.

As a point of departure for further analyses let us take by way of a paradigm example the proof of the expression W mentioned above.

Tab. 1

True				False
fy2–(fy1fy2) fy2 –(fy1fy2)				(Ex1) (x2)–[fx2–(fx1fx2)] (x2)–[fx2–(fy1fx2)] –[fy2–(fy1fy2)] fy1fy2
1		2		1 fy1		2 fy2
the end of stage 1
fy3–(fy2fy3) fy3 –(fy2fy3)		fy3–(fy1fy3) fy3 –(fy1fy3)		(x2)–[fx2–(fy2fx2)] –[fy3–(fy2fy3)] fy2fy3		(x2)–[fx2–(fy1fx2)] –[fy3–(fy1fy3)] fy1fy3
11	12	21	22	11 fy2	12 fy3	21 fy1	22 fy3
the end of stage 2

Analysing Tab. 1 it is easy to notice that the method of semantic tableaux makes it possible to dissolve compound expressions into ever smaller ones and to obtain finally some atomic expressions. The example shows that it is sometimes necessary to apply a rule (reduction schema) to the same quantifier more than once.

DEFINITION 2.2. If all the quantifiers of t are reduced for the first time and then all the fully open compound expression divided (by appropriate rules for truth–functors) into their atomic components, then we shall say that stage 1 of the tableau–construction of t is terminated. Inductively, the name “stage k of the tableau–construction of t” (k=2,3…) will be given to that part of a tableau–construction of t which starts after stage k–1 is terminated and comes into being when in each tableau of the construction to some of the quantifiers of t (at least to the last one – counting from the left to the right) appropriate rules have been applied for the k–th time, then every fully open compound expression reduced to its atomic components and terminates just before to any quantifier of t a rule is applied for the k+1 time.

DEFINITION 2.3. In case a tableau–construction C of t comes to an end with stage k, we call C “k–stage tableau–construction of t”. Then, every tableau T contained in a certain k–stage tableau–construction of t will be named “k–stage tableau” and the largest part of T which belongs to stage i (i  k) of the construction will be termed “i–th subtableau of T”. Hence T consists of k subtableaux.

DEFINITION 2.4. When all the tableaux of a construction are closed, we say that the whole construction is closed and makes a (k–stage) proof of t. If there is a k–stage proof P of t but for every i there is no i–stage proof of t, then P is an economic (k–stage) proof of t. In that case we shall say that the number k is the minimum length coefficient of the proof of t.

EXAMPLE 2.1. For instance, Tab. 1 is a specimen of 2–stage tableau–construction, which comprises four 2–stage tableaux because the initial common part splits into two subtableaux at stage 1 and then each subtableau of stage 1 splits again into two other ones. As all the four tableaux are closed, the whole 2–stage tableau–construction is a proof.

OBSERVATION 2.1. Splitting of a tableau is a result of an application of rule FC.

LEMMA 2.1. If a k–stage tableau–construction of t has n (n=1,2,…) subtableaux at stage 1, then every subtableau of stage i (i k) splits again into n subtableaux at stage i+1.

PROOF. According to definition 2.2 all appropriate rules for truth–functors have to be applied at each stage. Then if rule FC is used p times at stage 1 producing n subtableaux (n=2^p), rule FC must be applied also p times in each subtableau of stage 2. The same regularity holds good at further stages.

LEMMA 2.2. The number of tableaux in a construction depends on the fact how many times the rule FC is employed at stage 1. Suppose there is a k–stage tableau–construction of t and the rule FC has been applied p times at stage 1, producing n subtableaux, then the whole construction embraces n^k tableaux.

PROOF. There are n subtableaux at stage 1 and by Lemma 2.1 every subtableau of stage i (i<k) splits by FC into n subtableaux of stage i+1, hence the number of tableaux at stage i+1 is n times greater than at stage i.

ASSUMPTION 2.1 We assume that the order of transformations by FN, TN, FC, TC is at each stage i (i>1) the same as at stage 1.

DEFINITION 2.5. When a subtableau S of stage i splits into subtableaux S¹, S²,…, Sⁿ of stage i+1

(1≤ j ≤ n)	S^1 • • •
S	S^j • • •
	S^n

we shall say that S is anterior to S¹, S²,…, Sⁿ and S^j is on the j–th branch of S.

At the same time we take for granted that:

ASSUMPTION 2.2. For every S the branches of S are numbered on the same principle (i. e. in the same manner).

EXAMPLE 2.2. In Tab. 1 the subtableau No 1 of stage 1 is anterior to the subtableaux No 11 and No 12 of stage 2 and the subtableau No 11 is on the first branch of the subtableau No 1 whereas the subtableau No 12 is on the second branch of the subtableau No 1. The transformations of stage 2 are in accordance with Assumption 2.1 and 2.2.

REMARK 2.1. Observe in Tab. 1 that the subtableau No 2 is already closed at stage 1. However, it should be born in mind that further transformations – although useless – are admissible even on closed tableaux. Just to stress this possibility suitable rules have been applied at stage 2 in the subtableau No 21 and No 22 as well. This explains why our definition of “k–stage tableau–construction of t” could be so formulated that a l l  tableaux of the construction are k–stage tableaux.

REMARK 2.2. It is clear that it would be futile to use after a certain stage of a tableau–construction only rules for truth–functors because it would not result in creating new expressions different from those that exist already in the tableau–con­struction. Hence appropriate rules for quantifiers should be utilized at every stage. However, as a matter of fact in some cases it may turn out that in order to achieve a proof of t it would be enough at a certain stage i (i>1) to start transformations by reducing the j–th quantifier (j>1) instead of the first. To illustrate this possibility let us compare two tableau constructions, Tab. 2 and Tab. 3 below. Both tableau–constructions are proofs of the same expression. However, in Tab. 2 after the end of stage 1 the successive transformations start with the reduction of the third quantifier. On the contrary, in Tab. 3 stage 2 begins by reducing the first quantifier. None the less the set of atomic expre­ssions in these tableaux is similar: in the lower part of Tab. 2 we find the set Z₁={+gy₁y₁,+fy₂y₂,fy₃y₃} [the sign plus (lack of it) in front of an expression indicates that the expression stands in the left (right) column of the tableau] whereas in Tab. 3 the set Z₂={+gy₃y₃,+fy₂y₂,fy₄y₄} occurs. The difference between the sets Z₁, Z₂ is inessential because the sets are of the same kind. What means the phrase “the same kind” here will be explained later on (see p. 19, Definition 5.2).

Anyhow, it might be well to mention that in some economic proofs it is necessary to reduce universal quantifiers that appear at the beginning of t only once, namely at stage 1.

Tab. 2

True	False
(fy1y1–fy2y2) gy1y1 fy1y1–fy2y2 gy1y1 fy1y1 –fy2y2 the end of stage 1	(x1) (Ex2) (Ex3) (x4) (Ex5) – [(fx3x5–fx4x4) gx1x2] (Ex2) (Ex3) (x4) (Ex5) – [(fx3x5–fx4x4) gy1x2] (Ex3) (x4) (Ex5) – [(fx3x5–fx4x4) gy1y1] (x4) (Ex5) – [(fy1x5–fx4x4) gy1y1] (Ex5) – [(fy1x5–fy2y2) gy1y1] – [(fy1y1–fy2y2) gy1y1] fy2y2
(fy2y2–fy3y3) gy1y1 fy2y2–fy3y3 gy1y1 fy2y2 –fy3y3	(x4) (Ex5) – [(fy2x5–fx4x4) gy1y1] (Ex5) – [(fy2x5–fy3y3) gy1y1] – [(fy2y2–fy3y3) gy1y1] fy3y3

Tab. 3

True	False
Stage 1 is identical with that of Tab. 2 the end of stage 1
(fy2y2–fy4y4) gy3y3 fy2y2–fy4y4 gy3y3 fy2y2 –fy4y4	(Ex2) (Ex3) (x4) (Ex5) – [(fx3x5–fx4x4) gy3x2] (Ex3) (x4) (Ex5) – [(fx3x5–fx4x4) gy3y3] (x4) (Ex5) – [(fy2x5–fx4x4) gy3y3] (Ex5) – [(fy2x5–fy4y4) gy3y3] – [(fy2y2–fy4y4) gy3y3] fy4y4
the end of stage 2

REMARK 2.3. It is worth noting that a tableau can sometimes be closed on account of a compound fully open expression u being present in both columns of the tableau. Therefore in principle it would be justified to stop there without trying to terminate the stage. Still in such cases further transformations are always admissible for they yield a set of tableaux each of which is closed, too. And so suppose the expression u is a negation, then by a sequence of applications of rules TN, FN an expression v not being a negation comes into being in both columns of the tableau. For instance if u = – –v, we obtain:

True	False
– –v –v v	– –v –v v

If v is not a negation, then it must be a conjunction uw and by rules TC, FC the tableau splits into two closed tableaux: