Tree calculus

from Wikipedia, the free encyclopedia

Tree calculi or tableau calculi , after its inventor and Beth -Kalküle called, are Widerlegungskalküle of logic . Refutation calculi are logical calculi that do not directly prove the validity of an argument, but instead provide the proof by refuting its invalidity. Another well-known refutation calculus is the resolution calculus .

The name “tree calculus” comes from the fact that a tree structure is created when deriving from a Beth calculus. This statement is a description, not a definition, because not every calculus that creates tree structures is also called a tree calculus. The resulting tree structures are also called Beth-Tableaux or Beth-Tableaus (French or German plural of Beth-Tableau).

In this article, a tree calculus for classical propositional logic is presented: A calculus for classical logic because the first tree calculus historically was classical; a calculus for propositional logic because this is the simplest and forms the basis of many other tree calculi, initially for the tree calculus of predicate logic . Tableau calculi are also available for many non-classical logical systems.

Basics

For classical logics, a semantic final term can be grasped very intuitively: An argument is valid if and only if the conclusion is also true among all interpretations under which all premises are true; shorter, more concise and with Leibniz : only truth follows from truth . Thus an argument is invalid if and only if there is at least one interpretation under which all premises are true, but under which the conclusion is false.

According to classical semantics, if a sentence is false, then its negative is true. Instead of saying that an argument is invalid if and only if there is at least one interpretation under which all premises are true, but under which the conclusion is false , one can just as well say the following: An argument is invalid if and only if it gives at least one interpretation under which all premises are true and under which the negation of the conclusion is also true .

Shorter: An argument , where the set of premises is the conclusion and the metalogical sign indicates the validity of the argument, is invalid if and only if there is at least one interpretation I , under which every sentence is true, but under which is false . Since, according to the semantics of negation, I ( ) = F if and only if I ( ) = W, is invalid if and only if I not only makes every sentence off , but also true, i.e. if I makes every sentence from the set true. An argument is therefore invalid if and only if the set is satisfiable, and vice versa, if the set is unsatisfiable or inconsistent.

Beth calculi try to refute the validity of an argument (also therefore “refutation calculus”) by formalizing the process of specifying a model for . Thus the formation rules of the calculus are purely syntactic and can be applied without any semantic ulterior motives, but because they ultimately formalize the counter-model construction, they are highly semantically motivated.

Construct models

The first step is to consider how to create a model for the individual types of statements. The aim is a propositional language be based on the logical operators are as follows: ( negation ) ( Conjunction ) ( disjunction , non-exclusive Or) and (conditional or substantive implication ). The negation denies the truth value of a sentence; a conjunction connects two sentences to a new sentence which is true if and only if both connected sentences are true and which is false otherwise; the disjunction joins two sentences into a new sentence which is false only if both connected sentences are false and which is true otherwise; and the conditional connects two sentences to a new sentence that is false only if the left of the two connected sentences is true and the right is false.

  • The easiest way to construct a model for an atomic sentence is to set and have a suitable model.
  • It is not much more difficult to construct a model for (in which case any complex compound sentence can be used instead of ): You set and have a suitable model.
  • A model for is also quickly generated: one sets and includes the conjunction in a model for by defining the truth .
  • There are three possibilities to create a model for : (a) You bet , (b) You bet , or (c) You do both.
  • The construction of a model for also allows several possibilities: (a) One sets ; (b) you bet ; (c) you do both.

The transformation rules of the Beth calculus are modeled according to these possibilities.

A first look at the calculation

In the exit, all sentences of the set are written down one below the other. This is shown using the example of the argument . With this argument is and is , so is . is here so . One thus writes:

a.
b.
c.

The order is irrelevant, since it is a set of sentences. This set of sentences is seen as a node - a node - of a tree, hence the frame. The attempt is now made to build a model for this set of sentences, i.e. to make every sentence of this set true. In the case of sentences b. and c. is that simple: In order for an interpretation to be a model for b. is, must be. So that a model for c. is, must be. This gives you initial information about .

It is more difficult with sentence a. This sentence is a conditional, so there are three ways to satisfy it: (a) , (b) and (c) both. Write down possibilities (a) and (b) as children of the tree; Option (c) does not need to be written down separately because it means the combination of (a) and (b). To indicate that theorem a. has dealt with it, it is crossed out, checked off or removed entirely, depending on your taste. The following tree is created in this step:

a.
b.
c.
d.
e.

This reads node or sentence d. as follows: "In addition to the requirements my ancestors have not crossed out , I make the requirement that ." (This requirement resulted from the treatment of sentence a.)

