Should $\vdash$ in Theorem 24B In Enderton's logic book be $\models$ instead?

Question

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

Answer 1

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

Answer 2

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.