[FOM] response to Lasse Rempe-Gillen (Re: Formal verification)

[Till Mossakowski]

Am 22.10.2014 21:13, schrieb Dustin Wehr:
> It is not acceptable in the Interactive Theorem Proving community because:
> -It uses an axiomatic definition of < for the natural numbers, rather
> than a definition in terms of a provably-halting recursive function.
> -It takes as axioms that:
>   - n! + 1 > n
>   - for all n and positive m ≤ n, m divides n!
>   - for all n and m > 2, if m divides n then m does not divide n + 1
>
>
It is no problem to use Isabelle with additional axioms, although this
style is indeed not advocated.
Moreover, you can use Isabelle locales to reason about the consequences
of axioms. The Isabelle community uses this feature e.g. to reason about
the theory of groups, the theory of vector spaces etc.
Another option is to state sentences like n! + 1 > n as theorems and
postpone their proofs, using Isabelle's "oops" or "sorry".

Best,
Till