Definition:Language of Predicate Logic/Formal Grammar
Jump to navigation
Jump to search
Definition
Part of specifying the language of propositional logic is to provide its formal grammar.
The following rules of formation constitute a bottom-up grammar for the language of predicate logic $\LL_1$.
The definition proceeds in two steps.
First, we will define terms, and then well-formed formulas.
Terms
The terms of $\LL_1$ are identified by the following bottom-up grammar:
\((\mathbf T \ \textrm {VAR})\) | $:$ | Any variable of $\LL_1$ is a term; | |||||||
\((\mathbf T \ \FF_n)\) | $:$ | Given an $n$-ary function symbol $f \in \FF_n$ and terms $\tau_1, \ldots, \tau_n$:
is also a term. |
Well-Formed Formulas
The WFFs of $\LL_1$ are defined by the following bottom-up grammar:
\((\mathbf W ~ \PP_n)\) | $:$ | If $t_1, \ldots, t_n$ are terms, and $p \in \PP_n$ is an $n$-ary predicate symbol, then $\map p {t_1, t_2, \ldots, t_n}$ 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 $\paren {\mathbf A \circ \mathbf B}$ is a WFF | |||||||
\((\mathbf W ~ \forall, \exists)\) | $:$ | If $\mathbf A$ is a WFF and $x$ is a variable, then $\paren {\forall x: \mathbf A}$ and $\paren {\exists x: \mathbf A}$ are WFFs. |
Sources
- 1960: Paul R. Halmos: Naive Set Theory ... (previous) ... (next): $\S 2$: The Axiom of Specification
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.2$: Definition $2.2.2$
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\mathrm{II}.5$ First-Order Logic Syntax: Definition $\mathrm{II.5.3}$