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

id	ESCUELAIG2_6d0e05daff23457c18f7b38df43cd8b0
oai_identifier_str	oai:repositorio.escuelaing.edu.co:001/1480
network_acronym_str	ESCUELAIG2
network_name_str	Repositorio Institucional ECI
repository_id_str
dc.title.spa.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	CTG-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.spa.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-05-24T23:13:38Z 2021-10-01T17:22:44Z
dc.date.available.none.fl_str_mv	2021-05-24T23:13:38Z 2021-10-01T17:22:44Z
dc.type.spa.fl_str_mv	Artículo de revista
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	https://purl.org/redcol/resource_type/CAP_LIB
format	http://purl.org/coar/resource_type/c_3248
status_str	publishedVersion
dc.identifier.isbn.none.fl_str_mv	978-3-319-66561-0 978-3-319-66562-7
dc.identifier.uri.none.fl_str_mv	https://repositorio.escuelaing.edu.co/handle/001/1480
dc.identifier.doi.none.fl_str_mv	doi.org/10.1007/978-3-319-66562-7_55
dc.identifier.url.none.fl_str_mv	https://link.springer.com/chapter/10.1007%2F978-3-319-66562-7_55
identifier_str_mv	978-3-319-66561-0 978-3-319-66562-7 doi.org/10.1007/978-3-319-66562-7_55
url	https://repositorio.escuelaing.edu.co/handle/001/1480 https://link.springer.com/chapter/10.1007%2F978-3-319-66562-7_55
dc.language.iso.spa.fl_str_mv	eng
language	eng
dc.relation.ispartofseries.none.fl_str_mv	Communications in Computer and Information Science book series (CCIS, volume 735);
dc.relation.citationedition.spa.fl_str_mv	CCC 2017
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.spa.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). doi: 10.1007/978-3-319-23165-5_27 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). doi: 10.1007/978-3-540-78913-0_25 Tourlakis, G.J.: Lectures in Logic and Set Theory. Cambridge Studies in Advanced Mathematics, vol. 82–83. Cambridge University Press, Cambridge (2003)
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	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	12 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	Suiza
dc.source.spa.fl_str_mv	https://link.springer.com/chapter/10.1007%2F978-3-319-66562-7_55
institution	Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv	https://repositorio.escuelaing.edu.co/bitstream/001/1480/1/license.txt https://repositorio.escuelaing.edu.co/bitstream/001/1480/2/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf https://repositorio.escuelaing.edu.co/bitstream/001/1480/3/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/1480/4/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf.jpg
bitstream.checksum.fl_str_mv	5a7ca94c2e5326ee169f979d71d0f06e 8aeed3b8575822b210cfe6a39958eda3 ce17bbb4d4f1cbe9a2413e4ea88bb0b2 5e6449ca81e5fd3e68a22c7345d52a6a
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_	1808494277175541760
spelling	Acosta, Ernesto6db75777036e0bd7240d41677171e5e6600Aldana, Bernardadd9576ac3ffc19dd2889b032a359ad63600Bohórquez, Jaime34ca64f10c7c3bbadec92bdb453a4170600Rocha, Camilo649eba80a4c919beefa7d19955bc2950600CTG-Informática2021-05-24T23:13:38Z2021-10-01T17:22:44Z2021-05-24T23:13:38Z2021-10-01T17:22:44Z2017978-3-319-66561-0978-3-319-66562-7https://repositorio.escuelaing.edu.co/handle/001/1480doi.org/10.1007/978-3-319-66562-7_55https://link.springer.com/chapter/10.1007%2F978-3-319-66562-7_55The 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 probadas, principalmente, mediante la sustitución de "iguales por iguales". 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 artículo 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 en matemáticas e informática con el enfoque algebraico de Dijkstra y Scholten.Colombian Conference on Computing12 páginasapplication/pdfengSpringer NatureSuizaCommunications in Computer and Information Science book series (CCIS, volume 735);CCC 2017791775N/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). doi: 10.1007/978-3-319-23165-5_27Rocha, 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). doi: 10.1007/978-3-540-78913-0_25Tourlakis, G.J.: Lectures in Logic and Set Theory. Cambridge Studies in Advanced Mathematics, vol. 82–83. Cambridge University Press, Cambridge (2003)https://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_14cbhttps://link.springer.com/chapter/10.1007%2F978-3-319-66562-7_55Axiomatic Set Theory à la Dijkstra and ScholtenArtículo de revistainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248Textinfo:eu-repo/semantics/bookParthttps://purl.org/redcol/resource_type/CAP_LIBhttp://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 courseLICENSElicense.txttext/plain1881https://repositorio.escuelaing.edu.co/bitstream/001/1480/1/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD51open accessORIGINALAxiomatic Set Theory à la Dijkstra and Scholten.pdfapplication/pdf104087https://repositorio.escuelaing.edu.co/bitstream/001/1480/2/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf8aeed3b8575822b210cfe6a39958eda3MD52metadata only accessTEXTAxiomatic Set Theory à la Dijkstra and Scholten.pdf.txtAxiomatic Set Theory à la Dijkstra and Scholten.pdf.txtExtracted texttext/plain4https://repositorio.escuelaing.edu.co/bitstream/001/1480/3/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf.txtce17bbb4d4f1cbe9a2413e4ea88bb0b2MD53open accessTHUMBNAILAxiomatic Set Theory à la Dijkstra and Scholten.pdf.jpgAxiomatic Set Theory à la Dijkstra and Scholten.pdf.jpgGenerated Thumbnailimage/jpeg7812https://repositorio.escuelaing.edu.co/bitstream/001/1480/4/Axiomatic%20Set%20Theory%20%c3%a0%20la%20Dijkstra%20and%20Scholten.pdf.jpg5e6449ca81e5fd3e68a22c7345d52a6aMD54open access001/1480oai:repositorio.escuelaing.edu.co:001/14802022-10-24 18:09:04.619metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK

Axiomatic Set Theory à la Dijkstra and Scholten

Publicaciones similares