Nuprl Lemma : mFOL-proveable-formula-evidence-ext
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Proof
Definitions occuring in Statement :
mFOL-proveable-formula: mFOL-proveable-formula(fmla),
mFOL-evidence: mFOL-evidence(fmla),
mFOL: mFOL(),
uall: ∀[x:A]. B[x],
implies: P ⇒ Q
Lemmas :
lifting-strict-decide,
has-value_wf_base,
base_wf,
base_sq,
lifting-strict-spread,
strict4-spread,
length_of_cons_lemma,
spread_cons_lemma,
top_wf,
lifting-strict-atom_eq,
lifting-strict-isaxiom,
pair-eta
\mforall{}[fmla:mFOL()]. (mFOL-proveable-formula(fmla) {}\mRightarrow{} mFOL-evidence(fmla))
Date html generated:
2015_07_17-AM-07_57_16
Last ObjectModification:
2015_04_23-PM-11_31_55
Home
Index