# Re: [isabelle] The HOL-Omega Tutorial is now available

There was a bug in the previous version of the HOL-Omega system which
prevented it from building with Poly/ML 5.5, the current version of Poly/ML.

This has been fixed and posted to the public repository for HOL-Omega, and
the current version should build correctly. If anyone has tried building HOL
-Omega and been frustrated, please try again with this new version of HOL-
Omega.

Many thanks to Robert Solovay for reporting this bug.

Sincerely,

Peter V. Homeier

On Sat, Feb 9, 2013 at 3:59 PM, Peter Vincent Homeier <
palantir at trustworthytools.com> wrote:

> I am pleased to announce that, as promised, the HOL-Omega Tutorial is now
> available, at
>
>
> http://www.trustworthytools.com/holw/tutorial.pdf
>
>
> The HOL-Omega system is a significant extension of the popular and mature
> HOL4 theorem prover, which has been under development for twenty-five
> years. The HOL-Omega logic is virtually completely backwards compatible
> with HOL4, so that libraries, applications, and developments written for
> HOL4 will work in HOL-Omega without any changes, with very few exceptions.
>
>
> HOL4 users are thus encouraged to investigate HOL-Omega without any loss
> of functionality.
>
>
> But HOL-Omega adds significant new power of interest to all users of
> theorem provers, primarily centered around two key ideas, and what flows
> from each:
>
>
> (1) Types can be abstracted by type variables (similar to how terms are
> abstracted by term variables in the lambda calculus).
>
>
> --- Type operators are curried, so that they may take one argument at a
> time.
>
> --- Every type has a {\it kind}; kinds determine which type applications
> are sensible.
>
> --- Type variables can represent type operators.
>
>
> (2) Terms can be abstracted by type variables (similar to System F).
>
>
> --- The type of such an abstraction is a universal type.
>
> --- Such an abstraction may be applied as a function to a type argument.
>
> --- Such applications are managed by classifying all types into ranks.
>
>
> These extensions of traditional higher order logic in a classical setting
> were thought impossible for many years, proven to be inconsistent according
> to Girard's paradox. But by the careful structuring of the type system by
> ranks, soundness is maintained and Girard's paradox is defeated.
>
>
> This means that unlike other advanced-logic theorem provers that restrain
> their logics to an intuitionistic logic, HOL-Omega is a higher order
> logic in a fully classical setting, where the law of the excluded middle
> holds, equality of functions or predicates can be proven by extensionality,
> the Hilbert epsilon operator is available for non-deterministic choice, and
> all types are inhabited, supporting traditional HOL theorems like |- (!x.
> P x) ==> (?x. P x).
>
>
> The effect of these design choices is that the HOL-Omega logic is much
> more congenial, intuitive, and easy to work in than an intuitionistic
> logic, while still providing the powerful new forms of abstraction listed
> above.
>
>
> If the reader is interested and would like to try it, instructions for
> obtaining and installing theHOL-Omega system may be found at
>
>
> http://www.trustworthytools.com/id17.html
>
>
> Sincerely,
>
>
> Peter V. Homeier
>
>
> --
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)

--