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

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 A ⇒ B. 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 A_j be the hypothesis (of line j) removed by this line end. The fact A_j ⊢ 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 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.

• Either line A. or end A. must verify one of the following conditions
  1. be usable in this line
  2. be the conclusion of one of the rules ∧I, ∨I1, ∨I2, ⇒E, ∧E1, ∧E2, Efq (ex falso quod libet), Raa (reductio ad absurdum) whose premises are formulas usable in this line
  3. 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

1. if the line is therefore A ⇒ B. then Γ ⊢ A ⇒ B.
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 Γ, B ⊢ A

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