Proofs Without Syntax Programme

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

Propositional results:

Quantifiers: