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.

Formula	Case1	Case2	Etc.
P or Q ...	P	Q	...
not(P or Q ...)	not P, not Q, ...
P and Q ...	P, Q, ...
not(P and Q ...)	not P	not Q	...
if P then Q	not P	Q
not(if P then Q)	P, not Q
P iff Q	P,Q	not P, not Q
not(P iff Q)	P,not Q	not P, Q
not not P	P

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 Lewis Carrol by 1896 but his work was not published until 1977 when the drafts for Part II of "Symbolic Logic" [CarrollL77] were rediscovered, edited. and published.

Here is a graphic cheat sheet summarizing the rules for the tree based format [ semtab.gif ] , and here are three examples: [ semtaex.jpg ] Here [ LPCtaut.gif ] is a semantic tableaux that proves a tautology in the predicate calculus


1. (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

   
   
   1. (let)|- (1): P,
      
   2. (let)|- (2): if P then Q,
      
   3. (let)|- (3): not Q.
      
   4. (2)|-
      Case
      1. not P,
         
      2. (1)|-RAA
      
      (End of Case)
      Case
      1. Q
         
      2. (3)|-RAA
      
      (Close Case )
      
   
   (Close Let )
   

   These proofs lend themself to being expressed using a table
   Let

   
   
   1. (let)|- (1): P,
      
   2. (let)|- (2): if P then Q,
      
   3. (let)|- (3): not Q.
      
   4. (2)|-

      not P	Q
      (1)|-RAA	(3)|-RAA

   
   (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 [ 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.
   1. = P * ( -P+ Q) * -Q.
   2. = P * -P * -Q + P * Q * -Q.
   3. = 0 + 0
   4. = 0
   
   (Close Consider )
   

   In this form of derivation I'd suggest using these notations for semantic tableaux.

   P,Q,R,...	well formed formulas
   P[t/x]	replace all free variable x by a term t where no free variable in t is bound in P.
   n,m	numbers like 2,3,4,....
   and, or, not, iff, if_then	MATHS operators
   for all, for some, for no,....	quantifiers.
   *	Shorthand form for and from Boolean Algebra.
   +	Shorthand form for or from Boolean Algebra.
   0	Shorthand for false - closing an alternative

   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

2. P * Q * ...*R -(S). or in graphic form
   
   1. P
   2. Q
   3. ...
   4. R
   5. not(S)
   
   

   If the 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 semantic tableaux process. Firstly: use boolean algebra to maintain a disjunctive normal form where the possibilities are ored together. Use distributive and assorbative laws for embedded ors:

3. embedded_or::=following,
   Net
   
   
   1. |- (absorb): (P + Q) * Q = Q.
      
   2. |- (resolve): P * (-P+Q) = P*Q.
      
   3. |- (distribute1): (P+Q) * R = P*R + Q*R.
      
   4. |- (distribute2): (P+Q)*(R+S) = P*R + Q*R + P*S + Q*S.

   
   (End of 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.

   Given	Conditions	Add	Remove it?
   -- P	-	P	Yes
   -(P+Q)	-	- P * - Q	Yes
   -(if P then Q)	-	P * - Q	Yes
   if P then Q	-	- P+ Q	Yes
   P+Q	-	embedded_ors above	Yes
   P iff Q	-	(P *Q + - P * - Q)	Yes
   -(P iff Q)	-	(P * - Q + - P * Q)	Yes
   for some x(P)	v is some unused variable	P[v/x]	Yes
   - for all x(P)	v is some unused variable	- P[v/x]	Yes
   for one x(P)	v is some unused variable	P[v/x] and for all x( if P then x=v)	Yes
   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
   for all x(P)	t is ANY term	P[t/x]	No
   - for some x(P)	t is ANY term	- P[t/x]	No
   for no x(P)	t is ANY term	- P[t/x]	No
   - 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

   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
   1. for some x(F(x)) * for all x( if F(x) then G(x)) * - for some x(G(x)).
   2. F(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
   3. F(a)* if F(a) then G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
   4. F(a)* (- F(a)+ G(a))* for all x(if F(x) then G(x))* - for some x(G(x)).
   5. F(a)* G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
   6. F(a)* G(a)* not G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
   7. 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.

   More on Semantic Tableaux

   Online

   [ index.html ] (PC limitted interactive tool)

   [ index.pl?node_id=1513374 ] (brief description and theory)

   [ http://www.umsu.de/logik/trees/ ] (tool inputs a formula checks it for validity and generatest a semantic tableaux)

   Hodges77

   1. Wilfrid Hodges
   2. Logic
   3. Penguin Books Middlesex UK & NY NY 1977
   4. =TEXT FORMAL LOGIC Semantic Tableaux TREEs
   5. Describes an easy to learn and use method of proving/disproving results.
   6. Compare with earlier

   Jeffrey91

   1. Richard C Jeffrey (Princeton U)
   2. Formal Logic: Its Scope and Limits
   3. McGraw-Hill Higher Education NY NY 1991 ISBN 0-07-032357-7
   4. =TEXT FORMAL LOGIC semantic Tableaux TREES
   5. Previous edition was in 1960s.
   6. An easy to use way of proving things.
   7. Compare with the earlier Hodges77 above.

   Smullran95

   1. Raymond M. Smullyan
   2. First-Order Logic
   3. Dover Publications (1995) ISBN: 0486683702 QA9.S57
   4. Springer-Verlag, 1968

   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.

. . . . . . . . . ( end of section Semantic Tableaux) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see