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