Nuprl Definition : tcWO
The relation x > y is transitive, and for any infinite sequence f
there exists i < j 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 a weaker condition than the condition for a well-quasi-order.
If > is a 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 < j for which ⌜(f i) ≤ (f j)⌝, (and ⌜x ≤ y⌝ is transitive)
so, ⌜x ≤ y⌝ is a well-quasi-order.
But, if > is not a 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 a tactic, woInduction R, that can be used to prove
by induction things that have a 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; f 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: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
implies: P ⇒ 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: f a
FDL editor aliases :
tcWO
Latex:
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