Category:Propositional Calculus

Definition

The language of propositional logic can be defined as a formal system.

In order to do this, we need to specify the various components of this: the alphabet, the WFFs, the syntax and the axioms.

When expressed thus, propositional logic is referred to as the propositional calculus (or sentential calculus).

In fact, there is more than one way to define propositional logic as a formal system.

So although it is referred to as the propositional calculus, it is preferable to talk about a propositional calculus.

However, it is worth pointing out that although the formalizations themselves may vary considerably, the underlying system of logic that they define is in fact the same.

Similarly with propositional logic being referred to as PropLog, it is often abbreviated to PropCalc.

Definitions specific to this category can be found in Definitions/Propositional Calculus.

Specification

The propositional calculus can be expressed as a formal system.

We will use $\mathcal L_0$ to represent the formal language used to define propositional calculus as follows.

The Alphabet of Propositional Calculus

Propositional Symbols

The vocabulary of $\mathcal L_0$ can be any set $\mathcal P_0$ of arbitrary symbols.

It is usual to specify them as a limited subset of the English alphabet with appropriate subscripts.

A typical set of letters would be, for example:

$\mathcal P_0 = \left\{{p_1, p_2, p_3, \ldots, p_n, \ldots}\right\}$

The letters of $\mathcal L_0$, i.e. the elements of $\mathcal P_0$, are referred to as the propositional symbols of $\mathcal L_0$.

Some sources call the elements of $\mathcal P_0$ the propositional variables of $\mathcal L_0$.

Signs

The signs of the alphabet of $\mathcal L_0$ usually include (but may be a subset of) the following:

Connectives

• The signs $\land, \lor, \implies, \iff$ are called the binary connectives.

• The sign $\neg$ is called the unary connective.

Together they are known as the connectives of $\mathcal L_0$.

Length of Symbols

Whether subscripted or not, however they are defined, the elements of $\mathcal P_0$ are defined as having a length of $1$.

The signs of $\mathcal L_0$ are also defined to have length $1$.

Thus, each of the symbols of $\mathcal L_0$ is considered to have a length of $1$.

WFFs of Propositional Calculus

A WFF of propositional calculus, or just propositional WFF, can be specified in the following ways:

Formal Grammar: Backus-Naur Form

A WFF of $\mathcal L_0$ is a string generated by the following formal grammar expressed in Backus-Naur form:

Note that this is a top-down grammar: we start with a metasymbol <formula> and progressively replace it with constructs containing other metasymbols and/or primitive symbols, until finally we are left with a well-formed formula of $\mathcal L_0$ consisting of nothing but primitive symbols.

Formal Grammar: Bottom-Up Approach

A WFF of $\mathcal L_0$ is a string generated by finitely many applications of the following rules of formation.

• Let $\mathcal P_0$ be the vocabulary of $\mathcal L_0$.
• Let $Op = \left\{{\land, \lor, \implies, \iff}\right\}$.

The rules are:

Any string which can not be created by means of the above rules is not a WFF.

Abbreviation of WFFs

The WFFs of propositional calculus can be made more readable by allowing them to be abbreviated. The resulting strings are not actually WFFs as such, but can be translated back uniquely into full WFFs.

Rules for Abbreviation of WFFs

• The outermost brackets of a WFF need not be written.

• Brackets can be removed around parts of nested WFFs if the inner WFF has a higher precedence than the outer one.

• In the case of repeated $\land$ or $\lor$ connectives, we can replace:

$\left({\left({\mathbf A \land \mathbf B}\right) \land \mathbf C}\right)$ with $\left({\mathbf A \land \mathbf B \land \mathbf C}\right)$

but not

$\left({\mathbf A \land \left({\mathbf B \land \mathbf C}\right)}\right)$ with $\left({\mathbf A \land \mathbf B \land \mathbf C}\right)$

(there is a reason for this).

Standard Abbreviation

Any string obtained from a WFF $\mathbf A$ by applying any of the above rules is called an abbreviation of $\mathbf A$.

The string obtained by applying as many of the above rules to a WFF $\mathbf A$ as possible is known as the standard abbreviation of $\mathbf A$.

Thus it can be seen that there may be several abbreviations of a WFF, but only one standard abbreviation.

Precedence of Binary Connectives

The precedence of the binary connectives used in propositional calculus is defined as follows (highest precedence at the top):

• $\land$
• $\lor$
• $\implies$
• $\iff$