# How to deal with axioms in a proof assistant?

I'm currently formalizing a little language which has somehow ended up looking a lot like Lawvere theories/finite product theories. I guess it's starting to look a little like Twelf?

What I would love to do within the framework of the language I'm building up is postulate types, multiary terms and multiary relations much like the function symbols and relation symbols of a first order theory.

For example with something like IZF you should be able to postulate a type of sets, a membership relation and various function symbols like empty sets and pairing.

Axiom set: type.

Axiom member: set -/> set.

Axiom empty: 1 -> set.
Axiom pair: set * set -> set.
Axiom union: set -> set.
Axiom infinity: 1 -> set.


I'm still not at all sure how I'm going to deal with axiomizing semantics like a possible rule for empty sets Axiom notamember: member empty |- false.

I've run into the need to treat axioms separately from ordinary free variables or axiomizing them within the metalogical framework and I've been thinking about the issue for a while now so I'm curious what people think here.

The first approach I mentioned treats axioms as free variables.

Something like

Axiom extensionality: forall A B (f g: A -> B), (forall x. f x = g x) -> f = g.


being treated as almost but not quite the same as being merely shorthand for adding a parameter of type forall A B (f g: A -> B), (forall x. f x = g x) -> f = g to a definition.

However, this approach has troubles dealing with universe issues and also cannot handle substructural systems which entirely lack exponential types (function types.) Axioms should also be usable multiple times not just once.

Somewhat this issue dovetails with some of the details explored with definitorial expansion in this question on definite description operators.

My current approach is to add a constructor which only permits type variables as results.

Aside from my actual code using a bidirectional style my approach is basically similar to

$$\frac{\Gamma \vdash e \colon \tau}{\Gamma \vdash (\textit{K}\colon \tau \rightarrow \textit{A}) e \colon \textit{A}}$$

With a big step rule evaluating under a list of substitutions much like

$$\frac{e \circ \rho \Downarrow e'}{ ((\textit{K}\colon \tau \rightarrow \textit{A}) e) \circ \rho \Downarrow (\textit{K}\colon \tau \rightarrow \textit{A}) e'}$$

Because you can only create axioms landing in type variables you maintain nice computation properties for tuples and other primitive sorts.

I think I might add in a primitive sort of natural numbers at most but I'd still rather not bother with people declaring axioms like (* between 2 and 3 *) Axiom thwomble: 1 -> nat.

In the future it might be nicer to thread an extra context through for axioms but I don't know how I feel about this considering I already have to deal with threading a useage context through as well for linear typing purposes.

$$\frac{\begin{split} \textit{K} \colon \tau \rightarrow \textit{A} \in \Delta\\ \Delta ; \Gamma \vdash e \colon \tau \end{split}}{\Delta ; \Gamma \vdash \textit{K} e \colon \textit{A}}$$

In full I might end up with 3 or so sorts in a context: a useage context; a type context; and a context of axiomized types, relations and constructors.

I think that plumbing through an extra "axiom context" is probably best even it's annoying but I'm interested in hearing other people's thoughts and I wonder if there's any papers on the subject. I guess there stuff on adding rewrite rules but I'm not really sure much attention is put on the mechanics of axioms themselves?