2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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")? $\endgroup$ – Henning Makholm Dec 16 '13 at 21:56
  • $\begingroup$ 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. $\endgroup$ – Henning Makholm Dec 16 '13 at 22:18
  • $\begingroup$ @HenningMakholm It should be read as "is implied by" - my mistake. Thanks for catching me on that one. $\endgroup$ – user116234 Dec 16 '13 at 22:20
  • $\begingroup$ Yes, I'm thinking of intuitionistic type theory. $\endgroup$ – user116234 Dec 16 '13 at 22:22
4
$\begingroup$

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.
$\endgroup$
  • $\begingroup$ That is magnificent! $\endgroup$ – user116234 Dec 17 '13 at 8:30
  • 1
    $\begingroup$ Ah, an answer on SE I can really trust... $\endgroup$ – David Roberts May 14 '14 at 8:00
  • $\begingroup$ @user43208 - scroll down and/or right to see the rest of the code. $\endgroup$ – David Roberts May 15 '14 at 0:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.