1

For a natural deduction proof of $\Gamma_1 \vdash B_1$, I want to know whether a subproof $\Gamma_2 \vdash B_2$ in the proof is provable without uisng natural deduction (this subproof could be anywhere in the proof).

My feeling is that ($\Gamma_2 \vdash B_2$ is provable) $\implies$ ($\Gamma_1, \Gamma_2 \vDash B_2$ is true). Is this correct?

But I'm not sure whether it works both ways i.e.

($\Gamma_2 \vdash B_2$ is provable) $\iff$ ($\Gamma_1, \Gamma_2 \vDash B_2$ is true).

Can someone help?

(A formula $\Gamma \vDash B$ could be checked using a truth table etc.)

mmgro27
  • 201
  • $\Gamma \vdash B$ means that "$B$ is derivable from $\Gamma$ in a certain proof system". This means that it is not correct to insert into a Nat Ded proof a "foreign object", like e.g. a truth-table checking. – Mauro ALLEGRANZA Aug 25 '15 at 16:41

1 Answers1

2

Since you were mentioning truth tables, I asssume you're talking about classical propositional logic, and one of the standard natural deduction calculi for it.

Then, your first conjecture that

($\Gamma_2 \vdash B_2$ is provable) $\Rightarrow$ ($\Gamma_1, \Gamma_2 \models B_2$ is true)

is correct. By soundness of natural deduction, we have

($\Gamma_2 \vdash B_2$ is provable) $\Rightarrow$ ($\Gamma_2 \models B_2$ is true)

By monotonicity of classical logic, we have

($\Gamma_2 \models B_2$ is true) $\Rightarrow$ ($\Gamma_1, \Gamma_2 \models B_2$ is true)

Application of transitivity yields the desired result.

Your second conjecture that

($\Gamma_1, \Gamma_2 \models B_2$ is true) $\Rightarrow$ ($\Gamma_2 \vdash B_2$ is provable)

is not correct, however. Here is a counterexample: Set $\Gamma_1 = \{P\}$, $\Gamma_2 = \{P \rightarrow Q\}$ and $B_2 = Q$. Then $\Gamma_1, \Gamma_2 \models B_2$ is true (check with a truth table, if you like). But $\Gamma_2 \models B_2$ is not true, so by soundness again $\Gamma_2 \vdash B_2$ is also not provable.

Nonetheless (if that should be what you've meant),

($\Gamma_2 \models B_2$ is true) $\Rightarrow$ ($\Gamma_2 \vdash B_2$ is provable)

is correct, because natural deduction is also complete.