Formal systems

This post is a generalization to one of my previous posts, Hierarchy of logical systems.

Wikipedia states the following definition of a formal system:

A formal system is any well-defined system of abstract thought based on the model of mathematics

More formally, a formal system is consisted of:

1. A formal language, i.e.
   1. A finite set of symbols, that can be used for constructing formulas (i.e. finite strings of symbols).
   2. A grammar, which tells how well-formed formulas (abbreviated wff) are constructed out of the symbols.
2. A set of axioms.
3. A set of inference rules.

Once we defined a formal system, other systems can extend it.

For example, the ZFC set theory is based on first-order logic, which itself is based on propositional logic which is a formal system.

In general, we often put our focus on which parts of mathematics can be formalized in particular formal systems, rather than trying to find a theory in which all of mathematics can be developed, for the reason below.

Gödel’s incompleteness theorem states that there doesn’t exist* a formal system that is both complete and consistent.

Note that the statement above is about systems that allow expressing arithmetic of natural numbers (e.g. Peano, ZFC, but first-order logic also has some paradoxes if we allow self-referential statements).

In other words, for every such formal system, we will have either:

1. There will be statements that are true in that system, but which cannot be proved to be true inside the system (incomplete).

   A quick example is the statement “This statement is not provable”.
   The statement can either be true or false:
   True: It is not provable.
   False: It is provable, but we’re trying to prove something false.
   Thus the system is incomplete, because some truths are unprovable.

2. There will be a theorem in the system that is contradictory (inconsistent).

   We can start with the following statement: “This statement is false”.

   This statement is true if and only if it is false, and therefore it is neither true nor false (inconsistent).

The proof above tells us that we should keep thinking about our formal systems outside of their own definition, i.e. as the famous saying goes to think outside of the box, in order to improve our systems. Similarly to how we sometimes do meta-thinking to improve ourselves.

In conclusion, formal systems are our attempt to abstract models, whenever we reverse engineer nature in attempt to understand more. They may be imperfect, but can be very useful for our understanding.

We will look at an example of a formal system in my next post.