Concluding Remarks
The well known theorem of Godel shows that every system of logic is in a certain sense incomplete, but at the same time it indicates means whereby from a given system L of logic a more complete system L' may be obtained. By repeating the process we get a sequence L,
Li = L', L2 = L j, Lз = L2,... of logics each more complete than the preceding.
(A. M. Turing, 1938)
The authors have at this point prepared the ground for verifying, with a proof-checker based on set theory, the propositions in the first chapter of [14].[1] A variant of the Zermelo-Fraenkel set theory, postulating global choice, regularity and infinity,[2] underlies the logical armory of the proof-checker, Ref, on which our experimental activity relies. The formally checked proofs regard, for the time being, only certain parts of our planned work: in particular, we proved the conclusions of the The- orys about universes, superstructures, and ‘urification’ shown in Figs. 10.5 and 10.6, as well as the unique readability of the sets that encode terms inside the Theory termEncoding (see Figs. 10.8 and 10.9); the proof of the ultrafilter theorem was available from the outset,[3] along with many minor but useful facts about finiteness, rank, ordinals, the set constructs P, U, etc.
In the phase on which we have reported, anyway, our work has been mainly architectural: given the availability of a second-order construct, ‘Theory’, supporting modularization and proof reuse in Ref, we deem it wise to invest in designing the Theory interfaces before formalizing proofs meticulously.
We are confident that we can finish the envisaged proof-development tasks without getting entangled in unforeseen difficulties. Then, as said in the introduction, we must adopt schemes of notation and extended rules of inference that conveniently assist Ref’s users in exploitations of the nonstandard methods.
Even after those enhancements, Ref’s theory will be a conservative extension of the specific set theory available in Ref’s initial endowment. A more challenging and intriguing view on the extensibility of proof-checkers should cope with the progressive extension of theories, in a frame of mind close to some of Alan Turing’s early investigations (see [37]).
Acknowledgements Discussions with Francesco Di Cosmo helped in polishing this paper. The first author acknowledges partial support from the Polish National Science Centre research project DEC-2011/02/A/HS1/00395; and the second author from the project FRA-UniTS (2014) “Learning specifications and robustness in signal analysis.
- [1] A website reporting on our experiment is at http://www2.units.it/eomodeo/InitialSetupForNonStandardAnalysis.html, http://aetnanova.units.it/scenarios/InitialSetupForNonStandardAnalysis/.
- [2] In Ref the well-foundendess of membership and statements of the axiom of choice easily resultfrom the availability of the construct arb discussed in Sect. 10.6, thanks to the interplay of arbwith abstract set formers; infinity is embodied by Ref’s built-in constant aTC.
- [3] For a Ref-based proof of Zorn’s lemma (whence the ultrafilter theorem follows easily), see [35,pp. 373-405]. This lemma was used in Ref’s proof of the maximal ideal theorem for Booleanalgebras as presented in [9].
