Proofs definition

proof-definition

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

assume A.
therefore BC.
end A.
A.

A line, starting with the word assume (resp. therefore, end), is called a line assume (resp. therefore, end). In a proof, it is forbidden to follow an end line with a therefore line.

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. 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 AjAi (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

  1. if the line is therefore AB. then Γ ⊢ AB.
  2. if the line is A. then Γ ⊢ A
  3. if the line is end A. and if B is the hypothesis removed by this line then Γ, BA

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