http://www.cedar-forest.org/forest/events/festival/workshop1/abstracts.html

http://www.cedar-forest.org/forest/events/festival/workshop1/

ULTRA group Useful Logics, Types, Rewriting, and Applications |
UKII UK Institute of Informatics, UK |

The list of abstracts is as follows:

The theory, which includes infinitesimals and infinite numbers, is based on the hyperreal number system developed by Abraham Robinson in his Nonstandard Analysis (NSA). I shall first outline the ultrapower : construction of the hyperreals in Isabelle. This was carried out strictly through the use of definitions to ensure that the foundations of NSA in the prover are sound. The mechanization has required constructing the various number systems leading to the reals, and then going one step further to define the hyperreals using a mechanized theory of filters and ultrafilters.

I shall next describe the use of the new types of numbers and new relations on them to formalize familiar concepts from analysis such as sequences, limits, continuous functions, derivatives, power series, and transcendental functions. I will point out the merits of the nonstandard approach with respect to the practice of analysis and mechanical theorem proving. In particular, I will argue that the overall result is an intuitive, yet rigorous, development of real analysis, with a relatively high degree of proof automation in many cases.

Berardi (personal communication) has informed me that set theory has not been implemented this way in Coq because contradictions follow from the axiom of extensionality. In Coq set theory has been implemented with a new type for sets. None of the consistency results of \cite{seldin:PTCC} apply to this implementation. It is hardly surprising that contradictions follow from the axiom of extensionality, for the equality which is Leibniz' equality, is

In ordinary axiomatic set theory, set equality behaves like Leibniz equality in that equals may always be replaced by equals. This is clearly untrue in the calculus of constructions with $\mathsf{SetQ}$. However, there is a class of properties with respect to which equals under $\mathsf{SetQ}$ can be replaced by equals. This is the class of \emph{extensional properties}. The class of extensional properties can be shown to parallel the definition of well formed formulas in first-order axiomatic set theory.

As pointed out in \cite[Remark 17]{seldin:PTCC}, while we can prove most of the axioms of constructive set theory, we cannot prove the axioms of power set and $\in$-induction. Furthermore, we cannot expect to get all of set theory this way, because the consistency of this implementation follows from the strong normalization theorem for the calculus of constructions. If a complete set theory satisfying these axioms is desired, then the implementation given here will not do. But the need for a different (and, presumably, stronger implementation does not follow from any problem with the axiom of extensionality. See this extended abstract for further details.

Maintained by Fairouz Kamareddine ()