\( \DeclareMathOperator{\num}{number} \DeclareMathOperator{\wff}{wff} \newcommand{\ove}[2]{{\genfrac{}{}{0.5pt}{0}{#1}{#2}}} \)

\(\lambda\) Logic, Types, Functionality

To and beyond



Formal systems and what to do with them

Feb 29, 2019

What are formal systems?

Formal systems are a extremely simple yet powerful concept. They only consist of an alphabet (a collection of symbols), axioms, and inference rules. Axioms mark things (so-called obs) that are derivable (this word is somewhat similar to, but not the same as true) by definition, and inference rules consist of conditions that need to be furfilled to let another ob be derivable. Also, metavariables can be used, which state rules/axiom schemes for all obs.

A formal definition

Writing conventions

Axioms and axiom schemes are usually denoted as they are, used metavariables get listed beforehand. Rules are written \[ X \qquad Y \over Z \] where \(X, Y \) are the premises and \(Z\) is the conclusion. Read it as "Z follows from X and Y".

Additional information

Note that a rule only has one conclusion to keep the definition more basic, but if you needed a rule like \[ \begin{gather} X \qquad Y \over A \qquad B \end{gather} \] it'd be replaceable with two rules \[ \begin{gather} X \qquad Y \over A \\ \mbox{and}\notag\\ X \qquad Y \over B \end{gather} \]

Some examples: The systems \(\mathbb{N}_0\) and \(\mathbb{N}_{0\leq+}\)

Those systems are going to describe very basic relations between natural numbers. \(\mathbb{N}_0\) was taken and modified from CF58 . Used metavariables will be \(m,n,o\). The alphabet follows from used symbols. Axioms and rules will be stated here: $$ \begin{gather} \num 0 \tag{$\num$-I1} \\[8pt] \num n \over \num n' \tag{$\num$-I2} \\[8pt] \num n \qquad \num m \over \wff n = m \tag{$=$-F} \\[8pt] \vdash 0 = 0 \tag{$=$-I1} \\[8pt] \vdash n = m \over \vdash n' = m' \tag{$=$-I2} \\[8pt] \vdash n = m \over \vdash m = n \tag{$=$-symm} \\[8pt] \vdash n = m \qquad \vdash m = o \over \vdash n = o \tag{$=$-trans} \end{gather} $$ This system states three properties about obs: An ob is a number, an ob is a well-formed formula, and a ob is provable. It also states properties of equality etc. We can now prove things like 2 = 2: $$ \begin{gather} \qquad\ove{\ove{\vdash 0 = 0}{\vdash 0' = 0'}}{\vdash 0'' = 0''} \end{gather} $$ So you might see that in a treestyle deduction, you usually just put the premises of a used rule above the conclusion, and repeat that until you're using axioms. Now to be honest, you wouldn't consider this system exactly useful. There is not even a single operation defined, nor inequalities. So let's extend this with \(\leq\) and \(+\). $$ \begin{gather} \num n \qquad \num m \over \wff n \leq m \tag{$\leq$-F} \\[8pt] \num n \over \vdash 0 \leq n \tag{$\leq$-I1}\\[8pt] \vdash n \leq m \over \vdash n' \leq m' \tag{$\leq$-I2}\\[8pt] \vdash n = o \qquad \vdash n \leq m \over \vdash o \leq m \tag{$\leq=$-I1}\\[8pt] \vdash n = o \qquad \vdash m \leq n \over \vdash m \leq o \tag{$\leq=$-I2}\\[8pt] \vdash m \leq n \qquad \vdash n \leq o \over \vdash m \leq o \tag{$\leq$-trans} \\[8pt] \num n \qquad \num m \over \num (n + m) \tag{$+$-F} \\[8pt] \num m \over \vdash (0 + m) = m \tag{$+$-I1} \\[8pt] \num n \qquad \num m \qquad \num o \qquad m = n' \over \vdash (m + o) = (n + o)' \tag{$+$-I2} \end{gather} $$ This system is way more useful to play around with, because we can now prove things such as \(3+4\leq 9\). You might wonder why I listed the whole system if we are not going to use it now. That's because it is a fairly good example and will be needed for comparison and implementation in later articles. What you should know though is how addition recursively works: \(0+m\) is obviously \(m\). If the left summand is greater than 0, we take its predecessor, keep the right side untouched, and add one to the result.

Where are formal systems actually getting applied?

Pointing out the differences between classical and intutionistic/constructive is worth another article though.
However, we'll be taking a look at possible implementations of such systems soon.