# Tableaux for first order logic

The **Tableaux** is a logical calculation tool that allows checking the validity of a conclusion from a series of premises. In the previous article I explained briefly the fundamentals of Tableaux for predicate logic. In this article I will extend the program to the **first-order logic**, which has much more expressive capacity than **predicate logic**, although this makes also automatic calculation more difficult.

In this link you can download the project FOTableaux with the source code and the executable program written in **CSharp** with **Visual Studio** **2013**.

Let's start with a review of the elements of **first-order logic**. First, we have the **terms**:

**Constants**, which represent a particular individual and that, in the program, must be written always starting with the character '**_**', followed by a letter and any number of alphanumeric characters. They can also be used as constants the natural numbers.**Variables**, representing a generic individual. The program differentiates the**variables**of the**constants**because his name does not begin with the character '**_**', but by a letter followed by any number of alphanumeric characters.**Functions**, which are compound terms, as they have parameters that must be also**terms**. In the program, the**functions**are written with a name that begins with any letter followed by any number of alphanumeric characters and a list of parameters separated by commas enclosed in parentheses, for example:`f(x, y, _c)`

. The result of a**function**is an individual, that is, a**term**. For example "*the father of x*" is a function.

The **formulas** are constructed using the following elements:

- The symbols
**True**and**False**are**formulas**. - A
**proposition**or**relationship**relative to 0 or more terms is a**formula**. They should be written with a letter followed by any number of alphanumeric characters, with the list of terms to which it references separated by commas enclosed in brackets. The brackets should be placed although the proposal has no parameters. For example, "*x and y are friends*" is a**relationship**, and should be written`FR[x, y]`

. - An
**equality**is a**formula**. It consists of two terms connected with the**=**operator, for example`x = y`

. - A
**formula**to which is applied the**NOT**logical negation operator, is a**formula**. - Two
**formulas**connected by the logical operators**AND**,**OR**,**implication**and**double implication**is also a**formula**. - There are some elements, called
**quantifiers**, which refer to a particular variable in a formula and can refer to all possible individuals (**universal quantifier**) or only to one or more individuals (**existential quantifier**). A**formula**on which they apply a quantizer is also a**formula**.

Although the use of the program in this version is basically the same as in the previous article, I modified the symbols that appear in **formulas** so that they are written in a standard format; these are the keyboard keys and the symbols that they give:

**AND**operator, is obtained by pressing the**&**key, but the symbol that appears is the**˄**character.**OR**operator, is obtained by pressing**|**, but the symbol that appears is the character**˅**.**Implication**: pressing the**<**key the character**→**is obtained.**Double implication**: pressing the**>**key the**↔**character is obtained.**Universal quantifier**: it is obtained by pressing the**@**key.**Existential quantifier**: it is obtained by pressing the**#**key.**True**, it is obtained by pressing the**$**key, the symbol is**⟙**.**False**, it is obtained by pressing the**%**key, the symbol is**⟘**.

Parentheses can be used to group **formulas**. For example, is not the same `PT[x] → (PQ[x]˅PL[x]˅SV[x])`

than `PT[x] → PQ[x]˅PL[x]˅SV[x]`

as, in this program, the implication operator has higher precedence than the **OR** or **AND** operator.

Equalities must be enclosed in parentheses if you want to negate them. In general, it is best to always write the equalities in parentheses.

Parentheses are also used to apply a **quantifier** to a composite formula, such as `ᗄx(PT[x] → (PQ[x]˅PL[x]˅SV[x]))`

. If you do not put parentheses, the quantizer only applies to the first sub-formula, `PT[x]`

.

The program always transforms the **implications** in their equivalent formulas using the **AND** and **OR** connectives and the **NOT** operator. It also solves the negations of composite **formulas** before processing the **Tableaux**.

This is the program look:

To the functionality of the **Tableaux** for **predicate logic** I have added the following:

- Maximum number of steps (
**Max Steps**). A first order**Tableaux**can be infinite. It is also possible that, with a very complex set of**formulas**, the program will not be able to find the proper development to end the**Tableaux**. To prevent the program from hanging up, you can specify the maximum number of formulas to create until the program ends. **Normalize**. With this button, all formulas are rewritten in prenex normal form, which involves passing all quantifiers to the beginning of the**formula**. There is no need to use this option to calculate the**Tableaux**, but you can use it to correct exercises, for example.**Skolemize**: it involves passing formulas to Skolem normal form that is a prenex form where**existential quantifiers**have been eliminated and their quantified variables are replaced by**constants**or appropriate**functions**. The constants and functions introduced in this step are named using the following structure:***sk + order number**. To calculate the**Tableaux**is not recommended to use the standardized Skolem formulas, since the substitution of variables and functions is performed at each formula independently of the others, and it can change the meaning of the argumentation. This option can be used to correct exercises, by example.

As a result we obtain the **Tableaux** displayed in two different formats, more or less appropriate depending on the size of the result. On one side, a tree view is shown, in which the branches can be expanded or collapsed and that contain the formula list in the nodes of the **Tableaux** branches, this view is more appropriate for large sets of **formulas**.

The closed branches are indicated by the **#** symbol, as in the **Tableaux** for **predicate logic**, and the number of the formula that has been used to create new ones or make a branch is indicated in brackets after the letter **R**.

The existence of the **equality** operator introduces two new rules for creating formulas. On the one hand there is the rule of **reflexivity**, indicated by the letters **RF** which allows you to enter at the end of a branch the formula `t = t`

, where t is a term any of those in the branch. We can also use the **substitution** rule, indicated by the letters **ST**, which allows us to replace in a formula of the branch the term t by the term t', provided there is a formula of the form `t = t'`

in the branch.

To create new **formulas** from formulas with **quantifiers**, in the case of **existential quantifiers**, we replace the **variable** quantified by a new **constant**, called example, which has not been already used in the branch. There can't be more than one example of existentially quantified formula in the same branch. Quantified variables by the **universal quantifiers** can be substituted by any **term** present in the branch or by a new **constant**, if there is no term available. These constants, or functions, introduced to particularize quantified formulas are always named following the scheme ***t + sequential number**.

We also get a view of the **Tableaux** fully expanded that can be useful when the number of **formulas** is not too high:

This **Tableaux** can also be used to solve any problem of **predicate logic**, since it is a subset of **first-order logic**. However, the heuristics used to try to resolve the first order **Tableaux** doesn't goes beyond the next step, so that the algorithms may have to be quite improved for solving problems with complex sets of formulas. The program successfully solves all the exercises in the book that I used as a reference, and which is as follows (sorry, only in Spanish): Mathematical logic for informatics.