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 |