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. First, you can simply conclude an hypothesis:
If an hypothesis of the form not phi leads to a contradiction, you can derive phi and remove that hypothesis.
Of course, you can add hypothesis without destroying what you already proved:
Now, if you suppose p and derive q, you can irrevocably prove p -> q.
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
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:
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: