Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Does anyone have some simple examples of theorems in FOL that are most easily proven using proof by contrapostive? Every example that I have found so far involves aspects number theory. Any help would be appreciated.


share|cite|improve this question
My closest guess: FLower Of Life (FOL). Sorry just joking, may be you could save the trouble by writing First-Order Logic in full for FOL – user21436 Dec 27 '11 at 20:51
Could you be a bit more precise about why the number-theoretic examples don't satisfy you? Doing logic in the empty theory (or "pure predicate calculus") is a bit anemic -- it's a useful boundary case for theoretical purposes, but not exactly a source of intuitively meaningful examples. For that you have to work in some theory, and formal number theory is a well-known and well-understood source of pedagogical examples. – Henning Makholm Dec 27 '11 at 21:15
Henning, I am working on a tutorial on the methods of formal proof and want to keep the examples as simple as possible. I don't want to have to trot out Peano's Axioms and the like if I can avoid it at this stage. – Dan Christensen Dec 27 '11 at 21:33
You have to trot out some axioms; otherwise there will be no intuitive content to your examples and nobody who needs examples in the first place will be able to internalize them anyway. The axioms don't need to be Peano's ones; you're free to create a toy theory that has the assume-we-have-already-proved-this as axioms. – Henning Makholm Dec 27 '11 at 21:41
The way to get a result whose best proof is by contrapositive is to take the contrapositive of a result that is best proved directly. E.g. start with "Any number divisible by 4 is even" to get "Any number that is not even is not divisible by 4". I use this trick very often when teaching proofs classes. – Carl Mummert Dec 27 '11 at 21:44

Taking Carl's tip, say you want to prove that CpCqp. In one natural deduction system, with proof by contrapositive as a derived rule of inference you can then proceed as follows:

1 |   NCqp hypothesis
2 ||  p hypothesis
3 ||| q hypothesis
4 ||| p 2 repetition
5 ||  Cqp 3-4 conditional introduction
6 ||  KCqpNCqp 1, 5 conjunction introduction
7 |   Np 2-6 negation introduction
8     CNCqpNp 1-7  conditional introduction
9     CpCqp 8 proof by contrapositive

An even shorter example goes:

1 | p hypothesis
2   Cpp 1-1 conditional introduction
3   CNpNp 2 proof by contrapositive
share|cite|improve this answer
Sorry, I don't understand your notation, Doug. – Dan Christensen Dec 30 '11 at 4:20
It's Polish notation, a prefixing scheme: Logical operators get placed before their operands. In short, (p@q) in infix notation becomes @pq in a prefixing scheme, where @ indicates any (binary) operator (unary operators usually get placed to the left in infix, so nothing changes here). C means the material conditional, N negation, and K conjunction. Thus, KCqpNCqp in infix can go ((q->p)^~(q->p)) or equivalently ((qCp)KN(qCp)). CpCqp goes (p->(q->p)) or equivalently (pC(qCp)). – Doug Spoonwood Dec 30 '11 at 18:41

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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