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 ABC 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:


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


A first order formula can be defined inductively as follows: