My shitty guess is that you're basically right that giving a finite set of programs infinite money can sort of be substituted for the theorem prover. One issue is that logical inductor traders have to be continuous, so you have to give an infinite family of programs "infinite money" (or just an increasing unbounded amount as eps -> 0)
I think if these axioms were inconsistent, then there wouldn't be a price at which no trades happen so the market would fail. Alternatively, if you wanted the infinities to cancel, then the market prices could just be whatever they wanted (b/c you would get infinite buys and sells for any price in (0, 1)).
So this is a bunch of related technical questions about logical induction.
Firstly, do you need the formal theorem prover section? Can you just throw out the formal theorem prover, but give some programs in the market unbounded capital and get the same resultant behaviour? (For example, give the program that bets towards unbounded downside risk (downside risk of n on day n) ) This means the program would lose infinite money if X and both turned out to be true.
I think that any axioms can be translated into programs. And I think such a setup, with some finite number of fairly simple programs having infinite money available produces a logical inductor. Is this true?
What happens when the axioms added under this system are inconsistent. (so this is a logical induction market, without a theorem prover to settle the bets, and with agents with unlimeted money betting both for and against X, possibly indirectly like the bot betting for X, the bot betting for , and the bot described above trying to make ) Can the other agents make unbounded money? Do the prices converge? If I added a bot with infinite money that was convinced fermats last theorem was false to a consistent ZFC system, would I get a probability distribution that assigned high probability to basic arithmetic facts in the limit? Does this make a sensible system for logical counterfactuals?