Classical Axioms in Coq

For the past few days I’ve been working through an amazing text, Software Foundations, which aims to develop “basic concepts of functional programming, logic, operational semantics, lambda-calculus, and static type systems, using the Coq proof assistant”. This post is an annotated solution (I know, I’ve been doing a lot of those lately) to an interesting problem stated in the text.

The Problem

The following five statements are often considered as characterizations of classical logic (as opposed to constructive logic, which is what is “built in” to Coq). We can’t prove them in Coq, but we can consistently add any one of them as an unproven axiom if we wish to work in classical logic. Prove that these five propositions are equivalent.

Definition peirce := forall P Q: Prop,
  ((P->Q)->P)->P.
Definition classic := forall P:Prop,
  ~~P -> P.
Definition excluded_middle := forall P:Prop,
  P / ~P.
Definition de_morgan_not_and_not := forall P Q:Prop,
  ~(~P/~Q) -> P/Q.
Definition implies_to_or := forall P Q:Prop,
  (P->Q) -> (~P/Q).

Since logical equivalence is transitive and symmetric, it is sufficient to prove each of the following:

  • peirceclassic
  • classicde_morgan_not_and_not
  • classicexcluded_middle
  • excluded_middleimplies_to_or

We prove each of these by proving implication in both directions.

peirceclassic

We start with the usual niceties (I’ll omit these in later proofs):

Theorem peirce_classic: peirce  classic.
Proof.
  unfold iff. unfold peirce. unfold classic. unfold not.
  split.

This, followed by

  intros Peirce P Classic.

drops us into our first goal, incidentally the easier of the two:

  Peirce : forall P Q : Prop, ((P -> Q) -> P) -> P
  P : Prop
  Classic : (P -> False) -> False
  ============================
   P

This sub-proof seemed easier to me because here we’re free to choose Q. We can get P from Peirce if we can somehow manage a (P -> Q) -> P for a Q of our choice. Can we somehow use (P -> False) -> False to make a (P -> Q) -> P? To make a (P -> Q) -> P, we need make a P from a given P -> Q. We already have a (P -> False) -> False. If we set Q to False, using (P -> False) -> False we’ll get False and using False we can get anything!
This is all the intuition we need to prove PeirceClassic:

  assert ((P -> False) -> P) as P_False_P.
    intros P_False.
    apply Classic in P_False.
    inversion P_False. (** P_False is false now *)
  apply Peirce in P_False_P. (** P_False_P is now P *)
  apply P_False_P.

I found proving ClassicPeirce a bit harder since we are no longer free to choose Q to our convenience.

  Classic : forall P : Prop, ((P -> False) -> False) -> P
  P : Prop
  Q : Prop
  P_Q_P : (P -> Q) -> P
  ============================
   P

We first need to decide whether to start with Classic or with P_Q_P, both of them result in P and are fair game at first sight. If we try to use P_Q_P we’d have to somehow come up with a term for P -> Q, something that given a P gives a Q. But Q could be anything (pre-decided, out of our control)! This seems a great lot harder (if not impossible) than providing a term for (P -> False) -> False which has no such problems.

The intuition for getting a (P -> False) -> False is this: we have a (term of type) P -> False and need to somehow transform this to (a term of type) False. We can do this if we can get a term of type P from somewhere (the constructive analog of conjuring up a classical contradiction). P_Q_P can be used to get a P, but we don’t know how to create Q. However, this time around, we have with us a term (a hypothesis) of type P -> False and since False -> Z for any Z, we can have P -> Z for any Z. In other words, inside P -> Q, we can first use the P (antecedent) on the P -> False we already have to create a False and once we have False we can create anything (including Q) from it. Inside the (P -> False) -> False term, we first using above technique to create a P and then use that P on the given P -> False to create a False.

  (** From Classic to Peirce *)
  intros Classic P Q P_Q_P.
  assert ((P -> False) -> False) as P_Classic.
    intros P_False.
    assert (P -> Q) as P_Q.
      intros Given_P.
      apply P_False in Given_P.
      inversion Given_P. (** Given_P is false *)
    apply P_Q_P in P_Q. (** P_Q_P is now P *)
    apply P_False in P_Q.
    apply P_Q.
  apply Classic in P_Classic. (** P_Classic is P now *)
  apply P_Classic.

and this also proves peirceclassic.

Qed.

classicde_morgan_not_and_not

This is easier than the last proof. When proving classicde_morgan_not_and_not, Coq says

  Classic : forall P : Prop, ((P -> False) -> False) -> P
  P : Prop
  Q : Prop
  P_False_Q_False_False : (P -> False) / (Q -> False) -> False
  P_Or_Q_False : P / Q -> False
  ============================
   False

The trick for this proof is that given P / Q -> False, we can separately make both P -> False and Q -> False by simply injecting the P or Q into P / Q and then invoking the P / Q -> False term on it.

  assert ((P -> False) / (Q -> False)).
    split.
    (** P is False *)
    intros.
    apply or_introl with (Q:=Q) in H.
    apply P_Or_Q_False in H. apply H.

    (** Q is False *)
    intro.
    apply or_intror with (P:=P) in H.
    apply P_Or_Q_False in H. apply H.

