3

I know this may be a question not suitable to ask here or is a duplicate, but I'm just wondering if all proofs by contrapositives can be rephrased into a direct proof, without using the fact that they are logically equivalent?

Are there instances when a proof by contrapositive is not too hard, but direct proof is way more involved or literally impossible to do?

nabu1227
  • 879

2 Answers2

2

I assume below that by "proof by contrapositive" you mean the principle

You can prove $A\rightarrow B$ by showing that $\lnot B$ implies $\lnot A$.

or in other words

From $\lnot B\rightarrow \lnot A$ you may infer $A\rightarrow B$.

[EDIT: The above lines were added following Rob Arthan's comments]

Proof by contrapositive is a reasoning principle which is valid in classical logic, but not in intuitionistic logic. So if you have a proof by contrapositive of a theorem which is not intuitionistically valid (e.g., $\lnot\lnot A\rightarrow A$), you cannot really get rid of the contrapositive reasoning: At best (depending on the precise formulation of your proof system) you can replace it by another equivalent "non-constructive" principle such as double negation elimination or proof by excluded middle.

So how about classical theorems which are also intuitionistically valid? Here you can remove all non-constructive reasoning steps in proofs, but this might lead to much larger proofs. A nice and simple example of this is blowup is mentioned in the Introduction of:

M. Baaz, A. Leitsch and G. Reis, "A Note on the Complexity of Classical and Intuitionistic Proofs," 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, Kyoto, Japan, 2015, pp. 657-666, doi: 10.1109/LICS.2015.66.

For an intuitionistically valid theorem $A$, simply consider the formula $B:=A\lor\lnot A$. An intuitionistic proof of $B$ will essentially go through the proof of $A$ and the conclude $A\lor \lnot A$ in the last step, and so it can be as large as intuitionistic proofs can get (there is no computable upper bound on the size of intuitionistic proof of a (first-order) theorem $A$ relative to the size of $A$)! On the other hand, $B$ has a trivial classical proof as it is an instance of the law of excluded middle.

Timo
  • 1,059
  • You are not using the term contrapositive correctly. You are mixing it up with the law of double negation elimination or its equivalent, the law of the excluded middle. I agree that it is common to infer $\phi \to \psi$ from $\lnot \psi \to \lnot \phi$, but that combines the intuitionistically valid result $(\lnot \psi \to \lnot \phi) \to (\lnot\lnot \phi \to \lnot\lnot \psi)$ with double negation elimination. – Rob Arthan Feb 24 '21 at 13:41
  • @RobArthan I am not quite sure what you mean. Also contrapositive reasoning is equivalent to double negation: By contraposition, $\lnot\lnot A\rightarrow A$ is provable from $\lnot A\rightarrow \lnot\lnot\lnot A$, and the latter is an intuitionistic validity. – Timo Feb 24 '21 at 13:51
  • Contraposition is $(\phi \to \psi) \to (\lnot \psi \to \lnot\phi)$. $\lnot\lnot A \to A$ is not provable from $\lnot A \to \lnot\lnot\lnot A$ by contraposition alone. – Rob Arthan Feb 24 '21 at 14:01
  • Ok, then this is the source of our disagreement. For me the inference rule is "from $\lnot B\rightarrow \lnot A$ infer $A\rightarrow B$", i.e. the other direction (of course both are valid in classical logic). This is also the rule as described in this wikipedia article. Maybe LHC2012 can tell us what (s)he meant? – Timo Feb 24 '21 at 14:19
  • It does look like what I (and others) consider to be poor terminology is now so widespread, that we will have to agree to differ. – Rob Arthan Feb 24 '21 at 15:03
  • @RobArthan: I added a note of clarification at the top of my post. – Timo Feb 24 '21 at 15:45
  • Thanks! That makes it nice and clear. – Rob Arthan Feb 24 '21 at 16:03
0

Some existence theorems go into that direction: First one assumes that a solution does not exist, then use a contradiction argument using some deep (and non-constructive) theorem, like for instance Brouwer fixed point theorem or Hahn-Banach theorem.

daw
  • 49,113
  • 2
  • 38
  • 76
  • By how you phrased it "First assume a solution does not exist, then prove existence..." I thought that sound like a direct proof/proof by contrapositive phrased as a proof by contradiction. Could you clarify on what you mean? Thanks! – nabu1227 Feb 24 '21 at 07:01
  • edited :)...... – daw Feb 24 '21 at 07:22