2

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

Dan Christensen
  • 14,529
  • 3
    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 –  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. – hmakholm left over Monica 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. – hmakholm left over Monica Dec 27 '11 at 21:41
  • 4
    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
  • Thanks, Carl. In my tutorial, I already have a proof of the commutativity of the OR operator using proof by contradiction. I was able turn it around making use of proof by contrapositive. It's a bit forced and takes a few more lines, but it works! – Dan Christensen Dec 28 '11 at 04:46
  • Likewise for the associativity of OR. – Dan Christensen Dec 28 '11 at 05:11
  • @HenningMakholm I certainly don't see why you need to trot out any axioms. Won't proofs in classical propositional calculus calculus under a natural deduction system suffice here? Axioms may help things for many people indeed, but I don't see how they come as logically necessarily. I know the two examples I've provided don't have any axioms. – Doug Spoonwood Dec 30 '11 at 18:45

1 Answers1

-1

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
Doug Spoonwood
  • 11,211
  • 1
    Sorry, I don't understand your notation, Doug. – Dan Christensen Dec 30 '11 at 04:20
  • It's Polish notation, a prefixing scheme: http://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