Proofs definition

Proofs definition

Titre de la page A proof is a series of lines of the following form where A, B, C are formulas

assume A
therefore B ⇒ C
therefore ¬B
end A
A

A line, starting with the word assume (resp. therefore, end), is called a line assume (resp. therefore, end).

With each line of a proof is associated a context. The initial context is empty.
The line assume A adds the hypothesis A to the context, as the last hypothesis.
The line therefore A ⇒ B , the line therefore ¬ A and the line end A remove the last hypothesis of the context.

We define the conditions so that the formulas appearing on a line of a proof are usable in the rest of the proof to deduce other formulas.

We denote by A_i the formula of line i and by Γ_i the context of line i.
If this line is not an end line, the formula A_i is usable on all the following lines, having a context of which Γ_i is a non-strict prefix.

Let the line i be end A_i
Let Aj be the hypothesis (of line j) removed by this line end.
The fact Aj ⊢ A_i (read A_j results in A_i) is usable on all the following lines, having a context of which Γ_i is a non-strict prefix.

We complete the definition of what a proof is by indicating the conditions that must be satisfied by the therefore lines, the end lines and the lines reduced to a formula.

Let the line be therefore B ⇒ C
C must be usable on the previous line and B must be the hypothesis removed by the line therefore.
This condition is actually the application of the ⇒I rule.
Let the line be therefore ¬B
F (False) must be usable on the previous line and B must be the hypothesis removed by the line therefore.
This condition is actually the application of the ¬I rule.
Either line A or end A must verify one of the following conditions
- be usable in this line
- be the conclusion of one of the rules ∧I, ∨I1, ∨I2, ⇒E, ∧E1, ∧E2, ¬E, ⇔I, ⇔E1, ⇔E2, Efq (ex falso quod libet), Raa (reductio ad absurdum) whose premises are formulas usable in this line
- be the conclusion of the rule ∨E with the B ∨ C formula and the facts B ⊢ A, C ⊢ A usable in this line

A proof of formula A is a proof, in the sense above, of which the context of the last line is empty and whose last line is A. By induction on the length of the proofs, we can show that any line with context Γ satisfies

if the line is therefore A ⇒ B. then Γ ⊢ A ⇒ B
if the line is A. then Γ ⊢ A
if the line is end A. and if B is the hypothesis removed by this line then Γ, B ⊢ A

Hence, if there is a proof of formula A, then ⊢ A.