Proof by Contrapostive: Any simple examples in First-Order Logic?

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.

Dan

-
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

-
Sorry, I don't understand your notation, Doug. –  Dan Christensen Dec 30 '11 at 4:20
It's Polish notation, a prefixing scheme: en.wikipedia.org/wiki/Polish_notation. 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