Proofs Without Syntax Programme

1. What is a proof of classical first-order logic?
2. When are two proofs the same? Π₁ ≃ Π₂
3. Is there an intrinsic (non-syntactic?) representation?     Π₁ ≃ Π₂   iff   Rep(Π₁) = Rep(Π₂)
4. Representations should constitute a standalone proof system:
   • Sound and complete
   • Verifiable in polynomial time
5. What are the benefits? Proof search (e.g. theorem proving)? Computation (e.g. cut elimination)?

Papers:

• Proofs without syntax, Annals of Mathematics 143(3), 1065-1076, 2006.
• Towards Hilbert's 24th Problem. ENTCS 165, 2006.
• Intuitionistic proofs without syntax. Logic in Computer Science, 2019. With Willem Heijltjes and Lutz Straßburger.
• First-order proofs without syntax. ArXiv.org, June 2019.
• Combinatorial Proofs and Decomposition Theorems for First-order Logic. Logic in Computer Science, 2021. With Lutz Straßburger and Jui-Hsuan Wu