Formulas and proofs syntax

Formulas and proofs syntax

Logical connectives

& conjunction

+ disjunction

=> implication

<=> equivalence

- negation

F faux

A proof is a sequence of proof lines.
A proof line is either a formula, the word assume followed by a formula, or the word therefore followed by a formula.
This formula is the conclusion of the proof line. Each proof line is terminated by a period.
The word assume introduces an hypothesis.
The word therefore removed the last introduced hypothesis.
A formula is usable on a proof line, if it is the conclusion of a previous proof line whose hypotheses have not been removed.

Proof Line Effects Conditions

assume A. adds A to the end of the list of the hypothesis of the previous proof line no conditions

therefore A => B. removes the last introduced hypothesis. This proof line is the application of the rule =>I The removed hypothesis must be A.
The formula B must be usable on the previous proof line.
A. no effects The formula A must be a copy of a formula usable on this proof line or must be obtained by application of a rule to formulas usable on this line.

Operator priority : (high) - & + => <=> (low)
Between two identical operations, the left operation is prioritary, except for implication

Proof Line	Effects	Conditions
`assume` A.	adds A to the end of the list of the hypothesis of the previous proof line	no conditions
`therefore` A => B.	removes the last introduced hypothesis. This proof line is the application of the rule `=>I`	The removed hypothesis must be A. The formula B must be usable on the previous proof line.
A.	no effects	The formula A must be a copy of a formula usable on this proof line or must be obtained by application of a rule to formulas usable on this line.

A & B & C est (A & B)& C

A + B + C est (A + B) + C

A => B => C est A => (B => C)

A & B + C est (A & B) + C

A & B => C + D est (A & B) => (C + D)

- A + B est (- A) + B