Logical Bilateralism: Proofs, Models and Applications

August 2026

at The 2026 European Summer School in Logic, Language and Information (ESSLLI 2026), Prague

This is an intensive class on logical bilateralism, taught by Sara Ayhan and me at esslli 2026. Logical bilateralism is an approach to meaning and consequence that foregrounds a symmetry between certain notions, like assertion and denial, proof and refutation or truth and falsity. Bilateralist approaches to such dual distinctions take both sides as primitive rather than—as in conventional ‘unilateralist’ approaches—taking one notion to be fundamental and defining the other in its terms. In recent years different bilateralist logical systems have been developed, displaying a wide variety in their specific orientation. What is missing so far is a systematic framework putting these very different approaches on a map and thereby highlighting similarities, distinctions and connections between them. Though giving a complete picture will also not be possible within the scope of the intended course, our aim is to familiarize the attendants with many different forms of logical bilateralism and use these to exemplify both the variety of approaches and the coherence of the underlying principles.

This page will host slides for each day of the course, and pointers to relevant references.

• Day 1: Foundations: Natural deduction, sequent calculus and models.
• Day 2: Signed Bilateralist Natural Deduction: Signed bilateralist natural deduction and multi-conclusion sequent calculus.
• Day 3: Non-Classical Frameworks: Proofs and models for non-classical bilateralist logics, like N4, FDE, and 2Int.
• Day 4: Bilateralist Term Calculus: Parigot’s \(\lambda\mu\) calculus, Curien and Herbelin’s symmetric \(\overline{λ}μ\tilde{μ}\) calculus, and their computational and dialogical interpretations.
• Day 5: Recent Devlopments: Bilateralism as a road to contra-classical logics; coordination principles and toggle negation; uniqueness and bilateralism.

Readings and References

I’ll add to the reference list through the week.

Foundations

• Gerhard Gentzen, “Untersuchungen über das logische Schließen—I”, Mathematische Zeitschrift, 39(1):176–210, 1935.

• Gerhard Gentzen, The Collected Papers of Gerhard Gentzen, Translated and Edited by M. E. Szabo, North Holland, 1969.

• Dag Prawitz, Natural Deduction, Almqvist and Wiskell, 1965.

• Greg Restall, “Truth Values and Proof Theory” Studia Logica, 92(2):241–264, 2009.

• Greg Restall, Proofs and Models in Philosophical Logic, Cambridge University Press, 2023.

• Raymond Smullyan, First-Order Logic. Springer-Verlag, 1968.

Philosophical Issues

• Nuel Belnap, “Tonk, plonk and plink.” Analysis, 22 (6), 130-134, 1962.

• Robert Brandom, Articulating reasons: An introduction to inferentialism. Cambridge, MA: Harvard University Press, 2000.

• Rudolf Carnap, The Logical Syntax of Language. Trans. by A. Smeaton. Open Court Classics. 1934.

• Pedro del Valle-Inclan and Julian Schlöder. “Coordination and harmony in bilateral logic.” Mind 132(525), 192–207, 2023.

• Michael Dummett, “The Philosophical Basis of Intuitionistic Logic,” in H. E. Rose and J. C. Shepherdson (eds.): Logic Colloquium ’73, Amsterdam: North-Holland Publishing Co., 5-40, 1975.

• Michael Dummett, The Logical Basis of Metaphysics, London: Duckworth, 1991.

• Fernando Ferreira, “The co-ordination principles: A problem for bilateralism,” Mind 117 (468), 1051–1057, 2008.

• Nissim Francez, “Bilateralism does provide a proof theoretic treatment of classical logic (for non-technical reasons),” Journal of Applied Logics, IfCoLog Journal 5(8), 1653–1662, 2018.

• Nissim Francez and Roy Dyckhoff, “A Note on Harmony, Journal of Philosophical Logic 41, 613–628, 2012.

• Michael Gabbay, “Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons).” Journal of Applied Logic 25, 108–122, 2017.

