HOL Zero has 10 primitive inference rules. These give basic properties about equality, lambda abstraction, propositional deduction and instantiation, and correspond to classic rules of typed lambda calculus and propositional logic. All of these rules work modulo alpha-equivalence.

The descriptions of these rules and the three axioms of HOL Zero are by Mark Adams (mark@proof-technologies.com).

This is the reflexivity rule for equality. It takes a term, and returns a theorem stating that this term is equal to itself, under no assumptions. There are no restrictions on the supplied term.

```
`t`
--------
|- t = t
```

This is the beta reduction conversion. It takes a lambda abstraction application term, and returns a theorem stating that the application is equal to the lambda abstraction body but with all occurrences of the binding variable replaced with the application’s argument, under no assumptions.

```
`(\x. t) s`
---------------------
|- (\x. t) s = t[s/x]
```

This is the equality congruence rule for function application. It takes two equality theorems, and applies corresponding sides of the first theorem to the second, unioning the assumptions. The first theorem’s LHS/ RHS must be functions with domain type equal to the type of the second theorem’s LHS/RHS.

```
A1 |- f1 = f2 A2 |- t1 = t2
------------------------------
A1 u A2 |- f1 t1 = f2 t2
```

This is the equality congruence rule for lambda abstraction. It takes a variable and an equality theorem, and abstracts the variable from both sides of the theorem. The variable must not occur free in the assumptions of the supplied theorem.

```
`x` A |- t1 = t2 [ "x" not free in 'A' ]
------------------------
A |- (\x. t1) = (\x. t2)
```

This is the assumption rule. It takes a boolean term, and returns a theorem stating that the term holds under the single assumption of the term itself.

```
`p`
--------
{p} |- p
```

This is the implication introduction rule. It takes a boolean term and a theorem, and removes the term from the theorem’s assumptions (if present) and adds it as an antecedent of the conclusion. Note that the term does not have to be in the assumptions of the supplied theorem for the rule to succeed.

```
`p` A |- q
----------------
A\{p} |- p ==> q
```

This is the modus ponens rule. It takes an implication theorem and a second theorem, where the implication theorem’s antecedent is alpha- equivalent to the conclusion of the second theorem. It returns a theorem stating that the implication theorem’s consequent holds, under the unioned assumptions of the supplied theorems.

```
A1 |- p ==> q A2 |- p
------------------------
A1 u A2 |- q
```

This is the equality modus ponens rule. It takes an equality theorem and a second theorem, where the equality theorem’s LHS is alpha-equivalent to the conclusion of the second theorem. It returns a theorem stating that the equality theorem’s RHS holds, under the unioned assumptions of the supplied theorems.

```
A1 |- p <=> q A2 |- p
------------------------
A1 u A2 |- q
```

This is the variable instantiation rule. It takes a variable instantiation list and a theorem, and performs a single parallel instantiation of the free variables in the theorem’s assumptions and conclusion, according to the instantiation list. All free occurrences of instantiation list domain elements in the theorem get replaced. Each instantiation list domain element must be a variable, and each range element must have the same type as its corresponding domain element.

Binding variables in the resulting theorem are renamed as necessary to avoid variable capture. Note that instantiation list entries that do not apply are simply ignored, as are repeated entries for a given variable (beyond its first entry). If no instantiation list entries apply, then the returned theorem is the same as the input.

```
[(x1,t1);(x2,t2);..] A |- p
--------------------------------------
A[t1/x1,t2/x2,..] |- p[t1/x1,t2/x2,..]
```

This is the type variable instantiation rule. It takes a type variable instantiation list and a theorem, and performs a single parallel instantiation of the type variables in the theorem’s assumptions and conclusion, according to the instantiation list. All occurrences of instantiation list domain elements in the theorem get replaced. Each instantiation list domain element must be a type variable.

Binding variables in the resulting theorem are renamed as necessary to avoid variable capture. Note that instantiation list entries that do not apply are simply ignored, as are repeated entries for a given type variable (beyond its first entry). If no instantiation list entries apply, then the returned theorem is the same as the input.

```
[(tv1,ty1);(tv2,ty2);..] A |- p
----------------------------------------------
A[ty1/tv1,ty2/tv2,..] |- p[ty1/tv1,ty2/tv2,..]
```

HOL Light has a primitive `TRANS` rule (transitivity of
equality) and a primitve `DEDUCT_ANTISYM_RULE` that deduces
logical equivalence from deduction in both directions.

In place of these two, HOL Zero has a `prim_mp_rule` and a
`prim_disch_rule` as described above.

The remaining primitive rules are the same.

The core of HOL Zero has 3 axioms.

This axiom states that, for any given function, the lambda abstraction formed by applying the function to the binding variable is equal to the function.

```
∀ f. (\x. f x) = f
```

This axiom states the antisymmetry property for implication.

```
∀ p1 p2. (p1 ==> p2) ==> ((p2 ==> p1) ==> (p1 <=> p2))
```

This axiom states a crucial property about the selection operator, namely that any element satisfying a given predicate implies that the selected element for the predicate satisfies the predicate. Note that it says nothing about when there is no element that can satisfy the predicate.

```
∀ x. P x ==> P ($@ P)
```

The axioms refer to the universal quantifier, `∀`, which is
defined as

```
∀ = \P. P = (\x. true)
```

meaning that the given predicate is true for all possible values of its argument.

and `true` is defined as

```
true = ((\p. p) = (\p. p))
```

(where `p` is a boolean value), meaning that the identity
function on boolean values is equal to itself.
The biconditional (`<=>`) is an abbreviation for equality of
boolean values.

Some other defined constants are presented as part of the HOL Zero core, but are not referenced by the core axioms or primitive rules of inference.