The Universal Hybrid Calculus (UHC) is a simple logical formalism that has the power of the monadic predicate calculus but has no bound variables. Natural language statements (which also do not use variables) can be formulated more directly in the UHC. In particular, the UHC, like natural language, uses quantifier phrases (such as some Greeks or all mortals) rather than quantifiers and variables.

(This is joint work with my PhD student Omar Alaqeeli)

The UHC is based on the simplest of the modal logics, S5. S5 can be explained (in a nonstandard way) as follows: there is a nonempty universe of individuals (say, people). Properties of individuals are denoted by property constants, which are upper case letters. For example, M might denote the property of being mortal, and G the property of being Greek. Boolean combinations of property constants also denote properties in the obvious way; so that e.g. G∧M denotes the property of being Greek and Mortal.

In addition to the usual Boolean connectives we have two modal operators [] and <> (these should be a box and a diamond but wordpress doesn’t have them). The symbol [] denotes universal generalization and the symbol <>, existential generalization. Thus []M asserts that all individuals have the property M (everyone is mortal) and <>G asserts that some individual has the property G (someone is Greek). (Strictly speaking these assertions denote properties that are uniformly possessed or not possessed by every individual.)

The semantics outlined can be used to verify the S5 axioms, such as [][]A→[]A,
[](A→B)→[]A→[]B, or <>(A∨B)→(<>A ∨ <>B)

The UHC extends S5 by adding two extra features. The feature feature (what computer scientists would call “syntactic sugar”) is that both [] and <> are split into brackets that enclose a property formula. This property formula is then taken as a restriction on the range of the quantification. Thus [G]M asserts that all Greeks are mortal, and <G>A that some Greeks are Athenian.

From a formal point of view this feature is minor. Instead of writing [G]M you can write
[](G→M), and instead of <G>A you can write <>(G∧A). Pragmatically, this is a big deal. For one thing, students inevitably get this backwards. (I call this, and many other observations, “Wadge’s Law” – see a future post). For another, it means that quantifier phrases such as every Greek and some Greek can be translated into the UHC – this is not true of the standard quantifier-based predicate logic.

The major feature is that the UHC has individual constants and predication. The constants are lower case letters and predication is reverse juxtaposition; the constant is placed to the left of the property formula.

Suppose, for example, that p denotes Plato and s Socrates. Then sG asserts that Socrates is Greek and p(M∧A) that Plato is a mortal Athenian. There is no way to translate these statements into S5.

For the UHC proof system we use Beth-style tableaus, in which formulas appear on either side of a vertical line. Those on the left are assumed true, those on the right, false (in most proofs these lines branch and form a  tree). The individual constants allow us to use straightforward rules for quantification, without resorting to labelled deduction.

For example, the rule for [A]B on the right allows us to take a ‘new’ (not already in use) constant n, add nA on the left and nB on the right, and cancel [A]B. For [A]B on the left, we can choose any constant c (normally one already in use), split the tree, put cA on the right side of the first branch, and cB on the left side of the second branch. [A]B is not cancelled because we may need to reuse the rule on another constant.

Al Aqeeli in his dissertation (soon to be defended) presents the metatheory of UHC – completeness, soundness, compactness etc.

In case you think this system is too simple let me leave you with a bonus problem I gave to my third year class. Take the assumptions sG (Socrates is Greek) and [G]M (all Greeks are mortal). We know that sM (Socrates is mortal) is a logical consequence. How many other (logically distinct) consequences are there? Hint: there’s a lot! I’ll give the answer in a future post, though of course you’re welcome to submit your own.