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
- A formal system contains an alphabet of any symbols, called basic obs, and a method to combine them to get new obs.
- A formal system contains special obs, axioms, such that those axioms are per definition derivable in our system.
- A formal system contains deduction rules, which are uniquely determined by a finite sequence of obs, the premises, and a single ob at the bottom, the conclusion. If all the premises are derivable, the conclusion is too, per definition.
- Rules can also be derived. For this, it is necessary to derive the conclusion while the premises are being thought of as axioms in the derivation.
- Axiom schemes and rules might both contain metavariables, which are not part of the alphabet. Obs containing these will be formed in the same way as obs only containing symbols, but some (an indeterminate amount) of the symbols have been replaced by metavariables. Using those meta-obs, axiom schemes and rules can be formed. To derive actual axioms/rules or other axiom schemes from such meta-obs, any metavariables may be replaced again. In axiom schemes, they can be replaced by any ob or meta-ob. In rules, the same applies, as long as the replacement both happens in the conclusion and in the premises. The so-created axioms are also derivable per definition, same as the rules. Usually, it is not necessary to treat obs and meta-obs differently.
- There is also a premise that requires two metavariables to be replaced by entirely different obs, such that no part of e.g. \(x\) syntactically is \(y\) and the other way, it usually gets denoted \(x \not\equiv y\).
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?
- In set theory and logic: ZF(C) set theory is, as well as classical logic, just a formal system. It only uses one rule (modus ponens) and declares most things in axiom schemes, which makes it a Hilbert-style deduction system.
- In type theory and lambda calculi: Those theories are also quite easy to express in a formal systems, and are often intutionistic, which usually implies a need for contexts and a focus on inference rules. Systems mostly relying on such are often called natural deduction calculi.
- Literally everything in math: Mathematics relies on being exact, and a formal system is the most exact you can get. Most subdisciplines would gain a lot from clear definitions.
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.