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