Suppose I would like to proof modus tollens, i.e. $P\ \to Q,\ \lnot Q\ \vdash\lnot P$, based on Gentzen-style natural deduction for classical logic. Using rules of inference for NK as given in Katalin Bimbo's Proof Theory: Sequent Calculi and Related Formalism (p.270), I made the derivation below:
$\dfrac{\begin{matrix}\dfrac{\left(P\rightarrow Q\right)\land\lnot Q}{\lnot Q}\ \land\! E_1&\dfrac{\begin{matrix}\dfrac{\left(P\rightarrow Q\right)\land\lnot Q}{P\rightarrow Q}\land\! E_2&\begin{matrix}\\P\\\end{matrix}\\\end{matrix}}{Q}\ \to\!E\\\end{matrix}}{\dfrac{\bot}{\lnot P}\bot E}\bot I$
I have a few questions:
- Is my NK proof above correct? In its linear variant, I have seen some proofs that include $\neg Q \to \neg P$ as the last step after $\neg P$ (using $\to I$). Is that last step necessary? I mean, did we not already derive $\neg P$ (which is the right side of $\vdash$) from $P \to Q, \neg Q$?
- As I understand it, in this proof the only assumption I make is $P$ (to the left of $\to E$), whereas $P \to Q \wedge\neg Q$ is not an assumption but a premise (keeping in mind that they appear before $\vdash$ in the proposition, and so must be taken as given, not an arbitrary assumption). Is my reasoning correct?
- How to differentiate between theorem and true proposition in NK proof system? Semantically speaking, a theorem is a proposition that is true in all interpretations, whereas a true proposition need not be true on all interpretations. In truth table, this is easy to show. But in NK, I don't see anything like that. Is theorem a proposition which can be proved without assumption (only using premise), whereas true proposition (not a theorem) can only be proved with assumption? Is this related to the place of $\vdash$ in the proposition?
- Lastly, is NK proof for $P\ \to Q,\ \lnot Q\ \vdash\lnot P$ is the same as NK proof for $\vdash P\ \to Q \wedge \lnot Q\ \to \lnot P$ ? I mean, what is the difference between $\vdash$ and $\to$, on the one hand, and the difference between comma (,) and $\wedge$? Is it not just the difference between object-language and metalanguage that we must aware at all times yet, in the actual labour of proof, have no impact whatsoever in the way we operates on those symbols (both truth functionally/semantically and proof theoretically/syntactically)? I know that we must be mindful of tiny differences between levels of language so that we don't succumb to the dreadful self-referential paradoxes, such as Russel's or Gödel sentence. But, really, we don't stumble into Gödel sentence everyday, do we? So, back to the point, what is the actual, operational, difference between using $\vdash$ and $\to$ and between using comma (,) and $\wedge$ in natural deduction (or any other proof systems) other than healthy precautionary attitude of anticipating over something that happens once in a blue moon?
Best Answer
Somewhat.
$$\begin{split}&\dfrac{\dfrac{\dfrac{[P]^1\quad P\to Q}{Q}{\to\!\mathsf E}\quad\lower{1.5ex}{\lnot Q}}{\bot}{\lnot\mathsf E}}{\lnot P}{\lnot\mathsf I^1}\\[2ex]\hdashline\blacksquare &\quad P\to Q, \lnot Q\vdash \lnot P\end{split}$$
Technically $P$, $P\to Q$, and $\lnot Q$ are all assumptions. Premises are undischarged assumptions. But yes, $P$ is the only assumption you need to raise and discharge.
A theorem is a tautology: an unconditionally true statement. Since the classical logic natural deduction system (NK) is a complete, therefore every theorem can be derived unconditionally: that is, if $\phi$ is a theorem, then $\vdash \phi$. Conversely, since NK is sound, therefore if $\phi$ is unconditionally derivable, then $\phi$ is a theorem.
No, they are considered different claims, and they have distinct proof structures, although one may be inferred from the other.