Definition:Language of Propositional Logic/Basson-O'Connor

From ProofWiki
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$.

See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.


Signs

Brackets

The brackets used are round brackets:

\(\displaystyle \bullet \ \ \) \(\displaystyle (\) \(:\) \(\displaystyle \)the left bracket sign\(\)
\(\displaystyle \bullet \ \ \) \(\displaystyle )\) \(:\) \(\displaystyle \)the right bracket sign\(\)

See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.


Connectives

The following connectives are used:

\(\displaystyle \bullet \ \ \) \(\displaystyle .\) \(:\) \(\displaystyle \)the conjunction sign\(\)
\(\displaystyle \bullet \ \ \) \(\displaystyle \lor\) \(:\) \(\displaystyle \)the disjunction sign\(\)
\(\displaystyle \bullet \ \ \) \(\displaystyle \supset\) \(:\) \(\displaystyle \)the conditional sign\(\)
\(\displaystyle \bullet \ \ \) \(\displaystyle \equiv\) \(:\) \(\displaystyle \)the biconditional sign\(\)
\(\displaystyle \bullet \ \ \) \(\displaystyle \sim\) \(:\) \(\displaystyle \)the negation sign\(\)

See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.


Collation System

The collation system used is that of words and concatenation.

See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.


Formal Grammar

The following bottom-up formal grammar is used.


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

Let $Op = \left\{{., \lor, \supset, \equiv}\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 $\sim \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.

See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.


Also see


Sources