Nuprl Definition : consistent-model-fun
consistent-model-fun(Gamma;x;L) ==
x < ||Gamma||
∧ let H = context-lookup(Gamma;x) in
((↑mFOquant?(H))
∧ mFOquant-isall(H) = tt
∧ (∀p∈L.let i,j = p
in j < ||Gamma|| ∧ (mFOquant-body(H)[i/mFOquant-var(H)] = context-lookup(Gamma;j) ∈ mFOL())))
∨ ((↑mFOconnect?(H))
∧ (¬(mFOconnect-knd(H) = "and" ∈ Atom))
∧ (¬(mFOconnect-knd(H) = "or" ∈ Atom))
∧ (∀p∈L.let i,j = p
in i < ||Gamma||
∧ j < ||Gamma||
∧ (mFOconnect-left(H) = context-lookup(Gamma;i) ∈ mFOL())
∧ (mFOconnect-right(H) = context-lookup(Gamma;j) ∈ mFOL())))
Definitions occuring in Statement :
context-lookup: context-lookup(Gamma;x),
FOL-subst: fmla[nw/old],
mFOquant-body: mFOquant-body(v),
mFOquant-var: mFOquant-var(v),
mFOquant-isall: mFOquant-isall(v),
mFOquant?: mFOquant?(v),
mFOconnect-right: mFOconnect-right(v),
mFOconnect-left: mFOconnect-left(v),
mFOconnect-knd: mFOconnect-knd(v),
mFOconnect?: mFOconnect?(v),
mFOL: mFOL(),
l_all: (∀x∈L.P[x]),
length: ||as||,
assert: ↑b,
btrue: tt,
bool: 𝔹,
less_than: a < b,
let: let,
not: ¬A,
or: P ∨ Q,
and: P ∧ Q,
spread: spread def,
token: "$token",
atom: Atom,
equal: s = t ∈ T
Definitions occuring in definition :
let: let,
or: P ∨ Q,
mFOquant?: mFOquant?(v),
bool: 𝔹,
mFOquant-isall: mFOquant-isall(v),
btrue: tt,
FOL-subst: fmla[nw/old],
mFOquant-var: mFOquant-var(v),
mFOquant-body: mFOquant-body(v),
assert: ↑b,
mFOconnect?: mFOconnect?(v),
not: ¬A,
atom: Atom,
mFOconnect-knd: mFOconnect-knd(v),
token: "$token",
l_all: (∀x∈L.P[x]),
spread: spread def,
less_than: a < b,
length: ||as||,
and: P ∧ Q,
mFOconnect-left: mFOconnect-left(v),
equal: s = t ∈ T,
mFOL: mFOL(),
mFOconnect-right: mFOconnect-right(v),
context-lookup: context-lookup(Gamma;x)
FDL editor aliases :
consistent-model-fun
Latex:
consistent-model-fun(Gamma;x;L) ==
x < ||Gamma||
\mwedge{} let H = context-lookup(Gamma;x) in
((\muparrow{}mFOquant?(H))
\mwedge{} mFOquant-isall(H) = tt
\mwedge{} (\mforall{}p\mmember{}L.let i,j = p
in j < ||Gamma|| \mwedge{} (mFOquant-body(H)[i/mFOquant-var(H)] = context-lookup(Gamma;j))))
\mvee{} ((\muparrow{}mFOconnect?(H))
\mwedge{} (\mneg{}(mFOconnect-knd(H) = "and"))
\mwedge{} (\mneg{}(mFOconnect-knd(H) = "or"))
\mwedge{} (\mforall{}p\mmember{}L.let i,j = p
in i < ||Gamma||
\mwedge{} j < ||Gamma||
\mwedge{} (mFOconnect-left(H) = context-lookup(Gamma;i))
\mwedge{} (mFOconnect-right(H) = context-lookup(Gamma;j))))
Date html generated:
2016_05_15-PM-10_32_04
Last ObjectModification:
2015_09_24-PM-02_34_55
Theory : minimal-first-order-logic
Home
Index