Examples of Publishing Documents and Collecting Bounties

by Brown, Saturday, June 27, 2020, 18:05 (526 days ago) @ Brown

Here is the source for the Proofgold document proving the negation of the conjecture from Block 128:

https://pastebin.com/XwY2SnYr

The first line says its a document in the HOHF theory:

Document 6ffc9680fbe00a58d70cdeb319f11205ed998131ce51bb96f16c7904faf74a3d

The next lines give readable names to the base type (set) and various primitives that show up in the problem.

Before proving the main results, I first imported a few HOHF axioms (using "Known") and proved some basic logical results. These propositions and proofs are short enough that you should be able to understand them, assuming basic familiarity with Curry-Howard and proof terms. If not, feel free to ask about them here.

Before proving the negation of the Block 128 conjecture, I formulated and proved a general version:

Thm bountyprop_neg_128_lem : All A Prop Imp Ap Ap and A Ap not True All P Prop P

This says that for every proposition A, "A and not True" implies "forall P:Prop, P". Note that "implies forall P:Prop, P" is a form of negation that makes sense in every theory (even the empty theory) and is a way of writing negation Proofgold will generally recognize.

The proof term is in the text file and is not difficult. It makes use of some of the basic logical results that precede it.

The last result in the negation of the bounty conjecture. Omitting some details, it looks like this:

Thm bountyprop_neg_128 : Imp All X0 TpArr set Prop All X1 TpArr set set Ap Ap and ... Ap not Ap X0 ... All X0 Prop X0

with proof term given as

:= PrLa H ...
PrAp TmAp bountyprop_neg_128_lem
...
TmAp TmAp H Lam X set True Lam X set Empty

Essentially we assume the original proposition (referenced by H) and then obtain a proof of "All P Prop P" via bountyprop_neg_128_lem by giving a big formula to instantiate for the "A" in bountyprop_neg_128_lem (omitted here) and a proof of "A and not True". The proof of "A and not True" is H applied to the constantly True predicate and constant Empty function.

To check the document with the proofgold software, assume the text is in a file Pfg128.pfg and then use the readdraft command:

readdraft Pfg128.pfg

After the document was correct and ready to publish I had to add a nonce and publisher:

addnonce Pfg128.pfg

addpublisher Pfg128.pfg <some-address-in-my-wallet>

Then there's a "commitment" process before publishing. To make the commitment transaction, use commitdraft:

commitdraft Pfg128.pfg Pfg128.commit

The new file Pfg128.commit contains a Proofgold transaction that will record a digest of the document. A document cannot be published until the commitment has 12 confirmations. To send the transaction, use sendtxfile:

sendtxfile Pfg128.commit

No changes to the document can be made after the commitment is confirmed. (To be precise, a change would require creating a new commitment to publish the altered document.)

After the commitment has 12 confirmations, publishdraft can be used to publish the document:

publishdraft Pfg128.pfg Pfg128.pub

The new file Pfg128.pub contains the transaction to actually publish the document. To send this tx, use sendtxfile:

sendtxfile Pfg128.pub

After the publication tx confirmed, the address I used as publisher "owned" the propositions proven. As owner of the negation of the reward bounty conjecture from Block 128, I could use the collectbounties command to collect the bounty:

collectbounties <some-address-in-my-wallet> Pfg128.bounties

Again, the new file Pfg128.bounties contained a tx basically spending the bounty to the address I gave. The tx could be sent with sendtxfile:

sendtxfile Pfg128.bounties

That's a quick summary of how I claimed the bounty from Block 128. Afterwards it was clear a number of very basic results about logical connectives like "and" and "or" need to be proven, so I did this in a second document. I'll say more about this in a reply below.