Intuitionistic Logic according to Dijkstra's Calculus of Equational Deduction

Notre Dame Journal of Formal Logic 49 (4):361-384 (2008)

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert's style of proof and Gentzen's deductive systems. In this context we call it CED (Calculus of Equational Deduction). This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations (in Dijkstra's words, "letting the symbols do the work") have led to the "calculational style," an impressive array of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system (I-CED), we prove Leibniz's principle for intuitionistic logic and also prove that any (intuitionistic) valid formula of predicate logic can be proved in I-CED
Keywords intuitionistic logic   calculational style   equational deduction
Categories (categorize this paper)
DOI 10.1215/00294527-2008-017
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 47,330
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Varieties of Linear Calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
A Short Introduction to Intuitionistic Logic.G. E. Mint͡s - 2000 - Kluwer Academic / Plenum Publishers.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
A Note on Definability in Equational Logic.George Weaver - 1994 - History and Philosophy of Logic 15 (2):189-199.
A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.


Added to PP index

Total views
23 ( #411,972 of 2,291,077 )

Recent downloads (6 months)
1 ( #832,027 of 2,291,077 )

How can I increase my downloads?


My notes

Sign in to use this feature