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