Formal knowledge
Axiom footprint
The set of trusted axioms reached by a declaration's dependencies.
Definition
Axiom footprint
An axiom footprint lists the axioms, opaque declarations, or other trusted primitives on which a checked declaration depends.
The footprint follows the dependency graph rather than searching only the theorem's surface text. An empty footprint means no recorded axiom was reached through that route.
01
Example
A theorem proved from an axiom-free natural-number prelude can have an empty footprint even when its proof uses many earlier theorems.
02
Important distinction
An empty footprint does not prove that the formal statement matches an informal source or that the kernel implementation has no defects.
After reading this article, you should be able to
- Define Axiom footprint in the sense used on this site.
- Read an axiom footprint and state exactly what an empty result does and does not establish.