Megalodon 1.5

by Brown, Sunday, February 21, 2021, 16:30 (287 days ago)

Here is Megalodon 1.5: http://grid01.ciirc.cvut.cz/~chad/megalodon-1.5.tgz

There are new options -fof and -th0 to create fof and th0 problems for ATPs whenever a proof or subproof is justified by Admitted or admit. The th0 problems contain all known results and hypotheses in context. The fof problems only contain first-order known results and hypotheses and are only generated with the conclusion is first-order. If the ATP finds a proof, it is still up to the user to inspect the ATP proof and translate it to a Megalodon proof.

I also fixed some bugs in the Dieudonne_2_2 file from Megalodon 1.4. Some of these were pointed out by Blake (thanks for proofreading!). One bug was found by E prover ( http://eprover.org ) when I was testing the new -fof option. E claimed to find proofs that should've been too difficult for it. Looking into the details it was using the (unproven) versions of 2.2.3 from Dieudonne. Let me quote (2.2.3) from Dieudonne's book:

"Any finite subset A of R has a greatest element b and a smallest element a (i.e., a <= x <= b for every x in A)."

I formalized this as two conjectures:

Theorem Dieudonne_2_2_3a: forall A c= R, finite A -> exists a :e A, forall x :e A, a <= x.
Admitted.

Theorem Dieudonne_2_2_3b: forall A c= R, finite A -> exists b :e A, forall x :e A, x <= b.
Admitted.

I think it's fair to say that these correspond to what Dieudonne wrote. However, they are clearly not what Dieudonne meant. In contexts where E had either of these as a previous result to use, it applied it with the empty set for A. That's clearly finite. And if it had a smallest or greatest element it would contradict the fact that the empty set is empty! I don't want to speak for Dieudonne, of course, but the fact that these shouldn't apply where A is empty was probably considered too obvious to be explicit about. But in formal mathematics one must be tediously explicit about everything, and this is a nice simple example showing why. Here are the corrected versions in the new Dieudonne_2_2 file:

Theorem Dieudonne_2_2_3a: forall A c= R, A <> 0 -> finite A -> exists a :e A, forall x :e A, a <= x.
Admitted.

Theorem Dieudonne_2_2_3b: forall A c= R, A <> 0 -> finite A -> exists b :e A, forall x :e A, x <= b.
Admitted.

I also included a new file Dieudonne_2_2_extra.mg based on results from E. E claims to be able to prove (2.2.13b) from (2.2.11) and (2.2.13e) from (2.2.13c). The extra file includes these two relativized results as conjectures. If someone proves the relative results and then proves (2.2.11) or (2.2.13c), then the proof of (2.2.13b) or (2.2.13e) will just be using implication elimination to combine the results.

Finally I added a new file with some results I would like to prove if I had more time. That file is IntsAndDiadRationals1.mg. There are definitions and conjectures mostly related to integers and Diadic Rationals (as Surreal Numbers). Here is a pdf version that may be more readable:

http://grid01.ciirc.cvut.cz/~chad/IntsAndDiadRationals1.pdf