\( \DeclareMathOperator{\tr}{tr} \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}} % For +---- metric \newcommand{\BDpos}{} \newcommand{\BDneg}{-} \newcommand{\BDposs}{\phantom{-}} \newcommand{\BDnegg}{-} \newcommand{\BDplus}{+} \newcommand{\BDminus}{-} % For -+++ metric \newcommand{\BDpos}{-} \newcommand{\BDposs}{-} \newcommand{\BDneg}{} \newcommand{\BDnegg}{\phantom{-}} \newcommand{\BDplus}{-} \newcommand{\BDminus}{+} \)
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: Sat, 30 Apr 2022 10:01:45 -0700