Church's arithmetic in Coq

In your crash course on Coq, you have seen that Coq can do predicate logic.

You have also seen that, on top of this, the logic of Coq has the theory of equality and Peano's arithmetic built-in.

When those theories are encoded in predicate logic as in your INF412 course notes, the proof of `45*67=3015`

is huge.

And this is the case, whether we do it directly with Peano's axioms, or indirectly in a stronger theory of predicate logic such as set theory (ZF) -as you have seen in lectures.

Church's theory of simple types, today known as Higher-Order Logic, addresses this issue, incorporating direct computations (of e.g. `45*67`

) into the logic, so that the proof of `45*67=3015`

only takes a couple of steps.

The logic of Coq is an extension of Higher-Order Logic, but equality and natural numbers in Coq are not encoded the way Church suggested.

In this practical, we forget about Coq's in-built equality and natural numbers, to come back to Church's original presentation of arithmetic in Higher-Order Logic.

Open the file `church.v`

in Proof General.

Higher-Order Logic allows you to quantify over predicates, so that equality on type `a`

can be **defined** according to Leibniz's principle, rather than **assumed** axiomatically (as you do in predicate logic).

Using the definition provided,

`church.v`

.

Church's trick to represent natural numbers in higher-order logic can be illustrated by saying that the number 3 is *the concept of re-iterating three times a function f over an argument x*.

More generally, a number `n`

is represented as a function taking as arguments an element `x`

and a function `f`

, and producing the element obtained by applying `f`

, `n`

times over `x`

.

The (simple) type of natural numbers is therefore `a->(a->a)->a`

, which is parameterised by the type `a`

of the argument `x`

.
We abbreviate this type by `natT a`

.

Similarly, the number 0 (is represented by the function that) takes as arguments an element `x`

and a function `f`

, and produces the element obtained by applying `f`

, `0`

times over `x`

, in other words, producing `x`

.

Look at the corresponding representation of 0 in `church.v`

.

Now look at the definition of successor, addition, and multiplication.

To force it to hold, Church's trick is simply to restrict the notion of natural numbers to those inhabitant of `natT a`

that satisfy every hereditary property.

Look at the corresponding definition of `Nat a`

in `church.v`

Now every statement of the form "for all natural number n,..." will be represented by `forall n, Nat a n ->...`

Conversely, every statement of the form "there exists a natural n such that..." will be represented by `exists n, Nat a n /\...`

Of course, we should check that the natural numbers we can write **do** satisfy `Nat a`

.

`church.v`

Now

This cannot be proved for every kind of Church's numerals, but it **can** be proved for Church's numerals over a type `a`

that has two distinct inhabitants (a property defined as `two a`

in `church.v`

).

`Prop`

itself is such a type.

`True`

and `not True`

).

Now

Finally, the last missing axiom is the injectivity of successor.

There is no trick to enforce it, the only way to have it in Higher-Order Logic (at least with Church's numerals) is to assume it as an axiom (this is what we do in predicate logic anyway, and in set theory the injectivity of successor is the consequence of other axioms...)

This is what motivated the development of Coq on an *extension* of Higher-Order Logic with **inductive types**, which have all of these properties **built-in**.

`35*67=3015`

represented in Church's arithmetic. The proof has to hold in one command.

If you have time,