Isabelle's Logics

Isabelle can be viewed from two main perspectives. On the one hand it may serve as a generic framework for rapid prototyping of deductive systems. On the other hand, major existing logics like Isabelle/HOL provide a theorem proving environment ready to use for sizable applications.

The Isabelle distribution includes a large body of object logics and other examples (see the Isabelle theory library).

Isabelle/HOL
is a version of classical higher-order logic resembling that of the HOL System.
Isabelle/HOLCF
adds Scott's Logic for Computable Functions (domain theory) to HOL.
Isabelle/FOL
provides basic classical and intuitionistic first-order logic. It is polymorphic.
Isabelle/ZF
offers a formulation of Zermelo-Fraenkel set theory on top of FOL.

Isabelle/HOL is currently the best developed object logic, including an extensive library of (concrete) mathematics, and various packages for advanced definitional concepts like (co-)inductive sets and types, well-founded recursion etc. The distribution also includes some large applications, for example correctness proofs of cryptographic protocols (HOL/Auth) or communication protocols (HOLCF/IOA).

Isabelle/ZF provides another starting point for applications, with a slightly less developed library. Its definitional packages are similar to those of Isabelle/HOL. Untyped ZF provides more advanced constructions for sets than simply-typed HOL.

There are a few minor object logics that may serve as further examples: CTT is an extensional version of Martin-Löf's Type Theory, Cube is Barendregt's Lambda Cube. There are also some sequent calculus examples under Sequents, including modal and linear logics. Again see the Isabelle theory library for other examples.

Defining Logics

Logics are not hard-wired into Isabelle, but formulated within Isabelle's meta logic: Isabelle/Pure. There are quite a lot of syntactic and deductive tools available in generic Isabelle. Thus defining new logics or extending existing ones basically works as follows:

  1. declare concrete syntax (via mixfix grammar and syntax macros)
  2. declare abstract syntax (as higher-order constants)
  3. declare inference rules (as meta-logical propositions)
  4. instantiate generic automatic proof tools (simplifier, classical tableau prover etc.)
  5. manually code special proof procedures (via tacticals or hand-written ML)

The first three steps above are fully declarative and involve no ML programming at all. Thus one already gets a decent deductive environment based on primitive inferences (by employing the built-in mechanisms of Isabelle/Pure, in particular higher-order unification and resolution). For sizable applications some degree of automated reasoning is essential. Instantiating existing tools like the classical tableau prover involves only minimal ML-based setup. One may also write arbitrary proof procedures or even theory extension packages in ML, without breaking system soundness (Isabelle follows the well-known LCF system approach to achieve a secure system).