3

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 $Γ⊢φ$?

yashirq
  • 505
  • 2
    "However, we don't have the definition of formula and axiom yet". What meaning do you give to $\vdash$, then? How can you have the definition of proof without the definition of formula? – Git Gud Dec 17 '16 at 22:37
  • @Git $⊢$ means deduct. "If the proposition $φ$ is the conclusion of an argument (we just require some argument - there could be more than one) with the set of premises $Γ$, then we write $Γ⊢φ$." – yashirq Dec 17 '16 at 23:18
  • 2
    I maintain my question: how can you have a definition of "argument" without the definition of "formula"? – Git Gud Dec 18 '16 at 00:03

1 Answers1

5

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.

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • In the base case, "But if $φ∈Γ$, then obviously $φ$ is implied by $Γ$, so $Γ⊨φ$." I still don't understand how you get $Γ⊨φ$. The definition states that A set of propositions (the "premises") $Γ$ entails a proposition $φ$ (the "conclusion") if for every truth assignment $\mathcal{A}$, if $\mathcal{A}(\varphi) = 1$ when we have $\mathcal{A}(\psi) = 1$ for all $\psi \in \Gamma$. What can we get from $φ$ is implied by $Γ$? – yashirq Dec 18 '16 at 15:55
  • @yashirq I see ''logical entailment" as the same as ''logical implication''. Some texts see "logical implication" as something that holds between two statements, i.e. one statement logically implies another, whereas "logical entailment" would be between a set of sentences and some other sentence, but many texts use the terms interchangeably. But if the difference is important for you, then yes, please use ''entails" instead of "implies". – Bram28 Dec 19 '16 at 09:14