Unprovable Equivalence in Type Theory

Question

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 \begin{equation} (\forall a:A)\Big((\forall b:A)\big(b \prec a \supset P(b)\big)\supset P(a)\Big) \quad \text{true} \tag{*} \end{equation}

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$

\begin{equation} (\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{**} \end{equation}

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?

Answer 1

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.