Pravda - natural deduction
On this page, you will learn natural deduction. In natural deduction, you manipulate sequents, e.g. p, q |- p and q, composed of:
- On the left-hand side, there is a list of hypothesis, e.g.
p, q.
- The symbol
|- separates the left-hand side and the right-hand side.
- On the right-hand side, there is a formula: the conclusion that is proven, e.g.
p and q.
The left-hand side can be empty, e.g. |- p or not p. In that case, it means that the conclusion p or not p without any hypothesis.
In propositional logic
Examples of direct applications of rules
First, let us explore the rules in propositional logic.
Dealing with hypotheses
First, you can simply conclude an hypothesis:
Of course, you can add hypothesis without destroying what you already proved:
Absurd
If an hypothesis of the form not phi leads to a contradiction, you can derive phi and remove that hypothesis.
Implication
Now, if you suppose p and derive q, you can irrevocably prove p -> q.
If you have already proven p and you have p -> q, you have a proof for q:
Or
And
Not
Examples of proofs
Show that we can deduce p -> r from (p or q) -> r.
Show the contraposition rule : deduce p |- q -> r from p |- not r -> not q.
Show that we can prove not (p or q) -> not p and not q.
First-order logic
Examples of direct applications of rules
Existential quantifier
If you proved exists x P(x) and from P(x) you prove p, you deduce p only from the other hypothesis, as long as they do not depend on x.
Be careful, when the hypothesis depend on the involved variable x you cannot apply the elimination of exists as shown below:
Universal quantifier
If you proved P(x) and the hypothesis do not depend on x, then you deduce forall x P(x). That rule is called the introduction of forall.
Be careful, when the hypothesis depend on the involved variable x you cannot apply the introduction of forall as shown below:
Examples of proofs
Show the law of excluded middle : |- P(x) or not P(x)
Show that we can prove forall x (P(x) and Q(x)) from (forall x P(x)) and (forall x Q(x)).
Give a proof of not exists x P(x) -> forall x not P(x).
Funny example
Let us take a non-empty bar. Give a proof in natural deduction of the following sentence : "there exists a person such that, if he/she drinks then everybody drinks". You may use the formula P(x) to formalize the fact that the person denoted by x drinks.
Sandbox
In the following box, you can write any proof in natural deduction you want: