# 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.

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.

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).