- Semantic Tableaux
- : Introduction
- : The Method of Trees
- : Proof by Cases
- : Boolean Tableaux
- : Example 2
- : Bad News
- : More on Semantic Tableaux
- : : Online
- : : Hodges77
- : : Jeffrey91
- : : Smullran95
- : Note
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

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

(End of Case)

Case

(Close Case )

(Close Let )

These proofs lend themself to being expressed using a table

Let

(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 * ( -P+ Q) * -Q.
- = P * -P * -Q + P * Q * -Q.
- = 0 + 0
- = 0

P * (if P then Q) * -Q.

(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

- (let)|- (1): P,
- P * Q * ...*R -(S).
or in graphic form
- P
- Q
- ...
- R
- 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:

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

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

## More on Semantic Tableaux

- 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
- 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.
- Raymond M. Smullyan
- First-Order Logic
- Dover Publications (1995) ISBN: 0486683702 QA9.S57
- Springer-Verlag, 1968

### 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

### Jeffrey91

### Smullran95

## 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. - |- (absorb): (P + Q) * Q = Q.
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

- above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.

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.

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

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

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 ]

For a more rigorous description of the standard notations see