System

Difficulty: hard — 6 definitions, 0 abbreviations, 1 lemmas, 0 theorems, 0 examples.

definition lemma
legend

Proof systems in the abstract: what a deduction is, rather than only whether one exists.

Popper’s basis says that a conclusion is deducible from a list of premises. It does not say what the deduction looks like. A proof system supplies that witness. Fixing a collection of rules determines which trees count as deductions, and the deducibility relation is then read off: a conclusion follows from some premises exactly when a tree of that kind exists.

A rule says what has to be established for it to apply, and what it then concludes. Each of these is a claim in its own right, carrying the premises available for it. Writing a rule this way lets it close assumptions off, and also lets it restrict which assumptions may be present at all, as the rules of modal logic do.

Nothing about a basis comes for free at this generality. A rule application fixes exactly the premises it draws on, so enlarging them, or chaining deductions together, has to be earned. The next module carves out the rules for which it is.

Sources: Hiep, New Foundations for Separation Logic (PhD thesis, 2024), appendix A.3; Grabmayer, Relating Proof Systems for Recursive Types (PhD thesis, Vrije Universiteit Amsterdam, 2005), section 4.2.2, for the distinction between rules that can be checked from a single node and rules that inspect the assumptions standing above it.

An application of a rule: the claims that have to be established for it, and the claim it then yields. A rule, in Troelstra and Schwichtenberg’s sense, is a set of these. An application with nothing to establish is an axiom.

proof-rule
structure Logic.ProofTheory.Application (Obj : Type) : Type

  • What has to be established.

    premises : List (List Obj × Obj)

  • What the application yields.

    conclusion : List Obj × Obj
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, HEq, List, Nat, Prod, SizeOf, eq_of_heq

Used by: Logic.ProofTheory.CutFree.toDerivation, Logic.ProofTheory.Derivation, Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.DerivationsOf, Logic.ProofTheory.Instances, Logic.ProofTheory.ProofSystem, Logic.ProofTheory.Schema.instance, Logic.PropositionalLogic.derivable_mp, Logic.PropositionalLogic.derivation_of_axiom

A proof system over some type of objects: which applications it allows. Systems built in different ways, out of terms or out of pointer structures, are different instances over the same objects, so they stand side by side.

proof-system
structure Logic.ProofTheory.ProofSystem (Obj : Type) : Type

  • Which applications the system allows.

    rules : Logic.ProofTheory.Application Obj → Prop
Show details

Outer dependencies: (none)

Inner dependencies: Logic.ProofTheory.Application

Lean core dependencies: Eq, HEq, eq_of_heq

Used by: Logic.ProofTheory.Derivable, Logic.ProofTheory.Derivation, Logic.ProofTheory.DerivationsOf, Logic.ProofTheory.DerivationsOf.of_forall, Logic.ProofTheory.Schema.system, Logic.ProofTheory.toBasis1, Logic.PropositionalLogic.hilbert

A deduction of a conclusion from a list of premises: a finite tree. Its leaves appeal to a premise, and its other nodes either apply a rule or paste deductions together. The two structural nodes are the closure conditions every basis asks for, which a proof system’s deduction relation is taken to include.

deduction
inductive Logic.ProofTheory.Derivation {Obj : Type} (D : Logic.ProofTheory.ProofSystem Obj) :
  List Obj → Obj → Type

  • A premise stands as a deduction of itself.

    assumption : {P : List Obj} → {a : Obj} → a ∈ P → Logic.ProofTheory.Derivation D P a

  • Deductions of everything a further deduction draws on paste into it. Each is read against the same premises, which is what pasting them in requires.

    graft : {P Q : List Obj} →
{a : Obj} →
  Logic.ProofTheory.DerivationsOf D (List.map (fun b => (P, b)) Q) →
    Logic.ProofTheory.Derivation D Q a → Logic.ProofTheory.Derivation D P a

  • An allowed application applies once every claim it asks for has been established.

    apply : (r : Logic.ProofTheory.Application Obj) →
Logic.ProofTheory.ProofSystem.rules r →
  Logic.ProofTheory.DerivationsOf D r.premises →
    Logic.ProofTheory.Derivation D r.conclusion.1 r.conclusion.2
Show details

Outer dependencies: Logic.ProofTheory.ProofSystem

Inner dependencies: Logic.ProofTheory.Application, Logic.ProofTheory.DerivationsOf

Lean core dependencies: Eq, Eq.symm, HEq, List, List.map, Nat, Nat.ble, Nat.decEq, Not, PProd, PULift, PUnit, Prod, SizeOf, cond, dite, eq_of_heq

Used by: Logic.ProofTheory.CutFree.DerivationsOf.toDerivationsOf, Logic.ProofTheory.CutFree.toDerivation, Logic.ProofTheory.Derivable, Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.DerivationsOf, Logic.ProofTheory.DerivationsOf.forall_toCutFree, Logic.ProofTheory.DerivationsOf.of_forall, Logic.ProofTheory.derivable_iff_derivableCutFree, Logic.ProofTheory.toBasis1, Logic.PropositionalLogic.Formula.Derivable.toProofSystem, Logic.PropositionalLogic.derivable_mp, Logic.PropositionalLogic.derivation_of_axiom

