Mathematical Objects and Propositions as NFTs

by Brown, Tuesday, November 16, 2021, 16:31 (19 days ago)

Recently after explaining to someone that the entity who publishes a document defining a new mathematical object or proving a new mathematical proposition in Proofgold becomes the "owner" of the object/proposition, the person pointed out that essentially makes these "ownership assets" NFTs. Certainly they can be exchanged, and they cannot be duplicated (or destroyed). A criticism of most NFTs is that they don't actually give the owner any power (except to say they "own" it and be able to sell the NFT to someone else). In Proofgold though, the owner can decide if later documents can import the object opaquely (without redefining it) or the proposition opaquely (without reproving it). By default objects and propositions are free to use, but this can be changed by the owner. It can be changed to allow others to purchase rights for a declared price (in proofgold bars) for each document they use it in, or to even disallow anyone from using it (a "stay off my lawn" policy).

Playing around with these ideas, I found that I published a document defining Kuratowski pairs last year. (Given two sets x and y, {{x,y},{x}} is the Kuratowski pair of x and y.) I don't use Kuratowski pairs because I prefer a different definition of pairing with nice properties. (If you're interested, look up my 2015 Journal of Automated Reasoning paper "Reconsidering Pairs and Functions as Sets.") So I "own" Kuratowski pairs and decided to change them from being "free to use" to "no one can use." There's no good reason to use Kuratowski pairs and it's a good way to test out the ability to use these "NFTs" this way. I've now also defined 7 variants of Kuratowski pairs (e.g., {{x},{x,y}}, {{x},{y,x}}, etc.) and also disallowed using these (opaquely) in new documents.

Technically for each object/proposition there are two things owned: the pure version and the theory version. To be able to reuse something opaquely, both owners must allow it. For the original Kuratowski pairs I only disallowed the "pure" version, but that's good enough.

Declaring new definitions to allow no reuse is easy. In the Proofgold document do this:

NewRights KPair2 <owneraddress> None
NewPureRights KPair2 <owneraddress> None

That's what I did with the 7 variants. With the original I needed to create a transaction sending the ownership asset to myself, changing the rights policy in the process. I had to do this with creategeneraltx and it was quite painful. I might give more details in a reply to this message, but the point is that a command to handle this special case would make things much easier. Ideally there would also be a way for people who want to sell such ownership assets to auction them off for litecoin using an atomic swap.

Finally, to try to make sure I really can't include Kuratowski pairs in a new document, I tried. readdraft tells me the new document will not be publishable, but not very prominently. commitdraft warns more clearly and refuses to create the commitment transaction. However, commitdraft ends with the message "Refusing to commit to the draft until the issues above are result." I assume this is a typo and "result" should be something like "resolved."