Axiomatic Set Theory à la Dijkstra and Scholten

The algebraic approach by E.W. Dijkstra and C.S. Scholten to formal logic is a proof calculus, where the notion of proof is a sequence of equivalences proved – mainly – by using substitution of ‘equals for equals’. This paper presents Set , a first-order logic axiomatization for set theory using the...

Full description

Autores:
Acosta, Ernesto
Aldana, Bernarda
Bohórquez, Jaime
Rocha, Camilo
Tipo de recurso:
Part of book
Fecha de publicación:
2017
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
eng
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/1836
Acceso en línea:
https://repositorio.escuelaing.edu.co/handle/001/1836
Palabra clave:
Teoría axiomática de conjuntos
Lógica de Dijkstra-Scholten
Manipulación simbólica
SET
Axiomatic set theory
Dijkstra-Scholten logic
Derivation
Formal system
Zermelo-Fraenkel (ZF)
Symbolic manipulation
Undergraduate-level course
Rights
closedAccess
License
© Springer Nature Switzerland AG 2018
id ESCUELAIG2_4b527aa62c5e2c02759503ec569b5dec
oai_identifier_str oai:repositorio.escuelaing.edu.co:001/1836
network_acronym_str ESCUELAIG2
network_name_str Repositorio Institucional ECI
repository_id_str
dc.title.eng.fl_str_mv Axiomatic Set Theory à la Dijkstra and Scholten
title Axiomatic Set Theory à la Dijkstra and Scholten
spellingShingle Axiomatic Set Theory à la Dijkstra and Scholten
Teoría axiomática de conjuntos
Lógica de Dijkstra-Scholten
Manipulación simbólica
SET
Axiomatic set theory
Dijkstra-Scholten logic
Derivation
Formal system
Zermelo-Fraenkel (ZF)
Symbolic manipulation
Undergraduate-level course
title_short Axiomatic Set Theory à la Dijkstra and Scholten
title_full Axiomatic Set Theory à la Dijkstra and Scholten
title_fullStr Axiomatic Set Theory à la Dijkstra and Scholten
title_full_unstemmed Axiomatic Set Theory à la Dijkstra and Scholten
title_sort Axiomatic Set Theory à la Dijkstra and Scholten
dc.creator.fl_str_mv Acosta, Ernesto
Aldana, Bernarda
Bohórquez, Jaime
Rocha, Camilo
dc.contributor.author.none.fl_str_mv Acosta, Ernesto
Aldana, Bernarda
Bohórquez, Jaime
Rocha, Camilo
dc.contributor.researchgroup.spa.fl_str_mv Informática
dc.subject.armarc.SPA.fl_str_mv Teoría axiomática de conjuntos
Lógica de Dijkstra-Scholten
Manipulación simbólica
topic Teoría axiomática de conjuntos
Lógica de Dijkstra-Scholten
Manipulación simbólica
SET
Axiomatic set theory
Dijkstra-Scholten logic
Derivation
Formal system
Zermelo-Fraenkel (ZF)
Symbolic manipulation
Undergraduate-level course
dc.subject.armarc.ENG.fl_str_mv SET
dc.subject.proposal.eng.fl_str_mv Axiomatic set theory
Dijkstra-Scholten logic
Derivation
Formal system
Zermelo-Fraenkel (ZF)
Symbolic manipulation
Undergraduate-level course
description The algebraic approach by E.W. Dijkstra and C.S. Scholten to formal logic is a proof calculus, where the notion of proof is a sequence of equivalences proved – mainly – by using substitution of ‘equals for equals’. This paper presents Set , a first-order logic axiomatization for set theory using the approach of Dijkstra and Scholten. What is novel about the approach presented in this paper is that symbolic manipulation of formulas is an effective tool for teaching an axiomatic set theory course to sophomore-year undergraduate students in mathematics. This paper contains many examples on how argumentative proofs can be easily expressed in Set and points out how the rigorous approach of Set can enrich the learning experience of students. The results presented in this paper are part of a larger effort to formally study and mechanize topics in mathematics and computer science with the algebraic approach of Dijkstra and Scholten.
publishDate 2017
dc.date.issued.none.fl_str_mv 2017
dc.date.accessioned.none.fl_str_mv 2021-11-18T13:22:26Z
dc.date.available.none.fl_str_mv 2021-11-18T13:22:26Z
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_3248
dc.type.content.spa.fl_str_mv Text
dc.type.driver.spa.fl_str_mv info:eu-repo/semantics/bookPart
dc.type.redcol.spa.fl_str_mv http://purl.org/redcol/resource_type/ART
format http://purl.org/coar/resource_type/c_3248
status_str publishedVersion
dc.identifier.isbn.none.fl_str_mv 9783319665610
dc.identifier.uri.none.fl_str_mv https://repositorio.escuelaing.edu.co/handle/001/1836
identifier_str_mv 9783319665610
url https://repositorio.escuelaing.edu.co/handle/001/1836
dc.language.iso.spa.fl_str_mv eng
language eng
dc.relation.ispartofseries.none.fl_str_mv CCIS;Volumen 735
dc.relation.citationendpage.spa.fl_str_mv 791
dc.relation.citationstartpage.spa.fl_str_mv 775
dc.relation.indexed.spa.fl_str_mv N/A
dc.relation.ispartofbook.eng.fl_str_mv Advances in Computing
dc.relation.references.spa.fl_str_mv Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer, New York (1990)
Halmos, P.R.: Naive Set Theory. Undergraduate Texts in Mathematics. Springer, New York (1974)
Hodel, R.E.: An Introduction to Mathematical Logic. Dover Publications Inc., New York (2013)
Hrbacek, K., Jech, T.J.: Introduction to Set Theory. Monographs and Textbooks in Pure and Applied Mathematics, vol. 220, 3rd edn. M. Dekker, New York (1999). Rev. and expanded edition
Hsiang, J.: Refutational theorem proving using term-rewriting systems. Artif. Intell. 25(3), 255–300 (1985)
Jech, T.J.: Set Theory. Pure and Applied Mathematics, a Series of Monographs and Textbooks, vol. 79. Academic Press, New York (1978)
Kunen, K.: Set Theory. Studies in Logic, vol. 34. College Publications, London (2013). Revised edition
Meseguer, J.: General logics. In: Logic Colloquium 1987: Proceedings. Studies in Logic and the Foundations of Mathematics, 1st edn., vol. 129, pp. 275–330. Elsevier, Granada, August 1989
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)
Rocha, C.: The formal system of Dijkstra and Scholten. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 580–597. Springer, Cham (2015).
Rocha, C., Meseguer, J.: A rewriting decision procedure for Dijkstra-Scholten’s syllogistic logic with complements. Revista Colombiana de Computación 8(2), 101–130 (2007)
Rocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2008. LNCS, vol. 4988, pp. 337–351. Springer, Heidelberg (2008).
Tourlakis, G.J.: Lectures in Logic and Set Theory. Cambridge Studies in Advanced Mathematics, vol. 82–83. Cambridge University Press, Cambridge (2003)
dc.rights.eng.fl_str_mv © Springer Nature Switzerland AG 2018
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_14cb
dc.rights.uri.spa.fl_str_mv https://creativecommons.org/licenses/by/4.0/
dc.rights.accessrights.spa.fl_str_mv info:eu-repo/semantics/closedAccess
dc.rights.creativecommons.spa.fl_str_mv Atribución 4.0 Internacional (CC BY 4.0)
rights_invalid_str_mv © Springer Nature Switzerland AG 2018
https://creativecommons.org/licenses/by/4.0/
Atribución 4.0 Internacional (CC BY 4.0)
http://purl.org/coar/access_right/c_14cb
eu_rights_str_mv closedAccess
dc.format.extent.spa.fl_str_mv 17 páginas.
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.spa.fl_str_mv Springer Nature
dc.publisher.place.spa.fl_str_mv USA.
institution Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv https://repositorio.escuelaing.edu.co/bitstream/001/1836/1/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf
https://repositorio.escuelaing.edu.co/bitstream/001/1836/2/license.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1836/3/SPRINGER%20LOGO%20.pdf.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1836/5/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1836/4/SPRINGER%20LOGO%20.pdf.jpg
https://repositorio.escuelaing.edu.co/bitstream/001/1836/6/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf.jpg
bitstream.checksum.fl_str_mv ce3159b68d11073dc69f09df67ff8a9d
5a7ca94c2e5326ee169f979d71d0f06e
d784fa8b6d98d27699781bd9a7cf19f0
d784fa8b6d98d27699781bd9a7cf19f0
1ca2ce509f3cad8078a6994ce18899f7
1ca2ce509f3cad8078a6994ce18899f7
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
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_ 1814355580744105984
spelling Acosta, Ernesto6db75777036e0bd7240d41677171e5e6600Aldana, Bernardadd9576ac3ffc19dd2889b032a359ad63600Bohórquez, Jaime34ca64f10c7c3bbadec92bdb453a4170600Rocha, Camilo649eba80a4c919beefa7d19955bc2950600Informática2021-11-18T13:22:26Z2021-11-18T13:22:26Z20179783319665610https://repositorio.escuelaing.edu.co/handle/001/1836The algebraic approach by E.W. Dijkstra and C.S. Scholten to formal logic is a proof calculus, where the notion of proof is a sequence of equivalences proved – mainly – by using substitution of ‘equals for equals’. This paper presents Set , a first-order logic axiomatization for set theory using the approach of Dijkstra and Scholten. What is novel about the approach presented in this paper is that symbolic manipulation of formulas is an effective tool for teaching an axiomatic set theory course to sophomore-year undergraduate students in mathematics. This paper contains many examples on how argumentative proofs can be easily expressed in Set and points out how the rigorous approach of Set can enrich the learning experience of students. The results presented in this paper are part of a larger effort to formally study and mechanize topics in mathematics and computer science with the algebraic approach of Dijkstra and Scholten.El enfoque algebraico de E. W. Dijkstra y C. S. Scholten a la lógica formal es un cálculo de prueba, donde la noción de prueba es una secuencia de equivalencias demostradas, principalmente, mediante la sustitución de "igual por igual". Este artículo presenta Set, una axiomatización lógica de primer orden para la teoría de conjuntos utilizando el enfoque de Dijkstra y Scholten. Lo novedoso del enfoque presentado en este artículo es que la manipulación simbólica de fórmulas es una herramienta eficaz para enseñar un curso de teoría axiomática de conjuntos a estudiantes de segundo año de pregrado en matemáticas. Este documento contiene muchos ejemplos sobre cómo las pruebas argumentativas se pueden expresar fácilmente en Set y señala cómo el enfoque riguroso de Set puede enriquecer la experiencia de aprendizaje de los estudiantes. Los resultados presentados en este artículo son parte de un esfuerzo mayor para estudiar y mecanizar formalmente temas de matemáticas e informática con el enfoque algebraico de Dijkstra y Scholten.17 páginas.application/pdfengSpringer NatureUSA.CCIS;Volumen 735791775N/AAdvances in ComputingDijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer, New York (1990)Halmos, P.R.: Naive Set Theory. Undergraduate Texts in Mathematics. Springer, New York (1974)Hodel, R.E.: An Introduction to Mathematical Logic. Dover Publications Inc., New York (2013)Hrbacek, K., Jech, T.J.: Introduction to Set Theory. Monographs and Textbooks in Pure and Applied Mathematics, vol. 220, 3rd edn. M. Dekker, New York (1999). Rev. and expanded editionHsiang, J.: Refutational theorem proving using term-rewriting systems. Artif. Intell. 25(3), 255–300 (1985)Jech, T.J.: Set Theory. Pure and Applied Mathematics, a Series of Monographs and Textbooks, vol. 79. Academic Press, New York (1978)Kunen, K.: Set Theory. Studies in Logic, vol. 34. College Publications, London (2013). Revised editionMeseguer, J.: General logics. In: Logic Colloquium 1987: Proceedings. Studies in Logic and the Foundations of Mathematics, 1st edn., vol. 129, pp. 275–330. Elsevier, Granada, August 1989Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)Rocha, C.: The formal system of Dijkstra and Scholten. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 580–597. Springer, Cham (2015).Rocha, C., Meseguer, J.: A rewriting decision procedure for Dijkstra-Scholten’s syllogistic logic with complements. Revista Colombiana de Computación 8(2), 101–130 (2007)Rocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2008. LNCS, vol. 4988, pp. 337–351. Springer, Heidelberg (2008).Tourlakis, G.J.: Lectures in Logic and Set Theory. Cambridge Studies in Advanced Mathematics, vol. 82–83. Cambridge University Press, Cambridge (2003)© Springer Nature Switzerland AG 2018https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/closedAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_14cbAxiomatic Set Theory à la Dijkstra and ScholtenArtículo de revistainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/bookParthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85Teoría axiomática de conjuntosLógica de Dijkstra-ScholtenManipulación simbólicaSETAxiomatic set theoryDijkstra-Scholten logicDerivationFormal systemZermelo-Fraenkel (ZF)Symbolic manipulationUndergraduate-level courseORIGINALAxiomatic Set Theory à la Dijkstra and Scholten.pdfAxiomatic Set Theory à la Dijkstra and Scholten.pdfapplication/pdf114783https://repositorio.escuelaing.edu.co/bitstream/001/1836/1/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdfce3159b68d11073dc69f09df67ff8a9dMD51open accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1836/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTSPRINGER LOGO .pdf.txtSPRINGER LOGO .pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1836/3/SPRINGER%20LOGO%20.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD53open accessAxiomatic Set Theory à la Dijkstra and Scholten.pdf.txtAxiomatic Set Theory à la Dijkstra and Scholten.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1836/5/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD55open accessTHUMBNAILSPRINGER LOGO .pdf.jpgSPRINGER LOGO .pdf.jpgGenerated Thumbnailimage/jpeg4996https://repositorio.escuelaing.edu.co/bitstream/001/1836/4/SPRINGER%20LOGO%20.pdf.jpg1ca2ce509f3cad8078a6994ce18899f7MD54open accessAxiomatic Set Theory à la Dijkstra and Scholten.pdf.jpgAxiomatic Set Theory à la Dijkstra and Scholten.pdf.jpgGenerated Thumbnailimage/jpeg4996https://repositorio.escuelaing.edu.co/bitstream/001/1836/6/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf.jpg1ca2ce509f3cad8078a6994ce18899f7MD56metadata only access001/1836oai:repositorio.escuelaing.edu.co:001/18362022-10-24 18:10:18.075open accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK