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
Description
Summary: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.