The monadic hybrid calculus

摘要

We present the design goals and metatheory of the Monadic Hybrid Calculus (MHC), a new formal system that has the same power as the Monadic Predicate Calculus. MHC allows quantification, including relative quantification, in a straightforward way without the use of bound variables, using a simple adaptation of modal logic notation. Thus "all Greeks are mortal" can be written as [G]M. MHC is also 'hybrid'in that it has individual constants, which allow us to formulate statements about particular individuals. Thus "Socrates is Athenian and mortal" can be formalised as s(A A M). For our proof system, we use a simple adaptation of Beth-style tableaus. The availability of individual constants eliminates the need for labelled deduction. We discuss first the pragmatic and pedagogical advantages of MHC. Then we present the metatheory: formal syntax, semantics, proof rules, soundness, completeness and expressive equivalence with the Monadic Predicate Calculus.