Megalodon 1.8

by Brown, Friday, November 26, 2021, 18:05 (9 days ago)
edited by Brown, Friday, November 26, 2021, 18:09

Here is Megalodon 1.8:

http://grid01.ciirc.cvut.cz/~chad/megalodon-1.8.tgz

This version includes a formal construction of real (and complex) numbers via Conway's surreal numbers. All of it has been published into the Proofgold chain.

I also created an html/javascript presentation of the formalization split into 9 parts:

Basic Infrastructure:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part1.html

Surreal Numbers as an Ordinal and a Predicate:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part2.html

Surreal Numbers as Sets:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part3.html

Unary Minus:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part4.html

Addition:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part5.html

Multiplication:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part6.html

Integers and Diadic Rationals:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part7.html

Reals:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part8.html

Complex:
http://grid01.ciirc.cvut.cz/~chad/FormalNumbers/Part9.html

For most proofs there is an option to prove the theorem (often split into multiple goals) in a javascript interactive tableau theorem prover. The prover is classical, so the correspondence to Proofgold really only makes sense after excluded middle is proven early in Part 1 (via Diaconescu). The html/javascript files are available together here:

http://grid01.ciirc.cvut.cz/~chad/FormalNumbers.tgz

I've often gotten the feedback that my websites are "old-looking" so if anyone wants to download the collection and do fancy tricks to give it a facelift (i.e., make it look like people expect Google/Facebook/Twitter to look), then feel free.