How to solve propositional logic problems by induction

Question

I'm trying to solve a bunch of problems like this one and every time I get stuck. So I don't need an actual solution but to understand how you solve this kind of problems. I know they're usually solved by induction on the length of $A$ but I can't get the base and step to work. Here's my example:

Show that:

if $B$ and $C$ exist such that $ p\notin sub(B) \cup sub(C) $ and $ \models A \iff (p \land B) \lor C$

then $\models A[p/\bot] \implies A[p/\top] $

For this example I tried to set the base as $A=q$ which is an atom but then I couldn't find anyway to add B and C in the base since with $A = p$ or $q$ we always have $\models A[p/\bot] \implies A[p/\top] $

Can anyone explain what I'm doing wrong and how the problems are solved?

Answer 1

Long comment

"Obviously", induction on $A$ must assume as base case that $A:=p$ (otherwise the subst $A[p/\bot]$ has no effects).

Base : $A := p$. Then $A[p/\bot] = \bot$ and $A[p/\top]= \top$.

Thus we have that : $A[p/\bot] \Rightarrow A[p/\top]$ is $\bot \Rightarrow \top$ and we have :

$\vDash \bot \Rightarrow \top$.

Induction step : we have two sub-cases, for $\lnot$ and a binary connective, e.g. $\lor$.

---

Having said that, I'm not sure that induction is needed here.

We know that $A ⟺ (p ∧ B) ∨ C$.

Thus, $A[p/\bot] ⟺ (\bot ∧ B) ∨ C$, i.e. $A[p/\bot] ⟺ C$.

And : $A[p/\top] ⟺ (\top ∧ B) ∨ C$, i.e. $A[p/\top] ⟺ B ∨C$.

And :

$\vDash C \Rightarrow B \lor C$.