Nuprl Lemma : vr_test_55
(∀p:ℙ. ((¬¬p) ⇒ p)) ⇒ (∀p:ℙ. (p ∨ (¬p)))
Proof
Definitions occuring in Statement :
prop: ℙ,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q
Lemmas :
or_wf,
not_over_or,
not_wf,
all_wf
(\mforall{}p:\mBbbP{}. ((\mneg{}\mneg{}p) {}\mRightarrow{} p)) {}\mRightarrow{} (\mforall{}p:\mBbbP{}. (p \mvee{} (\mneg{}p)))
Date html generated:
2015_07_17-AM-08_08_08
Last ObjectModification:
2015_01_27-PM-00_06_06
Home
Index