\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Foundations of HOL

Table of Contents

1. Introduction

The foundations underlying HOL vary depending on implementation, but they are all variations on the same theme. Basically:

  • a simply-typed lambda calculus with:
    1. two base types (bool and ind for truth-values and non-logical constants, resp.), and
    2. some primitive symbols (like /\ [conjunction], \/ [disjunction], ==> [implies], <=> [logical equivalence], quantifiers — at least universal quantification).

We sometimes find type variables in the literature, but these are in the metalanguage and not HOL itself.

Last Updated 2022-04-30 Sat 09:07.