The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

There are two common ways to prove unprovability of a formula T.

The first one is to exhibit a "model" of the theory where T is false. A model is a mapping from the syntactical concepts of the system to mathematical structures, such that all rules are satisfied. You can prove that a formula is "admissible" (does not introduce a contradiction) by exhibiting a model where it is true, and that it is not provable by exhibiting a model where it is false. That's how we present a lot of unprovability results (Heyting algebras, etc.). The more complex the system, the more work it is to build a model, so building a model of (a reasonable subset of) Coq is a lot of work and the privilege of theory experts, but most people have "informal models" (vague idea of what a model could be) that provide them intuitions about the system. For example, we know that Coq admit proof-irrelevant models (models where all elements of Prop are equated), and proof-relevant models (models where some Prop have distinct elements, or even where all Props have distinct elements), and those alone can kill most "this should be an Axiom, it looks easy to prove" ideas about Prop.

The other solution is to just enumerate possible terms at the type T, and prove that there is none. For this to work (usually there are infinitely many possible terms at a type T), you have to restrict yourself to enumerating only "normal forms" in some sense. Again, the theory of Coq is complex and only experts know for sure what normal forms look like, but a good informal approximation is beta-normal eta-long lambda-terms that look like they have the type you expect. For your example, you can reason as follow:

- all terms of type ((P -> Q) -> P) -> P are equivalent to a term of the form (fun f => ?X), where (f : (P -> Q) -> P) and the hole ?X must have type P.

- the only way to get a (?X : P) in the context (f : (P -> Q) -> P) is to apply f: the hole is of the form (f ?Y), where ?Y must have type (P -> Q).

- all terms of this type (P -> Q) are of the form (fun (p : P) => ?Z), where ?Z must have type Q.

- no variable of the context (f : (P -> Q) -> P) allows to produce a Q, so there is no solution: ?Z cannot be filled, so neither ?Y and ?Z, this type is not inhabited without introducing extra axioms

The relation between these two techniques is as follows: to formally define an acceptable notion of "normal form", you must do meta-theoretical work that amounts to building a (rather specific) model of the theory: unsound systems (have no models and) don't let you define a suitable notion of normal-form. So enumerating normal forms is a way to reuse the works of your peers that did the hard-lifting.

On Fri, Apr 18, 2014 at 1:02 PM, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

Hi all,

I am slowly going through the CoqArt book.
In Section 3.7.2 it is claimed that Peirce's formula

    ((P -> Q) -> P) -> P

is not provable (in Coq).

I am curious, how does the proof (of Pierce's formula unprovability in Coq) look like?
(up to that point, all concepts and exercises seem clear).

Thanks in advance for whatever help.