# 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: