Next:
Contents
Contents
Introduction to natural deduction
Daniel Clemente Laboreo
August 2004 (reviewed at May 2005)
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
.
1
.
1
Truth introduction
7
.
1
.
2
False elimination
7
.
2
Rules about quantifiers
7
.
2
.
1
What's that
7
.
2
.
2
Existential introduction
7
.
2
.
3
Existential elimination
7
.
2
.
4
Universal introduction
7
.
2
.
5
Universal elimination
7
.
2
.
6
Examples
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
.
3
.
1
Brute force
8
.
3
.
2
Refutation theorem
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
About this document ...
Daniel Clemente Laboreo 2005-05-17