Node or set e. reads as follows: "In addition to the requirements that my ancestors have not crossed out , I make the requirement that ."

It can be seen that node d. poses an unsatisfiable requirement : The node requires that is based on theorem d . At the same time, however, he inherits from his father on the basis of sentence b. the requirement that is. Since these two demands are not compatible, the left attempt to form a model for failed early on. Mark this in the tree in a suitable way:

a.
b.
c.
d.
e.

One reads this as: "The left branch is closed".

The right branch is still open and the hope of finding a model has not yet been lost. When is a model for ? Based on the truth value definitions of the conjunction if and only if . You write that down and delete the sentence e:

a.
b.
c.
d.
e.
f.
G.

Now node e reads. as follows: "In addition to the requirements my father places on, I require that and that ."

The path that goes from the root to node e. only contains atomic sentences. The requirements for a model can therefore be read off directly: For such a model to be, it must meet the following requirements:

  1. from b. I (P) = W
  2. from c. I (Q) = F
  3. from f. I (Q) = W
  4. from g. I (R) = W

Claims b. and G. are unproblematic, but demands c. and f. contradict each other and therefore cannot be fulfilled. So it was not possible to create a model for in the second branch of the tree . The branch is also closed, its end node is marked:

a.
b.
c.
d.
e.
f.
G.

Since there are no more branches and all existing branches are closed, the whole tree is called closed. The closeness of the tree indicates that it is impossible to make a model for . That, in turn, means that it is impossible to refute the argument . Thus the argument is proven.

Final rules of the propositional tree calculus

And rule
If a statement occurs in a node , it is crossed out and the node is expanded to include the two sentences and .
Or rule
If a statement occurs in a node , it is crossed out and the node has two children. One of the two children contains the sentence , the other child contains the sentence .
Arrow rule
If a statement occurs in a node , it is crossed out and the node has two children. One of the two children contains the sentence , the other child contains the sentence .
Not-and-rule
If a statement occurs in a node , it is crossed out and the node has two children. One of the two children contains the sentence , the other child contains the sentence .
The no-or rule
If a statement occurs in a node , it is crossed out and the node is expanded by the sentence and the sentence .
No arrow rule
If a statement occurs in a node , it is crossed out and the node is expanded by the sentence and the sentence .

These rules must be applied to the tree until all non-atomic sentences are crossed out. The resulting tree is called closed if and only if every direct path from the root to an end node contains at least one contradiction. A path contains a contradiction if and only if it contains both a proposition and its negation .

Is the tree not closed, i.e. H. If there is at least one direct path from the root to an end node without contradictions, then the tree is called open.

The argument for which the tree was formed is valid if and only if the tree is closed. The argument is invalid if and only if the tree is open. In this case - but that is a semantic interpretation - a counterexample for the argument can be read from each open branch.

The Beth calculus for classical propositional logic, as established here, is correct and complete , and it is a decision-making procedure for the classical propositional validity of arguments.

literature

  • Evert Willem Beth: Semantic Entailment and Formal Derivability . In: Mededelingen of the Koninklijke Nederlandse Akademie van Wetenschappen , Volume 18, Number 13, Amsterdam 1955, pp. 309–342, abridged, translated reprint in Berka / Kreiser 1986, pp. 262 ff.
    First systematic elaboration of the tree calculus
  • Evert Willem Beth: A topological proof of the theorem of Löwenheim-Skolem-Gödel . In: Indag. Math. , 13, pp. 346-344
    First thoughts in the direction of a tree calculus
  • Karel Berka , Lothar Kreiser: Logic texts. Annotated selection on the history of modern logic . Academy, Berlin 1986
    Abridged, translated reprint by Beth 1955 from p. 262

Secondary literature

  • Ansgar Beckermann : Introduction to Logic . 3. Edition. De Gruyter, Berlin 2010, ISBN 978-3-11-025434-1 .
    In this introduction, a tree calculus for propositional and predicate logic is developed from scratch and at a level that beginners can understand.
  • Wilfrid Hodges : Logic . 2nd Edition. Penguin, London 2001, ISBN 0-14-100314-6 (English)
    A very simple introductory book to formal logic in which a tree calculus is slowly developed. For those new to formal logic who are proficient in English, it would be an excellent choice.
  • Wolfgang Bible: Deduction. Automation of logic (= Computer Science Manual 6.2). Oldenbourg, Munich 1992, ISBN 3-486-20785-7
    The title is representative of works whose objective lies within computer science and in automated proof, an objective which is predominantly worked with rebuttal calculations. A prerequisite for the fruitful study of such titles is prior knowledge of formal logic and programming.

Web links