Higher-Order Logic with Isabelle/HOL

Higher-Order Logic with Isabelle/HOL#

Author: Spencer Au

Topics#

  • Higher-order logic foundations

  • Function types and quantification

  • Isabelle/HOL advanced features

  • Theorem proving strategies

  • Industrial theorem proving

10.1 Idea and Introduction#

WIP

This chapter extends to higher-order logic in Isabelle/HOL, showing how to reason about functions as first-class objects and exploring the foundations of modern theorem proving.

Higher-order logic (HOL) extends the capabilities of first-order logic (FOL) by allowing quantifiers (such as \( \forall x \) and \( \exists x \)) to range over functions and predicates, not just individual elements. In addition, functions can be passed as arguments to other functions, returned as results, and manipulated just like any other data type. This enables more expressive statements about the properties of functions and their relationships.

10.2 Basic Theory#

10.2.1 First Order Logic#

WIP \( \forall x \) and \( \exists x\) where x is a variable/individual element

In higher order logic, we extend this to \( \forall f(x) \) and \( \exists f(x) \), where x is a function that takes x as an input

10.2.2 (Explicit) Type System#

WIP

10.2.3 Lambda Abstraction#

WIP

10.2.4 Rules of Inference#

The basic rules of inference of \(\mathcal{F}^w\), where \(\mathcal{F}\) is a system of \(\mathcal{w}\)-order logic which has all finite order logics as subsystems:

  1. Modus Ponens From \(A\) and \(A \to B\) to infer \(B\).

  2. Generalization From \(A\) to infer \(\forall x\,A\), where x is a variable of any type

Adapted from Andrews, 2002[1] using modern logic convention.

10.2.5 Axiom Schemata#

The axiom schemata of \(\mathcal{F}^w\) are:

  1. \(A \lor A \to A\)

  2. \(A \to (B \lor A)\)

  3. From \(A \to (B \to C)\), infer \( (A \to B) \lor C\)

  4. Universal Instantiation \(\forall x_\tau\,A \to A[y_\tau / x_\tau]\), where \(y_\tau\) is a variable or constant of the same type as the variable \(x_\tau\), and \(y_\tau\) is free for \(x_\tau\) in \(A\).

    Basically, from \(\forall x_\tau\,A\), we may infer \(A[y_\tau / x_\tau]\), meaning that if \(A\) holds for all \(x_\tau\), then it also holds for any particular instance \(y_\tau\) of the same type.

  5. Quantifier Distribution \(\forall x(A \lor B) \to (A \lor \forall x\,B)\), where \(x\) is any variable not free in \(A\).

    This means that if \((A \lor B)\) holds for all \(x\), and \(A\) does not depend on \(x\), then either \(A\) holds or \(B\) holds for all \(x\).

  6. Comprehension Axioms

    • 0-ary case (a proposition/Boolean) that names a theorem/statement.
      \( \exists u_{\mathbf{o}}\;[\,u_{\mathbf{o}} \leftrightarrow A\,] \) where \(u_{\mathbf{o}}\) does not occur free in \(A\).

    • n-ary case (a predicate/function of arity n) that names a property/relation.
      \(\exists u_{(\tau_1\ldots\tau_n)}\; \forall v^{1}_{\tau_1}\cdots \forall v^{n}_{\tau_n}\, \big[\,u_{(\tau_1\ldots\tau_n)}(v^{1}_{\tau_1},\ldots,v^{n}_{\tau_n}) \leftrightarrow A\,\big]\) where \(u_{(\tau_1\ldots\tau_n)}\) does not occur free in \(A\), and \(v^{1}_{\tau_1},\ldots,v^{n}_{\tau_n}\) are distinct variables.

    • These axioms allow us to define new symbols that stand for existing formulas.
      In the 0-ary case, a new propositional constant \(u_{\mathbf{o}}\) can name a statement \(A\).
      In the n-ary case, a new predicate \(u_{(\tau_1\ldots\tau_n)}\) can be introduced so that \(u(v^1,\ldots,v^n)\) is true exactly when \(A\) holds for those arguments.

  7. Axioms of Extensionality

    • 0-ary case (a proposition/Boolean) that names a theorem/statement.
      \((x_{\mathbf{o}} \leftrightarrow y_{\mathbf{o}}) \to (x_{\mathbf{o}} = y_{\mathbf{o}})\)

    • n-ary case (a predicate/function of arity n) that names a property/relation.
      \(\forall w^{1}_{\tau_1} \ldots \forall w^{n}_{\tau_n} [(x_{(\tau_1 \ldots \tau_n)}w^{1}_{\tau_1}\ldots w^{n}_{\tau_n}) \leftrightarrow (y_{(\tau_1 \dots \tau_n)} w^{1}_{\tau_1} \ldots w^{n}_{\tau_n})] \to (x_{(\tau_1 \ldots \tau_n)} = y_{(\tau_1 \ldots \tau_n)}) \)

    • These axioms state that two expressions are equal if and only if they behave identically in that their output result is the same in all evaluations. This formalizes the idea that in higher order logic, equality is extensional (based on meaning and behavior) rather than syntactic (based on form).

Adapted from Andrews, 2002[1] using modern logic convention.

10.3 Tool (Installation, First Example, First Exercise)#

10.3.1 Installation#

Installation Link for Isabelle

Isabelle processes the theory document incrementally in the background, meaning that there is no additional “compile” or “run” step. As you type in lines and commands, the background system will check them and automatically update the proof state and any relevant error reports. Just go line by line, or command by command in order to check the related output.

Isabelle uses *.thy (theory) files, and the general structure of the theory files is like this:

theory THEORY_NAME
    imports OTHER_THEORIES

begin

THEORY_BODY

end

