First, we’ll invert prices: true statements are worth $0, false statements $1, rather than the usual prices. The market infrastructure will allow anyone with any contract to freely convert that contract into an equivalent one, via atomic steps in the underlying logic. It will also allow traders to create/destroy contracts on axioms for free. So, if a trader knows a proof of some proposition, then they can use the proof to construct a contract on the proposition for $0. Conceptually, it’s similar to linear logic, but based on a very hand-wavy understanding of LL I don’t think they’re equivalent, since truth is free here.
The upshot is that someone with a proof can arbitrage without limit. Their proof will be revealed to the market mechanism (since the mechanism can see which propositions they’re converting between), but not to other traders.
(Also I really like this post. The problem of how to get “deeper” information out of prediction markets is an important one, and these are great ideas.)
This is similar to some stuff Sam was working on. I still personally suspect an equivalence to LL, but haven’t yet made it work.
This post also sorta touches on the problem of synchronous time in logical induction, which you and I discussed via private chat. A better understanding of time in logical induction / radical probabilism would seem useful here.
Yup, that was exactly the chat which got me thinking about the production-of-true-contracts thing. If a production approach worked, then ideally we could remove the deductive process entirely from the LI construction. Then the whole thing would look a lot more like standard economic models, and it should be straightforward to generalize to multiple decentralized markets with arbitrage between them.
Competing cross-market arbitrageurs would bound divergence between prices in different markets—it only takes a small price difference for an arbitrageur to move large quantities from one market to another. As a result, prices of all markets end up (nearly) identical, and the whole thing acts as a single market. The more general principle at work here: two markets in equilibrium act like a single market.
Mathematically: each market mechanism is computing a fixed point, and simultaneously solving two coupled fixed-point problems is equivalent to solving a single fixed-point problem.
In principle, this would also work for normal LI, but the deductive process would still be a single monolithic interface to the rest of the world, so we wouldn’t really gain much from it. With truth-producers, the producers can be spread across sub-markets.
Here’s one potential way to handle proofs.
First, we’ll invert prices: true statements are worth $0, false statements $1, rather than the usual prices. The market infrastructure will allow anyone with any contract to freely convert that contract into an equivalent one, via atomic steps in the underlying logic. It will also allow traders to create/destroy contracts on axioms for free. So, if a trader knows a proof of some proposition, then they can use the proof to construct a contract on the proposition for $0. Conceptually, it’s similar to linear logic, but based on a very hand-wavy understanding of LL I don’t think they’re equivalent, since truth is free here.
The upshot is that someone with a proof can arbitrage without limit. Their proof will be revealed to the market mechanism (since the mechanism can see which propositions they’re converting between), but not to other traders.
(Also I really like this post. The problem of how to get “deeper” information out of prediction markets is an important one, and these are great ideas.)
This is similar to some stuff Sam was working on. I still personally suspect an equivalence to LL, but haven’t yet made it work.
This post also sorta touches on the problem of synchronous time in logical induction, which you and I discussed via private chat. A better understanding of time in logical induction / radical probabilism would seem useful here.
Yup, that was exactly the chat which got me thinking about the production-of-true-contracts thing. If a production approach worked, then ideally we could remove the deductive process entirely from the LI construction. Then the whole thing would look a lot more like standard economic models, and it should be straightforward to generalize to multiple decentralized markets with arbitrage between them.
Oh hmmm. How would the generalization work?
Competing cross-market arbitrageurs would bound divergence between prices in different markets—it only takes a small price difference for an arbitrageur to move large quantities from one market to another. As a result, prices of all markets end up (nearly) identical, and the whole thing acts as a single market. The more general principle at work here: two markets in equilibrium act like a single market.
Mathematically: each market mechanism is computing a fixed point, and simultaneously solving two coupled fixed-point problems is equivalent to solving a single fixed-point problem.
In principle, this would also work for normal LI, but the deductive process would still be a single monolithic interface to the rest of the world, so we wouldn’t really gain much from it. With truth-producers, the producers can be spread across sub-markets.