6
$\begingroup$

I've read that System F cannot state or prove theorems of the First Order Theory of Arithmetic. I assume this is because we lack dependent types, so we cannot explicitly express $\forall n:\mathbb{N}.P(n)$ as an inhabitable type. Thus, $\lambda\Pi$/LF seems promising despite its lacking expressivity of functions.

My question concerns whether it is even possible to encode proofs of arithmetic in $\lambda\Pi$. I am assuming there would need to be some sense of equality, perhaps a type only inhabited when two terms are $\beta\eta$-equivalent. Some sense of induction seems necessary also. I'm not convinced that such things wouldn't require additional inference rules to the theory.

At a minimum, I'm interested in being able to encode statements like "$\forall x \forall y. x + y = y + x$", or "$\forall x\exists y.x<y\land\textrm{prime}(y)$", and I don't know if these can even be encoded as types.

  • Can theorems of arithmetic be encoded and proved in plain $\lambda\Pi$? If not, what's required?
Improve this question
$\endgroup$
6
  • $\begingroup$ Waht is $\lambda P$? Also, a lot depends on how you intend to encode arithmetic and logic in these systems. $\endgroup$ – Andrej Bauer May 25 '20 at 6:38
  • $\begingroup$ $\lambda P$/$\lambda\Pi$/LF logical framework is the Simply Typed Lambda Calculus with dependent types, generalizing function types to universal quantification. Whereas System F permits quantification over higher-order objects (types). Are you saying that proofs of arithmetic can be encoded in either of these systems? $\endgroup$ – bitconfused May 25 '20 at 15:56
  • $\begingroup$ Ah, $\lambda\Pi$, why didn't you say so :-) So you're proposing an axiomatization of Peano arithemtic inside $\lambda\Pi$ (in some fashion)? What I am saying is that a large part of your question involves figuring out what it means to "prove statements about arithmetic in $\lambda\Pi$". It would help if you sketched that out. $\endgroup$ – Andrej Bauer May 25 '20 at 16:44
  • 1
    $\begingroup$ My first istinct, without thinking carefully, would be that due to adequacy of LF if you formulate PA inside LF you will get precisely the provable statements of PA. So you will gain or lose precisely the difference between "second order definable functions" and "first order definable functions". $\endgroup$ – Andrej Bauer May 25 '20 at 16:46
  • $\begingroup$ @AndrejBauer That appears to be the case. I've summed up and refined my interests in the question. $\endgroup$ – bitconfused May 25 '20 at 17:45
5
$\begingroup$

As Andrej notes, $\lambda\Pi$ is a conservative extension of first-order logic which means:

Adding the axioms of PA to $\lambda\Pi$ gives exactly the same arithmetic theorems as PA.

However, because of the more expressive system, it is possible to finitely axiomatize induction using the following (encoding of) this axiom:

$$ \forall P: {\mathbb N}\rightarrow \mathrm{Type}, P\ 0 \rightarrow (\forall n, P\ n \rightarrow P\ (S\ n))\rightarrow \forall n, P\ n$$

Note that you need a single Martin-Löf universe to be able to state this. Adding equality and the other PA axioms (definitions for $+$, $\times$, injectivity of $S$) in a similar manner, one might ask if this axiomatization is conservative over PA, or rather HA, since we don't necessarily want the Excluded Middle.

The answer is yes, though this is quite a non-trivial thing! The proof involves some somewhat deep ideas from the field of realizability.

Finally, though this is a fine axiomatic system, it may be frustrating to note that $+$ and $\times$ (and equality, I guess) do not have the computational behavior one might expect in a dependently typed theory, as one would in a system like Coq or Agda.

This is where Martin-Löf's inductive families comes in: one can give a computational content to the induction axiom, which allows one to define addition and multiplication, as well as prove injectivity of $S$ if enough power is given to the type-level computation rules (this point is probably a story for another time).

And finally one can even define existential quantifiers and equality itself using these families, which is a quite remarkable observation from the theory of inductive families.

Note that Twelf seems to frown upon these last 2 steps, preferring to keep $\beta$ equality alone in its computation, and having predicates for everything else. They have their reasons, I guess.

Improve this answer
$\endgroup$
4
  • $\begingroup$ This is great! If induction is to be axiomatized as such (not as a function, but as a type former), wouldn't we need to be able to define predicates as so: $(\lambda n:\mathbb{N}.n+0=0):\mathbb{N}\rightarrow\textrm{Type}$. Are lambda abstractions which return a type part of the language of $\lambda\Pi$? $\endgroup$ – bitconfused May 27 '20 at 4:28
  • 1
    $\begingroup$ @bitconfused, yes, in the PTS version of $\lambda\Pi$, this is enabled by the $(*,\square)$ rule. $\endgroup$ – cody May 27 '20 at 11:34
  • $\begingroup$ Ah of course, thank you! Suppose we did give computational content to induction by adding an evaluation rule, e.g. reduce to the value inhabitting $P n$. Now we can fold and compute very powerful functions. Especially by using clever motives $P$, we can compute/prove the totality of Ackermann's function. Have we approached the computational expressivity of theories like System F? $\endgroup$ – bitconfused May 28 '20 at 0:05
  • 1
    $\begingroup$ No, you're still conservative over HA, so you can only define functions provably total in PA. You're still very (very very) far from system F, which is impredicative. $\endgroup$ – cody May 28 '20 at 12:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.