### 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