Using PL to Describe Properties of Systems

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:

• 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)$.

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:
  • $p\to (q\to p)$
  • $(p\to (q\to r))\to ((p\to q)\to (p\to r))$
  • $(\neg p\to \neg q)\to (q\to p)$
• 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.