5
$\begingroup$

In his exposition of FO-theory, Mendelson uses the Gen rule : $$A(x) \vdash \forall xA(x).$$

He also states the logical consequence relation : $$A ⊨ B$$ in terms of sequences : $A$ logically implies $B$ iff, in every interpretation $I$, every sequence $s$ that satisfies $A$ also satisfies $B$.

But with this definition, we have that NOT $A(x) ⊨ \forall xA(x)$.

As a consequence of Godel's Completeness Theorem, we have that (see pag.91 - Corollary 2.20d) : if a wff $B$ is a logical consequence of a wff $A,$ then $A \vdash B$.

But the viceversa is not stated (if I am right).

I do not understand the advantages of his definition of logical consequence.

Hunter (Metalogic [1972]) "restored the simmetry" avoiding the Gen rule.

Other textbooks more simply defined logical consequence in term of truth in an Interpretation: in this way we have that $A(x)$ is true iff $\forall xA(x)$ is true, so that $$A(x) ⊨ \forall xA(x).$$

$\endgroup$
3
$\begingroup$

The problem comes down to formulas with free variables. Suppose we have a formula $\phi(x,y) \equiv x = y$, and we have a structure $M$. What would it mean for $M$ to satisfy $\phi$? Well, it doesn't really make sense, because a variable "$x$" is not given an meaning by $M$ - $x$ doesn't denote anything, and neither does $y$. So $x = y$ has no truth value at all.

One solution is to strengthen the notion of a "model" so that it includes both a structure $M$ and a function that assigns an element of $M$ to each variable. This is essentially the method taken by Mendelson (and also by Enderton's classic textbook on logic). Now we have a a rigorous definition of what it means for a structure $M$ and variable assignment $s$ to satisfy $\phi(x,y)$; we might write $(M,s) \models x = y$.

The other option is to keep the notion of a model the same, but change the definition of $\models$. Now, $M \models x = y$ is defined to mean that, for every variable assignment $s$, $(M,s) \models x = y$ in the sense of the previous paragraph. But of course this is not likely to hold; in this sense we with have $M \not \models x = y$ as long as $M$ has at least two elements in its domain.

These approaches give the same truth values to all sentences - they only differ for formulas that have free variables. In many areas of mathematical logic, we are mostly interested in truth values of sentences. The main area where the second convention is useful is in universal algebra, where they often look at "equational theories". In that context, they tend to use formulas with free variables as axioms, rather than sentences without free variables. And they are interested in models where every variable assignment satisfies the formulas, not just some random variable assignment. So they often use the second convention.

I do recommend Enderton's book for a clear presentation of the first convention, the one where $A(x)$ does not necessarily imply $(\forall x)A(x)$.

$\endgroup$
  • $\begingroup$ Related: math.stackexchange.com/questions/97939/… $\endgroup$ – Carl Mummert Nov 22 '13 at 1:21
  • 1
    $\begingroup$ Thanks ! Cristal clear. My feeling is that (often) ML textbooks does not spend enough time clarifying this kind of "little" issues. $\endgroup$ – Mauro ALLEGRANZA Nov 22 '13 at 8:03
  • $\begingroup$ Example 1. Hunter [Metalogic (1972)] uses Mendelson's definition based on variable assignment, he avoids Gen rule, and so he is able to prove Deduction Theorem without usual restrictrions. At first reading, for me was diffuclt to grasp "how he can change" the Deduction Theorem. $\endgroup$ – Mauro ALLEGRANZA Nov 22 '13 at 8:07
2
$\begingroup$

Edit I've rewritten completely the answer after a re-read of Mendelson's book, apparently it has been passed from last time I've read that book.

As you noticed Mendelson's definition doesn't allow to deduce that

$$ A(x) \models \forall x A(x)$$

since it's not said that for any given sequence (i.e. an valuation of the variables $s$ if $s$ satisfies $A(x)$ then $s$ satisfies also $\forall x A(x)$).

Suppose we use a different semantics, for instance suppose that $$A \models B$$ means that for every interpretation that makes true $A$ makes true also $B$. From this would follows that $A(x) \models \forall x A(x)$. Nonetheless it wouldn't follow that $A \models B$ is equivalent to $\models A \rightarrow B$, indeed that's the case for the formulas $A(x)$ and $\forall x A(x)$: an interpretation for which $A(x)$ is one such that every sequence $s$ makes $A(x)$ true and so it must be that such interpretation makes $\forall x A(x)$ true, hence $A(x) \models \forall x A(x)$, anyway $\not \models A(x) \rightarrow \forall x A(x)$ since there are interpretations which don't make this true.

Having that $A \models B$ iff $\models A \rightarrow B$ is a really good property that we would like to have in our logic, since it states that $\rightarrow$ subsumes logical entailment.

I suppose that there are other good proprieties that Mandelson's definition preserve that aren't preserved by different semantics, at the moment I can't think about something else.

Of course you can avoid such problems if you use different semantics, for instance using semantics that doesn't use sequences at all. I can tell more about such semantics if you wish.

$\endgroup$
  • $\begingroup$ I agree with you about truth, but I'm understanding his (Mendelson) definition of logical consequence differently. I'm reading it as : for every int I, does not exist a sequence s such that s satisfy A and s does not satisfies B.Take F(x) as A and (x)F(x) as B: there is no interpretation for which F(x) is true and (x)F(x) is false (I agree with you) but there are sequences that satisfy F(x) and not (x)F(x) [domain N of natural number, F(x) is "x is even", let s assigns the number 2 to x : Even(2) is true but (x)Even(x) is not]. $\endgroup$ – Mauro ALLEGRANZA Nov 21 '13 at 17:46
  • $\begingroup$ Regarding the book, I refer to the Fourth edition (Chapman & Hall, 1997), but I've studied on the italian transaltion of the 1st ed (1964) and I'm coinvinced that the definition has not been changed sice then. $\endgroup$ – Mauro ALLEGRANZA Nov 21 '13 at 17:52
  • $\begingroup$ @MauroALLEGRANZA Apparently there has been passed long time since I've read Mendelson's book and I've forgotten some of the basic definition. Soon I'll gonna edit the answer. I've to sort some things out, be a little patient :) My apologize for mine mistake. $\endgroup$ – Giorgio Mossa Nov 21 '13 at 18:01
  • $\begingroup$ @MauroALLEGRANZA I've made some changes, let me know if this answer your question :) $\endgroup$ – Giorgio Mossa Nov 21 '13 at 19:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.