# 11

Logical InductionWorld Modeling
Frontpage

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?