Nuprl Lemma : mFOL-subst-abstract

The evidence that fmla[x/y] in Dom, S, is the same as the evidence
that fmla is true in Dom, S, a[y := x].⋅

[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(Dom)]. ∀[fmla:mFOL()]. ∀[x,y:ℤ].
  (Dom,S,a |= mFOL-abstract(fmla[x/y]) Dom,S,a[y := x] |= mFOL-abstract(fmla) ∈ ℙ)


Definitions occuring in Statement :  mFOL-subst: fmla[nw/old] mFOL-abstract: mFOL-abstract(fmla) mFOL: mFOL() FOSatWith: Dom,S,a |= fmla update-assignment: a[x := v] FOStruct: FOStruct(Dom) FOAssignment: FOAssignment(Dom) uall: [x:A]. B[x] prop: apply: a int: universe: Type equal: t ∈ T
Lemmas :  mFOL_wf equal_wf FOSatWith_wf mFOL-abstract_wf mFOL-rename_wf mFOL-rename-bound-to-avoid_wf cons_wf nil_wf AbstractFOFormula_wf l_disjoint_wf mFOL-boundvars_wf squash_wf true_wf FOAssignment_wf FOStruct_wf update-assignment_wf set_wf mFOL-abstract-rename cons_member l_member_wf
\mforall{}[Dom:Type].  \mforall{}[S:FOStruct(Dom)].  \mforall{}[a:FOAssignment(Dom)].  \mforall{}[fmla:mFOL()].  \mforall{}[x,y:\mBbbZ{}].
    (Dom,S,a  |=  mFOL-abstract(fmla[x/y])  =  Dom,S,a[y  :=  a  x]  |=  mFOL-abstract(fmla))

Date html generated: 2015_07_17-AM-07_54_41
Last ObjectModification: 2015_01_27-AM-10_07_12

Home Index