The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I'm always a bit wary of proofs like this: it seems dangerously close
to "proof by lack of imagination".  Not that I'm saying such a proof
is necessarily invalid, it's just that the model-based proofs are much
more (subjectively) convincing to me.

Even in the case of the informal argument that Coq's logic must be
valid: at first, the argument seemed good that a proof of False should
reduce in finite time to a normal form which is ridiculous.  Until I
saw the formalization of Russell's paradox in Coq that almost goes
through, except that it runs into a universe inconsistency.  And then
I realized that the notion of "everything reduces to a normal form in
finite time" is crucial, and significantly more complex than it seemed
at first.

In this particular case, Peirce's law is easily equivalent to classic
(forall P:Prop, P \/ ~P).  And I believe there should be a family of
models of Coq where Type(n) is the category of sheaves of types in
Type(n) on some topological space (or more generally, on some site),
and Prop is the set of open subsets -- or maybe the sheaf where
Prop(U) is the set of open subsets of U, with restriction maps given
by intersection.  But it's easy to see that, for example, if the
topological space is R, then the interpretation of classic fails.  For
example, if P = (0, inf) then ~P ends up being (-inf, 0), so P \/ ~P
is R \ {0} which is not globally true.

(Note that I'm a bit fuzzy on how exactly the model should work, as
you can probably tell, but I'm convinced that it should work if you
get everything sorted out on what should be interpreted globally and
what should be interpreted locally on sheaves.)

On Fri, Apr 18, 2014 at 4:17 AM, Gabriel Scherer
<gabriel.scherer AT gmail.com>
 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
>
> 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.
>
>