Saturday, 13 July 2013

Two Notions of Consequence/Deducibility in FOL

In the comments below the M-Phi post on $FS$ and the Deduction Theorem, Sam Roberts reminded me that what happens here depends on how we formulate restrictions on (Gen) and (DT). And Jack Woods mentioned some other very valuable discussion of closely related topics, of which Arnon Avron's
Avron, A. 1986 "Simple Consequence Relations" (LFCS Series Reports, University of Edinburgh)
is the best I've seen so far. (I return to this below.)

The difference turns on two different notions of deducibility/consequence.

We are thinking of standard first-order predicate logic. Let $L$ be a standard first-order language of some kind, over some signature. Let $\mathcal{M}$ be an $L$-interpretation and let:
$\sigma : Var(L) \to M$
be an assignment over $M$ (i.e., a function mapping each variable $x$ to an element $m \in M$). Then, assuming that the semantic "$\phi$ true in $\mathcal{M}, \sigma$" relation,
$\mathcal{M},\sigma \models \phi$ 
is already inductively defined over the $L$-formulas, we usually define semantic consequence:
(SEM) $\phi \vDash \theta$ 
to mean:
for all $\mathcal{M}, \sigma$: if $\mathcal{M},\sigma \models \phi$ then $\mathcal{M},\sigma \models \theta$ 
On this understanding, then the deducibility relation $\vdash$ satisfies:
Unrestricted Deduction Theorem (DT)
If $\Delta, \phi \vdash \theta$ then $\Delta \vdash \phi \to \theta$. 
Restricted Universal Generalization on a variable (UGV)
If $\Delta \vdash \phi$, then $\Delta \vdash \forall x \phi$ ($x$ not free in $\Delta$). 
But we can also define a slightly different notion of consequence---call it $\forall$-semantic consequence---so that:
($\forall$-SEM) $\phi \vDash^{\forall} \theta$
means:
for all $\mathcal{M}$: if ($\mathcal{M},\sigma \models \phi$, for all $\sigma$) then ($\mathcal{M},\sigma \models \theta$, for all $\sigma$). 
On this understanding, then the corresponding deducibility relation $\vdash^{\forall}$ satisfies:
Restricted Deduction Theorem (DT*)
If $\Delta, \phi \vdash^{\forall} \theta$ then $\Delta \vdash^{\forall} \phi \to \theta$ (where $\phi$ is a sentence).
Unrestricted Universal Generalization on a variable (Gen)
If $\Delta \vdash^{\forall} \phi$, then $\Delta \vdash^{\forall} \forall x \phi$. 
On the first, we have (DT) unrestricted and (Gen) is restricted (I call it (UGV)). And on the second, we have (DT) restricted (I call it (DT*) and (Gen) is unrestricted. These correspond to the different notions of semantic consequence, $\vDash$ and $\vDash^{\forall}$.

Of these, I generally assume $\vDash$. One advantage of $\vDash$ is that it fits with treating interpretations as interpreting everything, including variables. So, for me, an $L$-interpretation $\mathcal{A}$ interprets the variables too, so we have:
$x^{\mathcal{A}} \in A$. 
We can therefore forget about variables assignments $\sigma$ entirely, and this simplifies the formulation of the semantic clauses and simplifies many lemmas and subproofs in, e.g., the soundness and completeness theorems.

For example, the clause for the evaluation of universally quantified formulas is then:
$\mathcal{A} \models \forall x \phi$ iff, for every $a \in A$, $\mathcal{A}^x_a \models \phi$
where $\mathcal{A}^x_a$ is the interpretation just like $\mathcal{A}$ except that it assigns $a$ to the variable $x$.

And semantic consequence is then defined by:
$\phi \vDash \theta$ iff for all $\mathcal{A}$: if $\mathcal{A} \models \phi$ then $\mathcal{A} \models \theta$ 
One of my teachers, Moshe Machover, in his 1996 textbook Set Theory, Logic and Their Limitations, explained these differences as follows (Machover 1996, pp. 178-9):
9.13 Warning
Versions of classical Fopcal found in the literature come in two versions. One group consists of strong versions that are equivalent to ours. The group consists of weak versions that are equivalent to each other, but not to ours. To describe the relationship between the two groups, let us denote by '$\vdash^{\forall}$' the relation of deducibility in a weak version of Fopcal. The following four facts must be noted.
(i) Whenever $\Phi \vdash \alpha$ then also $\Phi \vdash^{\forall} \alpha$, but the converse does not always hold -- it is in this sense that $\vdash$ is stronger than $\vdash^{\forall}$.
(ii) For any set $\Phi$ of formulas, let $\Phi^{\forall}$ be a set of sentences obtained from $\Phi$ upon replacing each $\phi \in \Phi$ by $\forall x_1 \forall x_2 \dots \forall x_n \phi$, where $x_1, x_2, \dots, x_n$ are all the free variables of $\phi$. Then $\Phi \vdash^{\forall} \alpha$ iff $\Phi^{\forall} \vdash \alpha$.
(iii) While DT holds for $\vdash$ outright, only a restricted version of it, subject to certain conditions, holds for $\vdash^{\forall}$.
(iv) An unrestricted rule of generalisation holds for $\vdash^{\forall}$: if $\Phi \vdash^{\forall} \alpha$ then also $\Phi \vdash^{\forall} \forall x \alpha$, where $x$ is any variable. For $\vdash$ only a restricted version of this rule holds, as we shall see.
So, be careful which notions you're using!

For the deducibility relation, $\vdash$ (with restricted (GEN) and unrestricted (DT) is the notion that appears in Enderton, Bell & Machover & Machover. Machover (1996, Set Theory, Logic and Their Limitations) has a Hilbert-style linear deductive system with a single rule of inference---Modus Ponens---and formulates a version of (Gen) as a metatheoretic property of $\vdash$ and calls it (UGV), "universal generalization of a variable".

On the other hand, $\vdash^{\forall}$, with unrestricted (Gen) and restricted (DT), is the one in Mendelson's textbook. Note that Mendelson, however, does not define semantic consequence differently. His notion is the usual local notion, $\vDash$. I.e., $\phi \vDash \theta$ just if, for any $\mathcal{M}, \sigma$, (if $\mathcal{M}, \sigma \models \phi$, then $\mathcal{M}, \sigma \models \theta$).

Next, I mention Avron's discussion in "Simple Consequence Relations", that Jack Woods mentioned in the comments. I will use Avron's notation:
3.2 First-Order Logic
Let $A_1, \dots, A_n, B$ be formulas of some first-order language $L$ (i.e., they may contain free variables).
Truth: $A_1, \dots, A_n \vdash_t B$ iff $B$ is true in every model, relative to every assignment that makes all the $A_i$s true.
Validity: $A_1, \dots, A_n \vdash_v B$ iff $B$ is valid in any model (for $L$) in which all the $A_i$s are valid (by "valid" we mean true relative to all assignments).
Avron then notes that (changing notation a teeny bit):
$\forall x A(x)$ follows, for example, from $A(x)$ according to the second, but not according to the first. On the other hand, the classical deduction theorem holds for the first but not for the second. The two consequence relations are identical, though, from the point of view of theoremhood:
$\vdash_t A$ iff $\vdash_v A$,
(and in fact if all formulas of $\Gamma$ are closed, then $\Gamma \vdash_t A$ iff $\Gamma \vdash_v A$).
and then, applying similar ideas to the case of modal logic:
3.3 Propositional Modal Logic
Truth: $A_1, \dots, A_n \vdash_t B$ iff for any frame and any valuation in this frame, $B$ is true in every world in this frame in which all the $A_i$s are true.
Validity: $A_1, \dots, A_n \vdash_v B$ iff $B$ is valid (i.e. true in all worlds) in every frame relative to any valuation which makes all the $A_i$s valid.
and then Avron adds:
... The situation concerning them is similar to that in the previous case.
$A \vdash_v \square A$ but $A \nvdash_t \square A$.
The deduction theorem obtains for $\vdash_t$ but not for $\vdash_v$.
[UPDATE. 2 August 2013. I made a couple of revisions, as Aldo Antonelli pointed out to me that Mendelson's formulation of semantic consequence relation is the usual local noton (i.e., $\vdash_t$ in Avron's notation), though Mendelson's deductive consequence relation is the global one, $\vdash^{\forall}$. This can all be a bit confusing!]

7 comments:

  1. It is perhaps worth emphasizing that for a model theorist, the important notion is $\models^\forall$. E.g., model theorists talk about "open theory" as one where every formula is an open, i.e., has no quantifiers. At the same time, the underlying proof theory is assumed to be a Hilbert-type calculus and $T \vdash \phi$ means: there is a proof of $\phi$ from axioms in $T$. This system is based on unrestricted generalization, and hence the standard model-theoretic consequence relation used there is $\models^\forall$. At least that's how it was back when I learned model theory from Chang & Keisler.

    ReplyDelete
  2. PS: Found this: http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/ which is somewhat relevant

    ReplyDelete
  3. Hi Richard,

    That's an interesting post by Andrej; though I have to admit, I'm a little unclear exactly what view he is addressing.

    At least a few of his reasons struck me as wrong, however. For instance, reasons 3 and 4 not only fail to take account of $\vDash^\forall$ and $\vdash^\forall$, but they take restricted quantification to be equivalent to unrestricted -- $\forall x(x\in 0 \to \bot)$ doesn't entail $\bot$ even if $\forall x\phi$ is inter-derivable with $\phi$, for all $\phi$.

    Also, on reason 6: I wonder why one couldn't just think that free variables within a proof context are implicitly bound from the outside? Indeed, the initial ``Consider any $x$" suggests that this is so.

    All the best,
    Sam

    ReplyDelete
  4. Thanks chaps

    I think I'll write another thing on this, as the "global"/"local" distinction is quite interesting.

    Cheers,

    Jeff

    ReplyDelete
  5. I'm with you on problems with reason 6. There are more options available than treating expressions like ''Consider any x∈R'' as involving a free variable. Binding from the outside is possible, as is treating ''Consider any x∈R'' as a covert epsilon term.

    ReplyDelete
  6. Jack, the comments here will understand LaTeX. E.g.,
    $r \in \mathbb{R}$.
    Unfortunately, the comments preview doesn't understand LaTeX, so you only get one chance!
    But if you comment twice (or just once), and the LaTeX has a missing dollar sign or bracket, I'll fix it.

    Cheers,

    Jeff

    ReplyDelete
  7. Thanks for letting me know. I worried when the latex didn't show up in the preview.

    ReplyDelete