Nuprl Lemma : MP+truncated-KS-imply-truncated-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 :
quotient: x,y:A//B[x; y],
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,
true: True,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uiff: uiff(P;Q),
not: ¬A,
guard: {T},
nat: ℕ,
or: P ∨ Q,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
and: P ∧ Q,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
exists: ∃x:A. B[x],
so_apply: x[s],
so_lambda: λ2x.t[x],
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas referenced :
not_over_exists,
decidable__int_equal,
not-not-excluded-middle-quot-true,
implies-quotient-true2,
or_wf,
not_wf,
decidable_wf,
equiv_rel_true,
true_wf,
equal-wf-T-base,
iff_wf,
nat_wf,
exists_wf,
quotient_wf,
all_wf
Rules used in proof :
natural_numberEquality,
promote_hyp,
impliesFunctionality,
productElimination,
independent_functionElimination,
rename,
setElimination,
dependent_functionElimination,
cumulativity,
baseClosed,
functionExtensionality,
applyEquality,
intEquality,
independent_isectElimination,
hypothesisEquality,
because_Cache,
hypothesis,
functionEquality,
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{}. \00D9(\mexists{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (A \mLeftarrow{}{}\mRightarrow{} \mexists{}n:\mBbbN{}. ((a n) = 1))))
{}\mRightarrow{} (\mforall{}P:\mBbbP{}. \00D9(P \mvee{} (\mneg{}P)))
Date html generated:
2017_04_20-AM-07_36_09
Last ObjectModification:
2017_04_11-AM-05_18_24
Theory : continuity
Home
Index