Isabelle axiomatizations [isa-0019]

Isabelle's basic mechanism to define new things is the axiomatization command.

axiomatization (* constants *) where (* axioms *)

This defines the constants (with their types) in the constants section, and assumes the formulae stated in the axioms section.

Problem.

Isabelle does nothing to stop you from assuming false theorems as axioms in axiomatization commands, which can easily render the logic unsound. We shall later see safer ways to define new constants, which should be preferred over axiomatization in most cases.