A Set describing a data structure defined recursively with a finite collection of base and inductive cases.
- Base case Axioms that have no premise, universally true
- Inductive cases have premises and are true when their premises are true () (Like a Horn Clause)