.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