Publication:
Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction

Thumbnail Image
Files

Files

Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction.pdf (317.73 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Bohórquez, Jaime
Abstract (Spanish)
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.
Abstract (English)
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.
Extent
24 páginas.
URI: https://repositorio.escuelaing.edu.co/handle/001/1910
Collections

Collections

AD - CTG – Informática
References

Backhouse, R., “Mathematics and Programming. A Revolution in the Art of Effective Reasoning,” 2001. http://www.cs.nott.ac.uk/~rcb/inaugural.pdf

Backhouse, R., Program Construction: Calculating Implementations from Specifications, John Wiley and Sons, Inc., Hoboken, 2003.

Bell, J. L., and M. Machover, A Course in Mathematical Logic, North-Holland Publishing Co., Amsterdam, 1977.

Bijlsma, L., and R. Nederpelt, “Dijkstra-Scholten predicate calculus: Concepts and misconceptions,” Acta Informatica, vol. 35 (1998), pp. 1007–1036.

Birkhoff, G., Lattice Theory, 3d edition, vol. 25 of American Mathematical Society Colloquium Publications, American Mathematical Society, Providence, 1979.

Bohorquez, J., and C. Rocha, “Towards the effective use of formal logic in the teaching of discrete math,” 6th International Conference on Information Technology Based Higher Education and Training (ITHET), 2005.

Dijkstra, E. W., “Boolean connectives yield punctual expressions,” EWD 1187 in The Writings of Edsger W. Dijkstra, 2000.

Dijkstra, E. W., and C. S. Scholten, Predicate Calculus and Program Semantics, Texts and Monographs in Computer Science, Springer-Verlag, New York, 1990.

Gries, D., and F. B. Schneider, A Logical Approach to Discrete Math, Texts and Monographs in Computer Science, Springer-Verlag, New York, 1993.

Gries, D., and F. B. Schneider, “Equational propositional logic,” Information Processing Letters, vol. 53 (1995), pp. 145–52.

Gries, D., and F. B. Schneider, “Formalizations of Substitution of Equals for Equals,” Technical Report TR98-1686, Cornell University-Computer Science, Ithaca, 1998.

Lifschitz, V., “On calculational proofs (First St. Petersburg Conference on Days of Logic and Computability, 1999),” Annals of Pure and Applied Logic, vol. 113 (2002), pp. 207–24.

Nerode, A., “Some lectures on intuitionistic logic,” pp. 12–59 in Logic and Computer Science (Montecatini Terme, 1988), edited by A. Dold, B. Eckmann, and F. Takens, vol. 1429 of Lecture Notes in Mathematics, Springer, Berlin, 1990.

Rasiowa, H., and R. Sikorski, The Mathematics of Metamathematics, 3d edition, Monografie Matematyczne, Tom 41. PWN-Polish Scientific Publishers, Warsaw, 1970.

Simmons, G. F., Introduction to Topology and Modern Analysis, Robert E. Krieger Publishing Co. Inc., Melbourne, 1983. Reprint of the 1963 original.

Tourlakis, G., “A basic formal equational predicate logic,” Technical Report CS1998-09, York University-Computer Science, Toronto,1998.

Tourlakis, G., “On the soundness and completeness of equational predicate logics,” Journal of Logic and Computation, vol. 11 (2001), pp. 623–53.