Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: What happens with logical induction when..., published by Donald Hobson on March 26, 2023 on The AI Alignment Forum.

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 P(X) towards 1−P(¬X) unbounded downside risk (downside risk of n on day n) ) This means the program would lose infinite money if X and ¬X 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 ¬X, and the bot described above trying to make P(X)+P(¬X)=1 ) 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?

Thanks for listening. To help us out with The Nonlinear Library or to learn more, please visit nonlinear.org.