# First order logic tool

Use the input field below to write a first order formula. Confirm your input by pressing enter. To insert ¬, ∧, ∨, →, ←, ↔, ∀, ∃ type !, &, |, ->, <-, <->, \A, \E respectively.

## Purpose and usage of the tool

The purpose of this tool is to analyze propositional formulas like
*A* → *B* ∧ *C* and first order formulas like
∀*x* ¬∃*y* (*p*(*x*) → *q*(*y*)).

Given any formula of these types, the tool is able to calculate the degree and the height of the formula. It is also able to infer the meaning of each used symbol, which means it understands if the symbol stands for a variable, constant, function, or predicate. In addition, the tool derives a formula in prenex normal form which is logically equivalent to the initial formula. Given a propositional formula, it automatically generates the corresponding truth table.

To use the tool, simply write the formula to be analyzed in the input field above and press enter. The symbols ¬, ∧, ∨, →, ←, ↔, ∀, ∃ can be inserted by typing !, &, |, ->, <-, <->, \A (or \a), \E (or \e) respectively.

## Syntax of first order formulas

From a syntactical point of view, first order formulas are strings of symbols connected by logical operators, quantifiers and punctuation marks. Each symbol can represent a variable, constant, function, or predicate. Let’s take a look at an example:

¬∃*x* (*p*(*x*, *f*(*a*)) ∧ *p*(*x*, *g*(*a*)))

In the formula above, *x* would be a variable, *a* a constant, *p* a binary predicate, *f* an unary
function. ¬ and ∧ are logic symbols, ∃ is the existential quantifier, (, ), , are punctuation marks.

### First order language

A first order language 𝓛 is a language characterized by:

- A set of constant symbols (like
*a*,*b*,*c*, …); - A set of infinite variable symbols (like
*x*,*y*,*z*, …); - A set of function symbols, each with an associated arity (for example
*f*with arity 1,*g*with arity 3, …); - A set of predicate symbols (also called relation symbols), each with an associated arity (for example
*p*with arity 2,*q*with arity 1, …); - The logic symbols ¬, ∧, ∨, →, ←, ↔;
- The quantifier symbols ∀, ∃;
- The punctuation symbols (, ), ,.

### Terms

The terms of first order languages are the basic building blocks needed to write first order formulas. They are defined recursively as follows:

- Every variable is a term;
- Every constant is a term;
*f*(*t*_{1}, …,*t*_{n}) is a term if*t*_{1}, …,*t*_{n}are terms and*f*is a function of arity*n*.

In the example above, *a*, *f*(*a*), *g*(*a*) and *x* are terms of the formula.

### Formulas

A first order formula can be defined recursively as follows:

*p*(*t*_{1}, …,*t*_{n}) is a formula if*t*_{1}, …,*t*_{n}are terms and*p*is a predicate of arity*n*. A formula of this kind is called atomic;- (¬
*F*) is a formula if*F*is a formula; - (
*F*∧*G*), (*F*∨*G*), (*F*→*G*), (*F*←*G*), (*F*↔*G*) are formulas if both*F**and**G**are formulas;* - (∀
*x**F*), (∃*x**F*) are formulas if*x*is a variable and*F*is a formula.

In order to increase readability, parentheses can be dropped according to the following convention:

- The outermost parentheses are omitted;
*¬*,*∀*,*∃*have precedence on all other operators, making ∀*x**F*∨*G*equivalent to (∀*x**F*) ∨*G*;- ∧, ∨ have precedence over →, ←, ↔, making
*F*∧*G*→*H*equivalent to (*F*∧*G*) →*H*; - Parentheses may be omitted in formulas where the same binary operator is used multiple times, if the operator is one
of ∧, ∨, ↔. This makes
*F*↔*G*↔*H*equivalent to (*F*↔*G*) ↔*H*. Parentheses must not be dropped if mixed operators are used: for instance,*F*∧*G*∨*H*is*not*a valid formula.

