Formulas and proof syntax

The propositional variables are identifiers beginning with a lowercase letter, such as : a, b, p, q.
The logical connectives are :
 . conjunction + disjunction
 => implication <=> equivalence
 - negation
 F false
 [] necessary
 <> possibly
The operator priority are : (high) - [] <> & + => <=> (low).
Between two identical operations, the left operation is prioritary, except for implication.

 A . B . C is (A . B). C A + B + C is (A + B) + C A => B => C is A => (B => C) []A=>B is ([]A)=>B
 A . B + C is (A . B) + C A . B => C + D is (A . B) => (C + D) - A + B is (- A) + B <> A + B is (<> A) + B
To prove a formula A, we try to build a model of - A (the negation of A) by the given rules.
This proof attempt is a tree of branches. The main branch starts with the assumption 1:-A : the state 1 of the model must satisfy the formula -A. The other branches are starting with case i where i is the name of the branch, and are terminating (are closed) with end case i, when there is no model of the branch, because there is, on this branch, an assumption e:F, that is a state e satisfying the formula F always unsatisfiable.
Let's suppose that a branch contains the assumption e : A+B. When applying the disjunction rule to this assumption, we are creating two branches, one with the assumption e:A and the other with the assumption e:B. We do the same with the disjunctive assumptions e:(A =>B), e:-(A.B), e:-(A <=> B)

 examples | rules | syntax | info | home | download Last Modified : 24-Apr-2019