Nuprl Definition : generalized-markov-principle
GMPi.A[i]) == (¬(∀i:ℕ. A[i])) ⇒ (∃n:ℕ. (¬A[n]))
Definitions occuring in Statement :
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q
Definitions occuring in definition :
implies: P ⇒ Q,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
nat: ℕ,
not: ¬A
FDL editor aliases :
generalized-markov-principle
Latex:
GMPi.A[i]) == (\mneg{}(\mforall{}i:\mBbbN{}. A[i])) {}\mRightarrow{} (\mexists{}n:\mBbbN{}. (\mneg{}A[n]))
Date html generated:
2016_05_15-PM-03_20_46
Last ObjectModification:
2015_09_23-AM-07_42_54
Theory : general
Home
Index