Definition:Language of Propositional Logic/Labeled Tree

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 $\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

Retrieved from "https://proofwiki.org/w/index.php?title=Definition:Language_of_Propositional_Logic/Labeled_Tree&oldid=652479"