Formulas and proof syntax

Logical connectives
. conjunction
+ disjunction
=> implication
<=> equivalence
- negation
F false
[] necessary
<> possibly
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 est ([]A)=>B
A . B + C est (A . B) + C
A . B => C + D est (A . B) => (C + D)
- A + B est (- A) + B
<> A + B est (<> A) + B
A proof starting with the line case c followed by the assumption e : A and terminated by the corresponding end case c is a proof of e : - A

examples | rules | syntax | info | home| download Last Modified : 17-Dec-2021