# Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

For most proof assistants the name alone is common, E.g. Coq, Lean but with Isabelle it is often seen as Isabelle/<xyz>?
Why the two parts?

What is

• Isabelle/HOL
• Isabelle/FOL
• Isabelle/ZF
• Isabelle/ISAR
• Isabelle/Proof General

Are there others?

Isabelle the program is designed as a "generic" LCF-style proof assistant/logical framework; it gives you a very minimal base logic (based on Church's simple type theory (pdf) and called Isabelle/Pure) and some infrastructure to declare new types, typeclasses (ref), constants, and judgment forms, postulate new axioms and rules, and basic tactics for performing logical reasoning therein.

Using this logical framework, and writing ML code (Poly/ML) to interface with it, one can develop object logics (pdf) and other applications x within Isabelle; these are then called "Isabelle/x".

x = HOL, FOL, ZF, ... are object logics, they encode the rules of the particular logic in the language of Isabelle/Pure, and extend the framework with extra functionality for e.g. defining recursive functions, new tactics, theory libraries of formalizations, etc.

x = Isar is an extension of the original Isabelle framework to allow for declarative proofs; it's now been very tightly integrated into Isabelle, but in the beginning proofs were done tactic-style, similar to how it's still done (I believe) in the HOL family of ITPs.

x = Proof General is, I assume, the PG interface of the Isabelle prover.

To name a couple more interesting applications, there's Isabelle/auto2 by Bohua Zhan, it's a saturation-based theorem prover tool that enables very declarative proofs that don't require explicit tactic invocations after each claim. This allows for proofs that read quite similar to ones on paper, see e.g. here.

I myself have tried to develop HoTT as an object logic, but it's not currently being actively worked on.

I suppose this is similar to how Metamath works, but I'm not an expert on that.

• I was finishing my own answer when yours appeared. I'm leaving it for a while just in case Feb 17, 2022 at 12:08
• Very minor but mildly important squabble: I would push back a little, and point out that Isabelle is a meta-logical framework (which is stronger than "just" a logical framework because we can prove results about the object logic, whereas logical frameworks only facilitate reasoning within an object logic). (But this is an excellent answer, otherwise a minor point about a prefix.) Feb 17, 2022 at 20:36
• @GuyCoder I'm ready: what're your queries? Feb 17, 2022 at 23:02
• @GuyCoder I believe this is answered in "Rewriting logic as a metalogical framework" by David Basin, Manuel Clavel, and Jos Meseguer; the tl;dr is Isabelle does not provide sufficient mechanization of induction on its own, whereas Isabelle/HOL does. Feb 18, 2022 at 16:24