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