Using PL to Describe Properties of Systems

View

This is a book resource with multiple pages. Navigate between the pages using the buttons.

Generic description of a propositional calculus

A propositional calculus is a formal system ${\mathcal {L}}={\mathcal {L}}\left(\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} \right)$ , where:

The alpha set $\mathrm {A}$ is a countably infinite set of elements called proposition symbols or propositional variables. Syntactically speaking, these are the most basic elements of the formal language ${\mathcal {L}}$ , otherwise referred to as atomic formulas or terminal elements. In the examples to follow, the elements of $\mathrm {A}$ are typically the letters p, q, r, and so on.
The omega set Ω is a finite set of elements called operator symbols or logical connectives. The set Ω is partitioned into disjoint subsets as follows:

$\Omega =\Omega _{0}\cup \Omega _{1}\cup \cdots \cup \Omega _{j}\cup \cdots \cup \Omega _{m}$ .

In this partition, $\Omega _{j}$ is the set of operator symbols of arity j.

In the more familiar propositional calculi, Ω is typically partitioned as follows:

$\Omega _{1}=\{\lnot \}$ ,

$\Omega _{2}\subseteq \{\land ,\lor ,\to ,\leftrightarrow \}$ .

A frequently adopted convention treats the constant logical values as operators of arity zero, thus:

$\Omega _{0}=\{\bot ,\top \}$ .

Some writers use the tilde (~), or N, instead of ¬; and some use v instead of $\vee$ as well as the ampersand (&), the prefixed K, or $\cdot$ instead of $\wedge$ . Notation varies even more for the set of logical values, with symbols like {false, true}, {F, T}, or {0, 1} all being seen in various contexts instead of $\{\bot ,\top \}$ .

The zeta set $\mathrm {Z}$ is a finite set of transformation rules that are called inference rules when they acquire logical applications.
The iota set $\mathrm {I}$ is a countable set of initial points that are called axioms when they receive logical interpretations.

The language of ${\mathcal {L}}$ , also known as its set of formulas, well-formed formulas, is inductively defined by the following rules:

Base: Any element of the alpha set $\mathrm {A}$ is a formula of ${\mathcal {L}}$ .
If $p_{1},p_{2},\ldots ,p_{j}$ are formulas and $f$ is in $\Omega _{j}$ , then $fp_{1}p_{2}\ldots p_{j}$ is a formula.
Closed: Nothing else is a formula of ${\mathcal {L}}$ .

Repeated applications of these rules permits the construction of complex formulas. For example:

By rule 1, p is a formula.
By rule 2, $\neg p$ is a formula.
By rule 1, q is a formula.
By rule 2, $\neg p\lor q$ is a formula.