Formal system

A formal system is a precisely defined mathematical framework for manipulating symbols according to explicit rules.
It typically consists of four core components:

1. Alphabet
   A fixed set of primitive symbols (e.g., logical connectives, variables, predicates, parentheses) from which all expressions are built.
2. Formation rules (syntax)
   A recursive specification of which finite strings of symbols count as well-formed formulas (WFFs). These rules are purely mechanical and do not depend on meaning or truth.
3. Axioms
   Distinguished well-formed formulas taken as starting points of the system. They are assumed to be valid without proof.
4. Rules of inference
   Transformation rules that allow the derivation of new well-formed formulas from existing ones, thereby defining the notion of theorem.

A key observation about rules of inference is the Carrollian regress: a rule of inference cannot be applied without already assuming that very rule. Rules are not self-executing — they require an external agent (a mathematician, a computer) to follow them.

Example

The MIU-system.

Key distinction

• Well-formedness (syntactic notion): determined solely by formation rules; independent of meaning.
• Provability (syntactic notion): determined by axioms and inference rules.
• Truth (semantic notion): defined only after interpreting the system in a model (isomorphism, in the sense of the book GEB of Hofstadter).
  A central idea in logic is that these layers are independent: a formula can be well-formed without being provable, and provable without being true in every model.