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
- Verifiable in polynomial time
What are the benefits? Proof search (e.g. theorem proving)? Computation (e.g. cut elimination)?