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$.

But we can also define a slightly different notion of consequence---call it $\forall$-semantic consequence---so that:Restricted Universal Generalization on a variable(UGV)

If $\Delta \vdash \phi$, then $\Delta \vdash \forall x \phi$ ($x$not freein $\Delta$).

($\forall$-SEM) $\phi \vDash^{\forall} \theta$means:

for all $\mathcal{M}$: if ($\mathcal{M},\sigma \models \phi$, forOn this understanding, then the corresponding deducibility relation $\vdash^{\forall}$ satisfies:all$\sigma$) then ($\mathcal{M},\sigma \models \theta$, forall$\sigma$).

(DT*)RestrictedDeduction Theorem

If $\Delta, \phi \vdash^{\forall} \theta$ then $\Delta \vdash^{\forall} \phi \to \theta$ (where $\phi$ is asentence).

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}$.Unrestricted Universal Generalization on a variable(Gen)

If $\Delta \vdash^{\forall} \phi$, then $\Delta \vdash^{\forall} \forall x \phi$.

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.13So, be careful which notions you're using!Warning

Versions of classical Fopcal found in the literature come in two versions. One group consists ofstrongversions that are equivalent to ours. The group consists ofweakversions 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.

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.2Avron then notes that (changing notation a teeny bit):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).

$\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 relationsand then, applying similar ideas to the case of modal logic:areidentical, though, from the point of view oftheoremhood:

$\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$).

3.3and then Avron adds:Propositional Modal Logic

Truth: $A_1, \dots, A_n \vdash_t B$ iff for any frame and any valuation in this frame, $B$ istruein everyworldin 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.

... The situation concerning them is similar to that in the previous case.[UPDATE. 2 August 2013. I made a couple of revisions, as Aldo Antonelli pointed out to me that Mendelson's formulation of

$A \vdash_v \square A$ but $A \nvdash_t \square A$.The deduction theorem obtains for $\vdash_t$ but not for $\vdash_v$.

*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!]

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.

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

ReplyDeleteHi Richard,

ReplyDeleteThat'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

Thanks chaps

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

Cheers,

Jeff

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.

ReplyDeleteJack, the comments here will understand LaTeX. E.g.,

ReplyDelete$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

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

ReplyDelete