Nuprl Definition : mFO-uniform-evidence

An abstract formula fmla with free variables, vs, is true
given domain Dom and structure S over Dom
if it is true for any assignment into Dom of its free variables.
Evidence for that is given by the proposition (type)
∀a:FOAssignment(vs,Dom). Dom,S,a |= fmla

Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of that evidence.⋅

mFO-uniform-evidence(vs;fmla) == ⋂Dom:Type. ⋂S:FOStruct(Dom). ∀a:FOAssignment(vs,Dom). Dom,S,a |= fmla

Definitions occuring in Statement : FOSatWith: Dom,S,a |= fmla, FOStruct: FOStruct(Dom), FOAssignment: FOAssignment(vs,Dom), all: ∀x:A. B[x], isect: ⋂x:A. B[x], universe: Type
Definitions occuring in definition : universe: Type, isect: ⋂x:A. B[x], FOStruct: FOStruct(Dom), all: ∀x:A. B[x], FOAssignment: FOAssignment(vs,Dom), FOSatWith: Dom,S,a |= fmla
FDL editor aliases : mFO-uniform-evidence

Latex:
mFO-uniform-evidence(vs;fmla) == \mcap{}Dom:Type. \mcap{}S:FOStruct(Dom). \mforall{}a:FOAssignment(vs,Dom). Dom,S,a |= fmla Date html generated: 2016_07_08-PM-05_19_21 Last ObjectModification: 2015_09_23-AM-08_22_43 Theory : minimal-first-order-logic Home Index