Wednesday, 10 July 2013

Does FS Violate the Deduction Theorem?

$FS$ is an axiomatic truth theory, due to Harvey Friedman and Michael Sheard 1987, "An Axiomatic Approach to Self-referential Truth". The standard formulation is given by Volker Halbach, in 1994 "A System of Complete and Consistent Truth" and in his 2011 monograph Axiomatic Theories of Truth.

$FS$ satisfies the following closure conditions:
(Nec) If $FS \vdash \phi$ then $FS \vdash T\ulcorner \phi \urcorner$.
(CoNec) If $FS \vdash T\ulcorner \phi \urcorner$ then $FS \vdash \phi$.
The first of these is also sometimes called (T-Intro) and the second (T-Elim). These may also be formulated as "rules of inference" in a Hilbert-style deductive system:
(T-Intro) $\phi / T\ulcorner \phi \urcorner$.
(T-Elim)  $T\ulcorner \phi \urcorner / \phi$.
(See Friedman & Sheard 1987, p. 5) But please note, for later, that these specifications certainly do not mean:
$\phi \vdash T\ulcorner \phi \urcorner$.
$T\ulcorner \phi \urcorner \vdash \phi$.
Rather (T-Intro) and (T-Elim) mean:
(T-Intro) If you have a proof P of $\phi$ in $FS$, then you may add $T\ulcorner \phi \urcorner$ and the result is a proof P* of $T\ulcorner \phi \urcorner$ in $FS$.
(T-Elim) If you have a proof P of $T\ulcorner \phi \urcorner$ in $FS$, then you may add $\phi$ and the result is a proof P* of $\phi$ in $FS$.
A forthcoming Mind article, "Reaching Transparent Truth", by Pablo Cobreros, Paul Egré, David Ripley, Robert van Rooij, sets out a truth theory STT:
This paper presents and defends a way to add a transparent truth predicate to classical logic, such that $T\langle A \rangle$ and $A$ are everywhere intersubstitutable, where all T-biconditionals hold, and where truth can be made compositional. A key feature of our framework, called STT (for Strict-Tolerant Truth), is that it supports a nontransitive relation of consequence. At the same time, it can be seen that the only failures of transitivity STT allows for arise in paradoxical cases
In the article, the authors criticize $FS$ for "giving up the Deduction Theorem":
Even the classical theory FS described in [Friedman and Sheard, 1987] gives up the deduction theorem. (p. 8)
And the article goes on to argue that, with a Deduction Theorem, one "could derive A ⊃ T ⟨A⟩ from the rule Nec":
For STT, transitivity goes; for FS, it is the deduction theorem that must fail. With a deduction theorem, we could derive A ⊃ T ⟨A⟩ from the rule Nec, or T ⟨A⟩ ⊃ A from the rule Co-nec, and either would immediately trivialize the system. (p. 15)
I am baffled by this.

We do have the Deduction Theorem for $FS$ (more exactly, for $\vdash$), and we cannot derive $A \supset T\langle A \rangle$ from the rule Nec. The axiomatic truth theory $FS$ is formulated in a standard Hilbert deductive system. This deductive system has the property that:
Deduction Theorem
If $\Delta, \phi \vdash \theta$ then $\Delta \vdash \phi \to \theta$.
This is, properly speaking, a property of the deducibility relation $\vdash$.

If I understand the reasoning involved, the authors are mixing up
  • Conditional Proof (a rule of inference used in some deductive systems: e.g., Natural Deduction)
  • Deduction Theorem (a general property of the deducibility relation $\vdash$).
But one should be careful not to mix up truth-preserving rules of inference with rules that preserve theoremhood.

For example, in a Hilbert-style deductive system, Generalization (Gen) is a rule that preserves theoremhood, but does not preserve truth. That is, (Gen) allows us to infer $\forall x \phi$ when we have derived $\phi$ from assumptions that lack $x$ free. So long as $x$ does not occur free in the formulas in $\Delta$, then
If $\Delta \vdash \phi$, then $\Delta \vdash \forall x \phi$.
But it does not follow that:
$\phi \vdash \forall x \phi$.
For, if it did, then, by (DT), we should then have:
$\vdash \phi \to \forall x \phi$.
and hence, by universal generalization (Gen):
$\vdash \forall x(\phi \to \forall x \phi)$.
and hence, by prenexing and relabelling:
$\vdash \forall x \forall y(\phi \to \phi^x_y)$.
And the formula $\forall x \forall y(\phi \to \phi^x_y)$ is not a logical truth. For consider $\forall x \forall y(Fx \to Fy)$. This is false in the structure $\mathcal{A}$ with domain $\{0,1\}$ and where $F^{\mathcal{A}} = \{0\}$.

Analogously to this, modal systems $M$ often have the property (Necessitation):
If $\vdash_{M} \phi$ then $\vdash_{M} \square \phi$.
But it does not follow that:
$\phi \vdash_{M} \square \phi$.
There are a number of ways of expressing what is going on here. I prefer to say that:
  • There are rules that preserve truth.
  • There are rules that preserve some other property P (where P might be theoremhood, validity, necessity, etc.).
E.g., Modus Ponens preserves truth. Generalization does not preserve truth! It does, however, preserve theoremhood (or logical truth). For if $\phi(x)$ is a theorem of logic, then $\forall x \phi(x)$ must be also. But if $\phi(x)$ is merely true in, say, $\mathcal{M}, \sigma$ (i.e., some variable assignment), then there's no reason why $\forall x \phi(x)$ should also be true as well.

