# Definition:Language of Propositional Logic/Labeled Tree

## Definition

There are many formal languages expressing propositional logic.

The formal language used on $\mathsf{Pr} \infty \mathsf{fWiki}$ is defined on Definition:Language of Propositional Logic.

This page defines the formal language $\mathcal L_0$ used in:

Explanations are omitted as this is intended for reference use only.

### Alphabet

#### Letters

The letters used are an infinite set of symbols $\mathcal P_0$.

This is the same as the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.

#### Signs

##### Connectives

The following connectives are used:

 $\displaystyle \bullet \ \$ $\displaystyle \neg$ $:$ $\displaystyle$the negation sign $\displaystyle \bullet \ \$ $\displaystyle \lor$ $:$ $\displaystyle$the disjunction sign $\displaystyle \bullet \ \$ $\displaystyle \land$ $:$ $\displaystyle$the conjunction sign $\displaystyle \bullet \ \$ $\displaystyle \implies$ $:$ $\displaystyle$the conditional sign $\displaystyle \bullet \ \$ $\displaystyle \iff$ $:$ $\displaystyle$the biconditional sign $\displaystyle \bullet \ \$ $\displaystyle \oplus$ $:$ $\displaystyle$the exclusive or sign $\displaystyle \bullet \ \$ $\displaystyle \downarrow$ $:$ $\displaystyle$the nor sign $\displaystyle \bullet \ \$ $\displaystyle \uparrow$ $:$ $\displaystyle$the nand sign

### Collation System

The collation system used is that of labeled trees and adding ancestors.

### Formal Grammar

The following bottom-up formal grammar is used.

Let $\mathcal P_0$ be the vocabulary of $\mathcal L_0$.

The WFFs of $\mathcal L_0$ are the smallest set $\mathcal F$ of labeled trees such that:

 $(T1)$ $:$ For each letter $p \in \mathcal P_0$, the labeled tree with one node, whose label is $p$, is in $\mathcal F$. $(T2)$ $:$ For $T \in \mathcal F$, the labeled tree obtained by adding an ancestor with label $\neg$ to the root node of $T$, is again in $\mathcal F$. $(T3)$ $:$ For $T_1 \in \mathcal F$ and $T_2 \in \mathcal F$ and a binary connective $\mathsf B$, the labeled tree obtained by adding a common ancestor labeled $\mathsf B$ of the root nodes of $T_1$ and $T_2$, is again in $\mathcal F$.

Graphically, this means one has the following means to construct WFFs:

$\begin{xy}\xymatrix{ p & & \neg \[email protected]{-}[d] & & & \mathsf B \[email protected]{-}[ld] \[email protected]{-}[rd] \\ & & <{\sf WFF}> & & <{\sf WFF}> & & <{\sf WFF}> }\end{xy}$