theory THEORY_NAME declares the theory name and must exactly match the .thy filename. For example, if the file is called test.thy, then you would have theory test

imports OTHER_THEORIES tells it to import another theory; for example, one popular theory to import is Main.thy, which includes support for natural numbers, lists, and basic arithmetic

begin is the entry point into the theory body, while end is the end point of the theory body

10.3.2 Proof Solving via Sledgehammer#

10.3.3 First Example - Add Function#

For the first example, the goal will be to implement recursive addition via a function called “add”. The general form should be:

fun add :: "nat ⇒ nat ⇒ nat" where
    "base case"
    "recursive case"

where two natural numbers are added, and the result is a natural number that is the sum of the two input numbers. For example, sum m n should return the sum of m and n.

Show Answer
fun add :: "nat ⇒ nat ⇒ nat" where
  "add 0 n = n" |
  "add (Suc m) n = Suc (add m n)"

For a detailed explanation, See Section 10.3.2 Exercises

10.3.4 First Exercise - Associativity and Communativity of Add#

For the first exercise, we will be proving the associative and commutative properties of a custom add function in Isabelle. This exercise comes from Exercise 2.2 of Concrete Semantics Exercises

The custom add function is defined here:

Show Answer
fun add :: "nat => nat => nat" where
    "add 0 n = n" |
    "add (Suc m) n = Suc(add m n)"

We use 2 lemmas to prove each part of the exercise, namely:

lemma add_assoc: "add (add m n) p = add m (add n p)"
lemma add_comm: "add m n = add n m"

The full lemma proof for associativity is here:

Show Answer
lemma add_assoc: "add (add m n) p = add m (add n p)"
proof (induction m) 
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed

For a detailed explanation, See Section 10.3.3 Associative Property

Next, to prove the communative property, we will first prove 2 helper lemmas:

lemma add_0_right: "add m 0 = m"
lemma add_Suc_right: "add m (Suc n) = Suc (add m n)"

The helper lemma proofs for communativity

Show Answer
lemma add_0_right: "add m 0 = m"
proof (induction m)
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed

lemma add_Suc_right: "add m (Suc n) = Suc (add m n)"
proof (induction m)
  case 0
  show ?case by simp
next
  case (Suc m)
  show ?case by (simp add: Suc.IH)
qed

With the helper lemmas proven, we will use them to prove the commutative property

Show Answer
lemma add_comm: "add m n = add n m"
proof (induction m)
  case 0
  show ?case
    by (simp add: add_0_right)
next
  case (Suc m)
  show ?case
    by (simp add: Suc.IH add_Suc_right)
qed

For a detailed explanation, See Section 10.3.3 Communative Property

10.4 Introductory Examples - Tower of Hanoi or Insertion Sort#

Tower of Hanoi or Insertion Sort

10.5 The Landscape of Tools#

WIP

10.5.1 Interactive Proof Assistants#

HOL4 (classic HOL)

Coq (constructive higher-order/type theory)

Lean 4 (modern dependent/HOL hybrid)

10.5.2 Automated Higher Order Prover#

Leo III

Satallax

10.6 Algorithms#

10.7 Benchmark and Competitions#

10.8 Applications in Industry#

this is just scaffolding template for now; will add more detail and refine later

complex addressing hardware in SoCs via formal models in Isabelle/HOL

HOL-based systems used to verify hardware modules and FPGA implementations

Isabelle/HOL use in steam boiler system, process control (Steam Boiler System), data transmission (FlexRay communication protocol), memory and processing components (Automotive-Gateway System). (cite - https://arxiv.org/abs/1405.1512?)

Because these tools provide mathematical assurance of correctness (rather than testing alone), they are particularly suited to safety-critical systems (avionics, automotive safety, SoC design) where fault risk must be minimized and certification standards demands high trust.

10.9 Case Studies#

10.10 History#

10.10.1 Origins of Higher Order Logic#

Alonzo Church’s work in the 1930s (via \(\lambda\)-calculus) and Leon Henkin’s work in the 1950s (on general models semantics) lay the foundation for higher order logic. From their contributions arose an extension of First Order Logic (FOL) that allows quantification over predicates and functions, enabling reasoning about functions as first class entities

In the 1970s, Robert Milner develops LCF (Logic for Computable Functions) at Stanford and later Edinburgh, introducing the idea of an interactive theorem prover. LCF pioneers the use of a tactic-based proof automation and the ML meta language, which is designed to let users safely define proof strategies. ML later evovles into OCaml and Standard ML.

In the early 1980s, Michael J. C. Gordon builds upon LCF in order to create the HOL system, which explicitly uses higher-order logic as its core formalism. This HOL system would become the foundation for hardware verification, paving the way and influencing later provers like HOL4 and Isabelle/HOL.

10.10.2 Development of Isabelle/HOL#

Developed in the late 1980’s by Lawrence C. Paulson at Cambridge, Isabelle was created as a generic theorem proving framework capable of supporting multiple logical formalisms under a single meta-logic.

The HOL instantiation of Isabelle (Isabelle/HOL) became the most widely adopted version due to its strong expressiveness and balance between automation and manual control.

Isabelle introduced the Isar prof language in the 2000s, allowing structured and human readable proofs, improving clarity over traditional tactic-based approaches like in LCF.

Integration with automated tools such as Sledgehammer and SMT solvers further extend its power, bridging interactive reasoning and automation.

The creation of the AFP (Archive of Formal Proofs) established a reusable library of formalizd mathematics and computer science, solidifying Isabelle/HOL’s role in both academia and industry.

10.11 Current Development, Research Challenges, Conferences and Workshops#

10.12 References#

[1] Andrews, An Introduction to Mathematical Logic and Type Theory. Springer, 2002. Springer Link

10.13 Suggestions for Future Work#

Contents