Formal knowledge
Axiom
A proposition accepted without a proof term in the current formal environment.
Definition
Axiom
An axiom adds a trusted proposition or rule to a formal environment without deriving it from earlier declarations.
Axioms can be useful and mathematically standard. Recording them matters because every theorem that depends on an axiom inherits that assumption.
01
Example
The law of excluded middle can be added as an axiom to a constructive core.
02
Important distinction
An axiom-free theorem is relative to the environment and dependency analysis used to measure it.
After reading this article, you should be able to
- Define Axiom in the sense used on this site.
- Explain how an axiom changes the assumptions behind dependent theorems.