What do "completely described" and "complete formalisation" mean?

113 Views Asked by At

From Wikipedia

In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems.

An axiomatic system that is completely described is a special kind of formal system; usually though, the effort towards complete formalisation brings diminishing returns in certainty, and a lack of readability for humans.

What do "completely described" and "complete formalisation" mean? Thanks.

1

There are 1 best solutions below

2
On

Take a look at a mathematical logic textbook, like George Boolos & John Burgess & Richard Jeffrey Computability and Logic (5th ed - 2007); you will find versions of "formalized" arithmetic [see page 214-on] : usually Peano arithmetic ($\sf PA$) or some subset of it, like Robinson arithmetic.

Those system are completely formalized because they are based on the syntax and proof system of first-order logic, i.e.

  • the language of the system is specified : rules for terms and formulae formation

  • a complete list of logical axioms and rules of inference

  • a rigorous definition of what means to be derivable in the system, i.e. a definition of theorem

  • an "explicit" list of non-logical axioms (the f-o version of Peano axioms).

Having done this, we are able - in principle - the check in a "mechanical" way :

  • if a string of symbols is a (well-formed) term or formula of the system

  • if a formula is an (instance of an) axiom (logical or not) of the system

  • if a sequence of formulae is a derivation, in which case the last formula of the sequence is a theorem.

But, and this is the real value of this approach, we can study the system itself mathematically; i.e. we can prove relevant "facts" about the system, "doing" metamathematics : consistency, completeness, relation with weaker and stronger systems, and so on...