How to prove soundness of propositional logic

5.6k Views Asked by At

For any proposition $φ$ and any set of propositions $Γ$, if $Γ⊢φ$, then $Γ⊨φ$.

I find the same question here.

However, we don't have the definition of formula and axiom yet.

This is the hint given on the slide: The proof of the Soundness Theorem we will go through will proceed by induction on the length, $0≤k∈N$, of the shortest deduction of $φ$ from $Γ$, not including the premise lines.

For the base case, $k=0$, then we have $⊢φ$ automatically. But I still don't understand how we can derive $Γ⊨φ$. Actually what information we can get from $Γ⊢φ$?

1

There are 1 best solutions below

2
On

Assuming your proof system does not use any subproofs, a proof is a series of steps where each step is the application of some formal inference rules as applied to any of the earlier statements of this proof or the premises.

So basically, they want you to show by induction on the number of lines $n$, that any statement $\varphi$ that is derived on line $n$ from a set of premises $\Gamma$ does indeed logically follow from $\Gamma$. Thus: if there exists a proof of $\varphi$ given premises $\Gamma$ at all (we write this as $\Gamma \vdash \varphi$), then there exists a proof that derives $\varphi$ in $n$ steps for some $n$ (I am not sure why they want you to consider the 'shortest'proof, since it really works for any proof, but fine, it is of course also true that the shortest proof takes some number of steps). But whatever that number of steps is, you will show that in any formal derivation, each line is a logical result of the premises, and hence $\Gamma \vDash \varphi$ (again, assuming there are no subproofs to consider here, for if you have those, then the proof will get more complicated).

OK, but how do you do this proof by induction?

The base case is where $n=0$, which effectively says that you have no steps taken. This would be when $\varphi$ is one of the premises in $\Gamma$, so no steps are needed, but we can still say that $\Gamma \vdash \varphi$. But if $\varphi \in \Gamma$, then obviously $\varphi$ is implied by $\Gamma$, so $\Gamma \vDash \varphi$. This concludes the base case.

For the inductive step, you consider some number $n$, and assume that for any proof $\Gamma \vdash \varphi$ consisting of $n$ lines, we have that $\Gamma \vDash \varphi$. So now let's consider a proof $\Gamma \vdash \varphi$ that takes $n + 1$ steps.

OK, at this point you need to consider ech possible inference rule you have, since any of those could be the one used to infer $\varphi$ on line $n+1$ from earlier statements in the proof or the premises themselves. Since it is true that for any earlier statement we have that $\Gamma \vdash \psi$, we have by inductive hypothesis (since they all occur before line $n+1$) that it is also true that $\Gamma \vDash \psi$. And given that, you should then show that $\Gamma \vDash \varphi$ given the nature of the rule.

Now, I don't know what specific rules you have, but suppose you have the following rule:

$P\rightarrow Q$

$P$

$\therefore Q$ (Modus Ponens)

So first you point out that if this rule was used to derive $\varphi$ on line $n+1$ of the proof, then it must have been derived from two earlier statements of the form $\psi\rightarrow\varphi$ and $\psi$, and since they occur before line $n+1$, we can by inductive hypothesis say that $\Gamma\vDash\psi \to\varphi$ and that $\Gamma\vDash\psi$. OK, but from the definition of $\vDash$, we know that $\Gamma\vDash\psi\to\varphi$ if and only if $\Gamma\not\vDash\psi$ or $\Gamma\vDash\varphi$. But since we have $\Gamma \vDash\psi$, that means that $\Gamma\vdash\varphi$ as desired.

This process you will hav to repeat for every inference rule you have, where every time you use formal semantics, i.e. the definition of $\vDash$. And once you're done with that, your inductive step, and hence your whole inductive proof will be done.