Megalodon 1.8 (23257 "Conjectures")

by Brown, Saturday, November 27, 2021, 12:06 (8 days ago) @ Brown

Here's one of the unprovable conjectures:

Variable x:set.
Variable y:set.
Variable z:set.
Hypothesis H0: (forall w:set, w :e y -> ordinal x -> ordinal w -> x :e w \/ x = w \/ w :e x).
Hypothesis H2: ordinal y.
Hypothesis H3: nIn x y.
Hypothesis H4: z :e y.
Theorem Conj_ordinal_trichotomy_or__1__1: ordinal z -> z :e x.

This is from the middle of the proof of the trichotomy property for ordinals, but the assumption that x is an ordinal has been dropped. This makes the conjecture unprovable and we can state the negation as follows:

Theorem neg_Conj_ordinal_trichotomy_or__1__1: (forall x y z:set,
(forall w:set, w :e y -> ordinal x -> ordinal w -> x :e w \/ x = w \/ w :e x)
-> ordinal y
-> nIn x y
-> z :e y
-> ordinal z -> z :e x)
-> False.

To prove the negation we assume the property:

assume HC: forall x y z,
(forall w:set, w :e y -> ordinal x -> ordinal w -> x :e w \/ x = w \/ w :e x)
-> ordinal y
-> nIn x y
-> z :e y
-> ordinal z -> z :e x.

Now we prove False by giving appropriate choices for x, y and z:

set x := {1}.
set y := 1.
set z := 0.

From HC we get False with these choices if we can prove:

claim L1: forall w:set, w :e y -> ordinal x -> ordinal w -> x :e w \/ x = w \/ w :e x.

claim L2: ordinal y.

claim L3: x /:e y.

claim L4: z :e y.

claim L5: ordinal z.

claim L6: z /:e x.

All of these are easy to prove. Here are Megalodon proofs:

claim L1: forall w:set, w :e y -> ordinal x -> ordinal w -> x :e w \/ x = w \/ w :e x.
{ let w.
assume _.
assume H1: ordinal {1}.
prove False.
exact not_ordinal_Sing1 H1.
}
claim L2: ordinal y.
{ exact ordinal_1. }
claim L3: x /:e y.
{ assume H1: x :e y.
apply In_no2cycle x y H1.
prove y :e x.
exact SingI y.
}
claim L4: z :e y.
{ exact In_0_1. }
claim L5: ordinal z.
{ exact ordinal_Empty. }
claim L6: z /:e x.
{ assume H1: z :e x.
apply neq_0_1.
prove 0 = 1.
exact SingE 1 z H1.
}

Then finally we prove False as follows:

apply L6.
prove z :e x.
exact HC x y z L1 L2 L3 L4 L5.