Nuprl Definition : mFO-uniform-evidence

An abstract formula fmla 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(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{i:l}(fmla) == ∩Dom:Type. ∩S:FOStruct(Dom). ∀a:FOAssignment(Dom). Dom,S,a |= fmla

Definitions occuring in Statement : FOSatWith: Dom,S,a |= fmla, FOStruct: FOStruct(Dom), FOAssignment: FOAssignment(Dom), all: ∀x:A. B[x], isect: ∩x:A. B[x], universe: Type
FDL editor aliases : mFO-uniform-evidence
mFO-uniform-evidence\{i:l\}(fmla) == \mcap{}Dom:Type. \mcap{}S:FOStruct(Dom). \mforall{}a:FOAssignment(Dom). Dom,S,a |= fmla Date html generated: 2015_07_17-AM-07_53_12 Last ObjectModification: 2012_09_11-PM-05_56_26 Home Index