Nuprl Definition : consistent-context-model
consistent-context-model(Gamma;M) ==
  let consts,funs = M 
  in (∀c∈consts.consistent-model-const(Gamma;c)) ∧ (∀f∈funs.let x,L = f in consistent-model-fun(Gamma;x;L))
Definitions occuring in Statement : 
consistent-model-fun: consistent-model-fun(Gamma;x;L)
, 
consistent-model-const: consistent-model-const(Gamma;c)
, 
l_all: (∀x∈L.P[x])
, 
and: P ∧ Q
, 
spread: spread def
Definitions occuring in definition : 
and: P ∧ Q
, 
consistent-model-const: consistent-model-const(Gamma;c)
, 
l_all: (∀x∈L.P[x])
, 
spread: spread def, 
consistent-model-fun: consistent-model-fun(Gamma;x;L)
FDL editor aliases : 
consistent-context-model
Latex:
consistent-context-model(Gamma;M)  ==
    let  consts,funs  =  M 
    in  (\mforall{}c\mmember{}consts.consistent-model-const(Gamma;c))
          \mwedge{}  (\mforall{}f\mmember{}funs.let  x,L  =  f 
                                in  consistent-model-fun(Gamma;x;L))
Date html generated:
2016_05_15-PM-10_32_16
Last ObjectModification:
2015_09_24-PM-02_37_09
Theory : minimal-first-order-logic
Home
Index