This series is about prediction markets for mathematics.
Imagine a game where players trade tickets with mathematical sentences written on them. A ticket is redeemable for $1 if you can demonstrate a proof of the sentence written on it. (A ticket is like a prediction market share in that sentence.) In this system, it's also allowable to exchange a ticket for another ticket with a logically equivalent sentence written on it, if you can demonstrate a proof of that logical equivalence.
(Actually, this rule can be made even more permissive if we like: It's allowable to exchange an ticket for a ticket if . That way if your newly obtained ticket is worth anything, we know that the ticket would have been worth at least as much, and therefore your wealth either stayed the same or declined. As ticket Czars, this is very reassuring to us, because we certainly would not want for you to have gained wealth at our own expense. That kind of thing is supposed to be reserved for your interactions with other traders. This operation is called irreversible exchange, because once performed, it can't generally be undone.)
By issuing tickets in a given sentence for a price of less than $1, you can thus put bounties on mathematical theorems. People can buy the tickets for your lower price and sell them for $1, so long as they can prove the theorem.
This ticket-trading system functions as prediction market for mathematics. The price of a sentence corresponds to what people think the chance is that a proof will be found for it.
For completeness, we have to include a somewhat surprising trading rule into this system: Tickets with sentences are tradable (in either direction) for tickets with sentences . This rule is introduced in the original logical share splitting post linked above.
The second post notes that, since a real implementation of this ticket system would involve using an automatic formal proof checker to verify submitted proofs, we should probably pay some attention to how an automatic proof checker actually works. And these proof checkers are constructive by nature. In particular, this means that they don't naturally have the Law of Excluded Middle. Proof checkers can still be used to do classical logic, simply by adding the Law of Excluded Middle as an additional axiom. But they mesh most naturally with intuitionist logic.
In classical logic, there are many equivalent forms of the logical share splitting operation. For example, trading for $ \neg(B \Rightarrow A), A \Rightarrow B$. But, as the second post points out:
These classically equivalent rules can be intuitionistically distinct. And of these distinct rules, most of them are invalid. The original rule where we trade for remains valid. Therefore we should use that one.
Because of the property of intuitionist logic that the only way to prove is to provide a proof of or a proof of , there is a sense in which logical share splitting is more valid under intuitionist logic than otherwise. Under classical logic, a proof of may be possible, without any ability to prove or individually. So a trader who owns tickets with and that would be worthless on their own due to the lack of proofs, could perform logical share splitting to obtain and redeem that ticket. This would be an instance of logical share splitting allowing a trade of a valuable ticket for a value-less one. The intuitionist version prevents this.
Splitting up the work of writing proofs between multiple minimally-coordinated parties remains possible. However, it becomes somewhat less elegant; and somewhat more coordination is required.
So that was parts 1 and 2.
I've since managed to clean up the situation a bit more, reducing the amount of inter-party coordination needed back to the baseline from part 1. So in this post, I'll describe how to do that. We keep the basic framework of intuitionist logical share splitting, but for convenience build in a way of handling the classical logic side of things too.
Part 3: The Complement and Living in Both Worlds
The basic idea is that, while we do not have (the law of excluded middle) in general, we will introduce a weaker version of it. The intuition is that we want two kinds of negation. The first kind, , we are already familiar with. The second kind is distinct and new. We will call it "complement" instead of "negation". We write the complement of as . The point of the complement is that, while we do not have , we do have . Some version of the law of excluded middle holds for the complement.
Working in a system with both negation and complements lets us get the best of both worlds. We have the standard negation of intuitionist logic, and also a complement, that means that in some sense and cover all possibilities.
In the ticket trading system, we expect things with proofs to ultimately end up being worth $1. But it is not very rare at all for some sentences to be neither provable nor disprovable. Godel established that this must always be a possibility, and it's even more common in intuitionist mathematics. If neither of or have proofs then the eventual price of both must go to 0. But this is very different from what we expect from prediction markets, where the prices of YES and NO to sum to $1.
Fortunately, the prices of and do always sum to $1. This will be shown later in the post. But first I should go ahead and actually explain what the complement even is.
Implementation of the Complement
Declaration of AI use: Originally, I didn't think of the complement as being made of anything smaller. But this started to result in needing a lot of axioms (a total of 4, IIRC), so I asked ChatGPT to look at it and it found this simplification. Maybe in a world without AI I'd have found it anyway, and you'd be reading more or less the same post. Maybe not, hard to know.
Define a special constant . If it must stand for something, it stands for "elsehow". A more informative name (the one ChatGPT gave it), might be "nolem", meaning "No Law of Excluded Middle". is a type. (So it can be occupied or unoccupied, i.e. true or false.) If is unoccupied, this means the law of excluded middle holds.
Constructively, is unoccupied. But also, there is no constructive proof of this (of ).
When working with , we have an additional axiom available to us:
This axiom is what makes meaningful, rather than just another useless constant. If is false, then the axiom simplifies to the law of excluded middle.
So then the definition of the complement is as follows:
That's it. We can substitute this into the axiom above to find , as promised.
Now to prove some things.
Some basic identities
Potentially helpful terminology note: The term "explosion" refers to the principle of explosion, which says that implies any other sentence. This is true in intuitionist logic, not only classical logic. It arises as an automatic consequence of the inductive definition of .
Proof: By explosion.
Proof:
Proof:
Assume .
Then , so by explosion.
Proof:
Assume .
Then , so by explosion.
Proof:
Assume .
Assume .
is .
Proof: They are both true.
Proof:
Assume , which implies .
Assume
Then which is .
Proof of forward direction:
by already-proved identity
by already-proved identity
Proof of reverse direction:
(one of the intuitionistically valid DeMorgan's laws)
which is .
Proof of forward direction:
by already-proved identity
by already-proved identity
Proof of reverse direction:
Case :
Can make both of and by providing .
Case :
and (from our axiom)
Case : done (use )
Case : done (use )
Case : done (use either)
Case :
Use to derive
Done by explosion.
Some Non-identities
For extra clarity, some things that are not properties of :
Complement does not have a cancellation property. I.e. is not the same as . (In any case, I strongly doubt that you'd ever see occurring naturally). A plain language interpretation of might be "there is no proof of ' does not have a proof'".
There is no principle of explosion for complements either.
Cancellation
In part 2, we saw that the law of excluded middle permitted a "cancellation" procedure, where a ticket for and a ticket for could be exchanged for $1. This makes it hard to pay for a resolution to sentence where we'd be happy to accept either a proof of or a proof of . Distributing tickets for both would just result in traders cancelling them without proving either. Removing the law of excluded middle makes cancellation impossible. Now, with the complement, we have a situation where cannot be cancelled, while can, which is exactly what we'd hope for. The key part of the complement is that prices of a sentence and its complement to sum to $1.
Here is to to obtain $1 starting from :
initially
by splitting
by reversible equivalent exchange
is worthless, is worth $1.
As mentioned in part 2, tickets for and remain uncancellable.
So we have shown that prices of a sentence and its complement sum to at least $1. We should now also show that they sum to at most $1.
There is one rule change to the ticket system, besides introducing this new complement construct. It is that instead of handing out tickets for free, we hand out tickets for free. This is strictly more generous than we were before: Because (see the list of identities), by making an irreversible exchange, it's still possible to obtain by giving up . So it's still possible to get for free.
But now, we can obtain nicely from (the identity from above permits it as an irreversible exchange). So for free, we can start with $1, use it to buy , obtain for free, and then run the entire cancellation process above in reverse to obtain , as separate shares (i.e. separate tickets for ).
Work splitting
Xavier is trying to prove a statment . He starts with a ticket for that he wants to sell for at least $0.8 (he obtained it for $0.6 and wants to make a profit). He can prove for some hypothesis .
Step one is to take a ticket for . This can be converted into a ticket for .
This works as follows:
Therefore .
Therefore
So also , which is all Xavier needs to do an irreversible exchange starting from a free ticket.
Similarly, because , he can reversibly exchange for
So he can start with , and after conversions and distributing, gets:
and
Logical share splitting gives:
and
Next: Remember that Xavier knows (because of some secret mathematical insight he has) that . So he can prove that is equivalent to just . So now Xavier has:
and
Helga can prove . Thus, she finds it very cheap to produce tickets for . This works as follows:
Helga can prove , so she can also prove .
She irreversibly exchanges tickets for tickets and is done.
The process was pretty easy and cost nothing, but she still needs to make a profit and right now she's the only one who has a proof of . So thanks to monopoly pricing, she sells tickets for $0.2.
Xavier buys one. Because he spent $0.2 on it, he now needs to make back a whole dollar to hit his profit target. He now has the following tickets:
and and
and can be cancelled to get $1 right away, as described above. Profit target hit! Which is good, because is worthless.
Well, it is worthless in the scenario we've described at least. But Xavier doesn't necessarily know that it is. From his perspective, it may be that is provable and is not. In that case, might end up being worth something, allowing him to obtain a profit of more than $1. (This would only be possible if Helga sold him cheap not because she had a proof of , but because she was speculating that there would turn out to be such a proof.)
At a high level, this is exactly the setup described in the part 1, except with replacing to compensate for the lack of excluded middle. Helga need not know anything about Xavier's purpose in buying tickets. She need not know about the existence of as a conjecture of interest. Meanwhile, Xavier need not know whether Helga has a proof of or is just speculating. Almost zero coordination!
Supply Chains
What if Xavier instead wanted to cheaply produce tickets? The input is cheap tickets. He knows , therefore , so a single irreversible exchange allows him to obtain from (similar to how Helga made from . These tricks allow traders to form entire supply chains to produce various complement tickets cheaply.
Supply Chains with Multiple Dependencies
What if Xavier knows that ? Suppose that Alice has a proof of and Bob has a proof of .
Xavier cheaply buys from Alice and from Bob. He does a share splitting operation to turn this into (typically just waste) and , which is useful for Xavier's production of .
The relevant theorem in probability here is .
TLDR
Add a complement operation . Use the usual negation most of the time. Use the complement when you want things to act like classical logic.
Previously: Logical Share Splitting, Logical Share Splitting for Intuitionists
Recap:
This series is about prediction markets for mathematics.
Imagine a game where players trade tickets with mathematical sentences written on them. A ticket is redeemable for $1 if you can demonstrate a proof of the sentence written on it. (A ticket is like a prediction market share in that sentence.) In this system, it's also allowable to exchange a ticket for another ticket with a logically equivalent sentence written on it, if you can demonstrate a proof of that logical equivalence.
(Actually, this rule can be made even more permissive if we like: It's allowable to exchange an
By issuing tickets in a given sentence for a price of less than $1, you can thus put bounties on mathematical theorems. People can buy the tickets for your lower price and sell them for $1, so long as they can prove the theorem.
This ticket-trading system functions as prediction market for mathematics. The price of a sentence corresponds to what people think the chance is that a proof will be found for it.
For completeness, we have to include a somewhat surprising trading rule into this system: Tickets with sentences
The second post notes that, since a real implementation of this ticket system would involve using an automatic formal proof checker to verify submitted proofs, we should probably pay some attention to how an automatic proof checker actually works. And these proof checkers are constructive by nature. In particular, this means that they don't naturally have the Law of Excluded Middle. Proof checkers can still be used to do classical logic, simply by adding the Law of Excluded Middle as an additional axiom. But they mesh most naturally with intuitionist logic.
In classical logic, there are many equivalent forms of the logical share splitting operation. For example, trading
These classically equivalent rules can be intuitionistically distinct. And of these distinct rules, most of them are invalid. The original rule where we trade
Because of the property of intuitionist logic that the only way to prove
Splitting up the work of writing proofs between multiple minimally-coordinated parties remains possible. However, it becomes somewhat less elegant; and somewhat more coordination is required.
So that was parts 1 and 2.
I've since managed to clean up the situation a bit more, reducing the amount of inter-party coordination needed back to the baseline from part 1. So in this post, I'll describe how to do that. We keep the basic framework of intuitionist logical share splitting, but for convenience build in a way of handling the classical logic side of things too.
Part 3: The Complement and Living in Both Worlds
The basic idea is that, while we do not have
Working in a system with both negation and complements lets us get the best of both worlds. We have the standard negation of intuitionist logic, and also a complement, that means that in some sense
In the ticket trading system, we expect things with proofs to ultimately end up being worth $1. But it is not very rare at all for some sentences
Fortunately, the prices of
Implementation of the Complement
Declaration of AI use: Originally, I didn't think of the complement as being made of anything smaller. But this started to result in needing a lot of axioms (a total of 4, IIRC), so I asked ChatGPT to look at it and it found this simplification. Maybe in a world without AI I'd have found it anyway, and you'd be reading more or less the same post. Maybe not, hard to know.
Define a special constant
Constructively,
When working with
This axiom is what makes
So then the definition of the complement is as follows:
That's it. We can substitute this into the axiom above to find
Now to prove some things.
Some basic identities
Potentially helpful terminology note: The term "explosion" refers to the principle of explosion, which says that
Proof:
Proof:
Assume
Then
Proof:
Assume
Then
Proof:
Assume
Assume
Proof of forward direction:
Proof of reverse direction:
Some Non-identities
For extra clarity, some things that are not properties of
Complement does not have a cancellation property. I.e.
There is no principle of explosion for complements either.
Cancellation
In part 2, we saw that the law of excluded middle permitted a "cancellation" procedure, where a ticket for
Here is to to obtain $1 starting from
As mentioned in part 2, tickets for
So we have shown that prices of a sentence and its complement sum to at least $1. We should now also show that they sum to at most $1.
There is one rule change to the ticket system, besides introducing this new complement construct. It is that instead of handing out
But now, we can obtain
Work splitting
Xavier is trying to prove a statment
Step one is to take a ticket for
This works as follows:
Therefore
Therefore
So also
Similarly, because
So he can start with
Logical share splitting gives:
Next: Remember that Xavier knows (because of some secret mathematical insight he has) that
Helga can prove
Xavier buys one. Because he spent $0.2 on it, he now needs to make back a whole dollar to hit his profit target. He now has the following tickets:
Well, it is worthless in the scenario we've described at least. But Xavier doesn't necessarily know that it is. From his perspective, it may be that
At a high level, this is exactly the setup described in the part 1, except with
Supply Chains
What if Xavier instead wanted to cheaply produce
Supply Chains with Multiple Dependencies
What if Xavier knows that
Xavier cheaply buys
The relevant theorem in probability here is
TLDR
Add a complement operation