<p>I'll turn my comments into an answer: In general, if you do not have any axioms or "stuck" terms, you cannot have a normal proof of <span class="math-container">$\mathrm{False}\simeq\forall X:*,X$</span> in a system like the CoC (or extensions of it). The (classical) proof I outlined <a href="https://cstheory.stackexchange.com/a/36986/3984">here</a> applies, crucially using inversion in several places.</p>

<p>I believe it's not hard to have a normal proof of <span class="math-container">$\mathrm{True}\rightarrow\mathrm{False}$</span> in an inconsistent system, however, by "blocking" some of the redexes with a variable. Applying this proof to any closed term of type <span class="math-container">$\mathrm{True}$</span> would then lead to non-termination.</p>

<hr>

<p>This leads to a pretty natural question, which I will also outline here: is it possible to reason correctly about programs in an inconsistent language, as long as every "proof-like" term is normalized?</p>

<p>The answer to this seems to be mostly affirmative, though the meta-theory is quite finicky: it's easy to lose even type preservation if one is not careful!</p>

<p>The most comprehensive exploration of this idea to my knowledge is the PhD dissertation of Vilhelm Sjöberg: <a href="https://www.cis.upenn.edu/~sweirich/papers/sjoberg-thesis.pdf" rel="nofollow noreferrer">A Dependently Typed Language with Nontermination</a>.</p>

