Enderton's sentential "tautological implication" subsumed by Enderton's first-order "logical implication"?

Question

(My question is clearly marked at the bottom. I don't think I'm asking the same question as this math.stackexchange.com question.)

I'm working in the framework of Enderton's A Mathemtical Introduction To Logic, second edition.

In chapter 1 on sentential logic, a set $\Sigma$ of well-formed formulas is said to tautologically imply a wff $\phi$, written $$\Sigma \models \phi$$ when every truth assignment satisfying everything in $\Sigma$ also satisfies $\phi$.

In chapter 2 on first-order logic, a set $\Gamma$ of wffs is said to logically imply a wff $\phi$, written $$\Gamma\models \phi$$ when every structure (interpretation) $\mathfrak{A}$ and every substitution map $s$ from variables $\{v_n\}$ into the universe $|\mathfrak{A}|$ satisfying everything in $\Gamma$ also satisfies $\phi$.

Write $\models _{\mathfrak{A}} \phi [s]$ when a structure/substitution pair $(\mathfrak{A}, s)$ satisfies a wff $\phi$.

After defining logical implication, he says that the double turnstile notation "$\Sigma \models \phi$" will be used going forward only for logical implication.

This leads me to guess that his sentential logic tautological implication is somehow subsumed by his first-order logical implication, but I am trying to get a more concrete understanding.

A brief google indicates that sentential logic can be contained in first-order logic:

• Propositional logic statement = First order logic statement
• https://web.engr.oregonstate.edu/~afern/classes/cs532/notes/fo-ss.pdf

I am trying to get a better understanding of how S.L. implication and F.O.L. implication might relate, but I didn't easily find anything laying this out explicitly.

Question:
Is it correct that Enderton's sentential logic embeds into Enderton's first-order logic using the following first-order language and structure?

First-order language:

• No equality, no constants, no functions, and one single $1$-ary predicate symbol $P$.

Structure/interpretation $\mathfrak{A}$:

• Universe $|\mathfrak{A}|$ any set with at least two elements.
• Relation $P^{\mathfrak{A}}$ for $P$ any non-empty subset of $|\mathfrak{A}|$ whose compliment is also non-empty.

Relationship between S.L. and F.O.L.:

• Define a mapping $f$ obtaining a F.O.L. expression from a S.L. expression by replacing every S.L. sentence symbol $A_n$ with the F.O.L. term $Pv_n$.
• S.L. wffs become F.O.L. wffs.
• $\phi$ is a tautology in S.L. if and only if $\models _{\mathfrak{A}} f(\phi) [s]$ for every substitution $s$ (equivalently $\mathfrak{A}$ is a "model" of the fully universally quantified version of $f(\phi)$.)

Thanks for any help.

Answer 1

Usually classical first-order logic is defined so that classical propositional logic is a literal sublanguage of it. In particular, it is the sublanguage where all relation symbols are nullary (and omitting quantifiers which are essentially useless at that point). This makes it impossible for there to be any place to put terms. Semantically, it then doesn't matter what the domain is as there is no way to refer to any of its elements. The tautological implication relation is the logical implication relation restricted to this sublanguage.

Nevertheless, what you describe works insofar as the theorem in your last bullet holds, but it is kind of a weird way to go about it. You can improve and simplify it by making it a first-order theory rather than constraining the interpretation in an ad-hoc manner. You could add the axioms $\exists x.P(x)$ and $\exists x.\neg P(x)$ which would ensure the domain contains at least two elements and the interpretation of $P$ is non-empty and has a non-empty complement. It may be a bit clearer to just explicitly add two constants $\mathsf{tt}$ and $\mathsf{ff}$ and the axioms $P(\mathsf{tt})$, $\neg P(\mathsf{ff})$, and $\mathsf{tt}\neq\mathsf{ff}$.

There are many other ways to map propositional formulas to FOL formulas such that the original formulas are tautologies if and only if the resulting formula is valid. One notable one is to simply formalize the notion of a Boolean algebra. Alternatively, if you went the route you did because Enderton doesn't allow for nullary relation symbols (or maybe it just didn't occur to you), you could do essentially the same thing I suggested but producing distinct unary predicates for each propositional variable (sentence symbol). Then, to get effectively nullary predicates you could map the propositional variables to formulas like $\forall x.P_n(x)$ (or instead $\exists x.P_n(x)$ or $P_n(\mathsf{c})$ after adding a constant $\mathsf{c}$). This is clearly a bit of a hack to make up for not directly having nullary relation symbols.