<p>[Self-advertising follows, but I think that this is relevant.]</p>

<p>There are several possible approaches to this questions. One of the ways (that I explored during my PhD thesis in the context of an ML-like language) is to extend the type system with a first-order layer, so that terms of the language can be manipulated as objects of the underlying logic. Of course, you also need to include some predicates so that there is something to observe. In the case of my system, these predicates are term equivalences. In particular, if $t$ and $u$ are terms of the language, then the type $t \equiv u$ is only inhabited if $t$ and $u$ are indeed (observationally) equivalent. You can use first-order quantifiers to encode properties such as $\forall v, (\lambda x.x)\;v \equiv v$ in types, and they are proved by constructing programs inhabiting them.</p>

<p>Of course you can also assume equivalences, and there are several different forms of quantifiers (typed / untyped, universal / existential). This mechanism can be used to reason about any program (they do not have to be proved terminating or even typed). The only constraint is that programs that are used as proofs must be proved terminating by the system (arbitrary general recursion leads to inconsistency).</p>

<p>Here are a couple of references if you want to check this out:</p>

<ul>
<li><a href="https://lepigre.fr/files/docs/lepigre2017_pml2.pdf" rel="noreferrer">https://lepigre.fr/files/docs/lepigre2017_pml2.pdf</a> (recent paper with examples)</li>
<li><a href="https://tel.archives-ouvertes.fr/tel-01590363" rel="noreferrer">https://tel.archives-ouvertes.fr/tel-01590363</a> (PhD thesis in English)</li>
<li><a href="https://github.com/rlepigre/pml" rel="noreferrer">https://github.com/rlepigre/pml</a> (language implementation)</li>
</ul>

CC BY-SA 4.0
2018-05-24T12:04:19.690Z
2018-05-24T12:04:19.690Z
Rodolphe Lepigre
<p>I've recently attempted to implement Aaron's <a href="https://github.com/MaiaVictor/cedille-core" rel="noreferrer">Cedille-Core</a>, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded datatypes on it, which made clearer why his extensions would be necessary.</p>

<p>Nether less, I'm still left wondering where those extensions came from. Why they are what they are? What justifies them? I know, for example, that some extensions, such as recursion, ruin the language as a system for proofs. If I decided to also extend CoC with other primitives, how would I justify? I understand a proof of normalization is necessary, but that doesn't prove those primitives "make sense".</p>

<p>In short, what specifically what qualifies a language (and its type-system) as a system capable of proving theorems about its own terms?</p>

CC BY-SA 3.0
2018-03-16T08:16:25.883Z
I read a blog that was related to this question, but I am unable to find it now :( It contained the sentence "System T is enough!" or something like that and it talked about dependent type systems.
Labbekak
CC BY-SA 3.0
2018-03-16T08:23:40.377Z
Found it: https://queuea9.wordpress.com/2010/01/17/how-strong-a-type-theory-do-we-need/ It's actually written by Aaron Stump so you might already know about it.
Labbekak
CC BY-SA 3.0
2018-03-16T13:32:18.337Z
Unguarded recursion "ruins" the language as proof system, guarded recursion does not. To prove that the primitives make sense, I'd say that you build a model. And to prove theorems about its own terms, it needs a sort of Curry–Howard isomorphism, and dependent type so that the things you prove (types) can talk about your terms.
xavierm02
<type-theory><functional-programming><constructive-mathematics>
What makes a language (and its type-system) capable of proving theorems about its own terms?
MaiaVictor
# What makes a language (and its type-system) capable of proving theorems about its own terms?

(Asked by: username_0 on 2018-02-28)

I've recently attempted to implement Aaron's [Cedille-Core](https://github.com/MaiaVictor/cedille-core), a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded datatypes on it, which made clearer why his extensions would be necessary.

Nether less, I'm still left wondering where those extensions came from. Why they are what they are? What justifies them? I know, for example, that some extensions, such as recursion, ruin the language as a system for proofs. If I decided to also extend CoC with other primitives, how would I justify? I understand a proof of normalization is necessary, but that doesn't prove those primitives "make sense".

In short, what specifically what qualifies a language (and its type-system) as a system capable of proving theorems about its own terms?

**Tags:** type-theory, functional-programming, constructive-mathematics
> **Comments:**
> **username_1**: I read a blog that was related to this question, but I am unable to find it now :( It contained the sentence "System T is enough!" or something like that and it talked about dependent type systems.  
> **username_1**: Found it: https://queuea9.wordpress.com/2010/01/17/how-strong-a-type-theory-do-we-need/ It's actually written by Aaron Stump so you might already know about it.  
> **username_2**: Unguarded recursion "ruins" the language as proof system, guarded recursion does not. To prove that the primitives make sense, I'd say that you build a model. And to prove theorems about its own terms, it needs a sort of Curry–Howard isomorphism, and dependent type so that the things you prove (types) can talk about your terms.  

---

## 1 answers

### Answer by username_3 on 2018-05-24. Score: 5

[Self-advertising follows, but I think that this is relevant.]

There are several possible approaches to this questions. One of the ways (that I explored during my PhD thesis in the context of an ML-like language) is to extend the type system with a first-order layer, so that terms of the language can be manipulated as objects of the underlying logic. Of course, you also need to include some predicates so that there is something to observe. In the case of my system, these predicates are term equivalences. In particular, if $t$ and $u$ are terms of the language, then the type $t \equiv u$ is only inhabited if $t$ and $u$ are indeed (observationally) equivalent. You can use first-order quantifiers to encode properties such as $\forall v, (\lambda x.x)\;v \equiv v$ in types, and they are proved by constructing programs inhabiting them.

Of course you can also assume equivalences, and there are several different forms of quantifiers (typed / untyped, universal / existential). This mechanism can be used to reason about any program (they do not have to be proved terminating or even typed). The only constraint is that programs that are used as proofs must be proved terminating by the system (arbitrary general recursion leads to inconsistency).

Here are a couple of references if you want to check this out:

* <https://lepigre.fr/files/docs/lepigre2017_pml2.pdf> (recent paper with examples)
* <https://tel.archives-ouvertes.fr/tel-01590363> (PhD thesis in English)
* <https://github.com/rlepigre/pml> (language implementation)


---

