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 insatisfiable.
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 : 20-Nov-2019