Nuprl Definition : b-almost-full

binary relation on ℕ is almost full if every strictly increasing sequence s
must have pair s(n), s(m) (with n < m) related by R.
But the and need not be an extensional property of because we have
"squashed" the proposition ⌜∃n:ℕ. ∃m:{n 1...}. R[s n; 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-Ramseyis b-almost-full-intersectionwhich
uses monotone-bar-induction-strict3 
That is 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; 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: a add: 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: m natural_number: $n apply: a true: True
FDL editor aliases :  b-almost-full

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