Existence Proof of Logical Inductor

https://arbital.com/p/Logical_Induction_Algorithm_2016

by Tarn Somervell Fletcher Apr 12 2017 updated Apr 26 2017

A procedure for constructing an algorithm that is a logical inductor relative to any given deductive set.


Broad description

Recall that a market $~$\overline{\mathbb{P}}$~$ is said to satisfy the logical induction criterion relative to a deductive process $~$\overline{D}$~$ if there is no efficiently computable trader $~$\overline{T}$~$ that (plausibly) exploits $~$\overline{\mathbb{P}}$~$ relative to $~$\overline{D}$~$. A market that meets this criterion is called a logical inductor. Section 5 of the paper shows how to construct a computable belief sequence $~$\overline{LIA}$~$ given a deductive process $~$\overline{D}$~$ that satisfies this criterion.

Basically, the idea is that we can use Brouwer's Fixed-Point Theorem to construct a market that is never exploited by a particular trader relative to any deductive process, by approximating the appropriate fixed point. This can be interpreted as finding the trader's 'fair prices' for each day, so that the trader will mostly abstain from betting for that day, and earn at most a very small amount of value in all worlds. Then, we construct an supertrader to use this construction on to create the market. By cleverly building this trader out of an underlying set of traders, we can ensure that if the supertrader never exploits the market, neither do any of the underlying traders. By building the supertrader from an infinite sequence of traders and pitting it against the market in a recursion, we can find the fixed point that guarantees the market isn't exploited by any trader.

LIA is constructed by three subroutines, MarketMaker, TradingFirm, and Budgeter. Budgeter takes a trader, and turns into another trader with a potential loss bounded below by some constant $~$-b$~$, but leaves the trader untouched if it wouldn't have fallen below $~$-b$~$ otherwise. TradingFirm uses Budgeter to create a supertrader that exploits the marker whenever any trader does by using a computable enumeration of all traders and using more of them each day. MarketMaker constructs an inexploitable market based on the supertrader created by TradingFirm.

Details of MarketMaker

MarketMaker takes some trader $~$\overline{T}$~$ as an input and on each day $~$n$~$ sets price $~$\mathbb{P}_n$~$ on that day that guaruntee that the trades $~$T_n(\mathbb{P}_{\leq n})$~$ earns at most a small positive value. It does this by finding an approximate fixed point of the "price adjustment" function $~$\text{fix}(\mathbb{V})(\phi) := \max{(0,\min{(1, \mathbb{V}(\phi) + T(\mathbb{P}_{\leq n-1},\mathbb{V})[\phi])})}$~$. This map is a continuous function from the space of all valuations to itself, and so Brouwer's fixed point theorem applies.

Accordingly, it has some fixed point $~$\mathbb{V}^{\text{fix}}$~$ of the mapping - that is, for all sentences $~$\phi$~$, $~$\mathbb{V}^{\text{fix}}(\phi)= \max{(0,\min{(1, \mathbb{V}^{\text{fix}}(\phi) + T(\mathbb{P}_{\leq n-1},\mathbb{V}^{\text{fix}})[\phi])})}$~$

Basically, how this works is the function pushes prices up if the n-strategey would buy the shares, and down if it would sell them. Then, because the function satisfies the technical details of being a 1) continuous function mapping a 2) compact, 3) convex space onto 4) itself - namely $~$\mathcal{V}' \to \mathcal{V}'$~$. $~$\mathcal{V}'$~$ is $~$[0,1]^{S'}$~$, so it definitely fits. With a function matching those assumptions, Brouwer guarantees the existence of some point $~$x$~$ for which $~$f(x)=x$~$ - the function doesn't change anything.

Applying this to $~$\text{fix}\mathbb{V}(\phi)$~$ guarantees that any shares $~$T$~$ buys at the fixed point have value 1, and any shares it sells have a value of 0. Accordingly, in every single world the trader either loses or breaks even. MarketMaker finds a computable approximation, call it $~$\mathbb{P}$~$ to that fixed point, so that those conditions are true to within some small positive error - that is, the shares $~$T$~$ buys have value greater than $~$1-2^{-n}$~$, and those shares it sells have value less than $~$2^{-n}$~$.

Details of Budgeter

Budgeter modifies a trader to limit its' possible losses without affecting its' possible wins. It is a function $~$B(n,b, T_n, \mathbb{P}_{\leq n-1})$~$ taking as inputs two positive integers (a day and a lower bound), an n-strategy history (the past and current trades made by a trader), and a $~$(n-1)$~$ belief history (The set of prices set by the market on past days), and outputs another n-strategy. If there’s a day $~$m<n$~$ s.t. a P.C. world on day m thinks the total holdings of the n-strategy history over the first m days are worth less than -b, BUDGETER outputs 0. Basically, if the trader overspends their budget, BUDGETER forbids them from making any future trades. Otherwise, it multiplies the input trader by a scale factor determined by the possible ratio of losses to the remaining money in the budget (basically, the infimum over all possible worlds of 1 or the inverse of that ratio, whichever is smaller).

Details of TradingFirm