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 BC
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 AB , 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 Ai the formula of line i and by Γi the context of line i.
If this line is not an end line, the formula Ai is usable on all the following lines, having a context of which Γi is a non-strict prefix.

Let the line i be end Ai
Let Aj be the hypothesis (of line j) removed by this line end.
The fact Aj ⊢ Ai (read Aj results in Ai) 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.

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 Hence, if there is a proof of formula A, then ⊢ A.

examples | rules | formulas syntax | proofs definition | info | download | home Last Modified : 23-Feb-2023