Logical Share Splitting for Intuitionists

DaemonicSigil

Logical Share Splitting

I previously wrote a post based on the following law in probability theory:

This law relates the probabilities of given individual statements to the probabilities of logical combinations of them. Prediction market prices should approximate probabilities, and by combining this with the above equation, we produce a new rule for a kind of trade that prediction markets should allow, namely: A share in A and a share in B should be exchangeable for a share in A∧B and a share in A∨B (and the reverse of this should likewise be allowable). Such a trade is called a logical share split, and it lets us do several nice things:

Construct arbitrary logical combinations of prediction market outcomes.
In markets that incentivize ^[1] finding formal proofs of theorems, provide a mechanism for traders to subdivide the work of proving a given theorem between themselves.
Allow traders to “double-invest” invest conditional prediction markets on the two opposing sides of a given condition, without doubling the required capital.

This image provides some justification for the logical share splitting operation:

Imagine scattering dots representing possible worlds between the quadrants of the square, so that each world falls into some quadrant. The top two quadrants are where A is true. The right two quadrants are where B is true. So a dot in the top right quadrant is a world where both A and B are true. Blue shading indicates “having shares that are worth money” (in a prediction market, shares are only worth money if the corresponding proposition is true).

The first equation represents having a share in A and a share in B. The second equation represents a share in A∧B and a share in A∨B. The fact that the two equations have the same right-hand side means that going back and forth between the two situations doesn’t fundamentally change anything. Therefore, logical share splitting should always be an allowable operation.

Adding Intuitionism

One open problem with this market design as described in my previous post is that it allows the rejoining of shares in A and ¬A to produce $1, which means that if someone wants to subsidize finding either a proof OR a disproof of some open mathematical question A, they can’t just print ^[2] a bunch of shares of each one. Why?

Well, if we knew we were looking for a proof of A and not a disproof, things would be easy: We could just print shares in A alone. These could only be redeemed for $1 if it were possible to prove A. But having a bunch of shares of A and ¬A hanging around doesn’t mean that they only have value if a proof or disproof is found. It means that they have value right away because they can be cancelled with each other to yield $1. And once all those shares have been cancelled, there’s no value for traders in continuing to search for a proof or disproof.

Here’s how a trader holding both A and ¬A would perform the cancellation:

Do the logical share splitting operation to transform A and ¬A into A∧¬A and A∨¬A.
A∧¬A is logically equivalent to False. Worth $0.
A∨¬A is logically equivalent to True as a consequence of the Law of Excluded Middle. Worth $1.

It looks like the thing that caused the problem (that traders can weasel their way out of having to prove or disprove our theorem) was the Law of Excluded Middle (LEM). Is there some way we can just… not have the Law of Excluded Middle?

The answer is yes! And when we do this, we get something called Intuitionist Logic, which provides a way of doing mathematics without ever assuming LEM. In fact, formal proof languages like Lean and Agda most naturally operate in terms of intuitionist logic! While these languages can deal with classical logic, they do so simply by bolting on LEM as an additional assumption.

Without LEM, it’s not possible to prove that A is equivalent to ¬¬A. These are two different statements in intuitionist logic. Negation no longer undoes itself here. ^[3]

This all has an enormous number of fascinating consequences, but the one that concerns us most here is that the above trick for cancelling shares with their negations no longer works. We can print copies of A and ¬A with impunity and nobody can ruin our day by turning them back into money, at least not without proving one or the other, which is what we wanted them to be doing anyway.

But does adding intuitionism break everything?

A fairly important part of logical share splitting for mathematical markets is the fact that it allows traders who separately know how to prove A and A → B to collectively act as though they know how to prove B without too much coordination effort. Let’s say trader Alice can prove A and trader Bob ^[4] can prove A → B. Then if some B shares have been printed, but are publicly trading at a price of $0.8 because of the labour and uncertainty involved in finding a proof, Alice and Bob can do the following:

