Using PL to Describe Properties of Systems

Example 1. Simple axiom system

Let ${\mathcal {L}}_{1}={\mathcal {L}}(\mathrm {A} ,\Omega ,\mathrm {Z} ,\mathrm {I} )$ , where $\mathrm {A}$ , $\Omega$ , $\mathrm {Z}$ , $\mathrm {I}$ are defined as follows:

The set $\mathrm {A}$ , the countably infinite set of symbols that serve to represent logical propositions:

$\mathrm {A} =\{p,q,r,s,t,u,p_{2},\ldots \}$ .

The functionally complete set $\Omega$ of logical operators (logical connectives and negation) is as follows. Of the three connectives for conjunction, disjunction, and implication ( $\wedge ,\lor$ , and →), one can be taken as primitive and the other two can be defined in terms of it and negation (¬). Alternatively, all of the logical operators may be defined in terms of a sole sufficient operator, such as the Sheffer stroke (nand). The biconditional ( $a\leftrightarrow b$ ) can of course be defined in terms of conjunction and implication as $(a\to b)\land (b\to a)$ .

Adopting negation and implication as the two primitive operations of a propositional calculus is tantamount to having the omega set $\Omega =\Omega _{1}\cup \Omega _{2}$ partition as follows:

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

$\Omega _{2}=\{\to \}$ .

Then $a\lor b$ is defined as $\neg a\to b$ , and $a\land b$ is defined as $\neg (a\to \neg b)$ .

The set $\mathrm {I}$ (the set of initial points of logical deduction, i.e., logical axioms) is the axiom system proposed by Jan Łukasiewicz, and used as the propositional-calculus part of a Hilbert system. The axioms are all substitution instances of:
The set $\mathrm {Z}$ of transformation rules (rules of inference) is the sole rule modus ponens (i.e., from any formulas of the form $\varphi$ and $(\varphi \to \psi )$ , infer $\psi$ ).

This system is used in Metamath set.mm formal proof database.