Axiomatic set theory à la Dijkstra and Scholten

Ernesto Acosta, Bernarda Aldana, Jaime Bohórquez, Camilo Rocha

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationAdvances in Computing - 12th Colombian Conference, CCC 2017, Proceedings
EditorsAndres Solano, Hugo Ordonez
PublisherSpringer Verlag
Pages775-791
Number of pages17
ISBN (Print)9783319665610
DOIs
StatePublished - 2017
Event12th Colombian Conference on Computing, CCC 2017 - Cali, Colombia
Duration: 19 Sep 201722 Sep 2017

Publication series

NameCommunications in Computer and Information Science
Volume735
ISSN (Print)1865-0929

Conference

Conference12th Colombian Conference on Computing, CCC 2017
Country/TerritoryColombia
CityCali
Period19/09/1722/09/17

Keywords

  • Axiomatic set theory
  • Derivation
  • Dijkstra-Scholten logic
  • Formal system
  • Symbolic manipulation
  • Undergraduate-level course
  • Zermelo-Fraenkel (ZF)

Fingerprint

Dive into the research topics of 'Axiomatic set theory à la Dijkstra and Scholten'. Together they form a unique fingerprint.

Cite this