A deduction for each of a list of claims, each read against its own premises.

inductive Logic.ProofTheory.DerivationsOf {Obj : Type} (D : Logic.ProofTheory.ProofSystem Obj) :
  List (List Obj × Obj) → Type

  • Nothing to establish.

    nil : Logic.ProofTheory.DerivationsOf D []

  • One claim established, and the rest.

    cons : {s : List Obj × Obj} →
{rest : List (List Obj × Obj)} →
  Logic.ProofTheory.Derivation D s.1 s.2 →
    Logic.ProofTheory.DerivationsOf D rest → Logic.ProofTheory.DerivationsOf D (s :: rest)
Show details

Outer dependencies: Logic.ProofTheory.ProofSystem

Inner dependencies: Logic.ProofTheory.Application, Logic.ProofTheory.Derivation

Lean core dependencies: Eq, Eq.symm, HEq, List, List.map, Nat, Nat.ble, PProd, PULift, PUnit, Prod, SizeOf, cond, eq_of_heq

Used by: Logic.ProofTheory.CutFree.DerivationsOf.toDerivationsOf, Logic.ProofTheory.CutFree.toDerivation, Logic.ProofTheory.Derivation, Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.DerivationsOf.forall_toCutFree, Logic.ProofTheory.DerivationsOf.of_forall, Logic.ProofTheory.toBasis1

A conclusion is deducible from a list of premises when some deduction of it exists.

def Logic.ProofTheory.Derivable {Obj : Type} (D : Logic.ProofTheory.ProofSystem Obj) (P : List Obj)
  (a : Obj) : Prop
Show details 
| Logic.ProofTheory.Derivable D P a = Nonempty (Logic.ProofTheory.Derivation D P a)

Complexity: 23 (size of the value term)

Outer dependencies: Logic.ProofTheory.ProofSystem

Inner dependencies: Logic.ProofTheory.Derivation

Lean core dependencies: List, Nonempty

Used by: Logic.ProofTheory.DerivationsOf.of_forall, Logic.ProofTheory.derivable_iff_derivableCutFree, Logic.ProofTheory.toBasis1, Logic.PropositionalLogic.Formula.Derivable.toProofSystem, Logic.PropositionalLogic.derivable_mp, Logic.PropositionalLogic.derivation_of_axiom

Deducing every member of a list, one at a time, is deducing them all from those same premises.

theorem Logic.ProofTheory.DerivationsOf.of_forall {Obj : Type} {D : Logic.ProofTheory.ProofSystem Obj}
  {P Q : List Obj} :
  (∀ b ∈ Q, Logic.ProofTheory.Derivable D P b) →
    Nonempty (Logic.ProofTheory.DerivationsOf D (List.map (fun b => (P, b)) Q))
Show details 
fun {Obj} {D} {P} x x_1 =>
  List.brecOn (motive := fun x =>
    (∀ b ∈ x, Logic.ProofTheory.Derivable D P b) →
      Nonempty (Logic.ProofTheory.DerivationsOf D (List.map (fun b => (P, b)) x)))
    x Logic.ProofTheory.DerivationsOf.of_forall._f x_1

Complexity: 125 (size of the value term)

Dependencies: Logic.ProofTheory.Derivable, Logic.ProofTheory.DerivationsOf, Logic.ProofTheory.ProofSystem

Proof dependencies: Logic.ProofTheory.Derivation

Lean core dependencies: Eq, Eq.trans, List, List.map, Nonempty, Nonempty.elim, Or, Prod, True, congrArg, congrFun', eq_self, eq_true, of_eq_true, or_true, true_or

Used by: Logic.ProofTheory.toBasis1

Every proof system is a basis. Its deducibility relation satisfies generalised reflexivity, by appealing to a premise, and generalised transitivity, by pasting deductions together. Everything Popper’s chapter establishes therefore applies to every proof system, with no condition on its rules.

def Logic.ProofTheory.toBasis1 {Obj : Type} (D : Logic.ProofTheory.ProofSystem Obj) :
  Logic.Popper.Basis1 Obj
Show details 
| Logic.ProofTheory.toBasis1 D = { Deduce := Logic.ProofTheory.Derivable D, rg := ⋯, tg := ⋯ }

Complexity: 27 (size of the value term)

Outer dependencies: Logic.Popper.Basis1, Logic.ProofTheory.ProofSystem

Inner dependencies: Logic.ProofTheory.Derivable, Logic.ProofTheory.Derivation, Logic.ProofTheory.DerivationsOf, Logic.ProofTheory.DerivationsOf.of_forall

Mathlib dependencies: Nonempty.some

Lean core dependencies: List, List.map, Nonempty.elim, Prod

Used by: (none)

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.

definitionlemmadeclared elsewheredependencyproof dependency
legend