Definition:Language of Predicate Logic

From ProofWiki
Jump to: navigation, search


There are a lot of different formal systems expressing predicate logic.

Although they vary wildly in complexity and even disagree (to some extent) on what expressions are valid, generally all of these use a compatible formal language.

This page defines the formal language of choice on $\mathsf{Pr} \infty \mathsf{fWiki}$.

We will use $\mathcal L_1$ to represent the formal language of predicate logic in what follows.

In order to define $\mathcal L_1$, it is necessary to specify:



The letters of $\mathcal L_1$ are separated in three classes:

Each of these three classes is handled differently by the formal grammar of predicate logic.


The variables constitute an infinite set $\mathrm{VAR}$ of arbitrary symbols, for example:

$\mathrm{VAR} = \left\{{x, y, z, x_0, y_0, z_0, x_1, y_1, z_1, \ldots}\right\}$

Predicate Symbols

The predicate symbols are a collection of arbitrary symbols.

Each of these symbols is considered to be endowed with an arity (a natural number $n \in \N$).

We agree to write $\mathcal P$ for the set of predicate symbols, grouped by their arity:

$\mathcal P = \left\{{\mathcal P_0, \mathcal P_1, \mathcal P_2, \ldots, \mathcal P_k, \ldots}\right\}$

The symbols in $\mathcal P_0$ are inherited from the language of propositional logic.

For example, if $P \in \mathcal P_5$ then $P$ is a quinternary predicate symbol.

Function Symbols

The function symbols are a collection (possibly empty) of arbitrary symbols.

Each of these symbols is considered to be endowed with an arity (a natural number $n \in \N$).

We agree to write $\mathcal F$ for the set of function symbols, grouped by their arity:

$\mathcal F = \left\{{\mathcal F_0, \mathcal F_1, \ldots, \mathcal F_k, \ldots}\right\}$

The symbols in $\mathcal F_0$ are often called parameters or constants.

Some sources write $\mathcal K$ for the collection of parameters.


The signs of $\mathcal L_1$ are an extension of the signs of propositional logic.

They split in three classes:


The connectives of $\mathcal L_1$ comprise:

   \(\displaystyle \land \)   \(\displaystyle : \)   the conjunction sign             
   \(\displaystyle \lor \)   \(\displaystyle : \)   the disjunction sign             
   \(\displaystyle \implies \)   \(\displaystyle : \)   the conditional sign             
   \(\displaystyle \iff \)   \(\displaystyle : \)   the biconditional sign             
   \(\displaystyle \neg \)   \(\displaystyle : \)   the negation sign             
   \(\displaystyle \top \)   \(\displaystyle : \)   the top sign             
   \(\displaystyle \bot \)   \(\displaystyle : \)   the bottom sign             

The symbols $\land,\lor,\implies$ and $\iff$ are called the binary connectives.

The symbols $\neg$ is called a unary connective.

The symbols $\top$ and $\bot$ are called the nullary connectives.


The quantifiers of $\mathcal L_1$ are:

   \(\displaystyle \exists \)   \(\displaystyle : \)   the existential quantifier sign             
   \(\displaystyle \forall \)   \(\displaystyle : \)   the universal quantifier sign             


The punctuation symbols used in $\mathcal L_1$ are:

   \(\displaystyle ( \)   \(\displaystyle : \)   the left parenthesis sign             
   \(\displaystyle ) \)   \(\displaystyle : \)   the right parenthesis sign             
   \(\displaystyle : \)   \(\displaystyle : \)   the colon             
   \(\displaystyle , \)   \(\displaystyle : \)   the comma             

Collation System

The collation system for the language of predicate logic is that of words and concatenation.

The unique readability property is verified on Unique Readability for Language of Predicate Logic.

Formal Grammar

The following rules of formation constitute a bottom-up grammar for the language of predicate logic $\mathcal L_1$.

The definition proceeds in two steps.

First, we will define terms, and then well-formed formulas.


The terms of $\mathcal L_1$ are identified by the following bottom-up grammar:

\((\mathbf T ~ \textrm{VAR})\)   $:$   Any variable of $\mathcal L_1$ is a term;             
\((\mathbf T ~ \mathcal F_n)\)   $:$   Given an $n$-ary function symbol $f \in \mathcal F_n$ and terms $\tau_1, \ldots, \tau_n$:
$f \left({\tau_1, \ldots, \tau_n}\right)$

is also a term.   


Well-Formed Formulas

The WFFs of $\mathcal L_1$ are defined by the following bottom-up grammar:

\((\mathbf W ~ \mathcal P_n)\)   $:$   If $t_1, \ldots, t_n$ are terms, and $p \in \mathcal P_n$ is an $n$-ary predicate symbol, then $p \left({t_1, t_2, \ldots, t_n}\right)$ is a WFF.             
\((\mathbf W ~ \neg)\)   $:$   If $\mathbf A$ is a WFF, then $\neg \mathbf A$ is a WFF.             
\((\mathbf W ~ \lor, \land, \Rightarrow, \Leftrightarrow)\)   $:$   If $\mathbf A, \mathbf B$ are WFFs and $\circ$ is one of $\lor, \land, \mathord\implies, \mathord\iff$, then $\left({\mathbf A \circ \mathbf B}\right)$ is a WFF             
\((\mathbf W ~ \forall, \exists)\)   $:$   If $\mathbf A$ is a WFF and $x$ is a variable, then $\left({\forall x: \mathbf A}\right)$ and $\left({\exists x: \mathbf A}\right)$ are WFFs.             

Also defined as

Since most authors concern themselves only with one formal system for predicate logic, they tend to refer to the whole formal system as predicate logic or predicate calculus.

In correspondence, a particular author may decide to use only a subset of the signs.

Generally, the other signs then are considered definitional abbreviations.

Similarly, it is becoming increasingly common to make $=$ part of the signs.

At $\mathsf{Pr} \infty \mathsf{fWiki}$ we aim to incorporate all these different approaches, and thus we have come to separately define the formal language.

For the sakes of modularity and universality, we have settled for the formal language on this page as the language of choice on $\mathsf{Pr} \infty \mathsf{fWiki}$.

The page Definition:Translation Scheme for Predicate Logic documents how various other approaches from the literature can be translated into ours.

If so desired, a generic such formal system may be addressed as a predicate calculus, but this has to be used with reluctance and caution.

Also see

  • Results about the language of predicate logic can be found here.