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$
4
  • $\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$ Dec 16, 2013 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$ Dec 16, 2013 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, 2013 at 22:20
  • $\begingroup$ Yes, I'm thinking of intuitionistic type theory. $\endgroup$
    – user116234
    Dec 16, 2013 at 22:22

1 Answer 1

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