The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 18/04/14 12:17, Gabriel Scherer wrote:
> 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

Many thanks!

I did not study modal logic so I cannot immediately appreciate the first 
approach.
(It may be quite effective and general way to deal with these kind of 
problems (?))

The second approach is inspiring because it does not involve unfamiliar 
notions although I still hesitate to consider it convincing.
On the other hand I think similarly simple as well as rock solid argument can 
be made.
According to the context where the problem was stated, the complete set of 
tactics is:
- assumption
- exact
- apply
- intro

We can start with the original judgement:

  P Q : Prop ⊢? ((P → Q) → P) → P

and use tactics to exhaustively explore the "directed proof hypergraph"
(nodes are judgments
 hyperedges are tactics leading from the original goal to the generated 
subgoals)

The complete "proof hypergraph" in this case is managably small
(4 nodes and 3 hyperedges)

None of the nodes has empty consequent. Thus:

  P Q : Prop ⊬ ((P → Q) → P) → P