# Definition:Language of Propositional Logic/Keisler-Robbin

Jump to navigation Jump to search

## 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 a non-empty set of symbols $\mathcal P_0$.

#### Signs

##### Brackets

The brackets used are square brackets:

 $\displaystyle \bullet \ \$ $\displaystyle [$ $:$ $\displaystyle$the left bracket sign $\displaystyle \bullet \ \$ $\displaystyle ]$ $:$ $\displaystyle$the right bracket sign

##### Connectives

The following connectives are used:

 $\displaystyle \bullet \ \$ $\displaystyle \land$ $:$ $\displaystyle$the conjunction sign $\displaystyle \bullet \ \$ $\displaystyle \lor$ $:$ $\displaystyle$the disjunction sign $\displaystyle \bullet \ \$ $\displaystyle \implies$ $:$ $\displaystyle$the conditional sign $\displaystyle \bullet \ \$ $\displaystyle \iff$ $:$ $\displaystyle$the biconditional sign $\displaystyle \bullet \ \$ $\displaystyle \neg$ $:$ $\displaystyle$the negation sign

### Collation System

The collation system used is that of words and concatenation.

### Formal Grammar

The following bottom-up formal grammar is used.

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

Let $Op = \left\{{\land, \lor, \implies, \iff}\right\}$.

The rules are:

 $\mathbf W: \mathcal P_0$ $:$ If $p \in \mathcal P_0$, then $p$ is a WFF. $\mathbf W: \neg$ $:$ If $\mathbf A$ is a WFF, then $\neg \mathbf A$ is a WFF. $\mathbf W: Op$ $:$ If $\mathbf A$ and $\mathbf B$ are WFFs and $\circ \in Op$, then $\left[{\mathbf A \circ \mathbf B}\right]$ is a WFF.