Nuprl Definition : FOConnective+

FOConnective+(knd) ==
  λx,y,Dom,S,a. let p = Dom,S,a +|= x in
                 let q = Dom,S,a +|= y in
                 if knd =a "and" then (p ∧ q) ⋃ (S "false" [])
                 if knd =a "or" then (p ∨ q) ⋃ (S "false" [])
                 else (p ⇒ q) ⋃ (S "false" [])
                 fi 


Definitions occuring in Statement :  FOSatWith+: Dom,S,a +|= fmla,  nil: [],  b-union: A ⋃ B,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  let: let,  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  apply: f a,  lambda: λx.A[x],  token: "$token"
Definitions occuring in definition :  lambda: λx.A[x],  let: let,  FOSatWith+: Dom,S,a +|= fmla,  and: P ∧ Q,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  or: P ∨ Q,  b-union: A ⋃ B,  implies: P ⇒ Q,  apply: f a,  token: "$token",  nil: []
FDL editor aliases :  FOConnective+
Latex:
FOConnective+(knd)  ==
    \mlambda{}x,y,Dom,S,a.  let  p  =  Dom,S,a  +|=  x  in
                                  let  q  =  Dom,S,a  +|=  y  in
                                  if  knd  =a  "and"  then  (p  \mwedge{}  q)  \mcup{}  (S  "false"  [])
                                  if  knd  =a  "or"  then  (p  \mvee{}  q)  \mcup{}  (S  "false"  [])
                                  else  (p  {}\mRightarrow{}  q)  \mcup{}  (S  "false"  [])
                                  fi 


Date html generated: 2016_05_15-PM-10_12_34
Last ObjectModification: 2015_09_23-AM-08_22_47

Theory : minimal-first-order-logic


Home Index