Contents

• 1 Before starting...
  • 1.1 Who am I
  • 1.2 Why do I write this
  • 1.3 Whom is it addressed to
  • 1.4 License
  
  
• 2 Basic concepts
  • 2.1 Formalization
  • 2.2 Used symbols
  • 2.3 Precedence of operators
  
  
• 3 Natural deduction
  • 3.1 What it is for
  • 3.2 What it is not for
  • 3.3 Functioning
  • 3.4 Notation
  
  
• 4 The derivation rules
  • 4.1 Iteration
  • 4.2 Conjunction introduction
  • 4.3 Conjunction elimination
  • 4.4 Implication introduction
  • 4.5 Implication elimination
  • 4.6 Disjunction introduction
  • 4.7 Disjunction elimination
  • 4.8 Negation introduction
  • 4.9 Negation elimination
  • 4.10 No more rules
  
  
• 5 Explained exercises
  • 5.1 A very simple one.
  • 5.2 A bit more complicated.
  • 5.3 Starting to make suppositions.
  • 5.4 Using iteration.
  • 5.5 Reduction to the absurd.
  • 5.6 With subdemonstrations.
  • 5.7 One with proof by cases.
  • 5.8 One to think.
  • 5.9 Left side empty.
  • 5.10 Suppose the contrary.
  • 5.11 This one seems easy.
  • 5.12 An interesting one.
  • 5.13 I had this one in an exam.
  • 5.14 A ``short'' one.
  
  
• 6 Wrong things
  • 6.1 Introduction and elimination of ``what it would be nice to have''
  • 6.2 Iterate something from a non attainable subdemonstration
  • 6.3 Misplace parenthesis
  • 6.4 Finish inside a subdemonstration
  • 6.5 Skip steps
  
  
• 7 Making it harder
  • 7.1 Rules about truth and false
  • 7.2 Rules about quantifiers
  • 7.3 Derived rules
  
  
• 8 Extra
  • 8.1 Why is it called natural deduction?
  • 8.2 Is the solution unique?
  • 8.3 Other ways to prove validity
  • 8.4 How to prove invalidity
  • 8.5 Create your own exercises
  • 8.6 Programs which do natural deduction
  
  
• 9 Examples, lots of examples
  • 9.1
  • 9.2
  • 9.3
  • 9.4
  • 9.5
  • 9.6
  • 9.7
  • 9.8
  • 9.9
  • 9.10
  • 9.11
  • 9.12
  • 9.13
  • 9.14
  • 9.15
  • 9.16
  • 9.17
  • 9.18
  • 9.19
  • 9.20
  • 9.21
  • 9.22
  • 9.23
  • 9.24
  • 9.25
  • 9.26