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
Definitions :
product: x:A × B[x],
bool: 𝔹,
le: A ≤ B,
implies: P ⇒ Q,
not: ¬A,
exists: ∃x:A. B[x],
function: x:A ─→ B[x],
int_seg: {i..j-},
natural_number: $n,
all: ∀x:A. B[x],
nat: ℕ,
assert: ↑b,
apply: f a,
pair: <a, b>
FDL editor aliases :
Konig
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:
2015_07_17-AM-08_00_53
Last ObjectModification:
2008_02_27-PM-05_49_46
Home
Index