Proofs Without Syntax Programme
 What is a proof of classical firstorder logic?
 When are two proofs the same?
Π_{1} ≃ Π_{2}
 Is there an intrinsic (nonsyntactic?) representation?
Π_{1} ≃ Π_{2} iff
Rep(Π_{1}) = Rep(Π_{2})

Representations should constitute a standalone proof system:
 Sound and complete
 Correctness is polynomialtime (linear time?)

What are the benefits? Proof search (e.g. theorem proving), computation (e.g. cut elimination), ... ?
Propositional results:
Quantifiers:

Firstorder proofs without syntax.
Slides for Berkeley Logic Colloquium, 2014