# Does a constant symbol with a free variable imply a contradiction in FOL?

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.

• IMO it means simply that if we do not specify that the function "and" has two argument places, what we get from the program is the def of a "constant": $\lnot ( a \to \lnot b)$ that can have sometimes value T and sometimes F, meaning that is not constant. Commented Aug 11 at 15:39
• I think the gist of what Mario is saying is that if you have a symbol "$\mathrm{and}$" such that $\forall a b. (\mathrm{and} = a \land b)$ where $a$ and $b$ are universally quantified at the meta level, you can prove that $\top = \top \land \top = \mathrm{and} = \bot \land \bot = \bot$ and get a contradiction. Commented Aug 11 at 16:31