2
$\begingroup$

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

  • 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 FOL2011-12-27
  • 0
    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.2011-12-27
  • 0
    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.2011-12-27
  • 0
    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.2011-12-27
  • 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.2011-12-27
  • 0
    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!2011-12-28
  • 0
    Likewise for the associativity of OR.2011-12-28
  • 0
    @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.2011-12-30

1 Answers 1

-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
  • 1
    Sorry, I don't understand your notation, Doug.2011-12-30
  • 0
    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)).2011-12-30