Definition:Language of Predicate Logic/Alphabet
This page has been identified as a candidate for refactoring of advanced complexity. In particular: subpages once extension transclusion has been improved to work with ToC Until this has been finished, please leave {{Refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code. |
Definition
The alphabet $\AA$ of the language of predicate logic $\LL_1$ is defined as follows:
Letters
The letters of $\LL_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} = \set {x, y, z, x_0, y_0, z_0, x_1, y_1, z_1, \ldots}$
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 $\PP$ for the set of predicate symbols, grouped by their arity:
- $\PP = \set {\PP_0, \PP_1, \PP_2, \ldots, \PP_k, \ldots}$
The symbols in $\PP_0$ are inherited from the language of propositional logic.
For example, if $P \in \PP_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 $\FF$ for the set of function symbols, grouped by their arity:
- $\FF = \set {\FF_0, \FF_1, \ldots, \FF_k, \ldots}$
The symbols in $\FF_0$ are often called parameters or constants.
Some sources write $\KK$ for the collection of parameters.
Signs
The signs of $\LL_1$ are an extension of the signs of propositional logic.
They split in three classes:
- connectives;
- quantifiers;
- punctuation.
Connectives
The connectives of $\LL_1$ comprise:
\(\ds \land \) | \(\ds : \) | the conjunction sign | |||||||
\(\ds \lor \) | \(\ds : \) | the disjunction sign | |||||||
\(\ds \implies \) | \(\ds : \) | the conditional sign | |||||||
\(\ds \iff \) | \(\ds : \) | the biconditional sign | |||||||
\(\ds \neg \) | \(\ds : \) | the negation sign | |||||||
\(\ds \top \) | \(\ds : \) | the top sign | |||||||
\(\ds \bot \) | \(\ds : \) | 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 $\LL_1$ are:
\(\ds \exists \) | \(\ds : \) | the existential quantifier sign | |||||||
\(\ds \forall \) | \(\ds : \) | the universal quantifier sign |
Punctuation
The punctuation symbols used in $\LL_1$ are:
\(\ds ( \) | \(\ds : \) | the left parenthesis sign | |||||||
\(\ds ) \) | \(\ds : \) | the right parenthesis sign | |||||||
\(\ds : \) | \(\ds : \) | the colon | |||||||
\(\ds , \) | \(\ds : \) | the comma |
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.2$
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\text{II}.5$ First-Order Logic Syntax: Definition $\text{II}.5.1$
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\text{II}.5$ First-Order Logic Syntax: Definition $\text{II}.5.2$