CC BY-SA 4.0
2018-12-31T01:15:10.870Z
I'd like to recommend Vladimir Voevodsky's lecture [What if Current Foundations of Mathematics are Inconsistent?](https://www.youtube.com/watch?v=O45LaFsaqMA). The relevant part is that, even if it is inconsistent, in the type theory we can trust the proofs that we can normalize [but we can't be sure that all of them will].
Łukasz Lew
CC BY-SA 4.0
2018-12-31T02:31:28.200Z
@ŁukaszLew I'm not sure I can wholeheartedly endorse the content of that lecture, which I think many will agree is a bit strange. I think there's no real debate that the truth $\Delta_0$ statements is pretty much agreed upon (we have complete and plausible systems for them). But as I explained in the comments, those are the only ones normalization really helps with. I think the only real route for trust in formal systems is relative consistency statements, as the field has been exploring for many years.
cody
CC BY-SA 4.0
2018-12-31T16:44:41.027Z
@cody just letting you know that the andrew.cmu.edu/~croux link on your profile is broken.
MaiaVictor
CC BY-SA 4.0
2018-12-31T16:52:24.767Z
What are then all the properties a type system should have so that it can be used to reason correctly its about programs? Just soundness?
MaiaVictor
CC BY-SA 4.0
2019-06-26T14:55:17.280Z
@MaiaVictor late reply, but in general it depends what you want to know! Soundness is usually a big part of it though: it usually constrains very strongly what normal forms look like, if they exist. If you want to use propositions-as-types, you usually do want normalization.
cody
CC BY-SA 4.0
2018-12-29T16:50:54.807Z
2018-12-29T16:50:54.807Z
cody
<p>Suppose we take a language such as Agda and disable the features that make it consistent; for example, universe polymorphism, structural recursion checks and similar. Suppose then that we take a term in normal form, i.e., with no redex left. Could that term prove an absurd claim such as, for example, <code>1 = 2</code>, despite the fact it is normalised (and, thus, doesn't include infinite loops)?</p>

CC BY-SA 4.0
2018-12-25T18:08:39.627Z
No, there is no proof of false in normal form in a (non-pathological) type system which verifies progress and preservation. All proofs of false must be infinitely looping.
cody
CC BY-SA 4.0
2018-12-25T23:27:19.230Z
@cody thanks. Just to be sure, we can still have a proof of something like `f : Unit -> False`, right? Since `f void` would loop forever, but `f` itself not. Also I believe your comment should be a valid answer despite its brevity.
MaiaVictor
CC BY-SA 4.0
2018-12-26T02:16:06.417Z
That is correct: a you can "hide" redexes if you are in a function type. But a term of type $\forall X:*, X$ cannot be in normal form. I'll make it an answer if I can find a nice write up (I think I have one in another answer).
cody
CC BY-SA 4.0
2018-12-28T20:27:50.910Z
@cody I was wondering if a language with non-structural recursion could be used as a proof language by considering only normalised proofs valid. Of course, it wouldn't have a terminating checker, but as long as it doesn't emit false proofs, that's acceptable. Problem is, if you can have `Unit -> False`, then you can also have something like `∀ (a : Nat) -> a + 1 == a`, right? Thus, in such language, `->` could not be read a logical forall, making the idea flawed. Is this correct? Or is there a way to achieve what I want? Perhaps converting foralls to ADTs?
MaiaVictor
CC BY-SA 4.0
2018-12-29T16:53:33.190Z
that is correct, you can inhabit every type, and only $\Delta_0$ propositions can be checked to be correct by normalization. However, this is related to the notion of *partial* correctness, which is to replace proofs with statements of the form: "either this program doesn't terminate, or some proposition holds". I've tried to outline this in my answer.
cody
<type-theory><agda>
Can a term on normal form prove an illogical assertion?
MaiaVictor
# Can a term on normal form prove an illogical assertion?

(Asked by: username_0 on 2018-12-24)

Suppose we take a language such as Agda and disable the features that make it consistent; for example, universe polymorphism, structural recursion checks and similar. Suppose then that we take a term in normal form, i.e., with no redex left. Could that term prove an absurd claim such as, for example, `1 = 2`, despite the fact it is normalised (and, thus, doesn't include infinite loops)?

**Tags:** type-theory, agda
> **Comments:**
> **username_1**: No, there is no proof of false in normal form in a (non-pathological) type system which verifies progress and preservation. All proofs of false must be infinitely looping.  
> **username_0**: @cody thanks. Just to be sure, we can still have a proof of something like `f : Unit -> False`, right? Since `f void` would loop forever, but `f` itself not. Also I believe your comment should be a valid answer despite its brevity.  
> **username_1**: That is correct: a you can "hide" redexes if you are in a function type. But a term of type $\forall X:*, X$ cannot be in normal form. I'll make it an answer if I can find a nice write up (I think I have one in another answer).  
> **username_0**: @cody I was wondering if a language with non-structural recursion could be used as a proof language by considering only normalised proofs valid. Of course, it wouldn't have a terminating checker, but as long as it doesn't emit false proofs, that's acceptable. Problem is, if you can have `Unit -> False`, then you can also have something like `∀ (a : Nat) -> a + 1 == a`, right? Thus, in such language, `->` could not be read a logical forall, making the idea flawed. Is this correct? Or is there a way to achieve what I want? Perhaps converting foralls to ADTs?  
> **username_1**: that is correct, you can inhabit every type, and only $\Delta_0$ propositions can be checked to be correct by normalization. However, this is related to the notion of *partial* correctness, which is to replace proofs with statements of the form: "either this program doesn't terminate, or some proposition holds". I've tried to outline this in my answer.  

---

## 1 answers

### Answer by username_1 on 2018-12-29. Score: 3 | Accepted answer

I'll turn my comments into an answer: In general, if you do not have any axioms or "stuck" terms, you cannot have a normal proof of $\mathrm{False}\simeq\forall X:\*,X$ in a system like the CoC (or extensions of it). The (classical) proof I outlined [here](https://cstheory.stackexchange.com/a/36986/3984) applies, crucially using inversion in several places.

I believe it's not hard to have a normal proof of $\mathrm{True}\rightarrow\mathrm{False}$ in an inconsistent system, however, by "blocking" some of the redexes with a variable. Applying this proof to any closed term of type $\mathrm{True}$ would then lead to non-termination.

---

This leads to a pretty natural question, which I will also outline here: is it possible to reason correctly about programs in an inconsistent language, as long as every "proof-like" term is normalized?

The answer to this seems to be mostly affirmative, though the meta-theory is quite finicky: it's easy to lose even type preservation if one is not careful!

The most comprehensive exploration of this idea to my knowledge is the PhD dissertation of Vilhelm Sjöberg: [A Dependently Typed Language with Nontermination](https://www.cis.upenn.edu/~sweirich/papers/sjoberg-thesis.pdf).

> **Comments:**
> **username_2**: I'd like to recommend Vladimir Voevodsky's lecture [What if Current Foundations of Mathematics are Inconsistent?](https://www.youtube.com/watch?v=O45LaFsaqMA). The relevant part is that, even if it is inconsistent, in the type theory we can trust the proofs that we can normalize [but we can't be sure that all of them will].  
> **username_1**: @ŁukaszLew I'm not sure I can wholeheartedly endorse the content of that lecture, which I think many will agree is a bit strange. I think there's no real debate that the truth $\Delta_0$ statements is pretty much agreed upon (we have complete and plausible systems for them). But as I explained in the comments, those are the only ones normalization really helps with. I think the only real route for trust in formal systems is relative consistency statements, as the field has been exploring for many years.  
> **username_0**: @cody just letting you know that the andrew.cmu.edu/~croux link on your profile is broken.  
> **username_0**: What are then all the properties a type system should have so that it can be used to reason correctly its about programs? Just soundness?  
> **username_1**: @MaiaVictor late reply, but in general it depends what you want to know! Soundness is usually a big part of it though: it usually constrains very strongly what normal forms look like, if they exist. If you want to use propositions-as-types, you usually do want normalization.  

---

