<p>As Andrej notes, <span class="math-container">$\lambda\Pi$</span> is a conservative extension of first-order logic which means:</p>

<blockquote>
  <p>Adding the axioms of PA to <span class="math-container">$\lambda\Pi$</span> gives exactly the same arithmetic theorems as PA.</p>
</blockquote>

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

<p><span class="math-container">$$ \forall P: {\mathbb N}\rightarrow \mathrm{Type}, P\ 0 \rightarrow (\forall n, P\ n \rightarrow P\ (S\ n))\rightarrow \forall n, P\ n$$</span></p>

<p>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 <span class="math-container">$+$</span>, <span class="math-container">$\times$</span>, injectivity of <span class="math-container">$S$</span>) in a similar manner, one might ask if <em>this</em> axiomatization is conservative over PA, or rather HA, since we don't necessarily want the Excluded Middle.</p>

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

<p>Finally, though this is a fine axiomatic system, it may be frustrating to note that <span class="math-container">$+$</span> and <span class="math-container">$\times$</span> (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.</p>

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

<p>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.</p>

<p>Note that Twelf seems to frown upon these last 2 steps, preferring to keep <span class="math-container">$\beta$</span> equality alone in its computation, and having predicates for everything else. They have their reasons, I guess.</p>

CC BY-SA 4.0
2020-05-27T04:28:34.670Z
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$?
bitconfused
CC BY-SA 4.0
2020-05-27T11:34:05.810Z
@bitconfused, yes, in the PTS version of $\lambda\Pi$, this is enabled by the $(*,\square)$ rule.
cody
CC BY-SA 4.0
2020-05-28T00:05:56.057Z
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?
bitconfused
CC BY-SA 4.0
2020-05-28T12:51:46.087Z
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.
cody
CC BY-SA 4.0
2020-05-26T12:27:37.363Z
2020-05-26T12:27:37.363Z
cody
<p>I've read that System F cannot state or prove theorems of the <em>First Order Theory of Arithmetic</em>. I assume this is because we lack dependent types, so we cannot explicitly express <span class="math-container">$\forall n:\mathbb{N}.P(n)$</span> as an inhabitable type. Thus, <span class="math-container">$\lambda\Pi$</span>/<strong>LF</strong> seems promising despite its lacking expressivity of functions.</p>

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

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

<ul>
<li>Can theorems of arithmetic be encoded and proved in plain <span class="math-container">$\lambda\Pi$</span>? If not, what's required?</li>
</ul>

CC BY-SA 4.0
2020-05-25T06:38:59.957Z
Waht is $\lambda P$? Also, a lot depends on how you intend to encode arithmetic and logic in these systems.
Andrej Bauer
CC BY-SA 4.0
2020-05-25T15:56:07.620Z
$\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?
bitconfused
CC BY-SA 4.0
2020-05-25T16:44:49.377Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-05-25T16:46:38.103Z
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".
Andrej Bauer
CC BY-SA 4.0
2020-05-25T17:45:53.080Z
@AndrejBauer That appears to be the case. I've summed up and refined my interests in the question.
bitconfused
CC BY-SA 4.0
2020-05-25T20:33:06.243Z
Yes, it's possible to formalize PA in LF. If you search the Twelf sources you'll see rudiments of that, and of first-order logic with equality as well.
Andrej Bauer
<type-theory><proof-theory><typed-lambda-calculus>
What arithmetical theorems can plain $\lambda \Pi$ reason about?
bitconfused
# What arithmetical theorems can plain $\lambda \Pi$ reason about?

(Asked by: username_0 on 2020-05-24)

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", 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?

**Tags:** type-theory, proof-theory, typed-lambda-calculus

> **Comments:**
> **username_1**: Waht is $\lambda P$? Also, a lot depends on how you intend to encode arithmetic and logic in these systems.  
> **username_0**: $\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?  
> **username_1**: 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.  
> **username_1**: 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".  
> **username_0**: @AndrejBauer That appears to be the case. I've summed up and refined my interests in the question.  
> **username_1**: Yes, it's possible to formalize PA in LF. If you search the Twelf sources you'll see rudiments of that, and of first-order logic with equality as well.  

---

## 1 answers

### Answer by username_2 on 2020-05-26. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_0**: 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$?  
> **username_2**: @username_0, yes, in the PTS version of $\lambda\Pi$, this is enabled by the $(*,\square)$ rule.  
> **username_0**: 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?  
> **username_2**: 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.  

---

