So, to begin with, here's how the algorithm works.

The upstream algorithm iterates through all proofs, and records the lengths of all proofs of the form "a finite collection of sentences implies $\perp$". Also the proof length accounting is set up such that if $A,\varphi {⊢}_L\perp$ and $A,\psi {⊢}_L\perp$, then $A,\varphi \vee \psi {⊢}_{L+L^{\prime }}\perp$. Also, as soon as it checks all proofs of length $n$ or shorter from $A$+propositional tautology given $A$, with no contradictions found, it reports that $A$ is contradiction-free for at least $n$ steps. (this doesn't require searching an infinite set because the number of propositional tautologies with length shorter than $n$ is finite)

With $S$ being the set of all math sentences, and $P_{fin,pc}\left(S\right)$ being the set of all finite subsets of sentences that are propositionally consistent, the market $P$ is a partial of type $P_{fin,pc}\left(S\right)\times S\to [0,1]$, which fulfills the following four axioms.

(note: $A$ appearing where a sentence would normally go refers to the collection of statements in $A$ expressed as one big boolean and-statement, and $\varphi {⊢}_{pc}\psi$ means that given $\varphi$, $\psi$ is provable using only the rules of inference for propositional calculus)

1: Unitarity. $\forall A:P_A\left(A\right)=1$

2: Subadditivity. $\forall A,\varphi ,\psi :P_A\left(\varphi \right)+P_A\left(\psi \right)\ge P_A(\varphi \vee \psi )$

3: Law of Excluded Middle. $\forall A,\varphi :P_A\left(\varphi \right)+P_A\left(\neg \varphi \right)=1$

4: Propositional Monotonicity: $\forall A,\varphi ,\psi :A,\varphi {⊢}_{pc}\psi \to P_A\left(\psi \right)\ge P_A\left(\varphi \right)$

We will also consider a fifth axiom, propositional equivalence, which is implied by axiom 4.

5: Propositional Equivalence: $\forall A,\varphi ,\psi :A{⊢}_{pc}\varphi \leftrightarrow \psi \to P_A\left(\psi \right)=P_A\left(\varphi \right)$

The market fulfills axioms 1-4, the worlds we are defending against fulfill axioms 1-3 and 5. Axioms 1, 3, and 5 suffice to show the empty set property that $P_A\left(\perp \right)=0$, so that one comes for free and doesn't need to be specified.

Traders are poly-time algorithms that output a continuous circuit that takes as input the pricing $P$ and output a nonnegative number for each pair of the form $(A,\varphi )$. This should be interpreted as a bet against $\varphi$ in the $A$ counterfactual, and has a payoff of $P_A\left(\varphi \right)-V_A\left(\varphi \right)$. Due to law of excluded middle for both $V$ and $P$, selling these statements is exactly equivalent to betting against $\neg \varphi$.

The budgeting of the traders works the same way as usual, although dealing with finding the worst-case value for a trader's trades takes a bit more care since the space of allowable valuations isn't discrete. Also, the proof that the supertrader exploits if any component does goes through in the same way.

Let's show that finding the worst-case valuation is computable. We can split the trader's pile of shares into a bunch of subpiles, one for each $A$, and minimize these individually. For each A-pile, there's a finite collection of sentences $S$ that have been bet on. Then, define the following subset of $[0,1{]}^S$. The set of valuations that fulfill unitarity, subadditivity, known proof length bounds, law of excluded middle, and propositional equivalence (assumed to exist by previous post). Since the proof searcher reports the lengths of proofs it has found, as well as when it has verified that no disproofs exist below a certain length, this imposes rational number upper bounds on how much to value a sentence at. The set of valuations that fulfill all the constraints (again, assuming existence) is convex, compact, and defined by finitely many inequalities and equalities. The equation giving the wealth of the trader in a valuation, ${\sum }_{\varphi ,n}{c}_{\varphi ,n}\left(P_{n,A}\right(\varphi )-V_A(\varphi \left)\right)$ is linear because the prices just turn into constants, so it's just a "minimize this linear function over this definable convex set" problem, which there are well-known algorithms for. Do this for all $A$ and sum up the answers to get a worst-case value for the trader.

Now, finally, we need to show that given any bet from the supertrader, there exists a nonempty compact convex set of prices that fulfill all our axioms, make the bet unwinnable, and the function from prices to sets of prices has closed graph. Then we just need to apply the Kakutani fixed-point theorem, and argue that there is a neighborhood of points around the fixed point where it is verifiable that only a tiny amount of money could be earned, and we'll have our proof-length inductor and can start analyzing which nice properties it gets.

Definitions To State Fixpoint Proof:

Let $A$ be the set of all finite batches of sentences specified in the supertrader trade. This is basically "all the counterfactuals specified by a share someone purchased".

Let $S^{\ast }$ be the (infinite) set of sentences specified by: taking all the sentences specified in the supertrader trade (whether as part of some counterfactual $A$, or as a sentence named in a bet), breaking them down into atomic sentences (see page 12 in the logical induction trade), and making all possible boolean combinations of them. So if a sentence is a boolean combination of atomic sentences that all show up as a subformula of some sentence that some trader bet on, or as a subformula of some sentence in $\bigcup A$, it's in $S^{\ast }$.

Let $\Xi$ be the set of all functions of type $A\times S^{\ast }\to [0,1]$ that fulfills the four axioms of unitarity, subadditivity, law of excluded middle, and propositional monotonicity. The market prices are in this set.

Let $\Lambda$ be the set of all functions $A\times S^{\ast }\to [0,1]$ that fulfill the four axioms of unitarity, subadditivity, law of excluded middle, and propositional equivalence. The worlds we are defending against are the subset of this space which obeys the proof-length bounds that have been discovered so far.

$T$ is the continuous function that corresponds to the supertrader, a function of type $\Xi \to R_{\ge 0}^{A\times S^{\ast }}$, which gives the number of shares purchased for a particular $A,\varphi$ pair, which is non-negative (because selling shares of $\varphi$ is exactly the same as buying shares of $\neg \varphi$)

Now we can finally state our desired theorem.

Theorem 1:

$\exists P\in \Xi :\forall V\in \Lambda :{\sum }_{A,\varphi }T\left(P{)}_{A,\varphi }\right(P_A\left(\varphi \right)-V_A\left(\varphi \right))\le 0$

Or, in other words, there exists a set of prices which fulfills the four axioms, which ensures that in all possible worlds, the supertrader doesn't gain any money. Due to the continuity of $T$, a tiny change in $P$ results in the sum being bounded above by $ϵ$, so we can find such a $P$ by brute-force search.

Time for the proof.

Definitions For Proof Of Theorem 1:

Let $S$ be the set of all atomic sentences specified in the supertrader trade (whether as part of some counterfactual $A$, or as a sentence named in a bet), produced by breaking them down into atomic sentences. So if an atomic sentence shows up as a subformula of some sentence that some trader bet on, or as a subformula of some sentence in $\bigcup A$, it's in $S$. This set is finite. Or you can consider it as the set of all atomic sentences that appear in some sentence in $S^{\ast }$. As a toy example, if there's just a single bet on $(A,\varphi )$, it'd be all atomic sentences that appear as part of a sentence in $A$, or as a part of $\varphi$.

(yes, we used $S$ before to denote a different set while talking about worst-case world scoring. Sorry about that. We'll be consistent from this point on.)

$P$ is used to denote the powerset. $P\left(S\right)$ is the set of "worlds" (assignments of each statement under consideration to true or false). $P\left(P\right(S\left)\right)$ is the set of all subsets of worlds.

$L$ is the finite lattice produced by ordering $P\left(P\right(S\left)\right)$ by set inclusion. In this lattice, inf corresponds to set intersection, sup corresponds to set union.

$f$ is the surjective function of type $S^{\ast }\to L$, given by mapping a boolean to the set of worlds where it's true.

$g$ is the function of type $A\to S^{\ast }$ given by turning the collection of sentences which specify a counterfactual into a single sentence via ordering the sentences somehow and boolean and-ing them all together. Composing $f$ and $g$ lets you turn a collection of sentences defining a counterfactual into a single node in the powerset lattice $L$.

${\Xi }^{\prime }$ is the set of all functions $A\times L\to [0,1]$ which fulfill the following four axioms, which are the analogue of the four defining axioms for $\Xi$, but in the powerset lattice:

1: Unitarity: $\forall A\in A:V_A\left(f\right(g\left(A\right)\left)\right)=1$

2: Subadditivity: $\forall A\in A,E,F\in L:V_A\left(E\right)+V_A\left(F\right)\ge V_A(E\cup F)$

3: Law of excluded middle: $\forall A\in A,E\in L:V_A\left(E\right)+V_A\left(P\right(S\left)/E\right)=1$

4: Monotonicity: $\forall A\in A,E,F\in L:f\left(g\right(A\left)\right)\cap E\subseteq f\left(g\right(A\left)\right)\cap F\to V_A\left(E\right)\le V_A\left(F\right)$

Let $t$ be the function ${\Xi }^{\prime }\to \Xi$ s.t. $t\left(V{)}_A\right(\varphi )=V_A(f\left(\varphi \right))$. This translates a valuation over the powerset lattice to a valuation over sentences, because each sentence denotes a node in the powerset lattice via $f$, and $f$ is surjective. The defining axioms for ${\Xi }^{\prime }$ carry over to imply the defining axioms for $\Xi$.

Let $r$ be the function of type $R_{\ge 0}^{A\times S^{\ast }}\to \Delta (A\times L)$ defined by $r\left(\overrightarrow{T}\right)(A,E)=\frac{{\sum }_{\varphi \in f^{-1}\left(E\right)}{\overrightarrow{T}}_{A,\varphi }}{{\sum }_{A^{\prime },\varphi }{\overrightarrow{T}}_{A^{\prime },\varphi }}$ .

What this does is renormalize a trade of a supertrader into a probability distribution over $(A,E)$ pairs. Admittedly, the renormalization isn't well-defined in general, because the sum in the numerator may be infinite, or the denominator may be 0. For supertrader trades, the sum in the numerator won't be infinite because only finitely many sentences in $S^{\ast }$ can be bet on. And to prevent the denominator from being 0, we can just add a trader with a mass of $ϵ$ that purchases 1 share of $(\top ,\top )$. This always results in 0 net value no matter what, by unitarity, so the trader preserves its mass and can do the same trick the next turn, ensuring that the renormalization is always well-defined.

Let $F$ be our function from ${\Xi }^{\prime }\to P\left({\Xi }^{\prime }\right)$ that we'll apply the Kakutani fixed-point theorem to, defined by:

$F\left(V\right):={\text{argmin}}_{P^{\prime }\in {\Xi }^{\prime }}\left(E_{A,E\sim r\left(T\right(t\left(V\right)\left)\right)}{P}_A^{\prime }\right(E\left)\right)$

Or, in other words, it maps a potential pricing $V$ to the set of pricings which minimize the expected value. $V$ is converted to a pricing over sentences via $t$, and then evaluated by the supertrader $T$, and then $r$ is used to convert the supertrader trade to a probability distribution, which gives the weights for the sum.

Now, we have four lemmas, and we'll prove the first 3 now, and the fourth later.

Lemma 1: ${\Xi }^{\prime }$ is a nonempty, compact, convex subset of the finite-dimensional boolean hypercube $[0,1{]}^{A\times L}$

Lemma 2: For all $V\in {\Xi }^{\prime },F\left(V\right)$ is a nonempty, compact, convex subset of ${\Xi }^{\prime }$.

Lemma 3: $F$ has the closed-graph property.

Lemma 4: $\forall V\in \Lambda :\exists V\in {\Xi }^{\prime }:\forall A,\varphi \in A\times S^{\ast }:V_A\left(f\right(\varphi \left)\right)\le V_A\left(\varphi \right)$

Proof of Theorem 1:

By Lemmas 1, 2, 3 and the Kakutani fixed-point theorem, $\exists P^{\prime }:P^{\prime }\in F\left(P^{\prime }\right)$. This is equivalent to $P^{\prime }\in {\text{argmin}}_{V\in {\Xi }^{\prime }}\left(E_{A,E\sim r\left(T\right(t\left(P^{\prime }\right)\left)\right)}{V}_A\right(E\left)\right)$. Therefore, for all $V\in {\Xi }^{\prime }$,

$E_{A,E\sim r\left(T\right(t\left(P^{\prime }\right)\left)\right)}{P}_A^{\prime }\left(E\right)\le E_{A,E\sim r\left(T\right(t\left(P^{\prime }\right)\left)\right)}{V}_A\left(E\right)$

Then, by linearity of expectation, we can get that for all $V\in {\Xi }^{\prime }$

$E_{A,E\sim r\left(T\right(t\left(P^{\prime }\right)\left)\right)}\left(P_A^{\prime }\right(E)-V_A(E\left)\right)\le 0$

By multiplying both sides by ${\sum }_{A,\varphi }T\left(t\right(P^{\prime }){)}_{A,\varphi }$, and referring back to the definition of $r$, we get that for all $V$

${\sum }_{A,E}\left({\sum }_{\varphi \in f^{-1}\left(E\right)}T\right(t\left(P^{\prime }\right){)}_{A,\varphi })\left(P_A^{\prime }\right(E)-V_A(E\left)\right)\le 0$

And then by the definition of $t$, this can be rewritten as:

${\sum }_{A,\varphi }T\left(t\right(P^{\prime }\left){)}_{A,\varphi }\right(t\left(P^{\prime }{)}_A\right(\varphi )-t(V{)}_A\left(\varphi \right))\le 0$

Now, by applying the definition of $t$ again, and defining $P:=t\left(P^{\prime }\right)$

$\exists P\in \Xi :\forall V\in {\Xi }^{\prime }:{\sum }_{A,\varphi }T\left(P{)}_{A,\varphi }\right(P_A\left(\varphi \right)-V_A\left(f\right(\varphi \left)\right))\le 0$

And by applying Lemma 4, that any $V\in \Lambda$ has a $V\in {\Xi }^{\prime }$ that attains lower value (which can only increase the value of the sum), we get

$\exists P\in \Xi :\forall V\in \Lambda :{\sum }_{A,\varphi }T\left(P{)}_{A,\varphi }\right(P_A\left(\varphi \right)-V_A\left(\varphi \right))\le 0$

and Theorem 1 is proved. Time to take care of showing the lemmas.

Proof of Lemma 1:

Obviously, ${\Xi }^{\prime }$ is nonempty, because taking a probability distribution over $P\left(S\right)$, conditioning on $A$, and extending it to a valuation on $L$ fulfills all 4 defining properties. It's convex because any mixture of elements fulfilling the defining axioms of ${\Xi }^{\prime }$ also fulfills the defining axioms. All defining equations use $\ge$ or $=$, so the resulting set is closed, and since it's bounded by being a subset of a finite-dimensional hypercube, it's compact as well.

Proof of Lemma 2:

Continuous functions from compact spaces to the nonnegative reals have a closed and nonempty argmin set, and by the solution set being a subset of ${\Xi }^{\prime }$ which is compact, nonemptiness and compactness of $F\left(V\right)$ has been shown. As for convexity, observe that linearity of expectation implies that you can take a probabilistic mixture of any two points in the argmin set and it will preserve expected value, so the argmin set is convex.

Proof of Lemma 3:

For notational convenience, abbreviate $r\left(T\right(t\left(V\right)\left)\right)$ as $h\left(V\right)$. Equip ${\Xi }^{\prime }$ with the sup norm on the hypercube it is a subset of. A perturbation on $V$ of size $\delta$ leads to a perturbation of the price features by at most $\delta$, and by the continuity of the supertrader trade, induces at most a ${\delta }^{\prime }$ change in the sum of the coefficients for the supertrader trade, and because said sum of coefficients is uniformly bounded away from 0 by that one trader that just makes trivial bets, renormalizing leads to at most a $\frac{ϵ}{3}$ change in the probability distribution $h\left(V\right)$. By letting $\delta$ be sufficiently small, this shows that if $V^{\prime }$ differs from $V$ by less than $\delta$, then $d_{tv}\left(h\right(V),h(V^{\prime }\left)\right)<\frac{ϵ}{3}$. Also, under this norm, if $P$ differs from $P^{\prime }$ by less than $\frac{ϵ}{3}$, then for any probability distribution $\mu \in \Delta (A\times L)$, then $|E_{\mu }P-E_{\mu }{P}^{\prime }|<\frac{ϵ}{3}$.

Fix two sequences of valuations $\left\{P_n\right\}$, $\left\{V_n\right\}$, which limit to $P_{\infty }$ and $V_{\infty }$, where for all $n$, $P_n\in F\left(V_n\right)$. To show closed graph (ie, that $P_{\infty }\in F\left(V_{\infty }\right)$), by the definition of $F$, we need to show that there is no $P^{\prime }$ and $ϵ>0$ where $E_{h\left(V_{\infty }\right)}{P}_{\infty }-E_{h\left(V_{\infty }\right)}{P}^{\prime }>ϵ$.

Assume the opposite, that such a $P^{\prime }$ and $ϵ$ exist.

Because of the limiting sequences, there is some $n_0$ where, for all greater $n$, the distance between $V_{\infty }$ and $V_n$ is below $\delta$, and the distance between $P_{\infty }$ and $P_n$ is below $\frac{ϵ}{3}$.

$d_{tv}\left(h\right(V),h(V^{\prime }\left)\right)<\frac{ϵ}{3}$ implies that for all $P$, $|E_{h\left(V\right)}P-E_{h\left(V^{\prime }\right)}P|<\frac{ϵ}{3}$.

Since $V_{n_0}$ and $V_{\infty }$ differ by less than $\delta$, $d_{tv}\left(h\right(V_{n_0}),h(V_{\infty }\left)\right)<\frac{ϵ}{3}$.

So, $E_{h\left(V_{\infty }\right)}{P}_{\infty }-E_{h\left(V_{\infty }\right)}{P}^{\prime }>ϵ$ (by assumption) and $|E_{h\left(V_{n_0}\right)}{P}_{\infty }-E_{h\left(V_{\infty }\right)}{P}_{\infty }|<\frac{ϵ}{3}$ and $|E_{h\left(V_{n_0}\right)}{P}^{\prime }-E_{h\left(V_{\infty }\right)}{P}^{\prime }|<\frac{ϵ}{3}$, which implies $E_{h\left(V_{n_0}\right)}{P}_{\infty }-E_{h\left(V_{n_0}\right)}{P}^{\prime }>\frac{ϵ}{3}$

Finally, because $P_{\infty }$ and $P_{n_0}$ differ by less than $\frac{ϵ}{3}$, $|E_{h\left(V_{n_0}\right)}{P}_{\infty }-E_{h\left(V_{n_0}\right)}{P}_{n_0}|<\frac{ϵ}{3}$, we get $E_{h\left(V_{n_0}\right)}{P}_{n_0}-E_{h\left(V_{n_0}\right)}{P}^{\prime }>0$, which is impossible by $P_{n_0}\in F\left(V_{n_0}\right)$, so $P_{n_0}$ has the minimal possible expected value.

Thus, we have a contradiction and our original assumption was wrong, so $P_{\infty }\in F\left(V_{\infty }\right)$, and closed-graph for $F$ has been shown.

The proof of Lemma 4 will be deferred to the next post.