I’ve already described the relatively simple Monadic Hybrid Calculus that allows you to say simple things formally without bound variables. For example, sG may mean “Socrates is Greek”, [G]M “all Greeks are Mortal”, and the conclusion “Socrates is Mortal”, sM.

The MHC has a big brother, the Hybrid Predicate Calculus (HPC), which (apparently) has the power of full predicate logic. But at a certain point, it gets weird!

The basic idea is simple enough, you expand  MHC by allowing property constants to have extra arguments (still on the left). For example, to say that Socrates (s) likes Plato (p) you write

spL

Notice the verb comes last  – the HPC is an SOV language, like Japanese. (This means the  typical simple sentence has a subject, and object, and a verb, in that order).

As we saw, the MHC has expressions that correspond to natural language quantifier phrases, such as “All Greeks”. The HPC has them too, and they can be used like nouns. Thus

[G]pL

says that all Greeks  like Plato.

The HPC allows partial application – a relation constant (like L) does not have to have a full set of arguments. Thus L on its own denotes the liking relation, pL denotes the property of liking Plato, and thus spL can be understood as saying that Socrates has this property. In other words, that Socrates likes Plato.

Since pL is a property, we can form the quantifier phrase [pL], which clearly means “everyone who  likes Plato”. Thus

[pL]aL

says that everyone who likes  Plato likes Aristotle.

In this way we can nest brackets and say things that in conventional logic require nested quantifiers. 〈A〉L is the property of liking some Athenian. [〈A〉L] therefore means “everyone who likes some Athenian” and

[〈A〉L]sL

says that anyone who likes some Athenian likes Socrates.

The students and I managed to say some pretty complex things without bound variables. One of my bonus questions was

Every student registered in at least one course taught by professor Egdaw is registered in every course Pat is registered in.

We should use R as the registered relation, T as the teaches relation, e as professor Egdaw, and p as Pat.

However, we immediately run into a problem: how to express the property of being a course taught by professor Egdaw. eT doesn’t work, it’s the property of teaching professor Egdaw. What we need is  the taught-by relation, the converse of T. There is no way of doing this with what we have. But there’s an easy fix: add the converse operator. We denote it by the (suggestive) tilde symbol “~”. In general, ~K is the relation K with the first two arguments swapped, and in particular ~T is the taught-by relation (“~” often translates the passive voice).

We can now proceed in stages. e~T is the property of being taught by professor Egdaw and 〈e~T〉 is “some course taught by professor Egdaw”. 〈e~T〉R is the property of being registered in some course taught by (the brilliant) Egdaw, and [〈e~T〉R]  is “every student registered in a (at least one) course taught by professor Egdaw”.

Now for the second main quantifier phrase. p~R are the courses Pat is registered in, and [p~R] is “every course pat is registered in”. We simply put the two phrases one after another followed by R and get

[〈e~T〉R][p~R]R

I used to think this was hard but actually it’s pretty straight forward. It’s interesting to compare it with the first order logic formalization

∀s((∃c R(s,c) ∧ T(e,c)) →∀c (R(p,c) → R(s,c)))

Of course, it was not a a good sign that we had to introduce a new feature (the converse operator). Will other examples require other features? How far will this go?

Just a bit further. We run in to another problem if we try to say “Plato likes all Athenians who like themselves”.  How do we express the property of liking oneself?

Again, impossible with what we’ve got. We have to introduce a sort of  self operator /. /K is like K except the first argument to K  is duplicated. /L is the property of liking yourself and the expression we’re looking for is

p[A∧/L]L

We need one more operator that has the effect of ignoring an argument. We use “*” and *K is like K except *K ignores its first argument, its second argument is the first given to K, its third argument is the second given to K, and so on. We’d need it to express e.g. the relation of Spartans liking Athenians. The expression *S∧A∧L denote the relation that says that its second argument, who is Spartan, likes its first argument, who is Athenian.

Perhaps these equivalences will help

cba~K ↔ cabK
cba/K  ↔ cbaaK
cba*K ↔ cbK

You can think of these three operators as replacements for things  you can do with arbitrary use of  variables. First, variables can be out of order, hence ~; variables can be duplicated, hence /; and variables can be omitted, hence *.

The only problem is that these three operators  provide only simple cases of swapping, duplication, and omission. What if you need, say, to swap the third and second arguments, duplicate the third or omit the fourth? Don’t you need whole families of operators?

Not  quite; instead, we add a meta operator that generates these families. In general, if ⊗ is an operator then ⊗’ is the operator that works with the indexes of the arguments shifted by one. Thus ~’ swaps the third and second arguments, /’ duplicates the second argument, and *’ omits the second arguments and shifts the higher ones. This gives the equivalences

dcba~’K ↔ dbcaK
dcba/’K ↔ dcbbaK
dcba*’ ↔ dcaK

The meta-operator ‘ can be iterated (e.g. /”’) and can also be applied to any quantifier phrase.

I’m pretty sure that this is enough, that anything that can be said in first order logic can be said in HPC. The only problem is, sometimes the result looks like a dog’s breakfast. The experience has been that assertions that can be expressed simply in natural language can be expressed simply in  HPC, but that more technical statements (like the axioms of set theory) are often incomprehensible.

There’s more to the story. For example, HPC can be easily understood in terms of operations on relational tables. But I’ll leave that to a future post.