Proofs Without Syntax Programme
- What is a proof of classical first-order logic?
- When are two proofs the same?
Π1 ≃ Π2
- Is there an intrinsic (non-syntactic?) representation?
Π1 ≃ Π2 iff
Rep(Π1) = Rep(Π2)
Representations should constitute a standalone proof system:
- Sound and complete
- Correctness is polynomial-time (linear time?)
What are the benefits? Proof search (e.g. theorem proving), computation (e.g. cut elimination), ... ?
First-order proofs without syntax.
Slides for Berkeley Logic Colloquium, 2014