I am reading A Friendly Introduction to Mathematical Logic by Christopher Leary and Lars Kristiansen. Let $\beta$ be a $\mathcal{L}$-formula in first order language $\mathcal{L}$. In the first line of Page 52, the authors claim that if $\beta_P$, a formula in propositional logic, is a tautology then $\beta$ is valid.

$\beta_P$ is obtained from $\beta$ in the following fashion (which is written is Page 51):

  1. Find all subformulas of $\beta$ of the form $\forall x\alpha$ that are not in the scope of another quantifier. Replace them with propositional variables in a systematic fashion. This means that if $\forall yQ(y,c)$ appears twice in $\beta$, it is replaced by same letter both times, and distinct subformulas are replaced with distinct letters.

  2. Find all atomic formulas that remain, and replace them systematically with new propositional variables.

  3. At this point, $\beta$ will have been replaced with a propositional formula $\beta_{P}$.

I was trying to prove this by induction on the structure of formula $\beta$ but I got stuck in the base case. Here's my attempt: Let $\mathfrak{U}$ be any $\mathcal{L}$-structure and $s$ be any variable assignment function to $\mathfrak{U}$. Suppose that $\beta\equiv=t_1t_2$ (written in Polish notation) where $t_1 , t_2$ are terms of the language $\mathcal{L}$. Then $\beta_P$ is $A$ where $A$ is a propositional variable. Let's assume that $\beta _P$ is a tautology. We need to prove that $\beta$ is valid, i.e., $\mathfrak{U}\models \beta [s]$.

Here's my question: Since $\beta_P$ is a tautology, are not allowed to make the substitution $A=F$ because if we do, then $\beta_P$ would not longer be a tautology. How do we remedy this situation?


2 Answers 2


We need a preliminary Lemma in order to define a "procedure" that assigns to every interpretation $\mathfrak A$ and variable assignment function $s$ a boolean valuation $v$ such that:

(1) $\mathfrak A,s \vDash \beta \text { iff } v(\beta_{\text P})= \text T$.

The idea is to consider the rule for producing $\beta_{\text P}$ from $\beta$ above and let $P_i$ the propositional variable corresponding to subformula $Q_i$, i.e. an atom or subformula $\forall x \alpha$.

We define:

$v(P_i)= \text T \text { when } \mathfrak A,s \vDash Q_i, \text { and } v(P_i)= \text F$ otherwise.

And then we use the clauses for the satisfaction relation [Def.1.7.4, page 29] to prove (1) by induction, considering that we have three "atomic" cases: (1) $=t_1t_2$, (2) $Rt_1 \ldots t_n$ and (3) $∀xα$, and only two compound cases: (4) $¬ \varphi$ and $\varphi ∨ \psi$.

Having proved the Lemma, we can use it to prove the main result.

Let $\beta$ a formula and let $\mathfrak A$ and $s$ whatever.

We compute the corresponding $v$. But $\beta_{\text P}$ is a tautology; thus: $v(\beta_{\text P})=\text T$, that implies: $\mathfrak A,s \vDash \beta$.


As I see it, the problem is that the final $\beta_P$ might be a tautology while its parts you obtain in your induction might not be. You are right that the partial $\beta_P$ you get from e.g. $t_1 = t_2$ would be $A$ and thus not a tautology, but the complete $\beta_P$ might be $A \lor \neg A$, which is a tautology.

  • $\begingroup$ It is not an example. I was trying to prove it by induction on the structure of the formula. So, I begin with atomic formulas. But apparently, my attempt of proof does not work for atomic formulas. $\endgroup$
    – ash
    Commented Feb 26, 2021 at 10:45
  • $\begingroup$ Oh sorry, I misread apparently. I'll edit the answer to reflect this. $\endgroup$ Commented Feb 26, 2021 at 10:50
  • $\begingroup$ What do you mean by "partial" and "complete" $\beta _P$? $\endgroup$
    – ash
    Commented Feb 26, 2021 at 11:06
  • $\begingroup$ As I can see it, you consider the atoms of your formula like e.g. $t_1 = t_2$ and then construct the corresponding propositional formula $\gamma$. This corresponding formula $\gamma$ I call "partial" because your original FO formula $\beta$ might also have other atoms and hence $\beta_P$ can be a tautology even though $\gamma$ isn't. $\endgroup$ Commented Feb 26, 2021 at 11:32

You must log in to answer this question.

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