https://en.wikipedia.org/wiki/Proof_by_contradiction#Relationship_with_other_proof_techniques says

Proof by contradiction (general): assume $ \lnot P$ and derive a contradiction. This corresponds, in the framework of propositional logic, to the equivalence

$${\displaystyle {\text{p}}\equiv {\text{p}}\vee \bot \equiv \lnot \left(\lnot {\text{p}}\right)\vee \bot \equiv \lnot {\text{p}}\to \bot },$$ where $\bot$ is a logical contradiction or a false statement (a statement which truth value is false).

In the case where the statement to be proven is an implication ${\displaystyle A\rightarrow B}$, ...:

Proof by contradiction: assume $A$ and ${\displaystyle \lnot B}$ and derive a contradiction. This corresponds to the equivalences

$${\displaystyle {\text{p}}\to {\text{q}}\equiv \lnot {\text{p}}\vee {\text{q}}\equiv \lnot \left({\text{p}}\wedge \lnot {\text{q}}\right)\equiv \lnot \left({\text{p}}\wedge \lnot {\text{q}}\right)\vee \bot \equiv \left({\text{p}}\wedge \lnot {\text{q}}\right)\to \bot }.$$

In some mathematical logic books, e.g. Ebbinghaus' Mathematical Logic, $\bot$ is not defined. How can the two logical equivalence instances for proof by contradiction be represented?


  • $\begingroup$ If satisfied by one of the answer below, please accept it $\endgroup$ – Mauro ALLEGRANZA Sep 9 '20 at 14:19

When $\bot$ is not defined, then a contradiction is just that … some statement and its negation.

So, we just do likewise. Either derive $p\equiv\neg p\to(q\wedge\neg q)$ or... $$\begin{align}p &\equiv p\vee( q\wedge\neg q)\\&\equiv (p\vee q)\wedge(p\vee\neg q)\\&\equiv (\neg\neg p\vee q)\wedge(\neg\neg p\vee\neg q)\\&\equiv (\neg p\to q)\wedge(\neg p\to\neg q)\end{align}$$


In Ebbinghaus' system we have a contradiction in a proof when a pair of formulas: $ψ,¬ψ$ is derivable (see page 61).

Using the derived rule for conjunction (Ex.3.6. (b), page 65), from a contradictory pair we can derive the "usual" contradiction: $ψ ∧ ¬ψ$.

Ebbinghaus' system has no $\bot$ symbol and thus the Contradiction Rule (2.4, page 63) is expressed through two sequents deriving a contradictory pair of formulas.

Having said that, there are not two different "forms" of proof by contradiction.

The first one described in your post amounts to:

$\dfrac {\Gamma \ \lnot \varphi \vdash \bot}{\Gamma \ \ \ \ \ \vdash \varphi}$,

which is Ebbinghaus' Contradiction Rule written using $\bot$ symbol.

The second one is exactly the same:

$\dfrac {\Gamma \ \varphi \ \lnot \psi \vdash \bot}{\Gamma \ \varphi \ \ \ \ \ \ \vdash \psi}$.

Nothing has changed. We can use the so-called Deduction Theorem (aka: Conditional Proof rule, Ex.3.6. (c), page 66) to conclude with:

$\Gamma \vdash \varphi \to \psi$.

The result exploits the equivalence between the two formulas: $\lnot (\varphi \land \lnot \psi)$ and $(\varphi \to \psi)$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.