Examples of Publishing Documents and Collecting Bounties

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

Here is the source for the second document:

https://pastebin.com/ymJaXdXa

In the first document I proved a result like

"notE : not A -> A -> False"

Here I import this as "Known" since it's already been proven:

Known notE : All x1 Prop Imp Ap Prim 3 x1 Imp x1 Prim 1

Then I prove the converse, which hadn't already been proven:

"notI : (A -> False) -> not A"

Thm notI : All x1 Prop Imp Imp x1 Prim 1 Ap Prim 3 x1
:= TmLa x1 Prop TmAp not_def Lam _ TpArr Prop Prop Lam q TpArr Prop Prop Ap q x1

With some work it's not difficult to understand this proposition and its proof term. Of course, names like "x1" give away that I have some code helping to produce the text, but they are small enough to produce and consume by hand.

An axiom of the HOHF theory is dneg:

"dneg : not not A -> A"

Known dneg : All x4 Prop Imp Ap Prim 3 Ap Prim 3 x4 x4

Using this and some basic results about disjunction, excluded middle follows:

"xm : A or not A"

Thm xm : All x1 Prop Ap Ap Prim 5 x1 Ap Prim 3 x1
:= ...

An alternative form "xmcases" is also proven:

"xmcases : (A -> B) -> (not A -> B) -> B"

Finally, two results about equivalence (iff) are proven.

All results proven in this document can be included in future documents (in the HOHF theory) just by giving "Known" along with the proposition. The blockchain/ledger knows what theorems have been proven before.