Nuprl Lemma : mFOL-proveable-formula-evidence-ext3
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
Definitions unfolded in proof :
member: t ∈ T,
ifthenelse: if b then t else f fi ,
spreadn: spread3,
subtract: n - m,
pi1: fst(t),
pi2: snd(t),
genrec-ap: genrec-ap,
mFOL-proveable-formula-evidence-ext2
Lemmas referenced :
mFOL-proveable-formula-evidence-ext2
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[fmla:mFOL()]. (mFOL-proveable-formula(fmla) {}\mRightarrow{} mFOL-evidence(fmla))
Date html generated:
2019_10_16-AM-11_43_45
Last ObjectModification:
2018_10_16-PM-03_14_42
Theory : minimal-first-order-logic
Home
Index