Some authors express the distinction as between "rules of inference" and "rules of proof", a distinction that was drawn by T.J. Smiley, in:
Smiley 1963: "Relative Necessity" JSL.
Smiley's distinction is discussed here by Lloyd Humberstone:
Humberstone 2010: "Smiley's Distinction Between Rules of Inference and Rules of Proof". (For citation information, see here.)
[Many thanks to Branden Fitelson, Antonio Negro and Jack Woods for these references and links.]

A nice discussion of some of these topics (and covers the issue for modal logic) can also be found in:
Hakli & Negri 2010: "Does the Deduction Theorem Fail for Modal Logic?"
[UPDATE. 11 July: There are some changes and new links; thanks to comments below.]


  1. Hi Jeff,

    It's perhaps also worth noting that there are axiomatisations of first-order logic for which the unrestricted deduction theorem fails. The axiomatisation in Mendelson, for instance. There, Gen is unrestricted -- that is, $\phi \vdash \forall x\phi$ holds for arbitrary $\phi$. The difference corresponds to a difference in the semantics -- global consequence (if the premises are true on all assignments so is the conclusion) gives us unrestricted generalisation and a restricted deduction theorem, and local consequence (if the premises are true on an assignment $a$, then so is the conclusion) gives us restricted generalisation and an unrestricted deduction theorem.


  2. Hi Sam,

    Yes, that's right; I'd forgotten Mendelson's different setup.
    Machover in his textbook lays out the difference too somewhere. The local consequence relation is the one seems much more natural though, as it's nice to build the assignment into the structure too, so a structure $\mathcal{A}$ also interprets each variable $x$ as well as $x^{\mathcal{A}} \in A$.

    I should do an update.



  3. Smiley deserves more credit in this context than he is typically given. See:

  4. Thanks, Branden, yes, good point!
    Will include this when I update.


  5. Nice post. Branden beat me to it, but maybe it's worth double emphasizing Humberstone's paper and pointing to the original Smiley '63 paper ( on relative necessity.

  6. Hi Jeff,

    Thanks for your reply!

    Just to be clear: the Mendelson example was aimed at the implicit assumption that failure of the deduction theorem is clearly a bad thing. (It's also useful, it seems to me, to keep in mind with the debate about supervaluationism and logical revision -- there, most, if not all, putative examples of deviation from classical logic are shared by Mendelson's axiomatisation!)

    As you point out, in the RTT passage it's not (just) that they overvalue the deduction theorem, but that they misapply it. I'm not sure, though, if this is a result of mixing up the deduction theorem with conditional proof. It seems rather to be a result of mixing up T-intro, say, with $\phi\vdash T(\phi)$. I would have thought conditional proof is just as misapplied to T-intro to get T-in as is the deduction theorem. Or am I missing something?

    All the best,

    P.s. I find global consequence pretty natural :)

  7. Hi Sam,
    Yes, thanks - I pretty much agree with all that. You may be right that it's not (CP); but when something's gone awry, it's not clear what the exact thing is that's gone awry... Right, I already did an update, and mentioned the difference between T-Intro and $\phi \vdash T\phi$.
    But I want to do a separate post on this issue and the deduction theorem. It's got me interested and there are some things I'm still not clear about, and I'd like to learn about.

    Suppose we call global consequence $\vDash^{\forall}$.
    Then if $\phi \vDash \theta$, then $\phi \vDash^{\forall} \theta$ - but not conversely. Where are these terms "local" and "global" from? I've not heard them before, but they make perfect sense, of course. They sound like they might be from some modal logic textbook?



  8. Hi Jeff,

    You know, I think I just stole them from the supervaluational literature and reapplied them here!

    All the best,

  9. The distinction crops up in lots of areas. One sensible discussion is in Arnon Avron's ''Simple Consequence Relations'' (Reprinted in Gabbay's What is a Logical System?) I think it's also mentioned in Blackburn's Modal Logic, though it's been a long time since I looked at that.

    There's some play between this sort of distinction and categoricity for the logical constants as well since using preservation of something like local or something like global consequence makes a difference when you attempt to read a semantics off of a set of natural deduction rules. Humberstone also has a good paper on this--"Valuational Semantics for Rule Derivability"; James Garson has some work on it, and I've had a crack at it myself in a recent paper in Thought.

  10. Thanks both.
    Because the issue seems quite interesting, I did a separate post on the topic, and mentioned some of these papers. The Avron paper is very good: very clear.
    (Actually, come to think f it, I forgot to use the words "global" and "local".)



  11. Ok, I've now studied this all a bit more!

    The terms "global" and "local" that Sam mentioned come from the modal logic literature (this shows how little modal logic I've bothered to study!) and are fairly standard. I assume they appear in the supervaluationist literature. So we have

    logical consequence: $\vDash_{l}$
    global consequence: $\vDash_{g}$.

    And $\vDash_{l}$ is Machover's $\vDash$ and is Avron's $\vDash_{t}$

    While $\vDash_{g}$ is Machover's $\vDash^{\forall}$ and is Avron's $\vDash_{v}$.

    The local consequence relation is stronger in the sense that

    (i) If $\Delta \vDash_{l} \phi$ then $\Delta \vDash_{g} \phi$

    But not conversely, because,

    (ii) $\phi(x) \vDash_{g} \forall x \phi(x)$

    (iii) $\phi(x) \nvDash_{l} \forall x \phi(x)$

    Which is just a way of saying that unrestricted (Gen) holds for $\vDash_{g}$ but not for $\vDash_{l}$.

    In a sense, the global consequence relation treats an open formula $\phi(x)$ as equivalent to its universal generalization $\forall x \phi(x)$.