Bob buys a share of B for $0.8.
He irreversibly converts it to B∧(A∨¬A).
- Irreversible conversion is an operation where rather than trading for a logically equivalent statement as per usual (operation can be undone and the trader is protected from losing value), one trades for a logically stronger statement (cannot be undone, allows the trader to destroy some or all of the value of that share).
- It’s a bit like using unsafe in Rust: The guardrails that prevent the user from shooting themselves in the foot are removed.
B∧(A∨¬A) is equivalent to (B∧A)∨(B∧¬A).
False (costs $0 to obtain) is equivalent to (B∧A)∧(B∧¬A).
Bob does logical share splitting to obtain a share in B∧A and a share in B∧¬A.
The latter is junk in this case, but B∧A is equivalent to A if you are Bob and you can prove A → B. Bob does the conversion.
Bob sells his A share for $0.9. He has made a profit of $0.1. Alice buys it. Note how little coordination was needed here. Alice didn’t even need to know that Bob was buying B shares. Perhaps she simply saw an order go up selling A shares and filled it.
Because Alice has a proof for A, it is equivalent to True for her. She redeems her share for $1, making a profit of $0.1.

So one of the fundamental advantages of logical share splitting, its ability to allow separate traders to combine their lemmas, is preserved. It looks like intuitionism doesn’t break everything. ^[5]

The Middle Regions

If we’re missing the law of excluded middle, that means that a middle truth value between true and false actually exists, or at least we can’t prove that it doesn’t. So we have to replace our four quadrant diagram above with a nine cell diagram like this:

This image shows which of our statements A, B or their negations are probable in various possible worlds.

Of course, even in classical logic, it was possible for things to be undecidable, since that’s more about provability than mere truth values. It’s just even more relevant now and doesn’t only occur for special cases like the halting problem.

Let’s check that logical share splitting still conserves the payouts we get for a world in any of the nine cells in this diagram. Here’s the situation when we’re starting out with a share in A and a share in B:

This image shows which of our holdings A, B have proofs (and are therefore worth $1) in various possible worlds.

We can just figure out which statements have proofs by reading off of the previous image. After doing logical share splitting, we have a share in A∨B and a share in A∧B. Here is a diagram for that situation:

This image shows which of our holdings A∨B, A∧B have proofs (and are therefore worth $1) in various possible worlds.

Let’s briefly justify this last diagram:

A proof of A∧B is literally a pair consisting of a proof of A and a proof of B. So it can only be proved in the lower right cell where we have both.
A proof of A∨B is sum type which can be constructed only by either proving A or proving B. If neither of them is provable, then their disjunction is not provable either. So A∨B can only be proved in the lower row of cells or in the rightmost column of cells.

So even if we account for undecidability, intuitionist logical share splitting is always allowable. ^[6]

Important note if you skipped reading the original post: There is a trading rule that lets people convert shares in one statement to shares in any other statement that they can prove is logically equivalent. So if there are a lot of shares in the statement of some theorem hanging around, there is an incentive for people to prove that theorem so they can buy those shares and convert them to shares in True. (Shares in True are, as you might expect, worth $1.) ↩︎
“Printing” is when the market mechanism (the entity that defines the existence of shares, tracks who owns them, and implements the allowable trading rules) brings new shares into existence by fiat. The term is meant to evoke the image of a mint printing money. People who want a theorem proved can pay the market mechanism dollars to print shares in that theorem. (This is basically just a way of putting a bounty on a problem.) ↩︎
In formal proof systems, negation is built from the more primitive concept of implication. So ¬A actually means A → False. ↩︎
We’re copying the naming scheme from cryptography. It’s probably for the best that trading/finance scenarios requiring more than 9 traders at once are not very likely. ↩︎
You might like to read to Alice-Bob example in the original post and contrast with this one. That example inherently requires the law of excluded middle to make use of the ¬A share, and does not carry over to the intuitionist case. It seems we are not able to mix across polarities like that in intuitionist logic. But this method, which ultimately accomplishes the same result, works fine. ↩︎
Some alternate classical versions of logical share splitting are not intuitionistically valid. For example, ¬A, B being exchanged for ¬A∧B, A→B is a classically valid logical share split. However, even if A and B are both undecidable, it may still be possible to find a proof of A→B, despite being unable to find a proof or disproof of either individually. (Because classical logic does still have undecidable statements, one could argue that this makes classical logical share splitting itself invalid, at least in some sense.) The possibility that two statements could be undecidable but an implication between them could be provable is actually quite interesting. I may write a future post about it. ↩︎

The part I'm confused about is why Bob converts into . If the exchange is allowing you to convert shares into equivalent shares so long as you provide a proof that they are equivalent, why not make the more general rule that you can convert shares into stronger shares so long as you provide a proof that they are stronger? That way, you can directly convert shares in into shares in when you provide a proof of . I think that would simplify the whole business a lot.

Also, I think a weak part of this idea in either conception is that you have to provide a proof to make these exchanges. I think it would be neat for an exchange to have a proof-verifier, but that doesn't really seem to hold up to the promise of Alice and Bob working collectively to prove without a central authority who knows both and .

