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