In the example above, *p*(*x*, *f*(*a*)) and
*p*(*x*, *g*(*a*)) are atomic formulas. In addition,
*p*(*x*, *f*(*a*)) ∧ *p*(*x*, *g*(*a*) and
∃*x* (*p*(*x*, *f*(*a*)) ∧ *p*(*x*, *g*(*a*)))
are proper substrings of the original formula which are also formulas.

### Free and bound variables, open and closed formulas

Depending on the context, variables can be free or bound. For example, the variable *person* is free in the
formula *livesInItaly*(*person*) but is bound in the formula
∀*person* *livesInItaly*(*person*). The role of the symbol *person* is
different in the two cases: the first formula is neither true nor false as *person* is just an empty placeholder,
the second formula is false since it is not true that all people live in Italy.

Formally, if *F* is a formula and *x* is a variable appearing in *F*, all occurrences of *x* in
*F* are said to be bound in formulas of the kind ∀*x* *F* or
∃*x* *F*. Any occurrence of a variable which is not bound is said to be
free. Any formula containing at least one free occurrence of a variable is called an
open formula. If a formula is not open, it is said to be a sentence or closed formula.

Please note that different occurrences of the same variable can be free in one case and bound in another. For example,
in the formula *p*(*x*) ∧ ∃*x* *q*(*x*) the first occurrence of
*x* is free while the second one is bound.

## Semantic of first order formulas

Whether a sentence is true of not depends on the interpretation of predicate, function and constant symbols. For
instance, we could declare the symbols *p*, *f*, *g*, *a* of the example above to mean taller than,
father of, mother of, Mark respectively; with this interpretation, assuming that we are only talking about people, the
formula states that there doesn’t exist any person which is taller than both the father and the mother of Mark. We
could write a formula which is logically equivalent to the one above, but with self-describing symbols:

¬∃*person* (*taller*(*person*, *father*(*Mark*)) ∧ *taller*(*person*, *mother*(*Mark*)))

In turn, the interpretation of a sentence depends on the domain of discourse. In this case, the domain of discourse would be the set of people we’re talking about. If the domain of discourse consists only of Mark and we assume that Mark is shorter than his dad, the formula is trivially true; however if the domain of discourse is Mark and all his friends, then the truthfulness of the sentence also depends on the height of all his friends.

### Interpretation a sentence

Let 𝓛 be a first order language. The domain of discourse *D* is a non-empty set of elements. For each
constant symbol of 𝓛 there’s an element in *D*.

An interpretation *I* of 𝓛 is a function mapping every function and predicate symbol of 𝓛 to its
meaning:

- For every function symbol
*f*of 𝓛 there’s a mapping*I*(*f*):*D*^{n}→*D*, where*n*is the arity of*f*. - For every predicate symbol
*p*of 𝓛 there’s a set*I*(*p*) such that*I*(*p*) ⊆*D*.

In addition
*I*(*f*(*t*_{1}, …, *t*_{n})) = *I*(*f*)(*I*(*t*_{1}), …, *I*(*t*_{n})),
if *f* is a function of arity *n* and *t*_{1}, …, *t*_{n} are
terms.

### Truth value of a sentence

Given an interpretation *I* and a sentence *F* it is possible to determine its truth value, which
is either true (𝕋) or false (𝔽).

*p*(*t*_{1}, …,*t*_{n}) is true iff (*I*(*t*_{1}), …,*I*(*t*_{n})) ∈*I*(*p*);- ¬
*F*is true iff*F*is false; *F*∧*G*is true iff*F*and*G*are both true;*F*∨*G*is true iff*F*is true or*G*is true;*F*→*G*is true iff*F*is false or*G*is true;*F*←*G*is true iff*F*is true or*G*is false;*F*↔*G*is true iff*F*and*G*have the same truth value.

### Logical equivalence

Two sentences are logically equivalent if they are yield the same truth value independently of the interpretation given to them.

More formally, two sentences *F* and *G* are logically equivalent if, for every interpretation,
*F* is true if and only if *G* is also true.