From ZX to first order logic: a survey of string diagrammatic calculi
summary
Claims that string diagrams (ZX and variants) reconstruct fragments up to full first‑order logic by algebraic interaction of Hopf and Frobenius interaction and by adding a second, dual relation calculus. Concrete constructions: Cartesian/first‑order bicategories and linear bi‑categories with white/black relation calculus that model existential‑conjunctive vs universal fragments. Proven results: a goal‑style completeness theorem for relational models and a worked diagrammatic proof showing a nontrivial quantifier swap. Tool needs: graph rewriting and diagram editors to make the approach practical; existing ZX uses already aid circuit optimisation and error correction. completeness in the Gödel/goal sense
AI-written summary · about
chapters (10)
- 0:00String diagrammatic calculi intro
- 4:13Spider and EXP calculi origins
- 9:52Traditional string diagrams limits
- 13:57Relational string diagrams intro
- 20:13First-order logic via diagrams
- 29:12Algebraic structures for FOL
- 35:12Linear bi-categories completeness
- 37:21Negation insights
- 38:24String diagrams as syntax
- 40:12Q&A
related talks
23mFrom Fermions to Qubits: A ZX-Calculus Perspective
17mEncoding High-level Quantum Programs as SZX-diagrams
31mQuantum compilation using the ZX calculus
14mHybrid quantum-classical circuit simplification with the ZX-calculus
31mA tour of String diagrams and Monoidal categories
32mFault tolerance with the ZX-calculus and fusion complexes: tools for QEC development in the...
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs
27mFunctorial Semantics for Partial Theories