Nuprl Definition : consistent-model-const

consistent-model-const(Gamma;c) ==
  let x,lbl,i,j = c 
  in x < ||Gamma||
     ∧ let H = context-lookup(Gamma;x) in
           if lbl =a "function"
             then ((↑mFOconnect?(H)) ∧ (¬(mFOconnect-knd(H) = "and" ∈ Atom)) ∧ (¬(mFOconnect-knd(H) = "or" ∈ Atom)))
                  ∨ ((↑mFOquant?(H)) ∧ mFOquant-isall(H) = tt)
           if lbl =a "pair"
             then i < ||Gamma||
                  ∧ j < ||Gamma||
                  ∧ (↑mFOconnect?(H))
                  ∧ (mFOconnect-knd(H) = "and" ∈ Atom)
                  ∧ (mFOconnect-left(H) = context-lookup(Gamma;i) ∈ mFOL())
                  ∧ (mFOconnect-right(H) = context-lookup(Gamma;j) ∈ mFOL())
           if lbl =a "dpair"
             then j < ||Gamma||
                  ∧ (↑mFOquant?(H))
                  ∧ mFOquant-isall(H) = ff
                  ∧ (mFOquant-body(H)[i/mFOquant-var(H)] = context-lookup(Gamma;j) ∈ mFOL())
           if lbl =a "inl"
             then i < ||Gamma||
                  ∧ (↑mFOconnect?(H))
                  ∧ (mFOconnect-knd(H) = "or" ∈ Atom)
                  ∧ (mFOconnect-left(H) = context-lookup(Gamma;i) ∈ mFOL())
           if lbl =a "inr"
             then i < ||Gamma||
                  ∧ (↑mFOconnect?(H))
                  ∧ (mFOconnect-knd(H) = "or" ∈ Atom)
                  ∧ (mFOconnect-right(H) = context-lookup(Gamma;i) ∈ mFOL())
           else True
           fi   


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(),  length: ||as||,  assert: ↑b,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  bfalse: ff,  btrue: tt,  bool: 𝔹,  less_than: a < b,  let: let,  spreadn: spread4,  not: ¬A,  or: P ∨ Q,  and: P ∧ Q,  true: True,  token: "$token",  atom: Atom,  equal: s = t ∈ T
Definitions occuring in definition :  length: ||as||,  less_than: a < b,  and: P ∧ Q,  token: "$token",  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  context-lookup: context-lookup(Gamma;x),  mFOconnect-left: mFOconnect-left(v),  mFOL: mFOL(),  equal: s = t ∈ T,  mFOconnect-knd: mFOconnect-knd(v),  atom: Atom,  mFOconnect?: mFOconnect?(v),  assert: ↑b,  mFOquant-body: mFOquant-body(v),  mFOquant-var: mFOquant-var(v),  FOL-subst: fmla[nw/old],  bfalse: ff,  mFOquant-isall: mFOquant-isall(v),  bool: 𝔹,  mFOquant?: mFOquant?(v),  mFOconnect-right: mFOconnect-right(v),  btrue: tt,  not: ¬A,  or: P ∨ Q,  let: let,  spreadn: spread4,  true: True
FDL editor aliases :  consistent-model-const
Latex:
consistent-model-const(Gamma;c)  ==
    let  x,lbl,i,j  =  c 
    in  x  <  ||Gamma||
          \mwedge{}  let  H  =  context-lookup(Gamma;x)  in
                      if  lbl  =a  "function"
                          then  ((\muparrow{}mFOconnect?(H))
                                    \mwedge{}  (\mneg{}(mFOconnect-knd(H)  =  "and"))
                                    \mwedge{}  (\mneg{}(mFOconnect-knd(H)  =  "or")))
                                    \mvee{}  ((\muparrow{}mFOquant?(H))  \mwedge{}  mFOquant-isall(H)  =  tt)
                      if  lbl  =a  "pair"
                          then  i  <  ||Gamma||
                                    \mwedge{}  j  <  ||Gamma||
                                    \mwedge{}  (\muparrow{}mFOconnect?(H))
                                    \mwedge{}  (mFOconnect-knd(H)  =  "and")
                                    \mwedge{}  (mFOconnect-left(H)  =  context-lookup(Gamma;i))
                                    \mwedge{}  (mFOconnect-right(H)  =  context-lookup(Gamma;j))
                      if  lbl  =a  "dpair"
                          then  j  <  ||Gamma||
                                    \mwedge{}  (\muparrow{}mFOquant?(H))
                                    \mwedge{}  mFOquant-isall(H)  =  ff
                                    \mwedge{}  (mFOquant-body(H)[i/mFOquant-var(H)]  =  context-lookup(Gamma;j))
                      if  lbl  =a  "inl"
                          then  i  <  ||Gamma||
                                    \mwedge{}  (\muparrow{}mFOconnect?(H))
                                    \mwedge{}  (mFOconnect-knd(H)  =  "or")
                                    \mwedge{}  (mFOconnect-left(H)  =  context-lookup(Gamma;i))
                      if  lbl  =a  "inr"
                          then  i  <  ||Gamma||
                                    \mwedge{}  (\muparrow{}mFOconnect?(H))
                                    \mwedge{}  (mFOconnect-knd(H)  =  "or")
                                    \mwedge{}  (mFOconnect-right(H)  =  context-lookup(Gamma;i))
                      else  True
                      fi     


Date html generated: 2016_05_15-PM-10_31_51
Last ObjectModification: 2015_09_24-PM-01_33_29

Theory : minimal-first-order-logic


Home Index