Here's how they proved it in the source I was reading:
Assume both sentences $S$ and $\lnot S$ are derivable from the axioms (where $\lnot S$ is the negation of $S$).
We notice that $p\rightarrow (\lnot p \rightarrow q)$ is a theorem of the system.
Now we apply substitution rule and substitute $S$ for $p$:
$S\rightarrow (\lnot S\rightarrow q)$
After rule of detachment (since $S$ is a theorem):
$\lnot S\rightarrow q$
After rule of detachment (since $\lnot S$ is also a theorem):
$q$
So we conclude that any sentence $q$ must be derivable. Now we notice that our axioms and transformation rules only allow us to produce tautologies, so only tautologies are derivable. So since every sentence $q$ is not derivable, we have a contradiction.
Have I understood the proof correctly? But I think there is a more obvious way of proving it:
We first observe that only tautologies are derivable by our system. Now, by the definition of negation operation, both $S$ and $\lnot S$ can't be tautologies. So at least one of them has to be non-derivable.
This proof sounds simple. I might be missing something. Anything wrong with this proof?
Best Answer
Yes, both arguments are correct and clearly your second argument is more concise and elegant, if you already know a bit of logic.
By the way, your source is an excellent article to popularize logic $(*)$. I guess the main aim of that article is to write not the shortest proof of consistency but the "most informative" one for a reader that is not an expert. More precisely, in their proof of consistency of propositional logic, the authors introduce many interesting and relevant concepts, for instance:
This is, I guess, the reason why the authors preferred to show a longer path to conclude that propositional logic is consistent.
$(*)$ It is a short version of Nagel and Newman's book "Gödel's Proof", which I highly recommend to read if you are interested in logic, its motivations and its most famous result, Gödel's theorems.