Nuprl Definition : b-almost-full
A binary relation R on ℕ is almost full if every strictly increasing sequence s
must have a pair s(n), s(m) (with n < m) related by R.
But the n and m need not be an extensional property of s because we have
"squashed" the proposition ⌜∃n:ℕ. ∃m:{n + 1...}. R[s n; s m]⌝
using the quotient by //True.
This allows us to prove that relations are almost full using
bar induction on monotone bars, which relies on continuity -- which is
not extensional.
The key lemma used to prove the Intuitionistic Ramsey Theorem (Veldman & Bezem)
(See intuitionistic-Ramsey) is b-almost-full-intersection, which
uses monotone-bar-induction-strict3
That is a variant of bar induction on monotone bars, which follows from
bar induction on decidable bars and the strong continuity principle
-- two Brouwerian principles that we have proved to be true in Nuprl
using our Nuprl-in-Coq meta-theory.
⋅
b-almost-full(n,m.R[n; m]) == ∀s:StrictInc. ⇃(∃n:ℕ. ∃m:{n + 1...}. R[s n; s m])
Definitions occuring in Statement :
strict-inc: StrictInc,
quotient: x,y:A//B[x; y],
int_upper: {i...},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
true: True,
apply: f a,
add: n + m,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
strict-inc: StrictInc,
quotient: x,y:A//B[x; y],
nat: ℕ,
exists: ∃x:A. B[x],
int_upper: {i...},
add: n + m,
natural_number: $n,
apply: f a,
true: True
FDL editor aliases :
b-almost-full
Latex:
b-almost-full(n,m.R[n; m]) == \mforall{}s:StrictInc. \00D9(\mexists{}n:\mBbbN{}. \mexists{}m:\{n + 1...\}. R[s n; s m])
Date html generated:
2016_07_08-PM-04_49_56
Last ObjectModification:
2015_12_21-AM-00_33_13
Theory : continuity
Home
Index