Logical Share Splitting for Intuitionists

DaemonicSigil19 May 2026 0:42 UTC
19 points
9 comments5 min readLW link

Link post

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” in 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]

  1. ↩︎

    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.)

  2. ↩︎

    “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.)

  3. ↩︎

    In formal proof systems, negation is built from the more primitive concept of implication. So ¬A actually means A → False.

  4. ↩︎

    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.

  5. ↩︎

    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.

  6. ↩︎

    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.

DaemonicSigil19 May 2026 0:42 UTC
19 points
9 comments5 min readLW link