### The Title of This Post is False

#### Posted by David Corfield

Continuing our enquiry into what homotopy type theory can do for the formalisation of natural language, if we could make good sense of the phenomena of self-reference, that should pique the interest of those discontent with predicate logic. We won’t be explicitly involving the *homotopy* aspect of the type theory here, and yet who knows whether it might assert itself, as it did last time on the subject of ‘the’.

So, let’s take a look at the classic liar paradox:

This proposition is false.

Now, what rules of type formation would allow such a proposition-as-type,

$Id_{Prop}(This \: proposition, \bottom)?$

Well, section 4.14 of Aarne Rante’s book Type-Theoretical Grammar discusses indexicals:

$\frac{A: Type \qquad a : A}{this(A, a): A}.$

So to say ‘this proposition’ we had better already have established a type of propositions, $Prop$, as well as a term of that type which we intend to refer to as ‘this proposition’. The idea of the paradox is that we have such a term. ‘This proposition is false’ is supposed to be the term of type $Prop$:

$Id_{Prop}(This \: proposition, \bottom) : Prop$

But we can’t form this term without forming ‘this proposition’. We seem to need

this($Prop$, this proposition): $Prop$,

but we can’t form this since we haven’t formed ‘this proposition’. Is it as simple as that – incorrect term formation?

Was there a whiff of fixed-pointness here, ringing inductive or coinductive bells? What of the Gödel sentence which states of itself that it cannot be proved?

## Re: The Title of This Post is False

This has nothing to do with type theory or homotopy-theoretic foundations. You can perform exactly the same argument in ordinary first-order logic equipped with Russell’s descriptive operator ɩ, or in a number of other formal systems. They typically resolve the paradox in exactly the same way as you did, by observing that there is no way of forming “this proposition”.

The usual attempts at self-referential propositions involve fixed-point operators. A naive attempt to define your proposition would be as the fixed point of negation “fix (λ p : Prop . ¬p)”. But now we have to argue that such a fixed point exists, which it does not, so people typically change the rules of the game (by changing the logic, or negation, or in some other way).

Gödel’s argument goes through thanks to the arithmetic fixed-point theorem where the fixed point crucially passes through a level of encoding that makes everything magically tick. Think of the encoding as a layer of encapsulation that “freezes” the infinite descend into an abyss of self-reference. A programmer would say that we “suspend the recursive call by thunking it”.

So, no homotopy type theory here folks.