Nuprl Lemma : FOL-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()]. (FOL-proveable(s) ⇒ FOL-sequent-evidence{i:l}(s))
Proof
Definitions occuring in Statement :
FOL-proveable: FOL-proveable(s),
FOL-sequent-evidence: FOL-sequent-evidence{i:l}(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),
FOL-proveable: FOL-proveable(s),
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
fRulefalseE: falseE on hypnum,
fRuleexistsE: existsE on hypnum with var,
fRuleallE: allE on hypnum with var,
fRuleimpE: impE on hypnum,
fRuleorE: orE on hypnum,
ge: i ≥ j ,
fRuleandE: andE on hypnum,
fRulehyp: hyp,
fRuleorI: fRuleorI(left),
fRuleexistsI: existsI with var,
mFOL-sequent-freevars: mFOL-sequent-freevars(s),
mFO-dest-quantifier: mFO-dest-quantifier,
fRuleallI: allI with var,
fRuleimpI: impI,
isl: isl(x),
assert: ↑b,
bnot: ¬bb,
sq_type: SQType(T),
bfalse: ff,
nil: [],
list_ind: list_ind,
length: ||as||,
select: L[n],
subtract: n - m,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
cand: A c∧ B,
nat: ℕ,
guard: {T},
cons: [a / b],
le: A ≤ B,
false: False,
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
not: ¬A,
or: P ∨ Q,
decidable: Dec(P),
lelt: i ≤ j < k,
int_seg: {i..j-},
true: True,
less_than': less_than'(a;b),
squash: ↓T,
less_than: a < b,
top: Top,
ifthenelse: if b then t else f fi ,
band: p ∧b q,
uimplies: b supposing a,
uiff: uiff(P;Q),
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
exposed-bfalse: exposed-bfalse,
mFO-dest-connective: mFO-dest-connective,
FOLRule_ind: FOLRule_ind,
fRuleandI: andI,
FOLeffect: FOLeffect(sr),
mFOL-sequent: mFOL-sequent(),
pi1: fst(t),
and: P ∧ Q,
Wsup: Wsup(a;b),
correct_proof: correct_proof(Sequent;effect;s;pf),
subtype_rel: A ⊆r B,
so_apply: x[s],
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
proof-tree: proof-tree(Sequent;Rule;effect),
mFOquant: mFOquant(isall;var;body),
mFOconnect: mFOconnect(knd;left;right),
eq_atom: x =a y,
mFOconnect-right: mFOconnect-right(v),
mFOconnect-left: mFOconnect-left(v),
pi2: snd(t),
mFOconnect-knd: mFOconnect-knd(v),
mFOconnect?: mFOconnect?(v),
mFOatomic: name(vars),
let: let,
FOConnective+: FOConnective+(knd),
FOL-abstract: FOL-abstract(fmla),
FOSatWith+: Dom,S,a +|= fmla,
FOL-sequent-abstract: FOL-sequent-abstract(s),
mFOL_ind: mFOL_ind,
mFOL-freevars: mFOL-freevars(fmla),
FO-uniform-evidence: FO-uniform-evidence(vs;fmla),
FOL-sequent-evidence: FOL-sequent-evidence{i:l}(s),
map: map(f;as),
FOL-hyps-meaning: FOL-hyps-meaning(Dom;S;a;hyps),
FOStruct: FOStruct(Dom),
FOStruct+: FOStruct+{i:l}(Dom),
tunion: ⋃x:A.B[x],
b-union: A ⋃ B,
mFOquant-body: mFOquant-body(v),
mFOquant-var: mFOquant-var(v),
mFOquant-isall: mFOquant-isall(v),
mFOquant?: mFOquant?(v),
FOQuantifier+: FOQuantifier+(isall),
l_contains: A ⊆ B,
nequal: a ≠ b ∈ T ,
update-assignment: a[x := v],
FOAssignment: FOAssignment(vs,Dom),
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
colength: colength(L),
mFOL: mFOL(),
tuple-type: tuple-type(L),
reduce: reduce(f;k;as),
filter: filter(P;l),
mFOL-bound-rename,
mFOL-rename-bound-to-avoid: mFOL-rename-bound-to-avoid(fmla;L),
mFOL-subst: fmla[nw/old],
mFOL-ext,
uniform-comp-nat-induction,
mFOL-induction,
FOL-bound-rename,
FOL-rename-bound-to-avoid: FOL-rename-bound-to-avoid(fmla;L),
mFOL-rename: mFOL-rename(fmla;old;new),
FOL-subst: fmla[nw/old],
l_member: (x ∈ l),
sq_stable: SqStable(P),
null: null(as),
l_exists: (∃x∈L. P[x]),
istype: istype(T),
label: ...$L... t,
mFO-dest-atomic: mFO-dest-atomic,
ext-eq: A ≡ B
Lemmas referenced :
mFOL-sequent_wf,
FOL-proveable_wf,
int_seg_properties,
top_wf,
subtype_rel_product,
pi1_wf_top,
fRulefalseE_wf,
fRuleexistsE_wf,
fRuleallE_wf,
fRuleimpE_wf,
fRuleorE_wf,
istype-nat,
fRuleandE_wf,
nat_properties,
assert_of_lt_int,
lt_int_wf,
fRulehyp_wf,
deq-mFO_wf,
fRuleorI_wf,
fRuleexistsI_wf,
fRuleallI_wf,
equal-wf-T-base,
assert_wf,
iff_weakening_uiff,
mFOquant-var_wf,
mFOquant-body_wf,
FOL-subst_wf,
assert_of_eq_bool,
mFOquant-isall_wf,
eq_bool_wf,
mFOquant?_wf,
l_member_wf,
assert-deq-member,
mFOL-sequent-freevars_wf,
int-deq_wf,
deq-member_wf,
fRuleimpI_wf,
mFOL_wf,
fRuleandI_wf,
btrue_neq_bfalse,
btrue_wf,
bfalse_wf,
neg_assert_of_eq_atom,
assert-bnot,
bool_subtype_base,
bool_wf,
subtype_base_sq,
bool_cases_sqequal,
eqff_to_assert,
le-add-cancel,
add-zero,
add-associates,
add_functionality_wrt_le,
add-commutes,
minus-one-mul-top,
zero-add,
minus-one-mul,
minus-add,
condition-implies-le,
not-lt-2,
length_wf_nat,
product_subtype_list,
mFOconnect-right_wf,
cons_wf,
mFOconnect-left_wf,
cons_neq_nil,
list-cases,
istype-false,
select_wf,
istype-less_than,
istype-le,
int_term_value_var_lemma,
int_formula_prop_less_lemma,
int_formula_prop_and_lemma,
itermVar_wf,
intformless_wf,
intformand_wf,
decidable__lt,
int_formula_prop_wf,
int_term_value_constant_lemma,
int_formula_prop_le_lemma,
int_formula_prop_not_lemma,
istype-int,
itermConstant_wf,
intformle_wf,
intformnot_wf,
full-omega-unsat,
decidable__le,
less_than_wf,
length_of_nil_lemma,
istype-void,
length_of_cons_lemma,
assert_of_eq_atom,
mFOconnect-knd_wf,
eq_atom_wf,
eqtt_to_assert,
mFOconnect?_wf,
unit_wf2,
list_wf,
equal_wf,
FOLRule-induction,
W_wf,
FOL-sequent-evidence_wf,
proof-tree_wf,
subtype_rel_self,
correct_proof_wf,
length_wf,
int_seg_wf,
FOLeffect_wf,
FOLRule_wf,
W-induction,
FOL-sequent-evidence_and,
atom_subtype_base,
iff_weakening_equal,
istype-universe,
true_wf,
squash_wf,
mFOconnect_wf,
nil_wf,
subtype_rel_universe1,
equal-wf-base,
mFOL-induction,
FOStruct+_wf,
FOAssignment_wf,
mFOL-sequent-freevars-subset-2,
l_contains_wf,
union-contains,
cons_member,
union-contains2,
int-valueall-type,
val-union-l-union,
mFOL-freevars_wf,
mFOL-sequent-freevars-contains-concl,
mFOL-sequent-freevars-contained,
subtype_rel_FOAssignment,
FOL-hyps-meaning_wf,
null_cons_lemma,
tuple-type_wf,
FOL-abstract_wf,
FOSatWith+_wf,
ifthenelse_wf,
null_nil_lemma,
FOL-hyps-meaning-cons,
not-member-mFOL-sequent-freevars,
mFOatomic_wf,
mFOquant_wf,
not_wf,
subtype_rel_b-union-left,
update-assignment_wf,
FOL-subst-abstract,
assert_of_eq_int,
assert_of_bnot,
iff_transitivity,
int_subtype_base,
member_filter,
member-mFOL-sequent-freevars,
eq_int_wf,
bnot_wf,
filter_wf5,
l_all_iff,
l_exists_wf,
freevars-FOL-subst,
int_formula_prop_eq_lemma,
intformeq_wf,
neg_assert_of_eq_int,
AbstractFOFormula+_wf,
decidable__equal_int,
nat_wf,
int_term_value_add_lemma,
int_term_value_subtract_lemma,
itermAdd_wf,
itermSubtract_wf,
subtract_wf,
spread_cons_lemma,
set_subtype_base,
subtract-1-ge-0,
le_wf,
colength_wf_list,
colength-cons-not-zero,
l_all_wf2,
ge_wf,
l_exists_cons,
l_all_cons,
subtype_rel_list,
null_wf3,
mFOL-sequent-freevars-subset-1,
all_wf,
exists_wf,
mFOL-subst_wf,
freevars-mFOL-subst,
mFOL-sequent-freevars-subset-4,
FOL-sequent-evidence_transitivity1,
or_wf,
FOL-sequent-evidence-trivial,
select_member,
l_contains_transitivity,
FOL-sequent-evidence_transitivity2,
better-FOL-sequent-evidence_transitivity1,
l_contains_weakening,
spread-exception-type,
sq_stable-exception-type,
FOStruct-false-subtype-evidence,
assert_of_le_int,
bool_cases,
add-swap,
add-subtract-cancel,
le_int_wf,
select-cons,
mFOL-freevars-connect-right-contained,
mFOL-freevars-connect-left-contained,
select-map,
length-map,
select-tuple_wf,
istype-base,
stuck-spread,
decide-exception-type,
mFOL-freevars-connect-contained,
apply-exception-type,
decidable__l_member,
assert_elim,
eq_int_eq_true,
FOL-subst-trivial,
assert_of_null,
equal_functionality_wrt_subtype_rel2,
assert_of_band,
it_wf,
list_subtype_base,
mFOatomic-vars_wf,
mFOatomic-name_wf,
mFOatomic?_wf,
FOL-sequent-evidence-false-hyp,
proof-tree-ext,
sq_stable__correct_proof,
mFOL-bound-rename,
mFOL-ext,
uniform-comp-nat-induction,
FOL-bound-rename
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,
functionIsType,
intEquality,
sqequalBase,
unionIsType,
minusEquality,
addEquality,
hypothesis_subsumption,
promote_hyp,
because_Cache,
closedConclusion,
int_eqEquality,
imageElimination,
dependent_pairFormation_alt,
approximateComputation,
dependent_set_memberEquality_alt,
hyp_replacement,
baseClosed,
imageMemberEquality,
independent_pairFormation,
voidElimination,
isect_memberEquality_alt,
applyLambdaEquality,
tokenEquality,
independent_isectElimination,
equalityElimination,
inlEquality_alt,
independent_pairEquality,
unionEquality,
productElimination,
functionEquality,
productIsType,
independent_functionElimination,
dependent_functionElimination,
equalitySymmetry,
equalityTransitivity,
equalityIstype,
voidEquality,
natural_numberEquality,
unionElimination,
inhabitedIsType,
applyEquality,
lambdaEquality_alt,
sqequalRule,
productEquality,
cumulativity,
instantiate,
baseApply,
equalityIsType4,
equalityIsType1,
universeEquality,
atomEquality,
dependent_pairEquality_alt,
equalityIsType3,
setIsType,
inlFormation_alt,
equalityIsType2,
setEquality,
functionExtensionality,
functionIsTypeImplies,
axiomEquality,
intWeakElimination,
inrFormation_alt,
Error :memTop,
inrEquality_alt
Latex:
\mforall{}[s:mFOL-sequent()]. (FOL-proveable(s) {}\mRightarrow{} FOL-sequent-evidence\{i:l\}(s))
Date html generated:
2020_05_20-AM-09_12_01
Last ObjectModification:
2020_02_04-AM-08_18_27
Theory : minimal-first-order-logic
Home
Index