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, \E respectively.

Syntax of first order formulas

First order languages

A first order language is a language characterized by:

• A set of constant symbols;

• A set of variable symbols;

• A set of function symbols, each with an associated arity;

• A set of predicate symbols, each with an associated arity;

• The logic symbols ¬, ∧, ∨, →, ←, ↔;

• The quantifier symbols ∀, ∃;

• The punctuation symbols (, ), ,.

Terms

Terms are the basic building blocks needed to write first order formulas. They are defined inductively as follows:

• Every variable is a term;

• Every constant is a term;

• f(t₁, …, t_n) is a term if t₁, …, t_n are terms and f is a function of arity n.

Formulas

A first order formula can be defined inductively as follows:

• p(t₁, …, t_n) is a formula if t₁, …, 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.