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

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

examples | rules | syntax | info | download | home Last Modified : 18-Jan-2018