0
$\begingroup$

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

$\endgroup$
5
  • 4
    $\begingroup$ No, $\vdash$ is not a typo. Enderton means deductive consequence. $\endgroup$ Sep 11, 2020 at 15:40
  • $\begingroup$ (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$? $\endgroup$
    – Tim
    Sep 11, 2020 at 16:24
  • $\begingroup$ @Tim Re: $(2)$, yes of course by soundness/completeness. $\endgroup$ Sep 11, 2020 at 17:36
  • $\begingroup$ (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.) $\endgroup$ Sep 11, 2020 at 17:41
  • $\begingroup$ See also the post Logical implication vs Tautological implication $\endgroup$ Sep 12, 2020 at 17:07

2 Answers 2

3
$\begingroup$

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

$\endgroup$
9
  • $\begingroup$ 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. $\endgroup$
    – Tim
    Sep 11, 2020 at 18:05
  • $\begingroup$ @Tim Why do you think that? Has Enderton defined the phrase "logically implies" as referring to $\models$? $\endgroup$ Sep 11, 2020 at 18:27
  • $\begingroup$ @NoahSchweber Yes. $\endgroup$ Sep 11, 2020 at 18:39
  • $\begingroup$ p88 of 2ed 2001 $\endgroup$
    – Tim
    Sep 11, 2020 at 18:41
  • $\begingroup$ @Tim Ah, refrigerator blindness on my part! $\endgroup$ Sep 11, 2020 at 18:42
1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ This is based on the same error that my original answer was: Enderton uses "logically implies" to refer to $\models$, not $\vdash$. $\endgroup$ Sep 11, 2020 at 19:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .