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

  • 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 
  • 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