Church's first postulate for the foundation of logic

Question

In his paper, A Set of Postulates for the Foundations of logic, Church enumerates a set of postulates that he calls formal postulates. They are all said to be true and free from intuitive logic.

My question relates to the very first of these formal postulates:

$$ \Sigma(\varphi) \supset_\varphi\Pi(\varphi, \varphi)\tag{1} $$ It is short hand for,

$$ \Pi\left (\Sigma(\varphi), \Pi(\varphi, \varphi)\right )\tag{2} $$

I am going to assume that $\varphi$ is a function with a bound variable $x$, to simplify the explanation. I believe that there will be no loss of generality.

If we break the components down, $\Sigma(\varphi)$ is read as "there exists at least one value of $x$ for which $\varphi$ is true", $\Pi(\varphi,\varphi)$ is read as "$\varphi$ is a true proposition for all values of $x$ for which $\varphi$ is a true proposition."

So $(2)$ for me reads like "$\varphi$ is a true proposition for all values of $x$ for which $\varphi$ is a true proposition, and there exists a value for $x$ such that $\varphi$ is a true proposition."

Consider me a completely uninformed undergraduate student, why is that a significant postulate?

Answer 1

It seems to me that your reading is not completly correct; see :

• Alonzo Church, A Set of Postulates for the Foundation of Logic, Annals of Mathematics, (2nd series, Vol.33, Apr.1932), page 353-4.

Church introduces a new symbol $\Pi(F,G)$ in terms of which he defines the usual universally quantified conditional :

$F(x) \supset_x G(x)$ stands for : $\Pi(\lambda xF, \lambda xG)$,

where in the last one, it is not required that $F$ be defined for all values of $x$.

The first postulate is :

$\Sigma(\varphi) \supset_\varphi \Pi(\varphi,\varphi)$

i.e.

$\forall \varphi (\Sigma(\varphi) \supset \Pi(\varphi,\varphi))$

and it means :

"for every $\varphi$, if there is at least one value of $x$ for which $\varphi(x)$ is true [and thus $\varphi$ is defined for at least one value of $x$], then $\varphi(x) \supset \varphi(x)$ is true, for all those values of $x$ for which $\varphi$ is defined"

and it "looks good" because, with the proviso regarding the "domain of definition" of $\varphi$, $\varphi(x) \supset \varphi(x)$ is a logical truth.

Forgetting about the $\forall \varphi$, the difference with the FOL valid formula :

$\exists x \varphi(x) \supset \forall x (\varphi(x) \supset \varphi(x))$

is that with the Church's symbols we can handle the case when $\varphi(x)$ is only partially defined.

---

Compare with :

• S.C. Kleene and J.B. Rosser, The Inconsistency of Certain Formal Logics (1935), page 632, where the postulate is rewritten as Rule B4 :

if $F(A)$, then $\Pi(F,F)$.