## 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:

• `peirce``classic`
• `classic``de_morgan_not_and_not`
• `classic``excluded_middle`
• `excluded_middle``implies_to_or`

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

`peirce``classic`

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 `Peirce``Classic`:

```  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 `Classic``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`. 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 `peirce``classic`.

```Qed.
```

`classic``de_morgan_not_and_not`

This is easier than the last proof. When proving `classic``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` 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_not``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 `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 `classic``de_morgan_not_and_not`

```Qed.
```

`classic``excluded_middle`

I spent the most time proving this one, or rather, in proving `classic``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` 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_middle``classic` 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 `classic``excluded_middle`!

```Qed.
```

`excluded_middle``implies_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_or``excluded_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_middle``implies_to_or`.

The source is up on github.

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