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 $\LL_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 $\PP_0$.
This is the same as the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.
Signs
Connectives
The following connectives are used:
\(\ds \bullet \ \ \) | \(\ds \neg\) | \(:\) | \(\ds \)the negation sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \lor\) | \(:\) | \(\ds \)the disjunction sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \land\) | \(:\) | \(\ds \)the conjunction sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \implies\) | \(:\) | \(\ds \)the conditional sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \iff\) | \(:\) | \(\ds \)the biconditional sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \oplus\) | \(:\) | \(\ds \)the exclusive or sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \downarrow\) | \(:\) | \(\ds \)the nor sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \uparrow\) | \(:\) | \(\ds \)the nand sign\(\) |
See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.
Collation System
The collation system used is that of labeled trees and adding ancestors.
![]() | This article, or a section of it, needs explaining. In particular: "adding ancestors" signifies combining labeled trees into a new one by creating a common ancestor for their roots You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Explain}} from the code. |
See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.
Formal Grammar
The following bottom-up formal grammar is used.
Let $\PP_0$ be the vocabulary of $\LL_0$.
The WFFs of $\LL_0$ are the smallest set $\FF$ of labeled trees such that:
\((T1)\) | $:$ | For each letter $p \in \PP_0$, the labeled tree with one node, whose label is $p$, is in $\FF$. | |||||||
\((T2)\) | $:$ | For $T \in \FF$, the labeled tree obtained by adding an ancestor with label $\neg$ to the root node of $T$, is again in $\FF$. | |||||||
\((T3)\) | $:$ | For $T_1 \in \FF$ and $T_2 \in \FF$ 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 $\FF$. |
Graphically, this means one has the following means to construct WFFs:
- $\begin{xy}\xymatrix{
p
& &
\neg \ar@{-}[d]
& & &
\mathsf B \ar@{-}[ld] \ar@{-}[rd]
\\ & &
<{\sf WFF}>
& &
<{\sf WFF}>
& &
<{\sf WFF}>
}\end{xy}$ See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.
Also see
Sources
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.3$: Propositional logic as a formal language
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.1.1$: Definition $2.2$