Nuprl Lemma : mFOL-proveable-formula-evidence-ext2
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-ispair,
top_wf,
has-value_wf_base,
base_wf,
base_sq,
lifting-strict-isaxiom,
strictness-decide,
lifting-strict-decide,
lifting-strict-atom_eq,
lifting-strict-spread,
value-type-has-value,
atom-value-type,
strict4-spread,
lifting-strict-int_eq,
lifting-strict-less,
strictness-apply,
strictness-spread,
lifting-strict-ifthenelse
\mforall{}[fmla:mFOL()]. (mFOL-proveable-formula(fmla) {}\mRightarrow{} mFOL-evidence(fmla))
Date html generated:
2015_07_17-AM-07_57_18
Last ObjectModification:
2015_05_03-AM-00_44_41
Home
Index