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(Dom). Dom,S,a |= fmla.
NOTE:
Since there are no assignments into an empty domain, this means that any
evidence works when Dom is empty, so the intersection is essentially over
non-empty domains Dom.
Thus, (forall x. P(x)) => (exists x. P(x)) is uniformly valid
(i.e. has uniform evidence) so (by our completeness theorem) is provable.
A careful examination of the effect of the mFOL rules
(see mFOLeffect)
will show that it is indeed provable.⋅
∀[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
Lemmas :
mFOL-proveable_wf,
mFOL-sequent_wf,
W-induction,
mFOLRule_wf,
mFOLeffect_wf,
list_wf,
unit_wf2,
int_seg_wf,
length_wf,
all_wf,
correct_proof_wf,
subtype_rel_self,
proof-tree_wf,
mFOL-sequent-evidence_wf,
W_wf,
mFOLRule-induction,
mFOL_wf,
mFOconnect?_wf,
bool_wf,
eqtt_to_assert,
eq_atom_wf,
mFOconnect-knd_wf,
assert_of_eq_atom,
length_of_cons_lemma,
length_of_nil_lemma,
less_than_wf,
false_wf,
lelt_wf,
select_wf,
equal_wf,
list-cases,
cons_neq_nil,
mFOconnect-left_wf,
cons_wf,
mFOconnect-right_wf,
product_subtype_list,
length_wf_nat,
nat_wf,
decidable__lt,
condition-implies-le,
minus-add,
minus-one-mul,
zero-add,
add-commutes,
add_functionality_wrt_le,
add-associates,
add-zero,
le-add-cancel,
length_nil,
non_neg_length,
nil_wf,
length_wf_nil,
length_cons,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
bfalse_wf,
and_wf,
isl_wf,
btrue_wf,
btrue_neq_bfalse,
equal-wf-base-T,
mRuleandI_wf,
mRuleimpI_wf,
bl-all_wf,
l_member_wf,
bnot_wf,
deq-member_wf,
int-deq_wf,
mFOL-freevars_wf,
iff_transitivity,
assert_wf,
l_all_wf2,
not_wf,
iff_weakening_uiff,
assert-bl-all,
l_all_functionality,
assert_of_bnot,
assert-deq-member,
eq_bool_wf,
mFOquant-isall_wf,
assert_of_eq_bool,
mFOL-subst_wf,
mFOquant-body_wf,
mFOquant-var_wf,
equal-wf-T-base,
mRuleallI_wf,
mFOquant?_wf,
mRuleexistsI_wf,
mRuleorI_wf,
deq-mFO_wf,
mRulehyp_wf,
lt_int_wf,
assert_of_lt_int,
null_nil_lemma,
null_wf3,
subtype_rel_list,
top_wf,
null_cons_lemma,
sq_stable__le,
mRuleandE_wf,
mRuleorE_wf,
mRuleimpE_wf,
mRuleallE_wf,
mRuleexistsE_wf,
mFOL-induction,
mFOconnect_wf,
squash_wf,
true_wf,
iff_weakening_equal,
equal-wf-base,
atom_subtype_base,
mFOL-sequent-evidence_and,
map_cons_lemma,
tupletype_cons_lemma,
FOAssignment_wf,
FOStruct_wf,
map_nil_lemma,
tupletype_nil_lemma,
FOSatWith_wf,
mFOL-abstract_wf,
map_wf,
assert_of_null,
tuple-type_wf,
mFOquant_wf,
mFOatomic_wf,
mFOL-subst-abstract,
update-assignment_wf,
eq_int_wf,
assert_of_eq_int,
neg_assert_of_eq_int,
mFOL-abstract-functionality,
member_filter,
int_subtype_base,
list_induction,
l_all_cons,
mFOL-sequent-evidence_transitivity1,
mFOL-sequent-evidence-trivial,
mFOL-sequent-evidence_transitivity2,
select-cons,
le_int_wf,
le_wf,
add-swap,
decidable__le,
subtract_wf,
not-le-2,
minus-minus,
minus-zero,
le-add-cancel2,
less_than_transitivity2,
le_weakening,
bool_cases,
assert_of_le_int,
select-tuple_wf,
map_length,
select-map,
stuck-spread,
base_wf,
null-map,
less_than_transitivity1,
less_than_irreflexivity,
sq_stable__correct_proof,
proof-tree-ext
\mforall{}[s:mFOL-sequent()]. (mFOL-proveable(s) {}\mRightarrow{} mFOL-sequent-evidence(s))
Date html generated:
2015_07_17-AM-07_57_12
Last ObjectModification:
2015_02_03-PM-09_43_19
Home
Index