Before the Search Settles
Probabilities for mathematical facts that are already decided: a prior over theories from 2012, a bookmaker over sentences, presumptions of independence, and what they say about machines that improve without new evidence
In July 2012 Abram Demski, a friend at the time, sent me a draft of a paper called “Logical Prior Probability.” It defined a probability distribution over the theories of first-order logic. The construction was simple enough to state in a sentence. Draw sentences at random, one after another, and throw away any sentence that contradicts the ones already kept. The probability of a sentence is the chance that it ends up in the theory.
I read it closely and wrote back over the following months. Some of my notes were corrections. The convergence theorem for the paper’s sampling procedure held only with probability one, and the comparison with Solomonoff’s prior depended on the Turing machines being monotone, which the draft did not say. One note was a question. In August I sent it under the subject line “Defeasibility, impossible possible world, and incompleteness.” I asked how his prior fitted the framework of adaptive logics, which I had written slides about, and whether it, or a defeasible logic, could formalize reasoning under impossible possible worlds, “Like in determining self outputs.” I also observed that his distribution was unambiguously a distribution over structures, so it always had a most probable partial structure, “which might not have a completion, leading to defeasibility.” He answered that an improved version of his algorithm should handle impossible worlds well, because until a proof or a refutation turns up, it treats a statement inductively.
Around the same time we talked about building a neural network that would work like a Turing machine, trained by reinforcement learning to recognize languages that no finite automaton can recognize. We never got around to it.
Lately this blog has been revisiting the highlights of my intellectual life, alongside what the latest developments in AI bring up. Several of those essays go back to the same years. The slides became Presumed Normal. A lecture I taught in 2010, on automated bookmakers that are no-regret learners, became The Bookmaker Is a Learner. The subject of the correspondence went much further in other hands. In 2016 a group at the Machine Intelligence Research Institute (MIRI), where Abram went on to work, published Logical Induction: a bookmaker that prices sentences of logic, built on Abram’s framework. “Self outputs” became one of MIRI’s central problems. This essay returns to the question Abram and I were circling.
The question starts from a sentence in How Does a Policy Improve?: “Search in a known model can discover consequences that have not yet been computed.” What should a reasoner believe about those consequences before the search finishes? Is the 10^{100}th decimal digit of π a 7? The answer is settled; nobody knows it. “One in ten” seems the right credence. Probability theory, as usually stated, cannot give it.
There are three kinds of answer. A credence about a settled fact can be right because it follows from a good prior over the computation, because no adversary from a bounded class of tests can exploit it, or because it presumes independence except where structure has been found. Each answer fails where another succeeds. The last part of the essay asks what they imply for machines that improve themselves without new evidence, since whatever such a machine gains, it gains from its own computation.
Logical omniscience
A probability distribution in the textbook sense is defined over a space of possible worlds. A mathematical theorem is true in every world, so it gets probability 1, and its negation gets 0. Probability theory therefore models an agent who already knows every consequence of what it knows. Philosophers call this logical omniscience. Leonard Savage noticed the problem with the remote digits of π, and Teddy Seidenfeld, Mark Schervish and Joseph Kadane begin their 2012 survey with his example.
The repairs began in 1967. Ian Hacking’s “Slightly more realistic personal probability” replaced logical possibility with personal possibility: “For me, when is a proposition possible? When I do not know it to be false.” His probabilities attach to sentences, not to propositions, so two sentences with the same truth conditions can have different probabilities.
Clark Glymour posed the problem of old evidence in 1980. A datum already known has probability 1, so conditioning on it changes nothing. Yet the anomaly in Mercury’s perihelion, known since 1859, became strong evidence for general relativity in 1915. On Daniel Garber’s answer (1983), what was new in 1915 was not the datum but the fact that the theory implies it. He lets an agent learn that fact by treating the sentence “h ⊢ e” as a new atom, “unanalyzed and unanalyzable.” I. J. Good wrote of evolving or dynamic probability, which changes as one thinks, and of “Type II rationality,” which maximizes expected utility net of the cost of deliberating.
Haim Gaifman’s “Reasoning with limited resources and assigning probabilities to arithmetical statements” (2004) bounds what an agent has in view: “The restriction on resources is expressed in the framework by a restriction to some finite set of sentences.” The probability function is partial, and the axioms need hold only among the sentences in its domain. Gaifman considered bounding the length of proofs instead, and rejected it, because implication by short proofs is not transitive. Brian Weatherson’s “From classical to intuitionistic probability” (2003) gave a general recipe: for any logic, define the probability functions that respect its consequence relation. A weaker logic demands less of the agent.
Game-theoretic semantics offered a repair of its own. Jaakko Hintikka read a quantifier as a move in a game, in which a player draws an individual from the domain. Veikko Rantala’s urn models (1975) let the contents of the urn change between draws. A model can then be inconsistent only beyond the depth of quantifiers that anyone has examined, which Hintikka defended as “impossible possible worlds vindicated”. Gaifman bounds the set of sentences in view; urn models bound depth. Mark Jago later showed the limit: under Rantala’s semantics an agent still knows every tautology of propositional logic.
These repairs give permission to hold intermediate credences. None of them says how the credences should move as computation proceeds, or why one in ten is the right number for the digit.
A prior over theories
Abram’s prior answers both questions in principle. Its starting point was algorithmic probability. Ray Solomonoff’s prior gives every computable sequence a probability that falls with the length of the shortest program that computes it. Abram asked what happens if “describable” means “describable in first-order logic” instead of “computable.” A logical description can constrain a situation without specifying it, so more situations get positive probability.
Solomonoff induction. Solomonoff’s prior, from 1964, predicts how a sequence of bits continues. Take a universal Turing machine of a particular kind, a monotone one. It has three kinds of tape. It reads its program from an input tape whose head moves only forward. It writes its output on an output tape whose head also moves only forward, so nothing written is ever erased. It computes on work tapes, which it may read, write and rewrite freely, for as long as it likes between moves of the other two heads. It may read many bits before printing one, or print many after reading one. What makes it monotone is that reading more of the program can only extend the output, never revise it. Feed it fair coin flips as its program. The probability M(x) of a finite string x is the chance that the output begins with x. A program that has printed x by the time it has read its \ell bits, and not before, contributes 2^{-\ell}, so short programs carry most of the weight, and a string with a short description gets a high probability. The prediction that the next bit is 1 is M(x1)/M(x).
Monotonicity makes the probabilities of prefixes fit together. Because nothing printed is ever revised, each run of coin flips produces one output. No output begins with both x0 and x1, and every output that begins with either begins with x, so M(x0)+M(x1)\le M(x). The inequality can be strict, because some programs never print another bit. A machine that reads a whole program and prints a whole answer gives probabilities to finite strings, but not consistent ones to their continuations. This is the detail that Abram’s draft left out of its comparison.
The guarantee is dominance. For every computable probability \mu over sequences, M(x)\ge 2^{-K(\mu)}\mu(x), up to a constant factor that depends only on the machine, where K(\mu) is the length of the shortest program that computes \mu. In the bookmaker essay’s terms, this is a regret bound: on every sequence, the total log loss of M exceeds that of \mu by at most K(\mu) bits, plus a constant. If the sequence is in fact drawn from \mu, Solomonoff proved in 1978 that the expected squared errors of M’s predictions, summed over the whole infinite sequence, total at most about \tfrac{\ln 2}{2}K(\mu). So, with probability 1 under \mu, M’s predictions converge to \mu’s.
M is a Bayesian mixture. Up to a constant factor, it averages every predictor whose probabilities can be approximated from below, the computable ones among them, weighting each by 2^{-K} for its own description length. M is itself one of these predictors. Hedge, the learner at the center of the bookmaker essay, sees every expert’s loss each round and multiplies each expert’s weight by a factor that falls with that loss. Bayes’ rule is Hedge at log loss, so in that essay’s terms M is a market in which each of these predictors bets on its own predictions, starting with wealth that halves with every bit of its description.
The limit is computation. M is not computable. It can be approximated from below, by running more programs for longer, but no computable procedure says how close an approximation is. M is also logically omniscient about its programs. Its uncertainty is over which program produced the data, never over what a program outputs. Shown enough digits of π, it puts nearly all its weight on a short program for π, and it predicts every later digit with near certainty, because it runs that program to the end. A bounded reasoner faces the opposite case: it has found the short program, and still cannot run it far enough.
The prior must respect logic. Following Weatherson, the paper asks for four properties of a probability P on sentences:
\begin{aligned} &P(A)=0 \text{ if } A \text{ is refutable},\qquad P(A)=1 \text{ if } A \text{ is provable},\\ &P(A)\le P(B) \text{ if } A \text{ implies } B,\qquad P(A)+P(B)=P(A\lor B)+P(A\land B). \end{aligned}
The generative process supplies them. Let G be any distribution that gives every sentence positive probability. Draw S_1,S_2,\dots from G, rejecting each candidate that would make S_1\land\dots\land S_n contradictory. The sequence never stops, but whether any given sentence belongs to the theory is decided after finitely many steps. A provable sentence can never be rejected, so it is eventually drawn, with probability 1. If A implies B, whatever contradicts B contradicts A, so a theory containing A will eventually contain B. The additivity property follows by the same kind of argument.
Inconsistency is only semi-decidable. A procedure can confirm that a set of sentences is contradictory by finding a proof, but it cannot confirm that a set is consistent. The paper therefore approximates the prior by sampling. It generates random theories, spends a growing amount of time on each looking for contradictions, backtracks when it finds one, and counts how often the sentence of interest appears. As the time allowed grows, undetected contradictions become rarer, and the frequency converges to the prior’s probability. The paper says plainly that the prior is therefore computable in the limit, and it makes no claim of efficiency.
The approximation is where the prior meets logical uncertainty, as Abram’s reply to me said. Suppose a universal statement \forall x.\,S[x] follows from what the agent knows, but the proof is too long for the time allowed. The approximation then treats \forall x.\,S[x] like a sentence that is not provable, and its probability should rise with each instance S[i] that is found to be true. Until a proof settles a statement, the statement is learned about inductively.
The paper also states a limit of its own. Suppose every instance S[0], S[1], \dots is provable but \forall x.\,S[x] is not, as happens in incomplete theories. Then \exists x.\,\neg S[x] is consistent with the axioms, has positive probability of being drawn, and keeps \forall x.\,S[x] below 1. The prior cannot learn new axioms of arithmetic. In the paper’s words, it is limited to the incompleteness of whatever axioms it is given.
A year later the hope met a theorem. At a MIRI workshop in July 2013, Will Sawin and Abram proved that “Computable probability distributions which converge on believing true Π1 sentences will disbelieve true Π2 sentences.” A Π1 sentence is a universal claim like \forall x.\,S[x] with S decidable. The property Abram had wanted, credence approaching certainty as the instances are checked, is now called Gaifman inductivity, after Gaifman’s 1964 proposal. It cannot coexist with computable approximation and a weak form of coherence without making some short true Π2 claims, of the form \forall x\,\exists y\,R(x,y), arbitrarily improbable. The logical induction paper later summed up the impossibility: “an ideal belief state that is non-dogmatic, Gaifman inductive, and coherent in a weak sense has no computable approximation.” Marcus Hutter, John Lloyd, Kee Siong Ng and William Uther had defined an attractive prior on sentences of an expressive logic the year before. By the same result, it admits no computable approximation.
Sawin and Abram read their theorem as a case against the property. Its downsides, they wrote, are “so great as to argue strongly against Π1 convergence as a desirable property for rational agents.” On that reading a rational agent should behave like the 2012 prior, which never reaches certainty about an unprovable universal statement, however many instances it has seen.
The prior answer works where its domain is narrow. Probabilistic numerics puts Bayesian priors on the outputs of deterministic computations: the value of an integral, the solution of a differential equation, the solution of a linear system. Persi Diaconis made the case in 1988, Anthony O’Hagan built Bayesian quadrature in 1991, and Philipp Hennig, Michael Osborne and Mark Girolami surveyed the field in 2015 as uncertainty “arising from the loss of precision induced by numerical calculation with limited time or hardware.” These methods are calibrated in a measurable sense, and they ship. A Gaussian process over an integrand is a prior over a settled fact. What does not exist is a computable prior over all of mathematics that behaves well.
A bookmaker over sentences
The adversarial answer gave up the distribution over theories and priced sentences directly. Logical Induction, by Scott Garrabrant, Tsvi Benson-Tilsen, Andrew Critch, Nate Soares and Jessica Taylor, appeared in September 2016. Its related-work section traces the thread of probabilities on sentences from Łoś and Gaifman to “Demski (2012), whose framework we use.” It credits Abram’s paper with the first formal statement of the requirement that a reasoner give nonzero probability to every consistent, computably enumerable theory. It also says what is new: “Logical inductors are not the first computable procedure for assigning probabilities to sentences in a manner that is coherent in the limit; the algorithm of Demski (2012) also has this property. The main appeal of logical induction is that their beliefs become reasonable in a timely manner, outpacing the underlying deductive process.” Abram co-authored two of the papers that led to it, “Asymptotic Logical Uncertainty and the Benford Test” and “Inductive Coherence.”
The construction is a market. Fix a theory, such as Peano arithmetic, and a deductive process: an enumeration of its theorems, with D_n the finite set found by day n. A world W assigns a truth value to every sentence. On day n the plausible worlds are those propositionally consistent with D_n: they make every sentence in D_n true and respect the propositional connectives, treating quantified sentences as atoms. The market sets a price P_n(\varphi)\in[0,1] for every sentence. A share in \varphi pays $1 in a world where \varphi is true and nothing otherwise.
A trader buys and sells shares. On day n it chooses a number of shares T_n(\varphi) for finitely many sentences, each a continuous function of the day’s prices (it may also use past prices). The value of its holdings in world W after n days is
\sum_{i\le n}\ \sum_{\varphi} T_i(\varphi)\,\bigl(W(\varphi)-P_i(\varphi)\bigr).
A trader exploits the market if this value, taken over all days n and all worlds plausible on day n, is bounded below but not above. It risks a bounded amount and can win without bound. The logical induction criterion says: “there is no efficiently computable trader T that exploits P relative to D.” A trader is efficiently computable if its trading strategy for day n can be written down in time polynomial in n. The bound is on the traders, not on the market. A market that meets the criterion is a logical inductor.
The criterion is the bookmaker essay’s no-regret condition, turned around. In that essay the bookmaker’s prices were a learner’s weights, and its loss was bounded by the learner’s regret. Here the prices must be such that no trader of a given computational class makes unbounded profit. Exact coherence over all sentences would be the combinatorial wall of that essay, where pricing bets on combinations of outcomes is #P-hard, raised to undecidability. Logical induction asks only for coherence that bounded arbitrageurs cannot fault. Discipline does not wait for sentences to be settled. The paper’s notion of exploitation “rewards traders for arbitrage, even if they arbitrage between sentences that never ‘pay out’,” so prices are held to consistency with whatever has been proved. A trader that sees the prices of \varphi and \neg\varphi sum to well below $1 can buy both and profit without knowing which is true. Unlike Solomonoff’s predictors, in the paper’s words, “our ‘experts’ are not themselves predicting the world.”
The paper’s algorithm has three parts, and with them the criterion has a proof of a few lines. The first, a market maker, sets one day’s prices against a single trader. Because the trader’s orders are continuous in the prices, Brouwer’s fixed-point theorem guarantees prices at which the trader buys only shares priced at $1 and sells only shares priced at $0, so its trade can gain nothing in any world. The market maker finds rational prices close enough that the trade on day n gains at most 2^{-n}. Summed over all days, the trader never gains more than $1.
The second part, a budgeter, turns a trader into one that never loses more than a budget of b dollars in any plausible world. It scales each day’s trade down so that the trade cannot carry losses past b, and stops trading once they reach b. A trader that would never have lost b is left unchanged.
The third part, a trading firm, enumerates every polynomial-time trader by running each pair of a Turing machine and a polynomial, with the polynomial as a clock. Trader k joins the firm once for every budget b, with the fixed weight 2^{-k-b}. The weights halve along the enumeration, not with each bit of a trader’s description as in Solomonoff’s mixture, and the paper names Solomonoff and Gaifman as the two frameworks it merges. Each day the firm’s combined order goes to the market maker, and the prices that come back are the market’s.
Suppose some polynomial-time trader, number k in the enumeration, exploited the market. Its losses would be bounded, so for some budget b the copy with that budget is never cut off, and the firm holds 2^{-k-b} of its position. That share of an unbounded gain is unbounded. All the other copies together can lose at most \sum_{k',b'}2^{-k'-b'}\,b'=2 dollars. The firm’s gains would then be unbounded, but the market maker holds them below $1. So no polynomial-time trader exploits the market.
The inductor itself is far from polynomial time. Each day it runs every trader admitted so far and searches the rational prices by brute force. It is computable, and the paper says logical inductors have “abysmal runtime.” Being slower than every trader it defends against is the price of running them all itself.
The market maker is not the bookmaker of the earlier essay, Robin Hanson’s logarithmic market scoring rule (LMSR). Like that bookmaker, it deals with each trader at a quoted price, and the payout is fixed at the moment of the trade. Its pricing rule is different. An LMSR bookmaker moves its price along a cost function, and its liquidity parameter sets both its subsidy and its temperature. A logical inductor has no cost function, no liquidity parameter and no subsidy. Each day’s prices come from a clearing computation with all of that day’s orders in view. The nearest relative in that essay is the Eisenberg–Gale program of one of its boxes, whose clearing prices fix the odds of a betting pool. The tradeoff that temperature governs has no direct counterpart here. The nearest things to a learning rate are the trader weights and budgets.
The construction learns what the essay’s opening asked for. Its theorems are about sequences of sentences, so the single remote digit becomes a sequence of ever more remote ones, placed to outrun any efficient computation. Let \varphi_n say that the Ackermann(n,n)th decimal digit of π is 7. Each \varphi_n is easy to write down and hard to decide. If no polynomial-time method predicts these digits better than chance, the theorem on learning pseudorandom frequencies gives P_n(\varphi_n)\to 0.1. One in ten is the price at which no efficient trader can profit. Other theorems show that the market learns to price provable sentences near 1 well before the deductive process proves them, that prices become coherent in the limit, and that the market knows its own prices and trusts its future beliefs.
The guarantees are asymptotic, and their rates are uncomputable: the paper proves that no computable function bounds how long a provable sentence takes to reach a price above 1-\varepsilon. The paper’s list of desiderata also says what was given up. Logical induction is computably approximable, approximately coherent, and non-dogmatic, “so it cannot satisfy” Gaifman inductivity. Non-dogmatism means that in the limit no sentence the axioms leave open is priced at 0 or 1. Gaifman inductivity would price at 1 a universal statement whose instances are all provable, even when the statement itself is not. The property Abram’s 2012 draft wished for is the one the 2016 construction had to drop.
Why MIRI wanted it. MIRI’s research agenda of 2014, by Nate Soares and Benja Fallenstein, listed four problems under “Highly Reliable Agent Designs”: realistic world-models, decision theory, logical uncertainty and Vingean reflection. The reason was the agent’s own outputs, the “self outputs” of my 2012 email. An agent is part of the world it models. Its source code, its future actions and the programs around it are determined computations that it cannot fully evaluate, so most of its uncertainty is logical. Abram and Scott Garrabrant’s Embedded Agency (2018) made this embeddedness the core of their case against classical rationality. Decision theory needs logical counterfactuals: an agent deciding between actions asks what follows if its algorithm outputs one action, when in fact it outputs another. Counterfactual mugging asks whether an agent should pay a predictor now because, had a coin fallen the other way, the predictor would have rewarded agents that pay. Vladimir Nesov’s 2009 variant replaces the coin with “the 10000-th digit of pi.”
The “five-and-ten” problem shows why the counterfactuals are hard. An agent may take a $5 bill or a $10 bill. Suppose it decides by searching for proofs of statements of the form “if I take the five, I get u, and if I take the ten, I get v,” and takes the better action according to the first such statement it proves. Let \varphi be the statement with u=5 and v=0. If the agent takes the five, \varphi is true: the five does get 5, and “if I take the ten, I get 0” holds because its antecedent is false. With a suitable order of search, the agent can prove from its own code that if \varphi is provable, it takes the five, and so that \varphi is true if provable. Löb’s theorem says that whatever a theory proves true if provable, it proves. So the agent proves \varphi, takes the five, and the proof is valid. Under another order of search, the same argument proves that the ten gets 10 and the five gets 0, and the agent takes the ten. The logic does not decide which.
Logical induction did not supply logical counterfactuals either. Garrabrant described a logical-inductor agent that estimates its utility conditional on each action and takes the better one. A trader can push the estimate for the ten down to nothing at no cost, because a bet conditional on an action the agent never takes never settles. The agent takes the five, the trader’s bets conditional on the five are accurate, and the trader does the same the next round. Making the agent take any action that its own market gives it less than a small probability \varepsilon of taking lets it learn to take the ten, at the cost of taking a bad action, perhaps a disastrous one, a fraction \varepsilon of the time.
The agenda’s fourth problem asked how an agent can trust a successor it cannot predict. Proof-based trust meets Löb’s theorem, the “Löbian obstacle” of Eliezer Yudkowsky and Marcello Herreshoff. Logical inductors trust their future beliefs, which answered part of the problem. MIRI wrote in December 2020 that its undisclosed 2017 research directions had “largely failed,” and made policy and communication its priority in January 2024. Its agent-foundations team, Garrabrant among them, left in June 2024.
What a truth maintenance system lacks
Is the market essential, or would any system that tracks consistency do? A truth maintenance system, in Jon Doyle’s 1979 design or Johan de Kleer’s assumption-based version of 1986, records which beliefs depend on which assumptions, and withdraws beliefs when a contradiction appears. It is bookkeeping over derivations already made. In a logical inductor that bookkeeping belongs to the deductive process. Presumed Normal’s adaptive logics do the same job. An adaptive proof writes each conclusion on a line together with a condition, the abnormalities it assumes false, and marks the line when the proof so far shows that assumption unreliable. The condition plays the role of an assumption-based system’s label, and marking a line is retracting it.
A truth maintenance system lacks three things that the theorems need. The first is a price for what has not been derived. Kathryn Laskey and Paul Lehner showed in 1989 that an assumption-based system with probabilities on its assumptions is equivalent to Dempster–Shafer belief. The probabilistic system propagates a prior. It does not learn from which sentences turn out to be provable.
The second is a way to handle sentences that refer to the reasoner’s
own beliefs. Let \chi_n say “my price
for \chi_n on day n is below 0.5.” Doyle met the logical form
of this case as an “unsatisfiable circularity,” a justification under
which “the TMS must make F in if and only if it makes F out,” and his
system loops. Textbooks later called such a structure an odd loop. In
answer set programming, p :- not p. has no stable model. A
logical inductor prices the sentences toward 0.5. The paper’s theorem on
paradox resistance states, for any rational p strictly between 0 and 1 and any
efficiently computable sequence of such sentences,
\Gamma\vdash \chi_n\leftrightarrow P_n(\chi_n)<p \quad\text{for all } n \qquad\Longrightarrow\qquad \lim_{n\to\infty}P_n(\chi_n)=p.
“We attribute the success of logical inductors in the face of paradox to the continuity conditions.” A trader that bought when the price was below 0.5 and sold otherwise would leave no equilibrium. A trader whose demand varies continuously with the price leaves one. Continuity is the smallest example of what a price can do that a label cannot.
The third is aggregation. Budgets and weights let one algorithm stand up to every efficient trader at once.
None of the three needs a market. Glenn Shafer and Vladimir Vovk’s game-theoretic probability (Probability and Finance: It’s Only a Game!, 2001) defines a probability as a price that a gambler, whom they call Skeptic, cannot exploit. Vovk, Akimichi Takemura and Shafer’s “Defensive forecasting” (2005) proves that “for any continuous strategy for Skeptic there exists a strategy for Forecaster that does not allow Skeptic’s capital to grow, regardless of what Reality is doing.” The forecaster picks a probability p_n at which Skeptic’s continuous betting function is zero, which the intermediate value theorem guarantees. Logical induction’s Brouwer step is the many-dimensional form of the same move. The paper on defensive forecasting even makes the remark about the paradox: continuous tests “cannot sharply distinguish between the cases p_n<0.5 and p_n\ge0.5.” Mixing strategies for Skeptic does the work of logical induction’s budgets.
Multicalibration, from Úrsula Hébert-Johnson, Michael Kim, Omer Reingold and Guy Rothblum (2018), reaches the same structure from algorithmic fairness. A predictor p assigns each individual x a probability that an outcome y occurs. It is multicalibrated with respect to a class \mathcal C of efficiently identifiable groups if, within every group S\in\mathcal C and every level v of prediction,
\bigl|\ \mathbb E\,[\,y-p(x)\mid x\in S,\ p(x)=v\,]\ \bigr|\le\alpha .
The algorithm that achieves it repeats one step: find a group where the predictor is miscalibrated, and correct it there. That is a truth maintenance system whose violations are statistical tests instead of contradictions. The bookmaker essay met the same step twice, in the ellipsoid method’s search for a violated constraint and in the Frank–Wolfe oracle of combinatorial market makers.
The logical induction paper does not cite Shafer, Vovk or the fairness literature. Its closest named precedent is a 2012 market of Kelly bettors by Alina Beygelzimer, John Langford and David Pennock. Vanessa Kosoy noted the kinship with defensive forecasting in 2017. Juan Perdomo and Benjamin Recht have since connected defensive forecasting to the fairness notions, without logical induction.
What does the market add beyond the theorems? The bookmaker essay valued a market for its one shared state and for the credit that accumulates to traders who are right. Logical induction keeps the first in a stronger form. In that essay, consistency between linked markets is left to traders, so arbitrageurs draw a market’s boundary.
Polymarket shows how far they get. Oriol Saguillo and colleagues estimated about $39.6 million of arbitrage profit on Polymarket, in markets that resolved between April 2024 and April 2025. About $10.6 million came from yes–no markets whose two prices did not sum to $1, and about $29 million from markets with several exclusive answers whose prices did not sum to $1. Arbitrage across logically linked markets, all of it between pairs of US election markets, came to about $95,000. The structured incoherence is the kind that is hard to see, and profit from it was small.
A logical inductor also prices sentences one at a time, but its traders are inside it and the fixed point is computed jointly, so the coupling runs through its own state. Its boundary is the class of efficient traders.
Logical induction drops the market’s second virtue, credit. A trader’s weight is fixed from the start. Profit does not raise it, and losses only cut the trader off at its budget. Credit that accumulates belongs to the Kelly market. Like a logical inductor, that market sets its prices by a clearing computation. Its auctioneer takes no profit and absorbs no loss. Its price is a wealth-weighted average of the traders’ beliefs, and it “reacts exactly as if updating according to Bayes’ Law.” Bayes’ rule is Hedge at log loss, so the wealth that the bookmaker essay called a second learner is there exactly, with traders as its experts. A logical inductor remembers only which traders have gone broke.
Tests instead of worlds
Logical induction defines a good credence by what bounded tests cannot fault, not by a distribution over worlds. Complexity theory had done the same for randomness. A distribution is pseudorandom for a class of tests if no test in the class tells it apart from the uniform distribution. Boaz Barak connected pseudorandomness to logical uncertainty in a 2015 blog post, “A different type of pseudo”, which opens with the claim that the probability of a given digit of π being 7 is 10%. He called pseudorandomness “a computational analog of frequentist probability,” and the pseudo-distributions of the sum-of-squares method a computational analog of Bayesian probability. In their lecture notes, Barak and David Steurer describe a pseudo-distribution as the uncertainty “a computationally bounded observer” has about a hidden structure that is fully determined. The notes put logical learning in one sentence: “Despite learning no new information, as we invest more computation time, the algorithm reduces uncertainty in the beliefs by making them consistent with increasingly powerful proof systems.” They also say that pseudo-distributions ensure “no computationally easy dutch book strategy.”
Outcome indistinguishability, from Cynthia Dwork, Michael Kim, Omer Reingold, Guy Rothblum and Gal Yona (2021), asks the same of predictions about individuals. A predictor is outcome-indistinguishable for a class of distinguishers if none of them can tell real pairs (x,y) from pairs in which y is drawn from the predictor’s own probability \tilde p(x). The authors keep the individual “probabilities” in quotation marks, after A. P. Dawid’s argument that individual risk remains “subtle and elusive.” They allow that “Perhaps Nature is deterministic, but we do not have enough information or computing resources to carry out the predictions ourselves.” If Nature’s outcomes are fixed but two groups cannot be told apart by any efficient test, predicting one half for everyone in them is the best feasible account. That is logical uncertainty in the vocabulary of fairness. I have not found anyone who joins it to logical induction.
Debate, interactive proofs and a smarter oracle look like a different answer. They are not. They sit elsewhere on two axes along which the adversarial answer varies.
The first axis is where the adversary sits. In logical induction and multicalibration the tests are internal: the believer enumerates them and runs them. It must then out-compute each one, which is why a logical inductor’s runtime is abysmal. Multiaccuracy, a weaker cousin of multicalibration, asks only that a predictor be unbiased on each group. Dwork, Daniel Lee, Huijia Lin and Pranay Tankala proved in 2023 a lower bound on the size of multiaccurate predictors relative to their tests, refuting “the possibility of having ‘dream’ predictors that are more efficient than functions in C,” at least for predictors that use the tests as black boxes, as all known algorithms do. An internal adversary can only certify the believer against what the believer can simulate.
An external adversary can be stronger than the believer, and that changes what the believer can justify. A verifier running in polynomial time can decide every problem in PSPACE by interrogating a prover it does not trust (Adi Shamir; Carsten Lund, Lance Fortnow, Howard Karloff and Noam Nisan, 1992). Geoffrey Irving, Paul Christiano and Dario Amodei’s “AI safety via debate” (2018) showed that “debate with optimal play can answer any question in PSPACE given polynomial time judges (direct judging answers only NP questions).” A prediction market with outside traders is the external case too: the bookmaker learns from traders it cannot simulate, and pays them by a scoring rule. Logical induction is that market with the traders taken inside.
The second axis is what holds the adversary to account. Settlement over time does it in a market: bets pay as sentences resolve, or, in logical induction, as prices must stay consistent with what has been proved. The guarantees are aggregate. A logical inductor is calibrated across sequences of sentences and can be badly wrong about any one. Checks on demand do it in an interactive proof: the verifier examines one local step now, and needs no outcome. The guarantee is then per instance: for this statement, the chance of being fooled is below a stated bound. No aggregate notion of calibration gives that.
| settlement over time | checks on demand | |
|---|---|---|
| internal adversary | logical induction, multicalibration, defensive forecasting | self-play under exact rules; proof search with a proof checker |
| external adversary | prediction markets, scoring rules | interactive proofs, debate |
A trusted oracle falls outside the table. If a stronger reasoner’s word is taken as true, its answer is testimony, and logical uncertainty becomes empirical uncertainty about the reliability of a source. A mathematician who relies on a published theorem is in that position. So is a reasoner that adopts a claim because, in the terms of An Ontology That Pays for Itself, source P asserts T.
The corners combine. Beth Barnes, working with Christiano, described the obfuscated arguments problem in 2020: “a dishonest debater can often create arguments that have a fatal error, but where it is very hard to locate the error.” An honest debater may know that a flaw exists without being able to point to it. Jonah Brown-Cohen, Geoffrey Irving and Georgios Piliouras answered with prover–estimator debate (2025; a revised version of 2026 with Lijie Chen, Jiawei Li and Zhiyang Xun fixes an error in the main theorem). “The estimator (Bob) has the sole task of assigning probabilities to the prover’s subclaims. The prover uses these probabilities to decide which subclaim to recursively debate further.” The estimator’s guarantee, in their words, “is known as outcome indistinguishability.” Debate reduces a hard claim to steps that can be checked, and calibration prices the steps nobody can afford to check.
Presumed independent
The third answer is older than either of the others. Harald Cramér modeled the primes in 1936 as if each number n were prime independently with probability 1/\ln n. The model gets the density of the primes right by construction. It gets the number of twin primes wrong. It treats n and n+2 as independent. Yet if n is an odd prime, n+2 is odd too, which doubles its chance of being prime. Divisibility by 3, 5, 7 and the other small primes pulls the chance back down. Hardy and Littlewood’s conjecture of 1923 multiplies the naive count by the net correction, about 1.32. The structure that the naive model ignored is local and known. Each correction is a defeater of independence, applied where it is found.
Physics had made the same presumption sixty years before Cramér. The Demon Is a Learner tells how Ludwig Boltzmann derived the rise of entropy from colliding balls by assuming that two balls about to collide are independent. Mechanics does not supply that assumption, and a gas whose velocities have been reversed breaks it: each incoming pair carries the correlation of an earlier collision, and the entropy falls. That gas is a defeater on a grand scale. Like Hardy and Littlewood’s constant, it shows that a presumption holds until structure is found, and that the structure was there all along.
The presumption is also at work for money. The bookmaker essay reported that most dealers who quote parlays on Kalshi appear to price the legs as if they were independent, and one appears to model the correlations. The others presume independence, and that one dealer has found defeaters.
The Alignment Research Center (ARC), founded by Christiano, made presumed independence a research program. “Formalizing the presumption of independence” (Christiano, Eric Neyman and Mark Xu, 2022) asks for a heuristic estimator that assumes independence until an argument points out structure, and then accounts for it. The authors say what is missing: “it is not clear how to formalize this kind of defeasible reasoning.” They also say where they stand relative to logical induction. Such systems “would not revise the probability they assign to the twin prime conjecture after noticing the heuristic argument … although they would eventually learn to trust these arguments after observing them producing good predictions in practice.” A market finds that a correlation exists, by paying whoever exploits it; a heuristic argument says why it exists. ARC adds: “Heuristic estimators can be viewed as a type of interactive proof system with very weak guarantees.” Their 2024 paper on a law of iterated expectations for heuristic estimators borrows multiaccuracy from the fairness literature, so the presumption answer and the adversarial answer have begun to meet.
A presumption of independence is a default in the sense of Presumed Normal. That essay’s box on abnormalities with a price already holds the probabilistic version. A Markov logic network attaches a weight to each formula, and with weights fitted by maximum likelihood it is the maximum-entropy distribution that matches the formulas’ expected counts. With no formulas at all, the distribution is uniform over worlds and every ground atom is independent of every other. Each weighted formula is a found structure, and the distribution presumes independence everywhere else. The idea that conditional independence should be maximized by default goes back at least to Benjamin Grosof’s 1986 paper on nonmonotonic probabilistic reasoning, and the random-worlds method of Fahiem Bacchus, Adam Grove, Joseph Halpern and Daphne Koller derives “default assumptions of independence.” An adaptive logic whose abnormalities are dependences, withdrawn line by line when a dependence is derived, would be the proof theory to match. I have not found one.
Three answers
A prior gives structure, and in narrow domains such as numerical integration it gives calibrated numbers that a user can check. No general prior over mathematics is computable with good behavior, as Sawin and Abram’s theorem shows. The adversarial answer gives guarantees. They arrive at an uncomputable rate. The presumption answer gives reasons, such as Hardy and Littlewood’s constant. Nobody can yet say formally when a presumption is defeated, as ARC itself reports.
What is a reason, in this setting? The twin primes give the pattern. Hardy and Littlewood’s argument names a latent structure, divisibility by small primes, and presumes independence everywhere outside it. The predicted count follows. ARC’s heuristic arguments have the same form, and so does a Markov logic network, which is the maximum-entropy distribution given its weighted formulas. A reason, then, is a latent structure together with a presumption of independence beyond it. A price is the marginal probability that a reason implies for one sentence. A defeater is structure found outside the reason’s latent variables, and it calls for a new reason, not merely a new number. Prices underdetermine reasons, because different structures can imply the same marginals. In the terms of The Demon Is a Learner, a reason is a macrostate: what a predictor needs to keep, so that the rest can be presumed independent.
The three answers keep the structure in different places. A prior keeps it in its hypotheses: in the ontology essay, a concept earns its place by shortening the code, so the latent structure is the model part of a two-part code. A presumption keeps it in the explicit part of the argument. A logical inductor keeps it inside its traders. A trader that profits from the correlation between n and n+2 being prime has, somewhere in its code, something that tracks divisibility. The market retains only the prices. The bookmaker essay called this simulation by delegation: every model of the world runs inside some trader, and the market receives only the orders. A logical inductor stands to its reasons as Boltzmann’s one-ball distribution stands to a gas. The distribution records each ball’s statistics and none of the correlations among balls. The difference is that traders act on what they hold. A correlation left out of a gas’s description stays out. One left out of the prices is a profit for any efficient trader that finds it, so the market corrects it.
My August 2012 email to Abram drew the same contrast for a different purpose. To play games, I wrote, “you need a most probable model overall, not marginally most probable tuples (which can be inconsistent).” His prior was “unambiguously a distribution over structures.” Logical induction gained timeliness and guarantees by keeping marginals and delegating the structure. Where there is no structure for efficient tests to find, as with the Ackermann digits of π, nothing is lost: the reason is “no known structure,” and the presumption alone gives one in ten. The answers come apart only where structure exists.
My view, for now, is that logical induction has the right kind of definition and the wrong ambition. It defines what it is for a credence to be wrong in a way that someone could notice and profit from. That definition is the standard against which the other answers should be measured, and it is the right one for credences that will be acted on. It is not an account of mathematical understanding, because an understood fact comes with its latent structure, and a price is only that structure’s shadow on one sentence.
A reasoner worth building would keep the structure and still meet the standard. It would have three layers. A logic layer, such as an adaptive logic or the ontology essay’s provenance-tracking Self, records what has been derived and on which conditions. In a logical inductor the deductive process plays this part. A layer of reasons records what has been explained. A pricing layer, a market or a multicalibrated predictor, prices everything else.
The layers would work together. The market detects missing structure, the reason layer represents it, and the prior decides which representation to keep. A trader’s persistent profit signals structure that no current reason models. Finding it is abduction: what latent variable would make these prices coherent? The prior over structures, the ontology essay’s criterion of code length, chooses among the candidate reasons. Once adopted, the new reason absorbs the correlation and the profit stops. Prover–estimator debate is a small working instance of two of the layers: the steps that get checked are the logic layer, and the estimator’s probabilities are the pricing layer.
What explosion becomes
The logic layer need not be classical. Presumed Normal opened with paraconsistent logic, which blocks explosion, the classical principle by which a contradiction implies everything. Does it help with logical uncertainty? The two address different problems. Paraconsistency handles premises that are inconsistent. Logical uncertainty handles premises that are consistent but whose consequences have not been worked out. They meet in four places.
First, credences do not explode. A credence of 0.6 in p and 0.6 in \neg p does not make anything certain. What replaces explosion is exploitability. Schervish, Seidenfeld and Kadane measured incoherence by the rate at which a bookie with incoherent prices can be made a sure loser. Julia Staffel compared such measures in 2015. For a market, the measure is arbitrage profit. An adaptive logic confines a contradiction and withdraws what depends on it. A market confines it and charges for it.
Second, Presumed Normal already contains a probability that
tolerates contradiction. Its encoding of the paraconsistent logic CLuN
gives each sentence letter A two atoms,
true(A) and neg(A), at least one of which
holds. Write \sim for CLuN’s negation.
Weighting each model by e^{-wk}, where
k counts letters with both atoms true,
gives
P(A)+P(\sim A)=1+P(A\land\sim A),
which exceeds 1 for every finite w. The weight w measures how strongly consistency is presumed. As w grows, the probability concentrates on the models with the fewest contradictory letters. In Presumed Normal’s example those are the models that the adaptive strategy called Minimal Abnormality keeps, though in general that strategy minimizes by set inclusion, not by count.
Dominik Klein, Ondrej Majer and Soroush Rafiee Rad’s “Probabilities with gaps and gluts” (2021) develops such probabilities in general. In them the probabilities of \varphi and \neg\varphi “need not sum up to 1”: a sum below 1 is a gap, a sum above 1 a glut. J. Michael Dunn had described the two cases as “too little information (ignorance)” and “too much information (conflicted).” The distinction is one a logical inductor’s single price erases: “nobody has looked at this conjecture” against “a heuristic says yes and a failed proof attempt suggests no.”
Third, a weaker logic is cheaper. Hector Levesque’s “A logic of implicit and explicit belief” (1984) closed explicit belief under the entailment of relevance logic, which he analyzed with Nuel Belnap’s four-valued semantics, a paraconsistent one. His reason was cost. For a propositional knowledge base and a query, both in conjunctive normal form, deciding classical implication is co-NP-complete, but deciding this weaker entailment takes time proportional to the product of their sizes. Peter Patel-Schneider used four-valued semantics to make description logics tractable for the same reason. Weatherson’s recipe turns this into a notion of probability: coherence with respect to the weaker logic is the coherence a bounded agent can afford. Logical induction uses the same idea at its base. Its plausible worlds need only be consistent with the theorems found so far in propositional logic, with quantified sentences treated as atoms. The shape matches an adaptive logic’s: a cheap logic that always holds, and classical coherence approached in stages.
Fourth, a reasoner may doubt the consistency of its own theory. A logical inductor gives a price to the sentence asserting that Peano arithmetic is consistent. If the theory were inconsistent, the deductive process would eventually prove every sentence, and every price would go to 1. A paraconsistent base would keep such a reasoner useful. The case rarely matters for arithmetic. It matters for a reasoner like the ontology essay’s Self, which adopts claims from sources and is expected to meet contradictions.
Learning without new evidence
A logically omniscient Bayesian has nothing to learn from itself. It already holds every consequence of what it knows, so thinking cannot change its mind. Everything a logically uncertain reasoner learns without new observations, it learns from its own computation. Good’s evolving probability, Garber’s learning of implications, Abram’s inductive treatment of unproved statements and logical induction’s movement of prices as the deductive process proceeds all describe belief that changes by thinking. Abram later read logical induction as “merely a specific way to flesh out” Richard Jeffrey’s radical probabilism, in which beliefs change without conditioning on observations.
Machine learning met the same phenomenon from the other side. Who Teaches the Weights? described self-distillation, in which a model is trained toward its own outputs under better context. It works because a model can draw inferences in context that its weights do not contain. Andrew Lampinen and colleagues found that models reason about reversals and syllogisms better in context than after fine-tuning on the same facts, and that fine-tuning can “even exceed ICL generalization, by spending more train time compute to augment the training dataset using in-context reasoning.” If a model gains from training on its own reasoning, it was not logically omniscient. Self-distillation is logical learning made permanent: derivations that are slow in context are compiled into the weights, which How Does a Policy Improve? calls amortization. The theory of usable information of Yilun Xu and colleagues gives the formal version: “Unlike Shannon’s mutual information and in violation of the data processing inequality, V-information can be created through computation.” Information relative to a bounded family of predictors is the adversarial answer once more.
When is such learning sound? The Given and the Found argued that the confidence of a self-made training target sets the size of an update, while whether the target is grounded sets its sign. Logical uncertainty sharpens what grounding requires. The line does not fall between internal and external evidence. It falls between checks that are independent of the beliefs being trained and checks that are not.
AlphaZero is the clean case. The Given and the Found counted its game outcomes as grounding. They are also logical facts, since the value of a chess position is determined by the rules, so AlphaZero learned mathematics about chess with no evidence beyond its own play. Its check was internal and independent of its beliefs. The network Abram and I never built would have been in the same corner of the table of adversaries, because whether a string belongs to a language is decided exactly. MuZero learns its model of the game, so its search settles against a simulator that may be wrong, and How Does a Policy Improve? warns that “more search within the same erroneous simulator can intensify it.”
On-Policy Self-Training (OPST), a Google preprint of October 2026, sits at the far end. A model writes its own questions, rationales and answers from a topic name, keeps a sample only if it reaches the same answer again in a fresh context and after rewording, and trains toward a teacher, an average of its past selves, that sees the rationale. Nothing outside the model checks anything. The authors are clear about the consequence: “OPST can only amplify existing knowledge, and since pseudo-verification measures self-consistency rather than correctness, consistent errors still enter training.” In the bookmaker essay’s terms, OPST is a market that never resolves, in which traders are paid for agreeing. Coherence is necessary for a good credence and not sufficient. A coherent wrong completion passes every consistency filter, as a coherent myth told by many independent sources passes the ontology essay’s compression test.
OPST even has a liquidity parameter: the rate \beta at which the teacher follows the student, the moving teacher of Who Teaches the Weights?. With \beta=1 the teacher is the current student, the shallow market of the bookmaker essay, in which one trade can carry the price far. The authors report that “errors can reinforce themselves,” and the gain nearly vanishes. The best rate they found is \beta=0.05.
In the table of adversaries, OPST’s only test is internal, and neither settlement nor a check on demand holds it to account. There are two ways out of that position. One is an internal check that is independent of the beliefs: exact rules, a proof checker, an executable test. The other is an external check: a verifier, a debate in which a liar loses, a source whose testimony is trusted. Interactive proofs show that a bounded learner can obtain an independent check without computing the fact itself.
A second question concerns incentives. Does anything have a reason to bid up what the learner has priced near zero? Like a bandit, an on-policy learner learns only about what it samples, and it rarely samples what it has priced low. Who Teaches the Weights? showed such training collapsing onto one strategy. OPST adds a gate that makes the loss final: it drops a question once every rollout agrees. A question on which the model is unanimously wrong is dropped, and the error stays.
A logical inductor is in Hedge’s position, not a bandit’s. Every trade is evaluated against what has been proved, whatever price the market gave the sentence, and non-dogmatism keeps the limiting price of every sentence the axioms do not refute above zero. As the bookmaker essay put it, a trader who believes in a cheap outcome profits most by buying it. AlphaZero sits between. At each node of the search PUCT is a bandit rule, and its exploration bonus scales with the network’s prior, so the search rarely visits a move the network has priced near zero. Dirichlet noise added to the prior at the root keeps such moves alive, and the network then trains on the whole distribution of visits. A logic layer does not meet the problem at all. Unmarking a line in an adaptive proof restores its conclusion at once, while a learner that has driven a hypothesis near zero climbs back slowly, because a multiplicative step moves a probability in proportion to its size.
Steering the search
Old evidence is the human case of learning without new evidence. Mercury’s perihelion raised confidence in general relativity with no new observation. The logical induction paper lists the use of old evidence among its desiderata and claims only “a weak sense” in which logical inductors solve the problem: they get better at finding patterns in data they have already seen. A strong solution, it says, would have to explain “how to algorithmically generate new scientific theories,” and logical inductors “invent” theirs “by sheer brute force.” The gap is the one between a price and a reason.
Two operations make such a rise in confidence sound, and human reasoners can fail at each. One brackets the datum: Colin Howson asks how the hypothesis fares against a body of knowledge with the datum taken out. The reasoner then sees what the hypothesis says about that outcome and about the alternative. The other computes: for Garber, the news is that the theory implies the datum. Both failures feel empirical, because the reasoner is holding a real datum.
The first failure is not bracketing at all. Asked what a hypothesis predicted, the reasoner answers with what happened. Baruch Fischhoff showed in 1975 that people told to ignore a known outcome do not manage to. This failure does track a lack of sophistication, at least where the task names the demand. Asked to judge whether a syllogism is valid and to set aside whether its conclusion is believable, people of higher cognitive ability are swayed less by the belief. Keith Stanovich calls the skill decoupling.
The second failure comes after bracketing, and sophistication does not prevent it. Once finding “h ⊢ e” counts as learning, every derivation of a known fact raises the credence of the theory that implies it, and the reasoner chooses which derivations to look for. Ziva Kunda’s “The case for motivated reasoning” (1990) describes that choice. When one wants a particular conclusion, in Kunda’s words, “one feels obligated to construct a justification for that conclusion that would be plausible to a dispassionate observer. In doing so, one accesses only a biased subset of the relevant beliefs and rules.” Stanovich, Richard West and Maggie Toplak review studies in which this myside bias is largely independent of intelligence, and they name the difference from the syllogisms: nobody told these subjects to decouple. Ability supplies the capacity when the task asks for it. It does not supply the occasion. Nor does the reasoner notice. West, Russell Meserve and Stanovich found no negative correlation between cognitive ability and the blind spot about one’s own biases. So a sophisticated reasoner can believe they are an empiricist while much of their updating is logical learning that they steered.
Each step of such a search can be valid. A proof checker would pass every derivation, and the credence would still drift, because the failures go uncounted. A fair search cannot be expected to raise a credence: if finding a derivation would raise it, failing to find one must lower it. Logical induction states the constraint as a theorem, No Expected Net Update: a sentence’s price today approaches today’s expectation of its future price. Once a logical inductor has learned how expectations work, the paper says, “it will never say ‘I currently believe that the X variables have low values, but tomorrow I’m going to learn that they have high values.’” Someone who expects thinking to confirm their view is making that forecast.
OPST is the machine version of steering, since it chooses what to train on by what the model already favors. A logical inductor is protected by construction, because its deductive process does not consult its prices. The protection has a cost. The paper says its algorithm “does nothing akin to ‘thinking about what to think about,’” with “no obvious mechanism for steering its deliberations.” A bounded reasoner cannot run every search, so it has to steer. The remedy is bookkeeping: a credence built on checked derivations is only as sound as the reasoner’s account of what it searched for and failed to find.
Logical induction has a definite place in the demarcation of The Given and the Found. That essay separated search over a correctness condition that is given, such as the rules of a game, from the discovery of the condition. For logical induction the axioms are given, and the regularities of their consequences are found. It is induction over a given deductive closure. Abram’s 2012 draft had already marked the boundary: the prior cannot learn new axioms, because it is limited to the incompleteness of the axioms it is given. Gaifman inductivity would have crossed that line in one direction, by letting checked instances establish a universal statement that the axioms leave open. Its impossibility is one form of the line.
Trust between inductors
In June 2026 Abram posted “What comes with cheap math?” For two months he and Anson Berns had been “collaborating on a project modeling trust between logical inductors.” The aim is to use logical induction as a model of human scientific progress and of AI self-improvement, so that one can “formally ask: when can humans justifiably trust AI?” He did the work with Claude, asking it “to use Lean to verify everything.” He found that the formal proofs did not always prove what the informal claims said. “AI will try to do whatever you ask it to do, so it is much easier now to fool yourself with math.” A proof checker settles whether a theorem follows from its premises. It does not settle whether the theorem says what one meant: “Lean-verification can’t distinguish a good model from a bad one.” His conclusion: “The new bottleneck becomes something like care, or taste, or discernment.”
Abram’s experience shows the criterion of an independent check meeting its own limit. A proof checker is the cleanest independent check there is, and it certifies only the step from a formal statement to its proof. Whether the statement is the right one is a question about the given condition, which no internal check reaches. The question Abram is now asking with logical inductors, when a reasoner may trust another that computes more, is the problem MIRI’s 2014 agenda called Vingean reflection. Logical induction answered it only for a reasoner’s trust in its own future beliefs. OPST raises it about a model and its average past selves. In 2012 I asked him about “self outputs.” Fourteen years later he is working on a version of the same question.
Presumed Normal closed by asking whether a reasoner can always stop, and gave three answers. Logical uncertainty gives a fourth: no, but it can bet at every stage. That essay’s first proof derived r at line 5 and withdrew it at line 8. A reasoner who acted on r in between was right to, given what the proof had found so far. Its belief in r was a price, not a commitment, and the search had not settled.
Sources. Clark Glymour, Theory and Evidence (Princeton University Press, 1980). Abram Demski, “Logical Prior Probability,” in Artificial General Intelligence (AGI 2012), LNCS 7716, 50–59; the account above follows the July 2012 draft he shared with me. Will Sawin and Abram Demski, “Computable probability distributions which converge on believing true Π1 sentences will disbelieve true Π2 sentences,” MIRI technical report (workshop July 2013, released December 2014). Scott Garrabrant, Tsvi Benson-Tilsen, Andrew Critch, Nate Soares and Jessica Taylor, “Logical Induction,” arXiv:1609.03543 (2016). Teddy Seidenfeld, Mark Schervish and Joseph Kadane, “What kind of uncertainty is that?,” Journal of Philosophy 109 (2012), 516–533. Alina Beygelzimer, John Langford and David Pennock, “Learning performance of prediction markets with Kelly bettors,” AAMAS 2012. Vladimir Vovk, Akimichi Takemura and Glenn Shafer, “Defensive forecasting,” AISTATS 2005. Úrsula Hébert-Johnson, Michael Kim, Omer Reingold and Guy Rothblum, “Multicalibration,” ICML 2018. Cynthia Dwork, Michael Kim, Omer Reingold, Guy Rothblum and Gal Yona, “Outcome Indistinguishability,” STOC 2021. Paul Christiano, Eric Neyman and Mark Xu, “Formalizing the presumption of independence,” arXiv:2211.06738 (2022). Jonah Brown-Cohen, Geoffrey Irving, Georgios Piliouras, Lijie Chen, Jiawei Li and Zhiyang Xun, “Avoiding Obfuscation with Prover-Estimator Debate,” arXiv:2506.13609. Dominik Klein, Ondrej Majer and Soroush Rafiee Rad, “Probabilities with gaps and gluts,” Journal of Philosophical Logic 50 (2021). Hector Levesque, “A logic of implicit and explicit belief,” AAAI 1984. Leon Sick and colleagues, “On-Policy Self-Training,” arXiv:2610.32770 (2026). Ziva Kunda, “The case for motivated reasoning,” Psychological Bulletin 108 (1990), 480–498. Keith Stanovich, Richard West and Maggie Toplak, “Myside bias, rational thinking, and intelligence,” Current Directions in Psychological Science 22 (2013), 259–264.
This article was co-authored by Łukasz Stafiniak and Claude (Opus 5.5).