Boolean Terms

The Idea

• Variables of type $o as formulae
• Formulae (including variables) as terms
• BNF: Atomic formulae as terms

Examples

• ! [X: $o]: (X | ~X)
• imply: ($o * $o) > $o
  ! [X:$o,Y:$o]: (imply(X,Y) <=> (~X | Y))
• dom: $tType      ran: $tType      p: (dom * ran) > $o
  ! [X:dom,Y:ran,Z:ran]: imply(p(X,Y) & p(X,Z), Y = Z)