• Peter Milne, “Harmony, Purity, Simplicity and a ‘Seemingly Magical Fact’”, The Monist, 85(4):498–534, 2002

• Arthur Prior, “The runabout inference-ticket,” Analysis, 21 (2), 38–39, 1960.

• Stephen Read, “General-Elimination Harmony and the Meaning of the Logical Constants”, Journal of Philosophical Logic 39, 557-576, 2010.

• Greg Restall, “Multiple Conclusions” pp. 189–205 in Logic, Methodology and Philosophy of Science: Proceedings of the Twelfth International Congress, edited by P. Hájek, L. Valdés-Villanueva and D. Westerståhl, KCL Publications, 2005.

• Ellie Ripley, “Paradoxes and failures of cut,” Australasian Journal of Philosophy 91(1), 139–164, 2013.

• Ellie Ripley, “Anything Goes,” Topoi 34, 25-36, 2015.

• Ellie Ripley, “Bilateralism, coherence, warrant” In F. Moltmann & M. Textor (Eds.), Act-based conceptions of propositional content: Contemporary and historical perspectives (pp. 307–324). Oxford: Oxford University Press, 2017.

• Ian Rumfitt, “Yes and No”, Mind, 109(436), 781–823, 2000.

• Ian Rumfitt, “Unilateralism Disarmed”, Mind, 111(442), 2002.

• Ian Rumfitt, “Knowledge by Deduction”, Grazer Philosophische Studien, 77, 61-84, 2008.

• Neil Tennant, Natural Logic, Edinburgh: Edinburgh University Press, 1978.

• Neil Tennant, “Proof and Paradox,” Dialectica 36, 265-296, 1982.

Non-Classical Frameworks

• Ahmad Almukdad and David Nelson, “Constructible falsity and inexact predicates,” The Journal of Symbolic Logic 49, 231–233, 1984.

• Sara Ayhan: “A cut-free sequent calculus for the bi-intuitionistic logic 2Int”, 2020, part of: Sara Ayhan and Heinrich Wansing, “On synonymy in proof-theoretic semantics. The case of 2Int”, Bulletin of the Section of Logic 52(2), 187–237, 2023.

• Peter Gibbard, “Price and Rumfitt on rejective negation and classical logic,” Mind, vol. 111(442), pp. 297–303, 2002.

• I Johansson, “Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus,” Compositio Mathematica 4, 119–136, 1930.

• E. G. K. López-Escobar, “Refutability and elementary number theory,” Indagationes Mathematicae 34:362–74, 1972.

• David Nelson, “Constructible Falsity,” The Journal of Symbolic Logic 14(1), 16-26, 1949.

• Cecylia Rauszer, “A formalization of the propositional calculus of H-B logic,” Studia Logica, 33 (1), 23–34, 1974.

• Heinrich Wansing, “Falsification, natural deduction and bi-intuitionistic logic,” Journal of Logic and Computation 26 (1), 425–450, 2016.

• Heinrich Wansing (2017): “A more general general proof theory,” Journal of Applied Logic 25, 23-46, 2017.

Term Calculus

• Michel Parigot, “λµ-calculus: an algorithmic interpretation of classical natural deduction” In Proc. of the International Conference in Logic Programming and Automated Reasoning, St. Peterburg, LNCS 624, Springer, 1992.

• Pierre-Louis Curien and Hugo Herbelin, “The Duality of Computation”, Proceedings of ICFP 2000 (SIGPLAN Notices 35(9)), ACM, 2000.

• Hugo Herbelin, “On the Degeneracy of Σ-types in Presence of Computational Classical Logic” TLCA 2005, LNCS 3461 , Springer, 2005.

• Etienne Miquey, “A Classical Sequent Calculus with Dependent Types” ACM Transactions on Programming Languages and Systems, 41(2), 2019

• Greg Restall, “Structural Rules in Natural Deduction with Alternatives”, Bulletin of the Section of Logic, 52(2), 2023.

• Greg Restall, “What can we Mean? On Practices, Norms and Pluralisms,” Proceedings of the Aristotelian Society (125):1, 23–43, 2024.