The logic of Watson is dominated by three themes. It is algebraic (equational). An important role is played by definition by cases. Its higher order logic uses stratified abstraction. In this section, we will use notation closer to conventional mathematical notation than to Watson's internal language, which will be introduced in the next section.
-calculus and usual type
theories