Nuprl Lemma : mFOL-proveable-evidence
Soundness theorem for mFOL() with respect to uniform evidence semantics.
It says that from a correct proof of a mFOL sequent we may construct
uniform evidence mFOL-sequent-evidence for the sequent.
Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of evidence for ∀a:FOAssignment(vs,Dom). Dom,S,a |= fmla
where vs is the list of free variables of the formula.
NOTE:
If the formula is closed (i.e. the free vars is the nil list) then
an assignment a:FOAssignment([],Dom) exists even when Dom is an empty type..
Thus, (forall x. P(x)) => (exists x. P(x)) is not uniformly valid
because the premise is true for an empty domain while the conclusion is not.
By the soundness theorem, it is not provable.
By examining the effect of the mFOL rules
(see mFOLeffect)
one can see why this is so:
both forall elimination and exists introduction
can only be used with a variable already free in the sequent,
so there is no way to use either rule in a proof of this formula.⋅
∀[s:mFOL-sequent()]. (mFOL-proveable(s) ⇒ mFOL-sequent-evidence(s))
Proof
Definitions occuring in Statement :
mFOL-proveable: mFOL-proveable(s),
mFOL-sequent-evidence: mFOL-sequent-evidence(s),
mFOL-sequent: mFOL-sequent(),
uall: ∀[x:A]. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
prop: ℙ,
member: t ∈ T,
sq_exists: ∃x:A [B[x]],
proveable: proveable(Sequent;Rule;effect;s),
mFOL-proveable: mFOL-proveable(s),
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
isr: isr(x),
correct_proof: correct_proof(Sequent;effect;s;pf),
proof-abort: proof-abort(s;r),
pi1: fst(t),
assert: ↑b,
ifthenelse: if b then t else f fi ,
bfalse: ff,
false: False,
btrue: tt,
and: P ∧ Q,
isl: isl(x),
mFOLeffect: mFOLeffect(sr),
subtype_rel: A ⊆r B,
nat: ℕ,
make-proof-tree: make-proof-tree(s;r;L),
outl: outl(x),
int_seg: {i..j-},
lelt: i ≤ j < k,
le: A ≤ B,
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
mFOL-sequent: mFOL-sequent(),
l_all: (∀x∈L.P[x]),
fRuleandI: andI,
FOLRule_ind: FOLRule_ind,
mFO-dest-connective: mFO-dest-connective,
exposed-bfalse: exposed-bfalse,
bool: 𝔹,
unit: Unit,
it: ⋅,
uiff: uiff(P;Q),
band: p ∧b q,
less_than': less_than'(a;b),
cons: [a / b],
guard: {T},
cand: A c∧ B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
subtract: n - m,
true: True,
select: L[n],
less_than: a < b,
squash: ↓T,
length: ||as||,
list_ind: list_ind,
nil: [],
sq_type: SQType(T),
bnot: ¬bb,
fRuleimpI: impI,
fRuleallI: allI with var,
mFO-dest-quantifier: mFO-dest-quantifier,
mFOL-sequent-freevars: mFOL-sequent-freevars(s),
fRuleexistsI: existsI with var,
fRuleorI: fRuleorI(left),
fRulehyp: hyp,
fRuleandE: andE on hypnum,
ge: i ≥ j ,
fRuleorE: orE on hypnum,
fRuleimpE: impE on hypnum,
fRuleallE: allE on hypnum with var,
fRuleexistsE: existsE on hypnum with var,
fRulefalseE: falseE on hypnum,
mFOatomic: name(vars),
mFOconnect?: mFOconnect?(v),
mFOconnect-knd: mFOconnect-knd(v),
pi2: snd(t),
mFOconnect-left: mFOconnect-left(v),
mFOconnect-right: mFOconnect-right(v),
eq_atom: x =a y,
mFOconnect: mFOconnect(knd;left;right),
mFOquant: mFOquant(isall;var;body),
mFOL-sequent-evidence: mFOL-sequent-evidence(s),
mFO-uniform-evidence: mFO-uniform-evidence(vs;fmla),
mFOL-freevars: mFOL-freevars(fmla),
mFOL_ind: mFOL_ind,
mFOL-sequent-abstract: mFOL-sequent-abstract(s),
FOSatWith: Dom,S,a |= fmla,
mFOL-abstract: mFOL-abstract(fmla),
FOConnective: FOConnective(knd),
let: let,
mFOL-hyps-meaning: mFOL-hyps-meaning(Dom;S;a;hyps),
map: map(f;as),
mFOquant?: mFOquant?(v),
mFOquant-isall: mFOquant-isall(v),
mFOquant-var: mFOquant-var(v),
mFOquant-body: mFOquant-body(v),
FOQuantifier: FOQuantifier(isall),
l_contains: A ⊆ B,
update-assignment: a[x := v],
nequal: a ≠ b ∈ T ,
FOAssignment: FOAssignment(vs,Dom),
tuple-type: tuple-type(L),
mFOL: mFOL(),
colength: colength(L),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
mFOL-subst: fmla[nw/old],
l_disjoint: l_disjoint(T;l1;l2),
l_member: (x ∈ l),
filter: filter(P;l),
reduce: reduce(f;k;as),
l_exists: (∃x∈L. P[x]),
istype: istype(T),
sq_stable: SqStable(P),
ext-eq: A ≡ B
Lemmas referenced :
mFOL-sequent_wf,
mFOL-proveable_wf,
proof-tree-induction-ext,
FOLRule_wf,
mFOLeffect_wf,
correct_proof_wf,
mFOL-sequent-evidence_wf,
proof-tree_wf,
assert_witness,
bfalse_wf,
btrue_wf,
istype-void,
istype-true,
proof-abort_wf,
istype-assert,
make-proof-tree_wf,
l_all_wf2,
l_member_wf,
istype-int,
length_wf_nat,
set_subtype_base,
le_wf,
int_subtype_base,
outl_wf,
list_wf,
unit_wf2,
int_seg_wf,
length_wf,
select_wf,
int_seg_properties,
decidable__le,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
decidable__lt,
intformless_wf,
int_formula_prop_less_lemma,
intformeq_wf,
int_formula_prop_eq_lemma,
istype-le,
istype-less_than,
FOLRule-induction-ext,
equal_wf,
mFOconnect?_wf,
eqtt_to_assert,
eq_atom_wf,
mFOconnect-knd_wf,
assert_of_eq_atom,
istype-false,
list-cases,
length_of_nil_lemma,
cons_neq_nil,
mFOconnect-left_wf,
cons_wf,
mFOconnect-right_wf,
product_subtype_list,
length_of_cons_lemma,
not-lt-2,
condition-implies-le,
minus-add,
minus-one-mul,
zero-add,
minus-one-mul-top,
add-commutes,
add_functionality_wrt_le,
add-associates,
add-zero,
le-add-cancel,
all_wf,
subtype_rel_universe1,
equal-wf-base,
less_than_wf,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
btrue_neq_bfalse,
fRuleandI_wf,
mFOL_wf,
fRuleimpI_wf,
deq-member_wf,
int-deq_wf,
mFOL-sequent-freevars_wf,
assert-deq-member,
mFOquant?_wf,
eq_bool_wf,
mFOquant-isall_wf,
assert_of_eq_bool,
mFOL-subst_wf,
mFOquant-body_wf,
mFOquant-var_wf,
iff_weakening_uiff,
assert_wf,
equal-wf-T-base,
fRuleallI_wf,
fRuleexistsI_wf,
fRuleorI_wf,
deq-mFO_wf,
fRulehyp_wf,
lt_int_wf,
assert_of_lt_int,
nat_properties,
fRuleandE_wf,
istype-nat,
fRuleorE_wf,
fRuleimpE_wf,
fRuleallE_wf,
fRuleexistsE_wf,
fRulefalseE_wf,
mFOL-induction,
atom_subtype_base,
nil_wf,
mFOconnect_wf,
istype-atom,
squash_wf,
true_wf,
istype-universe,
subtype_rel_self,
iff_weakening_equal,
mFOL-sequent-evidence_and,
subtype_rel_FOAssignment,
mFOL-sequent-freevars-contained,
mFOL-sequent-freevars-contains-concl,
mFOL-freevars_wf,
val-union-l-union,
int-valueall-type,
union-contains2,
cons_member,
union-contains,
l_contains_wf,
mFOL-sequent-freevars-subset-2,
FOAssignment_wf,
FOStruct_wf,
mFOL-hyps-meaning-cons,
null_nil_lemma,
FOSatWith_wf,
mFOL-abstract_wf,
subtype_rel_function,
tuple-type_wf,
null_cons_lemma,
mFOL-hyps-meaning_wf,
not_wf,
mFOquant_wf,
mFOatomic_wf,
not-member-mFOL-sequent-freevars,
mFOL-subst-abstract,
update-assignment_wf,
l_all_iff,
filter_wf5,
bnot_wf,
eq_int_wf,
member-mFOL-sequent-freevars,
member_filter,
iff_transitivity,
assert_of_bnot,
assert_of_eq_int,
l_exists_wf,
freevars-mFOL-subst,
neg_assert_of_eq_int,
AbstractFOFormula_wf,
decidable__equal_int,
ge_wf,
colength-cons-not-zero,
colength_wf_list,
subtract-1-ge-0,
spread_cons_lemma,
subtract_wf,
itermSubtract_wf,
itermAdd_wf,
int_term_value_subtract_lemma,
int_term_value_add_lemma,
l_exists_cons,
l_all_cons,
ifthenelse_wf,
null_wf3,
subtype_rel_list,
top_wf,
mFOL-sequent-freevars-subset-1,
mFOL-rename-bound-to-avoid_wf,
mFOL-freevars-of-rename,
list_subtype_base,
mFOL-boundvars_wf,
mFOL-rename_wf,
mFOL-sequent-freevars-subset-4,
mFOL-sequent-evidence_transitivity1,
mFOL-sequent-evidence-trivial,
mFOL-sequent-evidence_transitivity2,
l_contains_transitivity,
select_member,
better-mFOL-sequent-evidence_transitivity1,
l_contains_weakening,
select-cons,
le_int_wf,
add-subtract-cancel,
add-swap,
bool_cases,
assert_of_le_int,
mFOL-freevars-connect-right-contained,
mFOL-freevars-connect-left-contained,
select-tuple_wf,
length-map,
select-map,
stuck-spread,
istype-base,
mFOL-freevars-connect-contained,
decidable__l_member,
mFOL-subst-trivial,
assert_elim,
assert_of_null,
sq_stable__correct_proof,
proof-tree-ext
Rules used in proof :
hypothesis,
hypothesisEquality,
isectElimination,
extract_by_obid,
introduction,
universeIsType,
cut,
rename,
thin,
setElimination,
sqequalHypSubstitution,
lambdaFormation_alt,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
instantiate,
cumulativity,
dependent_functionElimination,
lambdaEquality_alt,
productIsType,
sqequalRule,
functionEquality,
inhabitedIsType,
independent_functionElimination,
independent_pairEquality,
unionElimination,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
voidElimination,
productElimination,
because_Cache,
independent_isectElimination,
axiomEquality,
setIsType,
applyEquality,
intEquality,
natural_numberEquality,
sqequalBase,
hyp_replacement,
applyLambdaEquality,
functionIsType,
approximateComputation,
dependent_pairFormation_alt,
int_eqEquality,
Error :memTop,
independent_pairFormation,
dependent_set_memberEquality_alt,
unionEquality,
inlEquality_alt,
equalityElimination,
tokenEquality,
promote_hyp,
hypothesis_subsumption,
addEquality,
minusEquality,
closedConclusion,
imageElimination,
baseClosed,
imageMemberEquality,
unionIsType,
atomEquality,
universeEquality,
inlFormation_alt,
functionExtensionality,
setEquality,
intWeakElimination,
functionIsTypeImplies,
voidEquality,
baseApply,
inrFormation_alt,
productEquality
Latex:
\mforall{}[s:mFOL-sequent()]. (mFOL-proveable(s) {}\mRightarrow{} mFOL-sequent-evidence(s))
Date html generated:
2020_05_20-AM-09_10_57
Last ObjectModification:
2020_01_29-PM-02_03_12
Theory : minimal-first-order-logic
Home
Index