Yeah, this is exactly the "irreversible conversion" described above. As you point out, it would allow Bob to directly convert from shares to shares. Why do the more complicated procedure described above then? Well, Bob also gets (alongside ) from doing that procedure. In that specific example such shares are useless so there's effectively no difference, but in some cases it could be that Bob is unsure and thinks has some chance to end up being provable and so wants to end up with both in order to hedge.

Yeah, the exchange is a central authority that does get to know everything here. I haven't even really thought much about what a decentralized version of this would look like yet. Probably it would involve zero-knowledge proofs? Thanks for pointing my thoughts in this direction, I'll have to consider it more.

Perhaps another way to go about this is to introduce GL modal logic. Instead of creating shares in and , create shares in and . It's not possible to exchange a pair of shares in and for cash, because is not a logical tautology.

Yeah, that is kind-of the direction my thoughts went in when I wrote the first post. I was thinking then that would be formalized by formalizing a proof system and letting correspond to the statement that has a proof in that system. This looks quite complicated to implement, and also to use.

If there is a more synthetic version where is a fundamental part of the formal system, then maybe that is a lot easier to deal with? I'm not sure how one implements such a thing in a proof checker. ^[1] Is just a functions from types to types? Surely it is not as simple as that?

I found this, but I don't understand it at all right now. ↩︎

Well, if we knew we were looking for a proof of A and not a disproof, things would be easy: We could just print shares in A alone. These could only be redeemed for $1 if it were possible to prove A. But having a bunch of shares of A and ¬A hanging around doesn’t mean that they only have value if a proof or disproof is found. It means that they have value right away because they can be cancelled with each other to yield $1. And once all those shares have been cancelled, there’s no value for traders in continuing to search for a proof or disproof.

why is this a problem?

how does the attacker acquire the shares in A and not-A? they have to buy one of each, right? so presumably price(A) + price(not-A) = $1 +/- some transaction costs.

this seems like a desirable property of the market (if we accept the l.e.m.), since it ensures that the price of A (which we can interpret as the probability that A is true) is equal to $1 - price(not-A).

if we turn dollars into A + not-A, and allow them to trade on the open market, why is anyone incentivized to turn them back into dollars, unless they are closing out a position after market moves?

It's not a huge problem, but it is a minor problem, at least for people trying to set bounties on a problem.

In the intuitionist version, the prices of a statement and its negation can sum to at most $1, but less is possible. (As you say, they sum to exactly $1 if one assumes LEM.) ^[1] If traders know that a statement is undecidable, for example, then this sum should be $0 and not $1. They don't expect to be able to redeem shares in either the statement or its negation.

Imagine that I am trying to offer a bounty on a problem with statement , which can be resolved both by proving or by disproving the statement. I can sell a pair for some price . If we assume LEM:

If I set the price below $1, then people can get free money without proving the theorem by cancelling shares.
If I set the price at $1, then the deal I'm offering people who try to prove my theorem is that they can pay $1 to put in a bunch of effort to prove a theorem, from which they'll then earn $1, for a profit of $0.
Even if we account for transaction costs, cancelling shares is usually going to be much easier than proving theorems, so it will become profitable first.
Therefore, I have to set equal to $1 as the least of two evils. Provers can still make a profit by proving theorems if the market is trading at an intermediate price like $0.5, because they can use their inside knowledge from proving the theorem to correct the market. But this is not relevant in cases where "everyone knows" that the theorem should be true, but the hard part is to find a proof.

On the other hand, if cancellation is no longer possible, then the best option is simply to set less than $1. In a world where (or ) is provable, I do lose money. But that can only happen with a proof of (or ), which is exactly the thing I was trying to bounty.

Because an irreversible conversion from $1 to is possible, we have . It's always possible to create opposing shares in a statement. The reverse is not always possible (though it's possible for "oracle" statements that point to real-world events, i.e. the kind of statements that would be traded on non-mathematical prediction markets). ↩︎

I found this, but I don't understand it at all right now. ↩︎

Well, if we knew we were looking for a proof of A and not a disproof, things would be easy: We could just print shares in A alone. These could only be redeemed for $1 if it were possible to prove A. But having a bunch of shares of A and ¬A hanging around doesn’t mean that they only have value if a proof or disproof is found. It means that they have value right away because they can be cancelled with each other to yield $1. And once all those shares have been cancelled, there’s no value for traders in continuing to search for a proof or disproof.