Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction

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 equiva...

Full description

Autores:
Bohórquez, Jaime
Tipo de recurso:
Article of journal
Fecha de publicación:
2008
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
eng
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/1910
Acceso en línea:
https://repositorio.escuelaing.edu.co/handle/001/1910
Palabra clave:
Estilo de cálculo
Deducción ecuacional
Lógica intuicionista
calculational style
equational deduction
Intuitionistic logic
Rights
openAccess
License
http://purl.org/coar/access_right/c_abf2
id ESCUELAIG2_a0fb7fc0d370601c4c56ac98b8cf7acc
oai_identifier_str oai:repositorio.escuelaing.edu.co:001/1910
network_acronym_str ESCUELAIG2
network_name_str Repositorio Institucional ECI
repository_id_str
dc.title.eng.fl_str_mv Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
title Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
spellingShingle Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
Estilo de cálculo
Deducción ecuacional
Lógica intuicionista
calculational style
equational deduction
Intuitionistic logic
title_short Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
title_full Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
title_fullStr Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
title_full_unstemmed Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
title_sort Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
dc.creator.fl_str_mv Bohórquez, Jaime
dc.contributor.author.none.fl_str_mv Bohórquez, Jaime
dc.contributor.researchgroup.spa.fl_str_mv Informática
dc.subject.armarc.spa.fl_str_mv Estilo de cálculo
Deducción ecuacional
Lógica intuicionista
topic Estilo de cálculo
Deducción ecuacional
Lógica intuicionista
calculational style
equational deduction
Intuitionistic logic
dc.subject.proposal.eng.fl_str_mv calculational style
equational deduction
Intuitionistic logic
description 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.
publishDate 2008
dc.date.issued.none.fl_str_mv 2008
dc.date.accessioned.none.fl_str_mv 2021-12-07T16:42:59Z
dc.date.available.none.fl_str_mv 2021-12-07T16:42:59Z
dc.type.spa.fl_str_mv Artículo de revista
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_970fb48d4fbd8a85
dc.type.version.spa.fl_str_mv info:eu-repo/semantics/publishedVersion
dc.type.coar.spa.fl_str_mv http://purl.org/coar/resource_type/c_6501
dc.type.content.spa.fl_str_mv Text
dc.type.driver.spa.fl_str_mv info:eu-repo/semantics/article
dc.type.redcol.spa.fl_str_mv http://purl.org/redcol/resource_type/ART
format http://purl.org/coar/resource_type/c_6501
status_str publishedVersion
dc.identifier.issn.none.fl_str_mv 00294527
19390726
dc.identifier.uri.none.fl_str_mv https://repositorio.escuelaing.edu.co/handle/001/1910
identifier_str_mv 00294527
19390726
url https://repositorio.escuelaing.edu.co/handle/001/1910
dc.language.iso.spa.fl_str_mv eng
language eng
dc.relation.citationendpage.spa.fl_str_mv 384
dc.relation.citationissue.spa.fl_str_mv 4
dc.relation.citationstartpage.spa.fl_str_mv 361
dc.relation.citationvolume.spa.fl_str_mv 49
dc.relation.indexed.spa.fl_str_mv N/A
dc.relation.ispartofjournal.eng.fl_str_mv Notre Dame Journal Of Formal Logic
dc.relation.references.spa.fl_str_mv 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.
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.accessrights.spa.fl_str_mv info:eu-repo/semantics/openAccess
eu_rights_str_mv openAccess
rights_invalid_str_mv http://purl.org/coar/access_right/c_abf2
dc.format.extent.spa.fl_str_mv 24 páginas.
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.spa.fl_str_mv University of Notre Dame
dc.source.spa.fl_str_mv https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-49/issue-4/Intuitionistic-Logic-according-to-Dijkstras-Calculus-of-Equational-Deduction/10.1215/00294527-2008-017.full?tab=ArticleLink
institution Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv https://repositorio.escuelaing.edu.co/bitstream/001/1910/1/Intuitionistic%20Logic%20according%20to%20Dijkstra%e2%80%99s%20Calculus%20of%20Equational%20Deduction.pdf
https://repositorio.escuelaing.edu.co/bitstream/001/1910/2/license.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1910/3/Intuitionistic%20Logic%20according%20to%20Dijkstra%e2%80%99s%20Calculus%20of%20Equational%20Deduction.pdf.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1910/4/Intuitionistic%20Logic%20according%20to%20Dijkstra%e2%80%99s%20Calculus%20of%20Equational%20Deduction.pdf.jpg
bitstream.checksum.fl_str_mv fc6966a5ebc8a43beba24be5dae806ad
5a7ca94c2e5326ee169f979d71d0f06e
83e8559ea9b38e6018ba958a4bf51fd2
7b7b9eb97e8df0135ed90e429421409f
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
MD5
MD5
repository.name.fl_str_mv Repositorio Escuela Colombiana de Ingeniería Julio Garavito
repository.mail.fl_str_mv repositorio.eci@escuelaing.edu.co
_version_ 1814355581122641920
spelling Bohórquez, Jaime34ca64f10c7c3bbadec92bdb453a4170600Informática2021-12-07T16:42:59Z2021-12-07T16:42:59Z20080029452719390726https://repositorio.escuelaing.edu.co/handle/001/1910Dijkstra 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.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.24 páginas.application/pdfengUniversity of Notre Damehttps://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-49/issue-4/Intuitionistic-Logic-according-to-Dijkstras-Calculus-of-Equational-Deduction/10.1215/00294527-2008-017.full?tab=ArticleLinkIntuitionistic Logic according to Dijkstra’s Calculus of Equational DeductionArtículo de revistainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_6501http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/articlehttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85384436149N/ANotre Dame Journal Of Formal LogicBackhouse, R., “Mathematics and Programming. A Revolution in the Art of Effective Reasoning,” 2001. http://www.cs.nott.ac.uk/~rcb/inaugural.pdfBackhouse, 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.info:eu-repo/semantics/openAccesshttp://purl.org/coar/access_right/c_abf2Estilo de cálculoDeducción ecuacionalLógica intuicionistacalculational styleequational deductionIntuitionistic logicORIGINALIntuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction.pdfIntuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction.pdfArtículo principal.application/pdf325356https://repositorio.escuelaing.edu.co/bitstream/001/1910/1/Intuitionistic%20Logic%20according%20to%20Dijkstra%e2%80%99s%20Calculus%20of%20Equational%20Deduction.pdffc6966a5ebc8a43beba24be5dae806adMD51metadata only accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1910/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTIntuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction.pdf.txtIntuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction.pdf.txtExtracted texttext/plain42979https://repositorio.escuelaing.edu.co/bitstream/001/1910/3/Intuitionistic%20Logic%20according%20to%20Dijkstra%e2%80%99s%20Calculus%20of%20Equational%20Deduction.pdf.txt83e8559ea9b38e6018ba958a4bf51fd2MD53open accessTHUMBNAILIntuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction.pdf.jpgIntuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction.pdf.jpgGenerated Thumbnailimage/jpeg10002https://repositorio.escuelaing.edu.co/bitstream/001/1910/4/Intuitionistic%20Logic%20according%20to%20Dijkstra%e2%80%99s%20Calculus%20of%20Equational%20Deduction.pdf.jpg7b7b9eb97e8df0135ed90e429421409fMD54open access001/1910oai:repositorio.escuelaing.edu.co:001/19102022-07-01 09:32:55.596metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK