# Example of a logic where a proof by contradiction does not imply a direct proof.

It makes sense that for any logic that has axioms, an inference rule and a statement you want to prove P, you can take a direct proof of P and turn it into a proof by contradiction (you have already proven P and assumed not P. A cont reduction!) Are there any examples of (nontrivial) logics where the converse of that is not true? Given a proof by contradiction that proves p, you cannot construct a direct proof that proves p?

By direct proof I mean only generating statements from the the axioms the inference rule and the children of that rule.

Thanks

-

The question isn't quite clear to me, so I'll talk about a couple of interpretations of the question and hopefully the answers will be helpful.

Intuitionistic logic is basically classical logic without excluded middle ($P \vee \neg P$). We can recover the usual classical logic from intuitionistic logic either by adding excluded middle, or by adding the principle of double negation elimination, $\neg \neg P \rightarrow P$. If we define a direct proof to be one which is valid in intuitionistic logic, then the question becomes: is intuitionistic logic any different to classical logic?

The answer to that question is yes. It turns out that excluded middle is not provable in intuitionistic logic.

Alternatively, by direct proof you might mean a cut free proof. This isn't really related to proof by contradiction as such, but might be closer to what you mean. The cut rule is one of the rules of the sequent calculus, and states that from $\Gamma \vdash \Delta,A$ and $A, \Sigma \vdash \Pi$, we can deduce $\Gamma,\Sigma \vdash \Delta,\Pi$. Notice that $A$ appears in the antecedent but not in the consequent. The process of converting a proof to a cut-free proof is known as cut elimination.

In this case, the answer to the question is that cut elimination can usually be performed for logic on its own (this is certainly true for both classical logic and intuitionistic logic) but not in general when axioms are added to the system. In $PA$ (and if I recall correctly even in $HA$, the intuitionistic counterpart to $PA$) it is possible to perform cut elimination but only by switching to infinitary proofs. There are theorems in $PA$ that have no (finite) cut-free proof.

-

The resolution of Russell's paradox is probably the most famous proof by contradiction in set theory:

Suppose $\exists x \forall y (y\in x\leftrightarrow y\notin y)$

Let $r$ (the Russell set) be such that $\forall y (y\in r\leftrightarrow y\notin y)$ by existential specification.

Applying this definition of $r$ to $r$ itself, we obtain the contradiction $r\in r\leftrightarrow r\notin r$.

We conclude $\neg\exists x \forall y (y\in x\leftrightarrow y\notin y)$.

I don't see how this can be turned into a direct proof. (Change "$\in$" to any other logical predicate if your set theory doesn't allow self-membership. The logic of the proof would still work.)

-