Definition:Language of Predicate Logic/Alphabet

From ProofWiki
Jump to navigation Jump to search

Definition

The alphabet $\mathcal A$ of the language of predicate logic $\mathcal L_1$ is defined as follows:


Letters

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.


Variables

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.


Signs

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

They split in three classes:


Connectives

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.


Quantifiers

The quantifiers of $\mathcal L_1$ are:

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


Punctuation

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             


Sources