Nuprl Lemma : mFOL-proveable-formula-evidence
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 :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
mFOL-proveable-formula: mFOL-proveable-formula(fmla),
member: t ∈ T,
subtype_rel: A ⊆r B,
mFOL-sequent: mFOL-sequent(),
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
all: ∀x:A. B[x],
mFOL-evidence: mFOL-evidence(fmla),
mFO-uniform-evidence: mFO-uniform-evidence(vs;fmla),
prop: ℙ,
mFOL-sequent-evidence: mFOL-sequent-evidence(s),
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
pi2: snd(t),
pi1: fst(t),
false: False,
mFOL-sequent-abstract: mFOL-sequent-abstract(s),
FOSatWith: Dom,S,a |= fmla,
unit: Unit,
tuple-type: tuple-type(L),
list_ind: list_ind,
mFOL-hyps-meaning: mFOL-hyps-meaning(Dom;S;a;hyps),
map: map(f;as),
nil: [],
it: ⋅
Lemmas referenced :
mFOL-proveable-evidence,
nil_wf,
subtype_rel_product,
list_wf,
mFOL_wf,
subtype_rel_list,
subtype_rel_self,
FOAssignment_wf,
mFOL-freevars_wf,
FOStruct_wf,
mFOL-proveable-formula_wf,
subtype_rel_FOAssignment,
mFOL-sequent-freevars_wf,
mFOL-sequent-freevars-contained,
l_contains_weakening,
nil_member,
l_member_wf,
it_wf,
equal-wf-base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
sqequalHypSubstitution,
cut,
introduction,
extract_by_obid,
isectElimination,
thin,
independent_pairEquality,
voidEquality,
hypothesis,
hypothesisEquality,
applyEquality,
sqequalRule,
lambdaEquality,
independent_isectElimination,
voidElimination,
because_Cache,
independent_functionElimination,
cumulativity,
universeEquality,
dependent_functionElimination,
productElimination,
independent_pairFormation,
intEquality,
baseClosed
Latex:
\mforall{}[fmla:mFOL()]. (mFOL-proveable-formula(fmla) {}\mRightarrow{} mFOL-evidence(fmla))
Date html generated:
2018_05_21-PM-10_39_56
Last ObjectModification:
2017_07_26-PM-06_42_14
Theory : minimal-first-order-logic
Home
Index