# Intuitionistic Higher-Order Logic

The framework of proofgold is intuitionistic higher-order logic. This consists of a collection of simple types, simply typed terms and Curry-Howard style proof terms. A quick summary is given by the following grammar:
 Types (α, β) ::= Prop | Base n | (α → β) Terms (s, t) ::= x | Prim n | (s t) | (λ x:α . t) | (s → t) | (∀ x:α . t) | (∃ x:α . t) | (s =α t) Proofs (D, E) ::= u | Known s | (D E) | (D t) | (λ u:s . D) | (λ x:α . D) | (Ext α β)
Here n ranges over natural numbers and x ranges over term variables and u ranges over proof variables. Technically, term variables and proof variables are de Bruijn indices in the implementation.

In the implementation there is an additional term case that references a term by its hashroot. Also, the term in the Known proof case is always referenced by the hash root of the (allegedly) known proposition. A proposition can be known because it is an axiom of the current theory or if it has been proven in the theory.

The last two term cases (∃ and =) are included only for convenience and as part of normalization ∃ and = are expanded away as follows:
 (∃ x:α . s) expands to (∀ p:Prop . (∀ x:α . s → p) → p) (s =α t) expands to (∀ q:α → α → Prop. q s t → q t s)

The proof terms have the standard Curry Howard meaning. The last case (Ext α β) corresponds to functional extensionality. For two types α and β, (Ext α β) is a proof term for (∀ f g : αβ . (∀ x : α . f x =β g x) → (f =αβ g)).

## Specifying types, terms and proofs in Proofgold documents

Proofgold can read drafts of documents (and signatures and theories) using a basic "assembly" language (using prefix notation). See the commands readdraft, commitdraft and publishdraft. This assembly language is summarized below.

### Types

If Base types will be used, then the text should declare names for them as follows:
Base base0
...
Base basen-1
After this types can be written as follows:
AssemblyInformal
PropProp
basenBase n
TpArr α β (αβ)

### Terms

Closed terms that will be used often can be abbreviated by Let declarations, as follows:
Let letname : α := s
The Let declarations are completely transparent and are expanded away while reading the specification.

Proper definitions are declared as follows:
Def defname : α := s
These definitions are associated with the hash root of the term s and this hash root is used when reading specified terms.

Opaque definitions can also be declared by referencing the hash root. This assumes the definition has already been made and published in a previous document.
Param hashroot defname : α

Terms can be specified as follows:
AssemblyInformal
letname (term declared using Let earlier)
defname (term hash root declared using Def or Param earlier)
x x (local variable in the scope of λ, ∀ or ∃)
Prim n Prim n
Ap s t (s t)
Lam x α t x : α . t)
Imp s t (st)
All x α t (∀ x : α . t)
Ex x α t (∃ x : α . t)
Eq α s t (s =α t)

### Proofs

Axioms and previously proven theorems can be locally declared as follows:
Known knownname : s
The hash root of s is computed and checked to be in the collection of already known propositions.

Proofs are specified as follows:
AssemblyInformal
knownname (declared using Known earlier)
u u (proof variable in the scope of a λ)
PrAp D E (D E)
TmAp D t (D t)
PrLa u s D u : s . D)
TmLa x α D x : α . D)
Ext α β (Ext α β)