HOHF Theory

The logical framework of proofgold is intuitionistic higher-order logic. Different theories (declaring typed constructors and axioms) can be included on top of this framework. Proofgold builds in a (classical) higher-order theory of hereditarily finite sets (HOHF). The reward bounty propositions until Block 5000 were all conjectures relative to this specific theory.

The details of this theory can be printed with the command:
theory 6ffc9680fbe00a58d70cdeb319f11205ed998131ce51bb96f16c7904faf74a3d
The implementation is in the file checking.ml. Here we give a high level description.

The types consist of Prop (which we abbreviate as o below), one base type we call ι and all function types constructed from these. Two axioms (double negation and propositional extensionality) will imply o has (only) two elements (True and False). Constructors and axioms will imply ι consists of the hereditarily finite sets, and hereditarily finite sets will give the only standard model of the theory.

Primitive Typed Constructors

There are 104 primitive constructors, but 98 of these have a meaning determined by a definitional axiom. The only primitives for which there is no definitional axiom are: 0 [Eps_i] (a choice function), 7 [In] (set membership), 9 [Empty] (the empty set), 10 [Union] (union operator), 11 [Power] (power set operator) and 12 [Repl] (replacement set operator).

Axioms

There are 108 axioms. The first 10 are proper axioms and the remaining are definitional axioms.