# Unprovable Equivalence in Type Theory

Let $\prec$ be a binary relation on a set $A$… A predicate $P(x)$ set $(x:A)$ is said to be progressive with respect to $(A,\prec)$ if $$(\forall a:A)\Big((\forall b:A)\big(b \prec a \supset P(b)\big)\supset P(a)\Big) \quad \text{true} \tag{*}$$

The binary relation $(A,\prec)$ is said to be well founded if for every progressive predicate $P$ on $A$, $(\forall x: A)P(x)$.

In classical set theory $(A,<)$ is well-founded if and only if for any predicate $P$ on $A$

$$(\exists x: A)P(x) \supset(\exists x_{0}:A)\Big(P(x) \land (\forall y :A)\big(P(y) \supset \neg (y < x_{0})\big)\Big) \tag{**}$$

I was informed by my tutor that this equivalence is unprovable in type theory. Since he did not provide any justifications, I am curious to know what exactly makes this impossible? Would some unacceptable instances of PEM occur?

• What do you mean by "$\subset$" -- you seem to be using it as a logical connective rather than "subset"? Does it mean "is implied by", or is it an attempt to write "$\supset$" (which PM used for "implies")? Dec 16, 2013 at 21:56
• Also, is there a specific type theory you're speaking about? TTBOMK the unqualified term type theory as a "proper noun" usually refers to the system of Principia Mathematica, but there the law of excluded middle was considered "self-evident", so there can hardly be any "unacceptable instances" of it. Dec 16, 2013 at 22:18
• @HenningMakholm It should be read as "is implied by" - my mistake. Thanks for catching me on that one. Dec 16, 2013 at 22:20
• Yes, I'm thinking of intuitionistic type theory. Dec 16, 2013 at 22:22

Let $A = \{ 0, 1 \}$, the inductive type with two constant generators. One can prove (by induction) that the natural ordering on $A$ is well-founded in the sense of ($\ast$). Suppose it were well-founded in the sense of (${\ast}{\ast}$) instead. Let $Q$ be an arbitrary proposition and let $P$ be defined by induction as follows: \begin{align} P(0) & \equiv Q \\ P(1) & \equiv \top \end{align} Thus, there must exist $x_0 : A$ such that $P (x_0)$ and $\forall y : A . P (y) \to \lnot (y < x_0)$. But $\forall a : A . (a = 0) \lor (a = 1)$, so either $x_0 = 0$ or $x_0 = 1$. If $x_0 = 1$ then $P (0)$ holds, i.e. $Q$ holds. If $x_0 = 1$, then $P (0) \to \lnot (0 < 1)$, so $\lnot P (0)$ holds, i.e. $\lnot Q$ holds. Therefore $Q \lor \lnot Q$.

For those who like this kind of thing, here is a proof in Coq:

Inductive Two : Set :=
| zero : Two
| one : Two.

Definition LT (a : Two) (b : Two) : Prop.
destruct a.
destruct b.
exact False.
exact True.
exact False.
Defined.

Lemma LT_is_wf (P : Two -> Prop) (P_is_inductive : forall a : Two, (forall b : Two, (LT b a) -> P b) -> P a) : forall c : Two, P c.
Proof.
assert (P zero).

apply P_is_inductive.
intro b.
intro.
exfalso.
destruct b.
exact H.
exact H.

intro c.
destruct c.
exact H.
apply P_is_inductive.
intro b.
destruct b.
intro.
exact H.
intro.
exfalso.
exact H0.
Qed.

Lemma Two_is_decidable (a : Two) : (a = zero) \/ (a = one).
Proof.
destruct a.
auto.
auto.
Qed.

Definition decider (Q : Prop) : Two -> Prop.
intro a.
destruct a.
exact Q.
exact True.
Defined.

Theorem classical_wf_implies_lem (classical_wf : forall P : Two -> Prop, (exists a : Two, P a) -> (exists m : Two, P m /\ forall b : Two, P b -> not (LT b m))) (Q : Prop) : Q \/ not Q.
Proof.
set (P := decider Q).
assert (exists a : Two, P a).
exists one.
unfold P.
unfold decider.
tauto.
set (S := classical_wf P H).
destruct S.
destruct H0.
assert (x = zero -> Q).
intro.
cut (P zero).
tauto.
rewrite <- H2.
exact H0.
assert (x = one -> not Q).
intro.
intro.
refine (H1 zero _ _).
tauto.
rewrite H3.
unfold LT.
tauto.
cut (x = zero \/ x = one).
intro.
destruct H4.
left.
auto.
right.
auto.
exact (Two_is_decidable x).
Qed.

• That is magnificent! Dec 17, 2013 at 8:30
• Ah, an answer on SE I can really trust... May 14, 2014 at 8:00
• @user43208 - scroll down and/or right to see the rest of the code. May 15, 2014 at 0:16