Wednesday, 7 August 2013

Jacquette's Argument for the Inconsistency of Type Theory

Several years ago, Dale Jacquette wrote a piece in Analysis called "Grelling's Revenge" (2004), arguing that type theory (or higher-order logic, it makes not too much difference) is inconsistent. His argument is that Grelling's paradox reappears in type theory. I won't give the argument except to write down his "definition" of $\mathsf{H}^n$:
(D) $\forall F^n \forall F^{n - 1}[\mathsf{H}^n(F^{n-1}) \leftrightarrow \neg F^n(F^{n -1})]$ 
There were several submissions to Analysis replying to it, and the editor showed them to me. These analyses were mistaken; so the editor asked me to write a short reply explaining Jacquette's error. My reply was "Jacquette on Grelling's Paradox" (2005, Analysis).

The error is this: (D) is not a definition, as the definiens contains two free variables, $F^n$ and $F^{n-1}$ while the definiendum, $\mathsf{H}^n(F^{n-1})$, contains only one.

Let L be a language and suppose we introduce a new unary predicate P. And let us set down this "definition":
(D*) $P(x) \leftrightarrow F(x, y)$
where $F(x,y)$ is some formula from $L$. Now this is not an acceptable definition, because the free variable $y$ in the definiens $F(x,y)$ does not appear in the definiendum, $P(x)$.

In some cases, this will lead to inconsistency. For example, consider adding such a "definition" to arithmetic. E.g.,
(D**) $P(x) \leftrightarrow x < y$
Then, since we can prove $1 < 2$, we can prove
And since we can prove $\neg(1 < 0)$, we can prove
$\neg P(1)$
This is an inconsistency. Does this imply that $\mathsf{PA}$ is inconsistent? Well, no. It is simply caused by the presence of extra free variables in (D**).

Jacquette for some reason does not accept the error and continues to believe that type theory is inconsistent, and that these constraints on definitions are not important. His article is here:
Make of it what you will!

[Update (8th Aug): At the risk of belabouring the point, in his article, Jacquette writes:
$(1) \hspace{5mm} \forall x \forall y(P(x + y) \leftrightarrow x < y) \hspace{2cm}$ Definition
Obviously, (1) is not a definition: it contains both $P$ and the function symbol $+$.]


  1. I take a categorical view, which some might say could be deemed central to type theory. Categories are really 'the standard of standardization' in my view.

    I will assume I have some grasp of the logical phrase above. It seems to relate to set-theory concepts of spirals, or perhaps bounded boxes.

    No matter what it symbolizes, I will express my own interpretation.

    If H(^)n is take to mean the central value or parsing process, and if the repeated F^n-1 is taken to be a standard deviation from an opposite pair, expressed by F^n (assumed) and 'not' F^n, then the paradoxical expression is a very simple approach to categories, a denial of exclusion.

    Consider, in one theory of physics, the universe returns to the same point, but at infinite distance. It is the same problem. Either (1) The universe is cyclical, or (2) The universe is linear and unending.

    Then it is up to the logician or mathematician to decide (formally) if the 'system' used is itself cyclical, or instead, definite, and otherwise it may be seen as lacking a definition.

    This assumes, or posits, that a system is coherent. It is, as an alternate, possible to define a system as an amalgam of other systems, but this requires a still further system, which is capable of parsing amalgams. Perhaps that is the central, and un-addressed, issue. At any rate, the proposal that sets (or systems) are cyclical or definitive seems to be an adequate solution from my point of view.

    I have already applied this same idea in my interesting book, The Dimensional Philosopher's Toolkit (2013), not to be confused with Baggini and Fosl's classic.

  2. To clarify, I interpreted the problem as consisting of the subtraction and addition of value (or truth) from an entire set, with the idea that a paradox emerges when part of the outer bound has no truth or value, or if another part has additional truth which becomes relevant only because part of the context has been ignored. Perhaps that is clear.

  3. Dear Jeffrey,
    Your analysis seems entirely convincing; Jaquette's point is incomprehsible to me. Suppes, Introduction to Logic,Ch 8,rehearses the arguments for definitional variable restrictions in a nice way.

    With respect to the substative point that Jaquette was concerned to establish, namley the (in)consistency of Simple Type Theory, we may also point to Gentzen's trivial demonstration of its consistency in 'Die Widerspruchsfreiheit der Stufenlogik', Math. Zeitschrift 41(1936), pp.357-366. He uses the "one-elment model", and obtains a finitary consistency proof for STT, in much the same way as one reduces the consistency of predicate logic to propositional logic, by considering a domain with only one element. (Matters are different of course if we include an axiom of infinity; then there is no one-element model ....)

    Nothing that Jaquette has adduced can shake one's faith in that simple Gentzen demonstartion.

  4. Thanks, Göran.
    I don't know why Jacquette didn't just say, "Oops, my mistake". Instead, he insists he's right, nearly a decade later!

    Yes, Gentzen's method gives a simple model.