Definition:Language of Predicate Logic/Formal Grammar

From ProofWiki
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$:
$\map f {\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

Retrieved from "https://proofwiki.org/w/index.php?title=Definition:Language_of_Predicate_Logic/Formal_Grammar&oldid=444309"