Definition:Language of Propositional Logic
Definition
There are a lot of different formal systems expressing propositional logic.
Although they vary wildly in complexity and even disagree (to some extent) on what expressions are valid, generally all of these use a compatible formal language.
This page defines the formal language of choice on $\mathsf{Pr} \infty \mathsf{fWiki}$.
We will use $\LL_0$ to represent the formal language of propositional logic in what follows.
In order to define $\LL_0$, it is necessary to specify:
- An alphabet $\AA$
- A collation system with the unique readability property for $\AA$
- A formal grammar (which determines the WFFs of $\LL_0$)
Alphabet
Letters
The letters of $\LL_0$, called propositional symbols, can be any infinite collection $\PP_0$ of arbitrary symbols.
This article, or a section of it, needs explaining. In particular: "infinite collection" -- we need an informal way of referring to "infinite" without resorting to the machinery of set theory. 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. |
It is usual to specify them as a limited subset of the English alphabet with appropriate subscripts.
A typical set of propositional symbols would be, for example:
- $\PP_0 = \set {p_1, p_2, p_3, \ldots, p_n, \ldots}$
Signs
The signs of the language of propositional logic come in two categories:
Brackets
\(\ds \bullet \ \ \) | \(\ds (\) | \(:\) | \(\ds \)the left bracket sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds )\) | \(:\) | \(\ds \)the right bracket sign\(\) |
Connectives
\(\ds \bullet \ \ \) | \(\ds \land\) | \(:\) | \(\ds \)the conjunction sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \lor\) | \(:\) | \(\ds \)the disjunction sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \implies\) | \(:\) | \(\ds \)the conditional sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \iff\) | \(:\) | \(\ds \)the biconditional sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \neg\) | \(:\) | \(\ds \)the negation sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \top\) | \(:\) | \(\ds \)the tautology sign\(\) | |||||||||||
\(\ds \bullet \ \ \) | \(\ds \bot\) | \(:\) | \(\ds \)the contradiction sign\(\) |
These comprise:
- The nullary connectives $\top$ and $\bot$, representing the canonical tautology and contradiction, respectively
- The unary connective $\neg$, representing negation
- The binary connectives $\land, \lor, \implies$ and $\iff$, representing, respectively, conjunction, disjunction, implication and biconditional.
Collation System
The collation system for the language of propositional logic is that of words and concatenation.
To ensure the unique readability property, it is necessary that the vocabulary $\PP_0$ is chosen appropriately.
In particular, such that it does not conflict with the signs.
Formal Grammar
The formal grammar of the language of propositional logic (and hence its WFFs) can be defined in the following ways.
Backus-Naur Form
In Backus-Naur form, the formal grammar of the language of propositional logic takes the following form:
\(\ds \meta {formula}\) | \(\)::=\(\) | \(\ds p \ \mid \ \top \ \mid \ \bot\) | where $p \in \PP_0$ is a letter | |||||||||||
\(\ds \meta {formula}\) | \(\)::=\(\) | \(\ds \neg \meta {formula}\) | ||||||||||||
\(\ds \meta {formula}\) | \(\)::=\(\) | \(\ds (\meta {formula} \ \meta {op} \ \meta {formula})\) | ||||||||||||
\(\ds \meta {op}\) | \(\)::=\(\) | \(\ds \land \ \mid \ \lor \ \mid \implies \mid \iff\) |
Note that this is a top-down grammar:
- we start with a metasymbol $\meta {formula}$
- progressively replace it with constructs containing other metasymbols and/or primitive symbols
until finally we are left with a well-formed formula of $\LL_0$ consisting of nothing but primitive symbols.
Bottom-Up Specification
The following rules of formation constitute a bottom-up grammar for the formation of well-formed formulas (WFFs) of the language of propositional logic $\LL_0$.
- Let $\PP_0$ be the vocabulary of $\LL_0$.
- Let $\mathrm {Op} = \set {\land, \lor, \implies, \iff}$.
The rules are:
$\mathbf W: \text {TF}$ | $:$ | $\top$ is a WFF, and $\bot$ is a WFF. | |
$\mathbf W: \PP_0$ | $:$ | If $p \in \PP_0$, then $p$ is a WFF. | |
$\mathbf W: \neg$ | $:$ | If $\mathbf A$ is a WFF, then $\neg \mathbf A$ is a WFF. | |
$\mathbf W: \text {Op}$ | $:$ | If $\mathbf A$ is a WFF and $\mathbf B$ is a WFF and $\circ \in \mathrm {Op}$, then $\paren {\mathbf A \circ \mathbf B}$ is a WFF. |
This page has been identified as a candidate for refactoring of basic complexity. In particular: Implement the above using the {{Axiom}} templateUntil this has been finished, please leave {{Refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.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 {{Refactor}} from the code. |
Any string which can not be created by means of the above rules is not a WFF.
Also defined as
Since most authors concern themselves only with one formal system for propositional logic, they tend to refer to the whole formal system as propositional logic or propositional calculus.
In correspondence, a particular author may decide to use only a subset of the signs.
Generally, the other signs then are considered definitional abbreviations.
At $\mathsf{Pr} \infty \mathsf{fWiki}$ we aim to incorporate all these different approaches, and thus we have come to separately define the formal language.
For the sakes of modularity and universality, we have settled for the formal language on this page as the language of choice on $\mathsf{Pr} \infty \mathsf{fWiki}$.
The page Definition:Translation Scheme for Propositional Logic documents how various other approaches from the literature can be translated into ours.
If so desired, a generic such formal system may be addressed as a propositional calculus, but this has to be used with reluctance and caution.
Also see
- Definition:Language of Propositional Logic/Keisler-Robbin
- Definition:Language of Propositional Logic/Basson-O'Connor
- Results about the language of propositional logic can be found here.
Sources
- 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 4.2$: The Construction of an Axiom System
- 1964: Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning ... (previous) ... (next): $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$
- 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): Chapter $2$: The Propositional Calculus $2$: Introduction
- 1980: D.J. O'Connor and Betty Powell: Elementary Logic ... (previous) ... (next): $\S \text{I}: 1$: The Logic of Statements $(1)$
- 1993: M. Ben-Ari: Mathematical Logic for Computer Science ... (previous) ... (next): Chapter $1$: Introduction: $\S 1.2$: Propositional and predicate calculus