# Second-order-theorems

Notion of second-order theorem.

A second-order theorem is an ACL2 theorem
that depends on
one or more
function variables.
A second-order theorem is recorded implicitly,
not explicitly via `defsoft` (which must not be used on theorems).

The second-order theorem is universally quantified
over the function variables that it depends on.
These function variables may be replaced by functions of matching arities,
obtaining a new theorem that is an
instance
of the second-order theorem.

### Naming Conventions

Including in the name of a second-order theorem,
between square brackets (in any order),
the function variables that the theorem depends on,
as in the examples in the SOFT documentation pages,
makes the dependency more explicit when referencing the theorem.
This naming convention may arise naturally
when the name of the theorem includes names of second-order functions that
follow the naming convention described in second-order-functions,
or it may be explicitly followed when choosing the name of the theorem.
However, SOFT does not enforce this naming convention.

### Subtopics

- Defthm-2nd-order
- Introduce a second-order theorem.