Basic first-order model theory in Mizar
The author has submitted to Mizar Mathematical Library a series of five articles introducing a framework for the formalization of classical first-order model theory.In them, Goedel's completeness and Lowenheim-Skolem theorems have also been formalized for the countable case, to offer a first ap...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2010-01-01
|
| Series: | Journal of Formalized Reasoning |
| Online Access: | http://jfr.cib.unibo.it/article/view/1974/1361 |
| id |
doaj-06c6865a582646dc8a21696f44e66429 |
|---|---|
| record_format |
Article |
| spelling |
doaj-06c6865a582646dc8a21696f44e664292020-11-24T22:24:36ZengUniversity of BolognaJournal of Formalized Reasoning1972-57872010-01-01314977Basic first-order model theory in MizarMarco Bright CaminatiThe author has submitted to Mizar Mathematical Library a series of five articles introducing a framework for the formalization of classical first-order model theory.In them, Goedel's completeness and Lowenheim-Skolem theorems have also been formalized for the countable case, to offer a first application of it and to showcase its utility.This is an overview and commentary on some key aspects of this setup.It features exposition and discussion of a new encoding of basic definitions and theoretical gears needed for the task, remarks about the design strategies and approaches adopted in their implementation, and more general reflections about proof checking induced by the work done.http://jfr.cib.unibo.it/article/view/1974/1361 |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
Marco Bright Caminati |
| spellingShingle |
Marco Bright Caminati Basic first-order model theory in Mizar Journal of Formalized Reasoning |
| author_facet |
Marco Bright Caminati |
| author_sort |
Marco Bright Caminati |
| title |
Basic first-order model theory in Mizar |
| title_short |
Basic first-order model theory in Mizar |
| title_full |
Basic first-order model theory in Mizar |
| title_fullStr |
Basic first-order model theory in Mizar |
| title_full_unstemmed |
Basic first-order model theory in Mizar |
| title_sort |
basic first-order model theory in mizar |
| publisher |
University of Bologna |
| series |
Journal of Formalized Reasoning |
| issn |
1972-5787 |
| publishDate |
2010-01-01 |
| description |
The author has submitted to Mizar Mathematical Library a series of five articles introducing a framework for the formalization of classical first-order model theory.In them, Goedel's completeness and Lowenheim-Skolem theorems have also been formalized for the countable case, to offer a first application of it and to showcase its utility.This is an overview and commentary on some key aspects of this setup.It features exposition and discussion of a new encoding of basic definitions and theoretical gears needed for the task, remarks about the design strategies and approaches adopted in their implementation, and more general reflections about proof checking induced by the work done. |
| url |
http://jfr.cib.unibo.it/article/view/1974/1361 |
| work_keys_str_mv |
AT marcobrightcaminati basicfirstordermodeltheoryinmizar |
| _version_ |
1725760570429276160 |