Difficulty: moderate — 3 definitions, 0 abbreviations, 0 lemmas, 1 theorems, 0 examples.
Kinds of rule, and the styles of proof system they make.
A schema may let each branch discharge assumptions of its own. Forbidding that leaves the ordinary kind of rule, where every branch works from the premises already at hand. Forbidding branches altogether leaves an axiom.
A rule that discharges nothing anywhere is simple; any other is complex.
Source: Hiep, New Foundations for Separation Logic (PhD thesis, 2024), appendix A.3, on axioms, simple and complex proof rules.
An axiom: a schema with no branches, so it concludes outright.
axiom
def Logic.ProofTheory.Schema.IsAxiom {Obj : Type} (s : Logic.ProofTheory.Schema Obj) : Prop
Show details
| s.IsAxiom = (s.premises = [])
Complexity: 33 (size of the value term)
A simple rule: a schema no branch of which discharges anything, so every branch works from the premises already at hand.
simple-rule
def Logic.ProofTheory.Schema.IsSimpleRule {Obj : Type} (s : Logic.ProofTheory.Schema Obj) : Prop
Show details
| s.IsSimpleRule = ∀ p ∈ s.premises, p.1 = []
Complexity: 71 (size of the value term)
A complex rule: any schema that is not simple, so at least one branch discharges an assumption of its own.
complex-rule
def Logic.ProofTheory.Schema.IsComplexRule {Obj : Type} (s : Logic.ProofTheory.Schema Obj) : Prop
Show details
| s.IsComplexRule = ¬s.IsSimpleRule
Complexity: 13 (size of the value term)
Lean core dependencies: Not
An axiom is a simple rule, having no branch to discharge anything in.
theorem Logic.ProofTheory.Schema.IsSimpleRule.of_isAxiom {Obj : Type} {s : Logic.ProofTheory.Schema Obj}
(h : s.IsAxiom) : s.IsSimpleRule
Show details
fun {Obj} {s} h p hp =>
absurd
(Eq.mp
(congrArg (fun _a => p ∈ _a)
(Eq.mp (congrArg (fun _a => _a) (Logic.ProofTheory.Schema.IsAxiom.eq_1 s)) h))
hp)
(of_eq_true (Eq.trans (congrArg Not List.not_mem_nil._simp_1) not_false_eq_true))
Complexity: 533 (size of the value term)
Lean core dependencies: Eq, Eq.mp, Eq.trans, False, List, Not, Prod, True, absurd, congrArg, not_false_eq_true, of_eq_true
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.
definitiontheoremdeclared elsewheredependencyproof dependency
legend