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 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:
We prove each of these by proving implication in both directions.
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
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
(P -> False) -> False we’ll get
False and using
False we can get anything!
This is all the intuition we need to prove
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
Peirce 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 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
(** 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
This is easier than the last proof. When proving
de_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 / 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.
classic 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
Q set to
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
I spent the most time proving this one, or rather, in proving
excluded_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 / (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.
Classic is universally quantified over
apply it and explore:
apply Classic. intros H.
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
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.
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.
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
P_False_False to get a
P which we use on
H to get a
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.
classic is much easier:
intros H Prp Double_Neg. specialize H with Prp.
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
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
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.
excluded_middle is easy too, after introductions:
Implies_To_Or : forall P Q : Prop, (P -> Q) -> (P -> False) / Q P : Prop ============================ P / (P -> False)
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
The source is up on github.