Nuprl Definition : Konig
Konig(k) ==
∀tree:(n:ℕ × (ℕn ⟶ ℕk)) ⟶ 𝔹
((∀i,j:ℕ. ((i ≤ j) ⇒ (∀x:ℕj ⟶ ℕk. ((↑(tree <j, x>)) ⇒ (↑(tree <i, x>))))))
⇒ (¬(∃b:ℕ. ∀x:ℕb ⟶ ℕk. (¬↑(tree <b, x>))))
⇒ (∃s:ℕ ⟶ ℕk. ∀n:ℕ. (↑(tree <n, s>))))
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
assert: ↑b,
bool: 𝔹,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
pair: <a, b>,
product: x:A × B[x],
natural_number: $n
FDL editor aliases :
Konig
Latex:
Konig(k) ==
\mforall{}tree:(n:\mBbbN{} \mtimes{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}k)) {}\mrightarrow{} \mBbbB{}
((\mforall{}i,j:\mBbbN{}. ((i \mleq{} j) {}\mRightarrow{} (\mforall{}x:\mBbbN{}j {}\mrightarrow{} \mBbbN{}k. ((\muparrow{}(tree <j, x>)) {}\mRightarrow{} (\muparrow{}(tree <i, x>))))))
{}\mRightarrow{} (\mneg{}(\mexists{}b:\mBbbN{}. \mforall{}x:\mBbbN{}b {}\mrightarrow{} \mBbbN{}k. (\mneg{}\muparrow{}(tree <b, x>))))
{}\mRightarrow{} (\mexists{}s:\mBbbN{} {}\mrightarrow{} \mBbbN{}k. \mforall{}n:\mBbbN{}. (\muparrow{}(tree <n, s>))))
Date html generated:
2016_05_15-PM-11_50_02
Last ObjectModification:
2008_02_27-PM-05_49_46
Theory : randomness
Home
Index