Is it possible to prove a contradiction with natural deduction by negating the formula

logicnatural-deductionpredicate-logic

I want to show that a formula is a contradiction. Assume a very simple one like

$$ 1. \exists x Px \land \neg\exists x Px $$

Now negate the formula to

$$ 2. \neg(\exists x Px \land \neg\exists x Px) $$
$$ 3. \neg\exists x Px \lor \exists x Px $$
That is a tautology so one can follow that the negation of 2. is a contradiction so 1. is a contradiction as well. Is that possible for every contradiction?
Or is a semantic proof necessary to show contradictions (as for contingent formular)?

Best Answer

  1. is a contradiction because it is of the form $\varphi \land \neg \varphi$

  2. is a tautology, because it is of the form $\varphi \lor \neg \varphi$

Therefore, 2. is a tautology as well, since it is equivalent to 3

So all of that makes sense: If 1 is a contradiction, then 2, being the negation of 1, is a tautology.

Now, as far as formally demonstrating these things: in many systems pointing out that a statement is of the form $\varphi \land \neg \varphi$ is sufficient to prove that it is a contradiction. And in many systems, showing that a statement is of the form $\varphi \lor \neg \varphi$ is sufficient to show it is a tautology.

Some systems, however, have an explicit contradiction symbol, $\bot$, and so to show that a statement is a contradiction you either show that it is equivalent to $\bot$, or derive $\bot$ from it (any statement from which a contradiciton can be derived is a contradiction itself).

In some systems you can go straight to $\bot$ from $\varphi \land \neg \varphi$ as either a rule of equivalence or rule as inference, but in other systems you derive $\bot$ from a statement $\varphi$ and a second statement $\neg \varphi$

Likewise, some systems have an explicit symbol for the tautology: $\top$, and they will typically have an equivalence rule to go from $\varphi \lor \neg \varphi$ to $\top$. Unlike the $\bot$, though, formal systems typically do not have an inference rule to derive $\top$, because a tautology logically follows from any statement, and this the fact that a tautology can be inferred from some statement says nothing about that statement.

Instead, many systems will demonstrate a statement to be a tautology by demonstrating that its negation is a contradiction. This is the proof by contradiction proof technique of course.

Now, you actually do something very unusual: you negate statement 1, and show that the result is equivalent to a tautology. And yes, while that indeed show that the original statement is a contradiction, there would be few systems that would demonstrate statements to be a contradiction in this manner. As explained above, this would only work if you with equivalence rules only, and most such systems have a much more direct way to demonstrate a statement to be a contradiction.

Indeed, if you are talking about natural deduction, then you are probably talking about a system of inference, and remember that if you end up inferring a tautology from the negation of some statement, then that tells us nothing about the nature of that negation, and thus nothing about the original statement either.

So no, you typically do not demonstrate a statement to be a tautology using natural deduction by negating it and seeing what happens. Or, put differently, while a proof by contradiction demonstrates a statement to be a tautology by showing that the negation of that statement leads to a contradiction, in natural deduction there is no parallel proof technique that shows a statement to be a contradiction by showing that its negation leads to a tautology.

Related Question