Semantic tautology proof systems

Cook and Reckhow, The Relative Efficiency of Propositional Proof Systems, Journal of Symbolic Logic 44(1), 1979, Definition 1.3, p. 37 (PDF p. 3), define a proof system as a polynomial-time computable surjection onto a language.

This module isolates the surjection and proof-length layer. It deliberately does not claim polynomial-time computability; a later machine model will add that independent requirement to obtain a Cook-Reckhow system.

@[reducible, inline]

abbrev ComplexityTheory.Tautology : Type

A tautology bundled with the semantic proof that every assignment satisfies it.

Equations

• ComplexityTheory.Tautology = { formula : ComplexityTheory.BooleanFormula // formula.IsTautology }

structure ComplexityTheory.TautologyProofSystem : Type

The semantic core of a proof system for TAUT: every proof string produces a tautology, and every tautology is produced by at least one proof string.

• produce : BitString → BooleanFormula

  Return the formula named by a proof string.

• sound (proof : BitString) : (self.produce proof).IsTautology

  Every output formula is a tautology.

• complete (formula : BooleanFormula) : formula.IsTautology → ∃ (proof : BitString), self.produce proof = formula

  Every tautology occurs as an output.

def ComplexityTheory.TautologyProofSystem.Proves (system : TautologyProofSystem) (proof : BitString) (formula : BooleanFormula) : Prop

A string is a proof of formula when the proof map returns that formula.

Equations

• system.Proves proof formula = (system.produce proof = formula)

theorem ComplexityTheory.TautologyProofSystem.isTautology_of_proves (system : TautologyProofSystem) {proof : BitString} {formula : BooleanFormula} (hProof : system.Proves proof formula) : formula.IsTautology

Every accepted proof proves a tautology, restating system soundness relationally.

theorem ComplexityTheory.TautologyProofSystem.exists_proof (system : TautologyProofSystem) (tautology : Tautology) : ∃ (proof : BitString), system.Proves proof ↑tautology

Completeness supplies at least one proof of each bundled tautology.

theorem ComplexityTheory.TautologyProofSystem.exists_proof_length (system : TautologyProofSystem) (tautology : Tautology) : ∃ (length : ℕ) (proof : BitString), List.length proof = length ∧ system.Proves proof ↑tautology

Every tautology has some proof length at which a proof exists.

noncomputable def ComplexityTheory.TautologyProofSystem.proofCost (system : TautologyProofSystem) (tautology : Tautology) : ℕ

The minimum bit length of a proof of a tautology. This is noncomputable because the semantic structure does not yet provide a proof-search algorithm.

Equations

• system.proofCost tautology = Nat.find ⋯

theorem ComplexityTheory.TautologyProofSystem.exists_proof_of_length_proofCost (system : TautologyProofSystem) (tautology : Tautology) : ∃ (proof : BitString), List.length proof = system.proofCost tautology ∧ system.Proves proof ↑tautology

A proof attaining proofCost exists for every tautology.

theorem ComplexityTheory.TautologyProofSystem.proofCost_le_length (system : TautologyProofSystem) (tautology : Tautology) {proof : BitString} (hProof : system.Proves proof ↑tautology) : system.proofCost tautology ≤ List.length proof

No proof of a tautology is shorter than its declared minimum proof cost.