Reifying logic

24 Feb 2018, 14:38 • logic, nlp

This post describes formal logic embedded in formal logic. It sounds really weird but a simple example will illustrate why it might be useful.

This post is largely based on the work of computational linguist Jerry Hobbs. Imagine that we want to formalise utterances such as "Fido barks". Our first naïve guess might be

\[ bark(Fido) \]

However, if we had "I know that Fido barks", we'd need to refer to the barking. So the barking is also an entity and "Fido barks" would be more adequately expressed by

\[ bark(e,Fido) \]

where \(e\) is an eventuality. However, being Fido is also an eventuality so we really need

\[ bark(e_1,x) \land Fido(e_2,x) \]

or, more precisely

\[ \exists e_1,e_2,x . bark(e_1,x) \land Fido(e_2,x) \]

We'll henceforth assume that all variables in logical forms are existentially quantified.

Eventualities may represent real events but also only possible events or even something impossible in a given context. For example, in "I want to have a unicorn" the having eventuality will never obtain in the real world. We'll use \(true(e)\) to express that an eventuality really exists.

We now get to basic logical connectives. We can't use what FOL gives us because the usual \(\neg,\land,\lor\) can't be used with eventualities. Rather we need separate predicates to express "and", "or" and "not". These "logical predicates", like all other predicates, operate to eventualities whose truth value is given by the following axioms:

\[ \begin{array}{c} and(e_1,e_2,e_3) \supset (true(e_1) \equiv true(e_2) \land true(e_3)) \\ or(e_1,e_2,e_3) \supset (true(e_1) \equiv true(e_2) \lor true(e_3)) \\ not(e_1,e_2) \supset (true(e_1) \equiv \neg true(e_2)) \\ \end{array} \]

Similarly, we could have \(imply(e_1,e_2,e_3)\) or a predicate for exclusive disjunction, etc. There's also an elegant way of reifying quantification but this is a topic for a future post.