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