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
                 if knd =a "or" then p ∨ q
                 else p ⇒ q
                 fi 


Definitions occuring in Statement :  FOSatWith: Dom,S,a |= fmla,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  let: let,  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  lambda: λx.A[x],  token: "$token"
FDL editor aliases :  FOConnective
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
                                  if  knd  =a  "or"  then  p  \mvee{}  q
                                  else  p  {}\mRightarrow{}  q
                                  fi 


Date html generated: 2015_07_17-AM-07_53_15
Last ObjectModification: 2012_09_03-PM-11_06_20

Home Index