Nuprl Lemma : MP+KS-imply-LEM
(∀P:ℕ ⟶ ℙ. ((∀n:ℕ. Dec(P[n])) ⇒ (¬(∀n:ℕ. (¬P[n]))) ⇒ (∃n:ℕ. P[n])))
⇒ (∀A:ℙ. ∃a:ℕ ⟶ ℕ. (A ⇐⇒ ∃n:ℕ. ((a n) = 1 ∈ ℤ)))
⇒ (∀P:ℙ. (P ∨ (¬P)))
Proof
Definitions occuring in Statement :
nat: ℕ,
decidable: Dec(P),
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
guard: {T},
false: False,
or: P ∨ Q,
not: ¬A,
and: P ∧ Q,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
exists: ∃x:A. B[x],
so_apply: x[s],
nat: ℕ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas referenced :
decidable__int_equal,
not-not-excluded-middle,
or_wf,
not_wf,
decidable_wf,
equal-wf-T-base,
iff_wf,
nat_wf,
exists_wf,
all_wf
Rules used in proof :
natural_numberEquality,
voidElimination,
promote_hyp,
because_Cache,
impliesFunctionality,
independent_functionElimination,
productElimination,
dependent_functionElimination,
baseClosed,
rename,
setElimination,
functionExtensionality,
applyEquality,
intEquality,
hypothesisEquality,
hypothesis,
functionEquality,
cumulativity,
lambdaEquality,
sqequalRule,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
instantiate,
thin,
cut,
universeEquality,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
(\mforall{}P:\mBbbN{} {}\mrightarrow{} \mBbbP{}. ((\mforall{}n:\mBbbN{}. Dec(P[n])) {}\mRightarrow{} (\mneg{}(\mforall{}n:\mBbbN{}. (\mneg{}P[n]))) {}\mRightarrow{} (\mexists{}n:\mBbbN{}. P[n])))
{}\mRightarrow{} (\mforall{}A:\mBbbP{}. \mexists{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (A \mLeftarrow{}{}\mRightarrow{} \mexists{}n:\mBbbN{}. ((a n) = 1)))
{}\mRightarrow{} (\mforall{}P:\mBbbP{}. (P \mvee{} (\mneg{}P)))
Date html generated:
2017_04_20-AM-07_36_03
Last ObjectModification:
2017_04_10-PM-05_57_57
Theory : continuity
Home
Index