Javascript Interactive Higher-Order Theorem Prover

Contact Person
Chad E Brown

Foundations in DeTSeT

Foundations for Mathematics in a Dependently Typed Set Theory

Chad E Brown

Introduction

This is the title page of an online book containing a development of the foundations for mathematics starting from a basic set theory. The items in the book consist of primitive notions, axioms, notation, definitions and theorems. The items are arranged into chapters and sections. The chapters are listed in the Contents sidebar. Clicking on a chapter/section link shows links to the subsections of that chapter/section as well as any items in the chapter/section.

When viewing an item the relevant background (previous items which the current item depends on) either shown or hidden. Also, the user has the option of renaming some of the variables (with JavaScript code ensuring that the renaming preserves meaning). Users can also test their understanding of an item by filling in variable names to recover the original item (up to renaming of variables).

The items in this book were originally formalized in the proof assistant Scunak.

Quick Start

For a quick start, you can look at a simple theorem about binary unions. To fully understand the proof, examine it with the background information shown. In particular, you must know the definition of binary union in terms of the union of collections of sets.

Next look at the definition of ordered pairs as Kuratowski pairs. The fact that this provides a notion of ordered pair follows from this and this.