When listening to this talk, I came across an interesting claim (at 12:30) which I wanted to verify:
[...] We have defined a constant (called
and) which takes no arguments and unfolds to something containing variables $a$ and $b$, which can be whatever we like. It is an interesting exercise to show that a constant with such properties is inconsistent.
My interpretation of this claim in FOL is the following: We have a language of classical FOL (with identity!) with the signature $\{ T(x) \}$. For all terms $t$ and $k$, $T(t)$ and $T(k)$ are taken to be meta-logically equal, as if they were the same string.
Viewing $T(x)$ as a unary function from the domain onto itself, it is derivable that:
- $T(x)$ is a constant function, i.e., $\forall x \forall y.T(x) = T(y)$ (obvious, from the properties of constant symbols),
- $T(x)$ has a fixed point, i.e., $\exists y.y = T(y)$,
- the domain has only one element, i.e., $\forall x\forall y.x = y$ (this requires LEM).
However, I failed to derive a contradiction. I am interested in whether my interpretation of the exercise was even roughly correct in the first place, and if so, what is the solution. If not, I am interested in the correct interpretation of the exercise.
