1000 1 bar simple set theory bounties

by Brown, Saturday, June 20, 2020, 11:51 (533 days ago)

I published 5 documents each of which has 200 simple set theory conjectures. I put a 1 bar bounty on each of these. They should be easier to understand and (usually) easier to prove than the random bounty propositions.

Here is the first document in a format readable by the readdraft command:

https://pastebin.com/8xsrfaDL

I made several definitions at the beginning, e.g., disjointness of two sets:

Def disj : TpArr set TpArr set Prop := Lam X set Lam Y set All Z set Imp Ap Ap In Z X Ap Ap nIn Z Y

and the ordinal successor of 0 (the ordinal 1):

Def c0001 : set := Ap ordsucc Empty

In the remaining four documents, I import these objects opaquely as Params (see below).

Here is a simple example of a conjecture:

Conj atmost3_1027 : Ap not Ap atleast4 Ap Ap SetAdjoin c0003 c000A

The set c0003 is the set {0,1} (defined in a certain way) and c000A is the set {1,2} (defined in a certain way). So, informally this conjecture says {0,1,{1,2}} has at most 3 elements. More precisely, it says {0,1,{1,2}} does not have at least 4 elements. To prove this, one would assume {0,1,{1,2}} has at least 4 elements and unwind definitions to determine there must be sets X c= Y c= {0,1,{1,2}} where X has at least two elements, Y has at least three elements, Y is not a subset of X and {0,1,{1,2}} is not a subset of Y. With some work, a contradiction follows. Publishing a fully formal proof of the proposition in a document will make someone the "owner" of the proposition. The owner of a proposition (or the owner of its negation) is allowed to collect bounties on the proposition, so in this case the 1 bar bounty could be claimed.

The other four documents are here:

https://pastebin.com/emjk9NC0

https://pastebin.com/tDY8EW3X

https://pastebin.com/RRWH103M

https://pastebin.com/TbzF9zMX

As mentioned above, the definitions from the first document are imported opaquely in the remaining documents. For example:

Param 5b2442ea92009044fd3c96ca607ed2498f48caf1ef3d63f52cd11e7f9949c756 disj : TpArr set TpArr set Prop

and

Param 0738f95f806b4f24cec31019f705c04a2d2dcc38a6ea8fd411ada1e2398f40cf c0001 : set