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