.Open Semantic Tableaux
. Introduction
Semantic tableaux are a way to find out if a set of formulas in the Lower
Predicate Calculus is inconsistent. The process
is quite mechanical.
They may not terminate. They are not always
efficient. They can need a human to supply
creativity, luck, or insight. The semantic tableaux process is
good for theorem proving and solving puzzles.
The process always terminates on formulas in the propositional calculus.
The process can be extended by rules from any theorem, algebra, or calculus
that applies to the situation. Then the mechanical application
of rules can go wrong and fail to prove true statements.
The key point is that to prove that a set of premisses imply
a conclusion ( if P1 and P2 and P3 and .... then Q) we start
exploring the possible cases when P1, P2, P3, and (`not` Q) are
all true. We then show that every case leads to a contradiction.
The idea is to generate a set of cases that cover every possibility hidden
in the initial situation. If all cases are inconsistent then so is the
initial set.
The exploration of cases is mechanical for simple propositions. It is
based on the following expansions.
.Table Formula Case1 Case2 Etc.
.Row P or Q ... P Q ...
.Row not(P or Q ...) not P, not Q, ...
.Row P and Q ... P, Q, ...
.Row not(P and Q ...) not P not Q ...
.Row if P then Q not P Q
.Row not(if P then Q) P, not Q
.Row P iff Q P,Q not P, not Q
.Row not(P iff Q) P,not Q not P, Q
.Row not not P P
.Close.Table
These rules are pretty much equivalent to the normal propositional calculus.
. The Method of Trees
In the standard form
(suitable for board work or pen and pencil) a
tree is generated. Each node has a set of formulas. This process
cries out for a tool to help the user draw the tree and manage
the process.
This idea was worked out by
.Key Lewis Carrol
by 1896 but his work was not published
until 1977 when the drafts for Part II of "Symbolic Logic"
.See [CarrollL77]
were rediscovered, edited. and published.
Here is a graphic cheat sheet summarizing the rules for the
tree based format
.See http://www/dick/maths/semtab.gif
, and here are three examples:
.See http://www/dick/maths/semtaex.jpg
Here
.See ./LPCtaut.gif
is a semantic tableaux that proves a tautology in the predicate calculus
(LPC)|- (for all x (F(x) and G(x))) iff (for all x(F(x)) and for all x(G(x)))
. Proof by Cases
It is also possible to use the semantic tableaux process with my
syntax for "Proof by Cases". This is suitable for presentation
via the web using nested HTML tables or lists.
Here is a proof of `Modus Ponens`. Given `P` and `if P then Q`
show that Q must be true
.Let
(let)|-(1): P,
(let)|-(2): if P then Q,
(let)|-(3):not Q.
(2)|-
.Case not P,
(1)|- $RAA
.Else Q
(3)|- $RAA
.Close.Case
.Close.Let
These proofs lend themself to being expressed using a table
.Let
(let)|-(1): P,
(let)|-(2): if P then Q,
(let)|-(3):not Q.
(2)|-
.Table not P Q
.Row (1)|-$RAA (3)|-$RAA
.Close.Table
.Close.Let
I plan to have more examples of this -- Real soon now.
. Boolean Tableaux
There is another way to use the idea of semantic tableaux that is
suitable for work with a computer or palmtop device.
Instead of drawing a tree, a formula is
manipulated. Copy-and-Paste is very helpful here.
The proces is very like using
.See ./logic_25_Proofs.html#Boolean Algebra
and is essntial "reduction to Disjunctive normal form".
Here is a simple example of this style.
Suppose we wanted to prove `modus ponens`: that if P implies Q
and P is true then Q must also be true. We change this to
checking the inconsistency of `P`, `if P then Q`, and `not Q`.
Here I use The notation of Boolean algebra.
Prove `P` and `(if P then Q)` and `not Q` are inconsistent.
.Consider
P * (`if P then Q`) * -Q.
= P * ( -P+ Q) * -Q.
= P * -P * -Q + P * Q * -Q.
= 0 + 0
= 0
.Close.Consider
In this form of derivation I'd suggest using these
.Key notations for semantic tableaux.
.Table
.Row P,Q,R,... well formed formulas
.Row P[t/x] replace all free variable x by a term t where no free variable in t is bound in P.
.Row n,m numbers like 2,3,4,....
.Row and, or, not, iff, if_then MATHS operators
.Row for all, for some, for no,.... quantifiers.
.Row * Shorthand form for `and` from Boolean Algebra.
.Row + Shorthand form for `or` from Boolean Algebra.
.Row 0 Shorthand for false - closing an alternative
.Close.Table
.Key Start a semantic tableaux
by assuming all the premises
aand the `negation` of the consequence.
To attempt to prove a sequent P,Q,...,R|-S start with
P * Q * ...*R -(S).
or in graphic form
.List
P
Q
...
R
not(S)
.Close.List
If the
.Key semantic tableaux terminates
then either all possibilities are inconsistent
and the result is proved, or a set of counter examples has been generated.
Sometimes the process does not terminate without some luck or
inspiration.
Here is the
.Key semantic tableaux process.
Firstly: use boolean algebra to maintain a disjunctive normal form where
the possibilities are `or`ed together. Use distributive and assorbative
laws for embedded `or`s:
embedded_or::=following,
.Net
|-(absorb): (P + Q) * Q = Q.
|-(resolve): P * (-P+Q) = P*Q.
|-(distribute1): (P+Q) * R = P*R + Q*R.
|-(distribute2): (P+Q)*(R+S) = P*R + Q*R + P*S + Q*S.
.Close.Net
Use commutative laws to reorder the sub-formula.
Second, remove all conjunctions that have a formula `P` and its negation
`-P`. Remove conjunctions with false parts like (not x=x).
Pick a sub-formula and match it to the the table below. Check the
conditions and apply the step. Mostly replace one formula by others.
Sometimes the first formula is kept.
.Table Given Conditions Add Remove it?
.Row -- P - P Yes
.Row -(P+Q) - - P * - Q Yes
.Row -(if P then Q) - P * - Q Yes
.Row if P then Q - - P+ Q Yes
.Row P+Q - $embedded_ors above Yes
.Row P iff Q - (P *Q + - P * - Q) Yes
.Row -(P iff Q) - (P * - Q + - P * Q) Yes
.Row for some x(P) v is some unused variable P[v/x] Yes
.Row - for all x(P) v is some unused variable - P[v/x] Yes
.Row for one x(P) v is some unused variable P[v/x] and for all x( if P then x=v) Yes
.Row for n x(P) n>1, v is some unused variable, m=n-1 P[v/x], for m x( P and x<>v) Yes
.Row for all x(P) t is ANY term P[t/x] No
.Row - for some x(P) t is ANY term - P[t/x] No
.Row for no x(P) t is ANY term - P[t/x] No
.Row - for one x(P) y is free for x in P for no x(P) + for some x,y(x<>y and P and P[y/x] No
.Close.Table
You can split each alternative into a separate analysis if you need.
. Example 2
for some x(F(x)), for all x(if F(x) then G(x)) |- for some x(G(x))
.Consider
for some x(F(x)) * for all x( if F(x) then G(x)) * - for some x(G(x)).
F(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
F(a)* if F(a) then G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
F(a)* (- F(a)+ G(a))* for all x(if F(x) then G(x))* - for some x(G(x)).
F(a)* G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
F(a)* G(a)* not G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
0
.Close.Consider
. Bad News
The above rules allow choices. Choices imply non-determinism, intuition,
experience, luck, etc. all play a part.
In other words you may try a lot of wrong choices before getting
the right way to tackle the problem.
Non-termination comes from not deleting some formulas.
The rules can grow
large expressions. This is a symptom of is a known intractable problem.
.Open More on Semantic Tableaux
. Online
.See http://homepages.cwi.nl/~jacob/st/index.html
(PC limitted interactive tool)
.See http://www.everything2.com/index.pl?node_id=1513374
(brief description and theory)
.See http://www.umsu.de/logik/trees/
(tool inputs a formula checks it for validity and generatest a semantic tableaux)
.Open Hodges77
Wilfrid Hodges
Logic
Penguin Books Middlesex UK & NY NY 1977
=TEXT FORMAL LOGIC Semantic Tableaux TREEs
Describes an easy to learn and use method of proving/disproving results.
Compare with earlier
.Close
.Open Jeffrey91
Richard C Jeffrey (Princeton U)
Formal Logic: Its Scope and Limits
McGraw-Hill Higher Education NY NY 1991 ISBN 0-07-032357-7
=TEXT FORMAL LOGIC semantic Tableaux TREES
Previous edition was in 1960s.
An easy to use way of proving things.
Compare with the earlier $Hodges77 above.
.Close
.Open Smullran95
Raymond M. Smullyan
First-Order Logic
Dover Publications (1995) ISBN: 0486683702 QA9.S57
Springer-Verlag, 1968
.Close
.Close
. Note
Semantic Tableaux proofs tend to be almost mechanical
except for (1) choosing an
expression to substitute for universally quantified variables (2) selecting
the special cases to analyze. This can be quite difficult. Much theoretical
work has been done in the field of Artificial Intelligence to make this as
automatic as possible. It has been shown that in any interesting logic
there can not exist an algorithm that will prove all true statements.
.Close Semantic Tableaux