Nuprl Definition : tcWO

The relation x > is transitive, and for any infinite sequence f
there exists i < for which it is not the case that f(i) > f(j).
Thus there are no infinite descending sequences f(0) > f(1) > f(2) ...

This seems to be weaker condition than the condition for well-quasi-order.
If > is total order, then ⌜¬(x > y) ⇐⇒ (x y) ∨ (y > x)⌝.
In that case, letting ⌜x ≤ y⌝ be ⌜(x y) ∨ (y > x)⌝we have
that there exists i < for which  ⌜(f i) ≤ (f j)⌝(and ⌜x ≤ y⌝ is transitive)
so, ⌜x ≤ y⌝ is well-quasi-order.

But, if > is not total order, then this definition does not rule out
and infinite antichain 
(for which for all i<j,  ⌜((f i) > (f j))) ∧ ((f i) (f j))) ∧ ((f j) > (f i)))⌝.
Nevertheless, we can prove, using strong bar induction, that there is an
induction principle for any tcWO relation 
(i.e. transitive, constructively well-ordered relation).

We have the lemma tcWO-induction 
(which can be used to prove by induction
  things that are already known to be propositions)
and there is tactic, woInduction R, that can be used to prove
by induction things that have trivial witness. ⋅

tcWO(T;x,y.>[x; y]) ==  (∀x,y,z:T.  (>[x; y]  >[y; z]  >[x; z])) ∧ (∀f:ℕ ⟶ T. (↓∃i,j:ℕ(i < j ∧ (¬>[f i; j]))))

Definitions occuring in Statement :  nat: less_than: a < b all: x:A. B[x] exists: x:A. B[x] not: ¬A squash: T implies:  Q and: P ∧ Q apply: a function: x:A ⟶ B[x]
Definitions occuring in definition :  implies:  Q all: x:A. B[x] function: x:A ⟶ B[x] squash: T exists: x:A. B[x] nat: and: P ∧ Q less_than: a < b not: ¬A apply: a
FDL editor aliases :  tcWO

tcWO(T;x,y.>[x;  y])  ==
    (\mforall{}x,y,z:T.    (>[x;  y]  {}\mRightarrow{}  >[y;  z]  {}\mRightarrow{}  >[x;  z]))  \mwedge{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}i,j:\mBbbN{}.  (i  <  j  \mwedge{}  (\mneg{}>[f  i;  f  j]))))

Date html generated: 2016_07_08-PM-04_47_13
Last ObjectModification: 2015_09_22-PM-05_45_25

Theory : bar-induction

Home Index