Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Mechanized HOL Reasoning in Set Theory

Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kunčak

TL;DR

A mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms yields a form of soft type system supporting top-level polymorphism and ADTs over set theory, and offer tools to reason about functions in set theory.

Abstract

We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory. HOL proof steps are implemented as proof producing tactics in Lisa, and the types are interpreted as sets, with function (or arrow) types coinciding with set-theoretic function spaces. The embedded HOL proofs, as opposed to being a layer over the existing proofs, are interoperable with the existing library. This yields a form of soft type system supporting top-level polymorphism and ADTs over set theory, and offer tools to reason about functions in set theory.

Mechanized HOL Reasoning in Set Theory

TL;DR

A mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms yields a form of soft type system supporting top-level polymorphism and ADTs over set theory, and offer tools to reason about functions in set theory.

Abstract

We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory. HOL proof steps are implemented as proof producing tactics in Lisa, and the types are interpreted as sets, with function (or arrow) types coinciding with set-theoretic function spaces. The embedded HOL proofs, as opposed to being a layer over the existing proofs, are interoperable with the existing library. This yields a form of soft type system supporting top-level polymorphism and ADTs over set theory, and offer tools to reason about functions in set theory.
Paper Structure (15 sections, 10 theorems, 27 equations, 2 figures)

This paper contains 15 sections, 10 theorems, 27 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Preliminaries
  4. Set-Theoretic Semantics of HOL
  5. From HOL Formulas to First-Order Set Theory Formulas
  6. HOL in FOST Using Contexts
  7. Proof of Type Checking
  8. Simulating HOL Proofs
  9. Defining new constants
  10. Formalizing Algebraic Data Types
  11. Importing Proofs from HOL Light
  12. Conclusion
  13. Appendix
  14. Deduction Rules and axioms for FOL and ZF
  15. ZF Transfinite Recursion Schema

Key Result

Theorem 2.1

Let $K$ be a first order theory (for example, FOST), and $\phi$ a formula with free variables $y, x_1,...,x_n$. Suppose $\vdash_K \forall x_1,...,x_n \exists ! y. \phi$ and let the theory $K'$ be $K$ with the addition of a function symbol $f$ of arity $n$ and the axiom $\forall y, y = f(x_1,...,x_n)

Figures (2)

  • Figure 1: Deduction rules for higher-order logic as implemented in HOL Light.
  • Figure 2: Deduction rules for first order logic with equality.

Theorems & Definitions (25)

  • Theorem 2.1: Extension by Definition for First Order Logic
  • Definition 2.2: Set theoretic universe
  • Definition 2.3: Semantics of HOL
  • Definition 2.4: Syntactic and Semantic truth
  • Theorem 2.5
  • Theorem 2.6
  • Definition 3.1: Embedding of HOL into FOST
  • Definition 3.2: Non-Emptiness Context
  • Definition 3.3: Typing Context
  • Definition 3.4: Definitional Context
  • ...and 15 more