Logical inductors consider belief-states as prices over logical sentences ϕ in some language, with the belief-states decided by different computable “traders”, and also some decision process which continually churns out proofs of logical statements in that language. This is a bit unsatisfying, since it contains several different kinds of things.
What if, instead of buying shares in logical sentences, the traders bought shares in each other. Then we only need one kind of thing.
Let’s make this a bit more precise:
Each trader is a computable program in some language (let’s just go with turing machines for now, modulo some concern about the macros for actually making trades)
Each timestep, each trader is run for some amount of time (let’s just say one turing machine step)
These programs can be well-ordered (already required for Logical Induction)
Each trader pi is assigned an initial amount of cash according to some relation ae−b×i
Each trader can buy and sell “shares” in any other trader (again, very similarly to logical induction)
If a trader halts, its current cash is distributed across its shareholders (otherwise that cash is lost forever)
(Probably some other points, such as each trader’s current valuation of itself: if no trader is willing to sell its own shares, how does that work? does each trader value its own (still remaining) shares proportional to its current cash stock? how are the shares distributed at the start?)
This system contains a pseudo-model of logical induction: for any formal language which can be modelled with turing machines, and for any formal statement in that language, there exists a trader with some non-zero initial value, which lists out all possible statements in that language, halting if (and only if) it finds a proof of its particular proposition. This makes a couple of immediately obvious changes from Logical Induction:
There’s a larger “bounty” (i.e. higher cash prize) for proving simpler statements given by earlier turing machines, since the earlier a particular prover turing machine is expressed in our ordering, the larger its starting cash
We don’t have to also define a particular speed/order in which logical statements proofs become available, since it’s already part of the system
The market’s “belief” in that statement can be expressed as that particular turing machine’s share price divided by its cash holdings
We can also intervene in the market by distributing cash to certain traders, or setting up a forcible halting rule on traders.
Does this actually do the logical induction thing? I have no clue.
Neat idea, I’ve thought about similar directions in the context of traders betting on traders in decision markets
A complication might be that a regular deductive process doesn’t discount the “reward” of a proposition based on its complexity whereas your model does, so it might have a different notion of logical induction criterion. For instance, you could have an inductor that’s exploitable but only for propositions with larger and larger complexities over time, such that with the complexity discounting the cash loss is still finite (but the regular LI loss would be infinite so it wouldn’t satisfy regular LI criterion)
(Note that betting on “earlier propositions” already seems beneficial in regular LI since if you can receive payouts earlier you can use it to place larger bets earlier)
There’s also some redundancy where each proposition can be encoded by many different turing machines, whereas a deductive process can guarantee uniqueness in its ordering & be more efficient that way
Are prices still determined using Brouwer’s fixed point theorem? Or do you have a more auction-based mechanism in mind?
Simplified Logical Inductors
Logical inductors consider belief-states as prices over logical sentences ϕ in some language, with the belief-states decided by different computable “traders”, and also some decision process which continually churns out proofs of logical statements in that language. This is a bit unsatisfying, since it contains several different kinds of things.
What if, instead of buying shares in logical sentences, the traders bought shares in each other. Then we only need one kind of thing.
Let’s make this a bit more precise:
Each trader is a computable program in some language (let’s just go with turing machines for now, modulo some concern about the macros for actually making trades)
Each timestep, each trader is run for some amount of time (let’s just say one turing machine step)
These programs can be well-ordered (already required for Logical Induction)
Each trader pi is assigned an initial amount of cash according to some relation ae−b×i
Each trader can buy and sell “shares” in any other trader (again, very similarly to logical induction)
If a trader halts, its current cash is distributed across its shareholders (otherwise that cash is lost forever)
(Probably some other points, such as each trader’s current valuation of itself: if no trader is willing to sell its own shares, how does that work? does each trader value its own (still remaining) shares proportional to its current cash stock? how are the shares distributed at the start?)
This system contains a pseudo-model of logical induction: for any formal language which can be modelled with turing machines, and for any formal statement in that language, there exists a trader with some non-zero initial value, which lists out all possible statements in that language, halting if (and only if) it finds a proof of its particular proposition. This makes a couple of immediately obvious changes from Logical Induction:
There’s a larger “bounty” (i.e. higher cash prize) for proving simpler statements given by earlier turing machines, since the earlier a particular prover turing machine is expressed in our ordering, the larger its starting cash
We don’t have to also define a particular speed/order in which logical statements proofs become available, since it’s already part of the system
The market’s “belief” in that statement can be expressed as that particular turing machine’s share price divided by its cash holdings
We can also intervene in the market by distributing cash to certain traders, or setting up a forcible halting rule on traders.
Does this actually do the logical induction thing? I have no clue.
Neat idea, I’ve thought about similar directions in the context of traders betting on traders in decision markets
A complication might be that a regular deductive process doesn’t discount the “reward” of a proposition based on its complexity whereas your model does, so it might have a different notion of logical induction criterion. For instance, you could have an inductor that’s exploitable but only for propositions with larger and larger complexities over time, such that with the complexity discounting the cash loss is still finite (but the regular LI loss would be infinite so it wouldn’t satisfy regular LI criterion)
(Note that betting on “earlier propositions” already seems beneficial in regular LI since if you can receive payouts earlier you can use it to place larger bets earlier)
There’s also some redundancy where each proposition can be encoded by many different turing machines, whereas a deductive process can guarantee uniqueness in its ordering & be more efficient that way
Are prices still determined using Brouwer’s fixed point theorem? Or do you have a more auction-based mechanism in mind?