Once we have a P / Q -> False, getting a False is easy.

  apply P_False_Q_False_False in H. apply H.

de_morgan_not_and_notclassic is easy too:

  De_Morgan : forall P Q : Prop,
              ((P -> False) / (Q -> False) -> False) -> P / Q
  P : Prop
  Classic : (P -> False) -> False
  ============================
   P

The trick here is to specialize De_Morgan with both P and Q set to P.

  assert ((P -> False) / (P -> False) -> False).
    intros.
    inversion H as [P_False0 P_False1].
      apply Classic in P_False0. apply P_False0.

  apply De_Morgan in H.
  inversion H as [Ans_0 | Ans_1].
    apply Ans_0.
    apply Ans_1.

and were done proving classicde_morgan_not_and_not

Qed.

classicexcluded_middle

I spent the most time proving this one, or rather, in proving classicexcluded_middle. After the usual introductions,

  Classic : forall P : Prop, ((P -> False) -> False) -> P
  P : Prop
  ============================
   P / (P -> False)

We could try to get a P out of Classic and then inject that P into P / (P -> False). However, this approach didn’t look like it’d work out: I don’t know if P is true (which is very close to what we’re trying to prove — even though we don’t know whether there is a term for P or not, either there is one for P or one for P -> False) and hence I should not be able to arbitrarily deduce the existence of the a term of that type.

Since Classic is universally quantified over P, we apply it and explore:

  apply Classic.
  intros H.

gives

  Classic : forall P : Prop, ((P -> False) -> False) -> P
  P : Prop
  H : P / (P -> False) -> False
  ============================
   False

We can’t use Classic here, since if we did, we’d have to instantiate P with False and have to provide a term of the type (False -> False) -> False. Given a False -> False, the only way to get a False is to provide a False to the antecedent (False -> False). But, if we had a way to get a False from somewhere (given a False -> False) we could use that directly (without going inside (False -> False) -> False) since it is trivial to create a False -> False term out of nowhere.

The only other possibility is to come up with a P / (P -> False) and use H on it.

  assert ((P -> False) -> False) as P_False_False.
    intro P_False.

gives

  Classic : forall P : Prop, ((P -> False) -> False) -> P
  P : Prop
  H : P / (P -> False) -> False
  P_False : P -> False
  ============================
   False

We’re finally at the point where things get obvious. We can now inject P_False to a P / (P -> False) and use that to get the False we need.

    apply or_intror with (P:=P) in P_False.
    apply H in P_False.
    apply P_False.

gives

  Classic : forall P : Prop, ((P -> False) -> False) -> P
  P : Prop
  H : P / (P -> False) -> False
  P_False_False : (P -> False) -> False
  ============================
   False

This goal is slightly tricky, but we’re almost done. We use Classic on P_False_False to get a P which we use on H to get a False.

  apply Classic in P_False_False.
  apply or_introl with (Q:=(P -> False)) in P_False_False.
  apply H in P_False_False.
  apply P_False_False.

excluded_middleclassic is much easier:

  intros H Prp Double_Neg.
  specialize H with Prp.

gives

  Prp : Prop
  H : Prp / (Prp -> False)
  Double_Neg : (Prp -> False) -> False
  ============================
   Prp

H tells us that P is either true or false. In case it is true, the conclusion directly follows. In case it isn’t. we use Double_Neg to get a False, from which anything follows:

  inversion H as [P | NegP].
  (** P is true *)
  apply P.
  (** P is false *)
  apply Double_Neg in NegP. inversion NegP.

And this proves classicexcluded_middle!

Qed.

excluded_middleimplies_to_or

This is probably the easiest one. After usual introductions,

  Excluded_Middle : forall P : Prop, P / (P -> False)
  P : Prop
  Q : Prop
  Implication : P -> Q
  ============================
   (P -> False) / Q

Excluded_Middle either gives us a term of type P from which we can get a Q using Implication or it gives us a term of type (P -> False). In either case, we have a way to construct (P -> False) / Q.

  specialize Excluded_Middle with P.
  inversion Excluded_Middle.
    apply Implication in H. right. apply H.
    left. apply H.

Proving implies_to_orexcluded_middle is easy too, after introductions:

  Implies_To_Or : forall P Q : Prop, (P -> Q) -> (P -> False) / Q
  P : Prop
  ============================
   P / (P -> False)

Note that Implies_To_Or with P := P and Q := P proves our goal for (almost) free.

  specialize Implies_To_Or with P P.
  assert (P -> P).
    intros. apply H.
  apply Implies_To_Or in H.
  inversion H as [HL | HR].
    right. apply HL.
    left. apply HR.

and this proves excluded_middleimplies_to_or.

The source is up on github.

Advertisements
This entry was posted in Computers and tagged , , , , , , . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s