Defining Church numerals in higher order logic.

Question

I'm looking for some help with Exercise 5.11. in Bacon's A Philosophical Introduction to Higher-Order Logics.

1. Construct an explicit definition of the finite Church numerals, Num$_{\sigma}$, in higher-order logic.

As per the text: "the finite Church numerals are the smallest collection of entities of type $(\sigma \to \sigma) \to (\sigma \to \sigma)$ containing 0 and closed under succesor."(p. 107). The successor function Suc is supposed to yield $\lambda X x. X((X^n)x)$. Bacon provides it as such:

Suc $:= \lambda n X x.X((nX)x)$

So, $n$ is not a number. It takes in the operation $X$ and yields the result of the operation's iteration to the n-th power. It should be of type $(\sigma\to\sigma)\to(\sigma\to\sigma)$. This is my first thought:

Num$_\sigma := \lambda n X x.(C(x) \wedge C(X((nX)x)))$

Counterpoint to my first thought: I am an idiot. Ergo, my first thought must be wrong. Is this closed under Suc? I am worried that $\lambda n$ does not specify that $C(X((X^i)x))$ are in the Church numerals for all of $0\leq i \leq (n-1)$. Is this wrong?

Answer 1

It seems to me it should look more like this:

$$\operatorname{FCN}_\sigma(x) = \forall X (0\in X \land \forall c.( c\in X \to \operatorname{Suc}(c)\in X))\to x\in X$$

Here I've defined $\operatorname{FCN}(x)$ as a one-place predicate which is true if and only if $x$ is a finite Church numeral. The clause $$ \forall c. (c\in X \to \operatorname{Suc}(c)\in X)$$ should be understood as a predicate $\operatorname{Closed}(X)$ which is true if and only if $X$ is closed under the successor operation. With this definition, we can abbreviate $\operatorname{FCN}_\sigma(x)$ as $$\operatorname{FCN}_\sigma(x) = \forall X.(( 0\in X \land \operatorname{Closed}(X))\to x\in X).$$That is, $x$ is a finite Church numeral if and only if it is in every set $X$ that includes $0$ and that is closed under $\operatorname{Suc}$.

Note that your proposal doesn't appear to say anywhere that the set of finite Church numerals includes $0$. I'm not sure what (if anything) your expression denotes, but I think it can't be right for this reason.

(Warning: I may know even less about this than you do, and I am definitely missing a lot of context about notational conventions and such. For example, should there be a $\lambda T$ on the front of $\operatorname{FCN}$ to capture the type $\sigma$ for its implicit use in $\forall_{(T\to T)\to(T\to T)}c$? To know that I would have to read the book. But perhaps this post will be a useful source of ideas despite my ignorance.)