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)?

  • 4
    $\begingroup$ 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. $\endgroup$ – cody Dec 25 '18 at 18:08
  • 1
    $\begingroup$ @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. $\endgroup$ – MaiaVictor Dec 25 '18 at 23:27
  • 1
    $\begingroup$ 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). $\endgroup$ – cody Dec 26 '18 at 2:16
  • $\begingroup$ @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? $\endgroup$ – MaiaVictor Dec 28 '18 at 20:27
  • $\begingroup$ 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. $\endgroup$ – cody Dec 29 '18 at 16:53

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

  • $\begingroup$ I'd like to recommend Vladimir Voevodsky's lecture What if Current Foundations of Mathematics are Inconsistent?. 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]. $\endgroup$ – Łukasz Lew Dec 31 '18 at 1:15
  • $\begingroup$ @Ł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. $\endgroup$ – cody Dec 31 '18 at 2:31
  • $\begingroup$ @cody just letting you know that the andrew.cmu.edu/~croux link on your profile is broken. $\endgroup$ – MaiaVictor Dec 31 '18 at 16:44
  • $\begingroup$ 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? $\endgroup$ – MaiaVictor Dec 31 '18 at 16:52
  • $\begingroup$ @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. $\endgroup$ – cody Jun 26 '19 at 14:55

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.