transitivity of subformula relation - proof

Question

Problem: prove that the relation "is a subformula of" is transitive for propositional formulas.

let $\phi \in Sub(\psi)$ and $\psi \in Sub(\chi)$ prove that $\phi \in Sub(\chi)$.

my proof:

if $\phi \in Sub(\psi)$ then $\phi=\psi_i$ with $i\leq n$ (with $\psi_i$ a step of the formation sequence of $\psi$ and $\psi_n=\psi$)

if $\psi \in Sub(\chi)$ then $\psi=\chi_j$ with $j\leq m$ (with $\psi_j$ a step of the formation sequence of $\chi$ and $\psi_m=\psi$)

Then must be $\psi_i=\chi_k$ with $k\leq j$

So $\phi=\chi_k$ and $\phi \in Sub(\chi)$ $\square$

I was wandering whether my proof was correct and looking for a different proof which uses the recursive definition of subformula of a formula.

Answer 1

As always in these cases, we can apply induction on the "complexity" of the formula, i.e. on the number of occurrences of connectives, which amounts to follow the formation tree.

See Definition 2.1.7 [page 12] for the definition of the set $Sub(\varphi)$ of subformulas of $\varphi$.

i) Basis : If $\varphi$ is atomic, then $Sub(\varphi)$ contains only $\varphi$; but the only subformula of $\varphi$ is $\varphi$ itself. Thus the subformulas of subformulas of $\varphi$ are subformulas of $\varphi$, and the property holds.

ii) Induction step : We have to consider the basic connectives : $\land$, $\lor$ and $\lnot$.

For $\land$, consider $\varphi := \varphi_1 \land \varphi_2$ :

$Sub(\varphi_1 \land \varphi_2) = Sub(\varphi_1) \cup Sub(\varphi_2) \cup \{ \varphi_1 \land \varphi_2 \}$

and we assume that the property holds for $\varphi_1$ and $\varphi_2$.

This means that if $\sigma \in Sub(\theta)$ and $\theta \in Sub(\varphi_i)$, then $\sigma \in Sub(\varphi_i)$.

Thus, if $\sigma \in Sub(\theta)$ and $\theta \in Sub(\varphi)$, we have two cases :

a) $\theta$ is $\varphi$ itself, and we are done; otherwise :

b) $\theta$ is a subformula of $\varphi_i$, in which case the induction hypotheses apply.

Answer 2

By Induction Principle(Theorem 1.1.3 on van Dalen's Logic and Structure) you can prove that $ \psi \in Sub(\phi) \implies Sub(\psi) \subset Sub(\phi) $, using the recursive definition of $ Sub $ function. The transitivity of $ \subset $ on sets do the rest.

Let $ \square $ be any connective and $ \neg $ the not symbol.

Let $ P(\phi) \iff \forall \psi \in Sub(\phi)( Sub(\psi) \subset Sub(\phi) ) $.

(i) If $ \phi $ is atomic then $ \psi \in Sub(\phi)= \{\phi\} \iff \psi = \phi \iff Sub(\psi) = Sub(\phi) $.

(ii) Let $ P(\phi_{1}) $ and $ P(\phi_{2}) $, and let $ \psi \in Sub((\phi_{1}\square\phi_{2})) = Sub(\phi_{1})\cup Sub(\phi_{2}) \cup \{(\phi_{1}\square\phi_{2})\} $, then $ \psi $ must be in one of these 3 sets.

If he's in the first by $ P(\phi_{1}) $ we have $ Sub(\psi) \subset Sub(\phi_{1}) \subset Sub((\phi_{1}\square\phi_{2})) $, if in the second we have the same, if in the third we have equality of the sets. We have then $ P((\phi_{1}\square\phi_{2})) $.

(iii) Let $ P(\phi) $, then if $ \psi \in Sub((\neg \phi)) = Sub(\phi)\cup \{ (\neg \phi)\} $, $ \psi $ must be in one of these 2 sets, again implying that $ Sub(\psi) \subset Sub((\neg\phi)) $, giving $ P((\neg \phi)) $.

By (i), (ii) and (iii) we have $ \forall \phi \in PROP \,\,P(\phi) $.