0

SECTION 2.4 A Deductive Calculus In Enderton's A Mathematical Introduction to Logic divides the set of axioms into several groups. The first group is called "tautologies" on p114, which are obtained from tautologies in Sentential Logic, by treating the primary formulas in FOL as sentence symbols in SL.

Theorem 24B on p115 says logical implication in FOL and tautological implication in SL are equivalent. Is $\vdash$ in Theorem 24B intended to mean logical implication in FOL? Should $\vdash$ be $\models$ instead? (Given that this is from a section for a proof system, and soundness and completeness haven't been introduced, it is possible that $\vdash$ is not a typo.)

enter image description here

Tim
  • 47,382
  • 4
    No, $\vdash$ is not a typo. Enderton means deductive consequence. – spaceisdarkgreen Sep 11 '20 at 15:40
  • (1) Is the theorem related to the remark above it? (2) To improve the remark, is it true that $\Gamma \models \phi$, iff $\Gamma \cup \Lambda$ tautologically implies $\phi$? – Tim Sep 11 '20 at 16:24
  • @Tim Re: $(2)$, yes of course by soundness/completeness. – Noah Schweber Sep 11 '20 at 17:36
  • (2) Yes it's true, since by the completeness theorem, $\Gamma\models \phi$ iff $\Gamma\vdash \phi.$ (1) I'm not that familiar with this book but I would guess 24b is a stepping stone that will be used in the proof of the completeness theorem. The remark is related in the sense of your (2), but won't be fleshed out till the completeness theorem is proved. (But note the remark could also say that $\forall x P(x)$ deductively implies $P(c)$ whereas it doesn't tautologically imply.) – spaceisdarkgreen Sep 11 '20 at 17:41
  • See also the post Logical implication vs Tautological implication – Mauro ALLEGRANZA Sep 12 '20 at 17:07

2 Answers2

3

As spaceisdarkgreen says, there is no typo here: Enderton means "$\vdash$" in the theorem, and "logical entailment" ($\models$) in the remark. The remark observes that there is a gap between $\models$ and tautological implication. The theorem on the other hand says that we can "reduce" $\vdash$ to tautological implication: if we want to know whether $\Gamma\vdash\varphi$, it's enough to know whether $\Gamma\cup\Lambda$ tautologically implies $\varphi$.

Despite this, the remark and theorem are connected, even if somewhat loosely. The point is that that theorem should be thought of as partially filling in the gap exhibited in the remark by showing how tautological entailment can be connected to a particular relation on first-order sentences which we know is going to wind up being the same as $\models$ (see the introduction to Section $2.4$). So while we'll have to wait for the soundness/completeness theorem to be able to prove the equivalence we really want, namely that $\Gamma\models\varphi$ iff $\Gamma\cup\Lambda$ tautologically implies $\varphi$, the theorem following the remark is still relevant.

It's true that if we forget about the context in which we've introduced $\vdash$, the connection becomes much more tenuous (although it's still there: both the remark and theorem focus on the extent to which propositional logic can be applied to first-order logic in some sense). However, that context is there for a reason: all of this is much harder to motivate if we don't begin with the explicit goal of giving a "concrete" description of $\models$.

Noah Schweber
  • 245,398
  • Thanks. "the remark preceding the theorem observes that there is a gap between ⊢ and tautological implication. " The remark before the theorem says "If tautologically implies ϕ , then it follows that also logically implies ϕ . " I think that "logically implies" is not $\vdash$ but $\models$. I suspect that remark is unrelated to the theorem after it. – Tim Sep 11 '20 at 18:05
  • @Tim Why do you think that? Has Enderton defined the phrase "logically implies" as referring to $\models$? – Noah Schweber Sep 11 '20 at 18:27
  • @NoahSchweber Yes. – spaceisdarkgreen Sep 11 '20 at 18:39
  • p88 of 2ed 2001 – Tim Sep 11 '20 at 18:41
  • @Tim Ah, refrigerator blindness on my part! – Noah Schweber Sep 11 '20 at 18:42
  • @Tim Nonetheless, I don't think that makes them unrelated per se. Note that we could replace the world 'logically' with 'deductively' in the remark and it would be correct, and pertinent. – spaceisdarkgreen Sep 11 '20 at 18:43
  • @spaceisdarkgreen I don't think the remark wants to mention $\vdash$ in place of $\models$ – Tim Sep 11 '20 at 18:44
  • @Tim I've edited to address this. They are still related. – Noah Schweber Sep 11 '20 at 18:46
  • @Tim Well, I don't know what the remark wants. And it was certainly intentional to use $\models$ there. But my point is if the remark wanted to, it could have used $\vdash.$ After all, deductive and logical implication are (nontrivially) the same thing. – spaceisdarkgreen Sep 11 '20 at 18:47
1

Long comment

It is not a typo.

Having said that, the Theorem is a sort of "preliminary" result, that will be superseded later by the Soundness and Completeness Th for FOL (Sect.2.5, page 131-on).

The key fact (stated in previous Enderton's comment) is that:

If $\Gamma$ tautologically implies $\varphi$, then it follows that $\Gamma$ also logically implies $\varphi$. But the converse fails.

Thus, with insight, having that

for FOL $\vdash \text { iff } \vDash$ holds,

and having shown that $\vDash$ and $\vDash_{\text { TAUT}}$ are not equivalent, we can conclude that also $\vdash$ and $\vDash_{\text { TAUT}}$ are not equivalent.

IMO the $(\Rightarrow)$ part of the theorem is not very interesting: the proof technique (by induction) is basically the same used for Soundness.

The interesting part is the $(\Leftarrow)$ part: the fact that considering the set $\Delta$ of logical axioms as "additional assumption" is enough to have derivability is proved in a quite simple way (about 10 lines), compared to the complex proof needed for Completeness (5 full pages).

A second interesting feature of the Theorem (IMO) is that it shows the benefit of Enderton's proof system, compared to "traditional" FOL proof systems, like that of Mendelson, using two rules of inference: $\text { Modus Ponens }$ and $\text { Gen }$ (this approach to FOL is due to Frege (1879) and Whitehead & Russell's Pricipia Mathematica (1910)).

Enderton's proof system uses more quantifier axioms, and in this way it can avoid $\text { Gen }$ rule: this fact has the big benefit of simplifying the Deduction Theorem.

In this context, the Th can be read as showing that the additional quantifier axioms are enough to replace the misssing $\text { Gen }$ rule.

Mauro ALLEGRANZA
  • 94,169
  • This is based on the same error that my original answer was: Enderton uses "logically implies" to refer to $\models$, not $\vdash$. – Noah Schweber Sep 11 '20 at 19:29