Nuprl Definition : KripkeSchema
KripkeSchema == ∀P:ℙ. ∃f:ℕ ⟶ ℕ. (((∀n:ℕ. ((f n) = 0 ∈ ℕ)) ⇒ (¬P)) ∧ ((∃n:ℕ. 0 < f n) ⇒ P))
Definitions occuring in Statement :
nat: ℕ,
less_than: a < b,
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
apply: f a,
natural_number: $n,
less_than: a < b,
nat: ℕ,
exists: ∃x:A. B[x],
implies: P ⇒ Q,
not: ¬A,
equal: s = t ∈ T,
all: ∀x:A. B[x],
and: P ∧ Q,
function: x:A ⟶ B[x],
prop: ℙ
FDL editor aliases :
KripkeSchema
Latex:
KripkeSchema == \mforall{}P:\mBbbP{}. \mexists{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (((\mforall{}n:\mBbbN{}. ((f n) = 0)) {}\mRightarrow{} (\mneg{}P)) \mwedge{} ((\mexists{}n:\mBbbN{}. 0 < f n) {}\mRightarrow{} P))
Date html generated:
2017_10_03-AM-10_16_02
Last ObjectModification:
2017_09_18-PM-05_18_13
Theory : reals
Home
Index