{'fraction_non_alphanumeric': 0.038352064321136185, 'fraction_numerical': 0.0082162035270988, 'mean_word_length': 4.4755784061696655, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 10, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Formal Approach to the Problem of Logical Non-Omniscience

We present the logical induction criterion for computable algorithms that assign probabilities to every logical statement in a given formal language, and refine those probabilities over time. The criterion is motivated by a series of stock trading analogies. Roughly speaking, each logical sentence phi is associated with a stock that is worth $1 per share if phi is true and nothing otherwise, and we interpret the belief-state of a logically uncertain reasoner as a set of market prices, where pt_N(phi)=50% means that on day N, shares of phi may be bought or sold from the reasoner for 50%. A market is then called a logical inductor if (very roughly) there is no polynomial-time computable trading strategy with finite risk tolerance that earns unbounded profits in that market over time. We then describe how this single criterion implies a number of desirable properties of bounded reasoners; for example, logical inductors outpace their underlying deductive process, perform universal empirical induction given enough time to think, and place strong trust in their own reasoning process.


Introduction
Every student of mathematics has experienced uncertainty about conjectures for which there is "quite a bit of evidence", such as the Riemann hypothesis or the twin prime conjecture. Indeed, when Zhang [51] proved a bound on the gap between primes, we were tempted to increase our credence in the twin prime conjecture. But how much evidence does this bound provide for the twin prime conjecture? Can we quantify the degree to which it should increase our confidence?
The natural impulse is to appeal to probability theory in general and Bayes' theorem in particular. Bayes' theorem gives rules for how to use observations to update empirical uncertainty about unknown events in the physical world.
However, probability theory lacks the tools to manage logical non-omniscience: probability-theoretic reasoners cannot possess uncertainty about logical facts so long as their beliefs respect basic logical constraints. For example, let φ stand for the claim that the 87,653rd digit of π is a 7. If this claim is true, then (1 + 1 = 2) ⇒ φ . But the laws of probability theory say that if A ⇒ B then Pr(A) ≤ Pr(B). Thus, a perfect Bayesian must be at least as sure of φ as they are that 1 + 1 = 2! Recognition of this problem dates at least back to [23].
Many have proposed methods for relaxing the criterion Pr(A) ≤ Pr(B) until such a time as the implication has been proven (see, e.g., the work of [26,7]). But this leaves open the question of how probabilities should be assigned before the implication is proven, and this brings us back to the search for a principled method for managing uncertainty about logical facts when relationships between them are suspected but unproven.
In this paper we describe what we call the logical induction criterion for reasoning under logical uncertainty. Our solution works, more or less, by treating a reasoner's beliefs as prices in a market that fluctuate over time, and requiring that those prices not be exploitable indefinitely by any sequence of trades constructed by an efficient (polynomial-time) algorithm. The logical induction criterion can be seen as a weakening of the "no Dutch book" criteria that Ramsey [42], de Finetti [14], Teller [48], and Lewis [36] used to support standard probability theory, which is analogous to the "no Dutch book" criteria that von Neumann and Morgenstern [40] and Joyce [33] used to support expected utility theory. Because of the analogy, and the variety of desirable properties that follow immediately from this one criterion, we believe that the logical induction criterion captures a portion of what it means to do good reasoning about logical facts in the face of deductive limitations. Section 2 lists desiderata for reasoning under logical uncertainty. Section 3 lists further related work. Section 4 presents an overview of the logical induction framework. Section 5 discusses a collection of properties satisfied by logical inductors. Section 6 gives concluding remarks. Note on abridgement: Due to space considerations, this paper does not include proofs of claims, and describes some results only at a high level. The formal details of our definitions and theorems, additional properties of logical inductors, proofs of properties, a construction of a logical inductor, and further discussion can be found in [18].

Desiderata for Reasoning under Logical Uncertainty
For historical context, and to further reify the problem, we now review a number of desiderata that have been proposed in the literature as desirable features of "good reasoning" in the face of logical uncertainty. Desideratum 3 dates back to at least Good [23], who proposes a weakening of the condition of coherence that could apply to the belief states of limited reasoners. Hacking [26] proposes an alternative weakening, as do Garrabrant et al. [19].
Desideratum 4 (Learning of Statistical Patterns). In lieu of knowledge that bears on a logical fact, a good reasoner should assign probabilities to that fact in accordance with the rate at which similar claims are true.
For example, a good reasoner should assign probability ≈ 10% to the claim "the nth digit of π is a 7" for large n (assuming there is no efficient way for a reasoner to guess the digits of π for large n); see [44].
Desideratum 5 (Calibration). Good reasoners should be well-calibrated. That is, among events that a reasoner says should occur with probability p, they should in fact occur about p proportion of the time. In the domain of logical uncertainty, Desideratum 6 can be traced back to Carnap [6,Sec. 53], and has been demanded by many, including Gaifman [16] and Hutter [31].
Desideratum 7 (Uniform Non-Dogmatism). A good reasoner should assign a non-zero probability to any computably enumerable consistent theory (viewed as a limit of finite conjunctions).
(Discussed in Section 5.2.) The first formal statement of Desideratum 7 that we know of is given by Demski [9], though it is implicitly assumed whenever asking for a set of beliefs that can reason accurately about arbitrary arithmetical claims (as is done by, e.g., Savage [44] and Hacking [26] Desideratum 10 (Self-knowledge). If a good reasoner knows something, she should also know that she knows it.
(Discussed in Section 5.4.) Proposed by Hintikka [30], Desideratum 10 is popular among epistemic logicians. This desideratum has been formalized in many different ways; see [8,5] for a sample.
Desideratum 11 (Self-Trust). A good reasoner thinking about a hard problem should expect that, in the future, her beliefs about the problem will be more accurate than her current beliefs. As noted by Eells [10], the Dutch book constraints used by von Neumann and Morgenstern [40] and de Finetti [14] are implausibly strong: all it takes to run a Dutch book according to de Finetti's formulation is for the bookie to know a logical fact that the reasoner does not know. Thus, to avoid being Dutch booked by de Finetti's formulation, a reasoner must be logically omniscient.
Hacking [26] and Eells [10] call for weakenings of the Dutch book constraints, in the hopes that reasoners that are approximately inexploitable would do good approximate reasoning. This idea is the cornerstone of our framework-we consider reasoners that cannot be exploited by betting strategies that can be constructed by a polynomial-time machine.

Additional Related Work
The study of logical uncertainty is an old topic. It can be traced all the way back to Bernoulli, who laid the foundations of statistics, and later Boole [4], who was interested in the unification of logic with probability from the start. Refer to [27] for a historical account. Our algorithm assigns probabilities to sentences of logic directly; this thread can be traced back through Łoś [38] and later Gaifman [15], who developed the notion of coherence that we use in this paper.
When it comes to the problem of developing formal tools for manipulating uncertainty, our methods are heavily inspired by Bayesian probability theory, and so can be traced back to Pascal, who was followed by Bayes, Laplace, Kolmogorov [34], Savage [43], Carnap [6], Jaynes [32], and many others. Polya [41] was among the first in the literature to explicitly study the way that mathematicians engage in plausible reasoning, which is tightly related to the object of our study.
In addition to Good [23], Savage [44], and Hacking [26], the flaw in Bayesian probability theory was also highlighted by Glymour [21], and dubbed the "problem of old evidence" by Garber [17] in response to Glymor's criticism. Eells [10] gave a lucid discussion of the problem, revealed flaws in Garber's arguments and in Hacking's solution, and named a number of other desiderata which our algorithm manages to satisfy; see [53] and [47]. Adams [2] uses logical deduction to reason about an unknown probability distribution that satisfies certain logical axioms. Our approach works in precisely the opposite direction: we use probabilistic methods to create an approximate distribution where logical facts are the subject.
Some work in epistemic logic has been directed at modeling the dynamics of belief updating in non-omniscient agents; see for example [35,50,3]. Our approach differs in that we use first-order logic, and therefore use the recursion theorem to make reflective statements instead of using explicit knowledge or belief operators; the potential paradoxes of self-reference are circumvented by allowing beliefs to be probabilistic. The mechanism used by our logical inductor to update its beliefs is not very transparent, leaving open the possibility of a more principled understanding of the local mechanics of updating probabilities on logical or inductive inferences.
Straddling the boundary between philosophy and computer science, Aaronson [1] has made a compelling case that computational complexity must play a role in answering questions about logical uncertainty. Fagin and Halpern [12] also straddled this boundary with early discussions of algorithms that manage uncertainty in the face of resource limitations. (See also their discussions of uncertainty and knowledge. [13,28])

The Logical Induction Criterion
We propose a partial solution to the problem of logical non-omniscience, which we call logical induction. Roughly speaking, a logical inductor is a computable reasoning process that is not exploitable by any polynomial-time computable strategy for making trades against it, using its probabilities as the prices of shares. In this section we give a high-level overview of the criterion and the main result (details are in [18]), before giving precise statements in Section 5 of some of the properties satisfied by logical inductors.
Very roughly, our setup works as follows. We consider reasoners that assign probabilities to sentences S written in some formal language L .
Here P(φ ) is interpreted as the probability of φ . We can visualize a pricing as a list of (φ , p) pairs, where the φ are unique sentences and the p are rational-number probabilities, and P(φ ) is defined to be p if (φ , p) occurs in the list, and 0 otherwise. (In this way we can represent belief states of reasoners that can be written down explicitly in a finite amount of space.) The output of a reasoner is then nothing but a sequence of pricings: The pricings (P 1 , P 2 , . . .) represent the belief states of a reasoner progressively refining their opinions about the logical statements in S . In the background, there is some process producing progressively larger sets of trusted statements: The deductive process D can be thought of as a theorem prover for some trusted logical theory Γ in the language L . Indeed, we will henceforth assume that Γ = n D n . Thus the goal of our reasoner P is to anticipate which statements will be proven or disproven by Γ, well before the rote proof-search D decides those statements.
As in classical Dutch book arguments for probability theory, in addition to seeing P(φ ) = p as an assignment of subjective credence to φ , we also view P(φ ) as a stance with respect to which bets are desirable or not. That is, we interpret P(φ ) = p to mean that the price of a φ -share according to P is p, where (roughly speaking) a φ -share is worth $1 if φ is true. This allows us to set up Dutch book arguments against a reasoner using computable bookies: where each T n is a trading strategy for day n.
Without belaboring the details, a trading strategy for day n is a strategy for responding to the day's market prices P n with buy orders and sell orders for shares in sentences from S . (Formally, it is a continuous function from pricings to linear combinations of sentences, expressed in some computable language.) Over time, a trader accumulates cash and stock holdings from the trades it makes against P.
The logical induction criterion then demands of market prices P that no efficiently computable trader can reliably make money by trading against the market prices (P 1 , P 2 , . . .): Definition 4.0.5 (The Logical Induction Criterion). A market P is said to satisfy the logical induction criterion relative to a deductive process D if there is no efficiently computable trader that exploits P relative to D. A market P meeting this criterion is called a logical inductor over D.
Again glossing over details, a trader is said to exploit P relative to D if the possible values of the trader's holdings from trading against P are unboundedly high over time, without being unboundedly low, where holdings are evaluated by what truth assignments to S are propositionally consistent with D n at time n. Here, "efficiently computable" (abbreviated e.c.) can be taken to mean computable in time polynomial in n, but this is not crucial to the definition. Given the assumption that Γ = n D n , we also say that P is a logical inductor over Γ.
Our key theorem is that this criterion, while gratifyingly strong, is also feasible: Theorem 4.0.6. For any deductive process D, there exists a computable belief sequence P satisfying the logical induction criterion relative to D.

Properties of Logical Inductors
Here is an intuitive argument that logical inductors perform good reasoning under logical uncertainty: Consider any polynomial-time method for efficiently identifying patterns in logic. If the market prices don't learn to reflect that pattern, a clever trader can use that pattern to exploit the market. Thus, a logical inductor must learn to identify those patterns.
This section will substantiate this argument by stating a number of properties satisfied by logical inductors, corresponding to some of the desiderata discussed in Section 2. Proofs of Theorem 4.0.6 and the theorems in this section can be found in [18].

Notation
Throughout, we assume that P is a logical inductor over the theory Γ. We also assume that Γ represents computations in the technical sense, i.e. we can write terms in L that stand for computations, and Γ proves that those terms evaluate to their correct value (and no other value).
We will enclose sentences in quotation marks when they are used as syntactic objects. An underlined symbol should be replaced by the expression it stands for. For example, f (n) stands for a program that computes the function f given input n, whereas f (n) stands for the numeral f (n) evaluates to.
We use an overline to denote sequences of sentences, probabilities, and other objects, as in P and D; for example, φ is the sequence of sentences (φ 1 , φ 2 , . . . ). A sequence x is efficiently computable (e.c.) if and only if there exists a computable function n → x n with runtime polynomial in n. Given any sequences x and y, we write x n n y n for lim n→∞ x n − y n = 0, and x n n y n for lim inf n→∞ x n − y n ≥ 0. Roughly speaking, if P never makes up its mind about φ , then it can be exploited by a trader arbitraging shares of φ across different days. That is, suppose by way of contradiction that P n (φ ) never settles down, but rather oscillates by a substantial amount infinitely often. Then there is a trader that repeatedly buys a share in φ when the price is low, and sells it back when the price is high. This trader accumulates unbounded wealth, thereby exploiting P, which contradicts that P is a logical inductor; therefore the limit P ∞ (φ ) must in fact exist.

Properties of the limit
This sketch showcases the main intuition for the convergence of P, but elides a number of crucial details; see [18]. Next, the limiting beliefs of a logical inductor represent a coherent probability distribution: First formalized by Gaifman [15], coherence says that beliefs should satisfy probabilistic versions of logical consistency; for example, the reasoner should assign Pr(φ ) ≤ Pr(ψ) if φ ⇒ ψ, etc. This theorem is proven using methods analogous to standard Dutch book arguments for coherent beliefs, translated into the language of traders. Convergence and coherence together justify that a logical inductor P approximates a belief state that is consistent with the background theory Γ. What else is there to say about the limiting beliefs P ∞ of a logical inductor?
For starters, P learns not to assign extreme probabilities to sentences that are independent from Γ: Non-dogmatism can be viewed as an inductive property: non-dogmatic beliefs can be easily conditioned on events (sentences) that haven't already been observed (proved or disproved), producing a coherent conditional belief state, whereas conditioning dogmatic beliefs can cause problems. We can push the idea of inductive reasoning much further, following the work of Solomonoff [45,46], Zvonik and Levin [52] and Li and Vitányi [37] on empirical sequence prediction. They describe an inductive process (known as a universal semimeasure) that predicts as well or better than any computable predictor, modulo a constant amount of error. Although universal semimeasures are uncomputable, we can ask logically uncertain reasoners to copy those successes given enough time to think: . Let M be a universal continuous semimeasure. Then there is some positive constant C such that for any finite bitstring σ ≤n , In other words, logical inductors are a computable approximation to a normalized probability distribution that dominates any lower semicomputable semimeasure. In fact, this dominance is strict: P ∞ will e.g., assign positive probability to sequences that encode completions of Peano arithmetic, which the universal semimeasure does not do. 1

Outpacing deduction
It is not too difficult to define a reasoner that assigns probability 1 to all (and only) the provable sentences, in the limit: simply assign probability 0 to all sentences, and then enumerate all logical proofs, and assign probability 1 to the proven sentences. The real trick is to recognize patterns in a timely manner, well before the sentences can be proven by slow deduction. Furthermore, let ψ be an e.c. sequence of disprovable sentences. Then P n (ψ n ) n 0.

Proof sketch.
Suppose not. Then there is a trader that buys a share in φ n whenever the price is too far below $1, and then waits for φ n to appear in the deductive process D, repeating this process indefinitely. This trader would exploit P, a contradiction.
In other words, P will learn to start believing φ n by day n at the latest, despite the fact that φ n won't be deductively confirmed until day f (n), which is potentially much later. In colloquial terms, if φ is a sequence of facts that can be generated efficiently, then P inductively learns the pattern, and its belief in φ becomes accurate faster than D can computationally verify the individual sentences.
Analogy: Ramanujan and Hardy. Imagine that the statements φ are being output by an algorithm that uses heuristics to generate mathematical facts without proofs, playing a role similar to the famously brilliant, often-unrigorous mathematician Srinivasa Ramanujan. Then P plays the historical role of the beliefs of the rigorous G.H. Hardy who tries to verify those results according to a slow deductive process (D). After Hardy (P) verifies enough of Ramanujan's claims (φ ≤n ), he begins to trust Ramanujan, even if the proofs of Ramanujan's later conjectures are incredibly long, putting them ever-further beyond Hardy's current abilities to rigorously verify them. In this story, Hardy's inductive reasoning (and Ramanujan's also) outpaces his deductive reasoning.
To further emphasize the meaning of Theorem 5.3.1 (Provability Induction), consider the famous halting problem of Turning [49]. Turing proved that there is no general algorithm for determining whether or not an arbitrary computation halts. Let's examine what happens when we confront logical inductors with the halting problem.

Theorem 5.3.2 (Learning of Halting Patterns). Let m be an e.c. sequence of Turing machines, and x be an e.c. sequence of bitstrings, such that m n halts on input x n for all n. Then
P n ("m n halts on input x n ") n 1.
Of course, this is not so hard on its own-a function that assigns probability 1 to everything also satisfies this property. The real trick is separating the halting machines from the non-halting ones.
By undecidability, there are Turing machines q that fail to halt on input y, but such that Γ is not strong enough to prove this fact. In this case, P ∞ 's probability of q halting on input y is positive, by Theorem 5.2.3 (Non-Dogmatism). Nevertheless, P still learns to stop expecting that those machines will halt after any reasonable amount of time: Theorem 5.3.3 (Learning not to Anticipate Halting). Let q be an e.c. sequence of Turing machines, and let y be an e.c. sequence of bitstrings, such that q n does not halt on input y n for any n. Let f be any computable function. Then P n ("q n halts on input y n within f (n) steps") n 0.
These theorems can be interpreted as justifying the intuitions that many computer scientists have long held towards the halting problem: It is impossible to tell whether or not a Turing machine halts in full generality, but for large classes of well-behaved computer programs (such as e.c. sequences of halting programs and provably non-halting programs) it's quite possible to develop reasonable and accurate beliefs. The boundary between machines that compute fast-growing functions and machines that never halt is difficult to distinguish, but even in those cases, it's easy to learn to stop expecting those machines to halt within any reasonable amount of time.
As a consequence of of Theorem 5.3.3 (Learning not to Anticipate Halting), a logical inductor will trust their (computable) underlying deductive process D to remain consistent for arbitrarily long specified periods of time, if in fact D is consistent. In other words, a logical inductor over the theory Γ will learn trust in the finitary consistency of Γ.
One possible objection here is that the crux of the halting problem (and of the Γ-trust problem) is not about making good predictions, it is about handling diagonalization and paradoxes of self-reference. So let us turn to the topic of P's beliefs about P itself.

Self-knowledge
Because we're assuming Γ can represent computable functions, we can write sentences describing the beliefs of P at different times. What happens when we ask P about sentences that refer to itself? Theorem 5.4.1 (Self-knowledge). Let φ be an e.c. sequence of sentences, let a, b be e.c. sequences of probabilities. Then, for any e.c. sequence of positive rationals δ → 0, there exists a sequence of positive rationals ε → 0 such that for all n: 1. if P n (φ n ) ∈ (a n + δ n , b n − δ n ), then P n ("a n < P n (φ n ) < b n ") > 1 − ε n , 2. if P n (φ n ) / ∈ (a n − δ n , b n + δ n ), then P n ("a n < P n (φ n ) < b n ") < ε n .
In other words, for any pattern in P's beliefs that can be efficiently written down (such as "P's probabilities on φ are between a and b on these days"), P learns to believe the pattern if it's true, and to disbelieve it if it's false (with vanishing error). (Recall that the underlines indicate that the underlined expression should be expanded to the appropriate logical formula or term, representing e.g., the source code of an algorithm implementing P.) At a first glance, this sort of self-reflection may seem to make logical inductors vulnerable to paradox. For example, consider the sequence of sentences χ 0.5 defined using the diagonal lemma by χ 0.5 n := "P n (χ 0.5 n ) < 0.5" such that χ 0.5 n is true iff P assigns it a probability less than 50% on day n. Such a sequence can be defined by Gödel's diagonal lemma. These sentences are probabilistic versions of the classic "liar sentence", which has caused quite a ruckus in the setting of formal logic [24,39,20,25,11]. Because our setting is probabilistic, it's perhaps most closely related to the "unexpected hanging" paradox-χ 0.5 n is true iff P thinks it is unlikely on day n. How do logical inductors handle this sort of paradox? Theorem 5.4.2 (Paradox Resistance). Fix a rational p ∈ (0, 1), and define an e.c. sequence of "paradoxical sentences" χ p satisfying Γ ⊢ χ p n ↔ P n (χ p n ) < p for all n. Then lim n→∞ P n (χ p n ) = p.
In words, a logical inductor responds to paradoxical sentences χ p by assigning them probabilities that converge on p.
To understand why this is desirable, imagine that your friend owns a high-precision brain-scanner and can read off your beliefs. Imagine they ask you what probability you assign to the claim "you will assign probability <80% to this claim at precisely 10am tomorrow". As 10am approaches, what happens to your belief in this claim? If you become extremely confident that it's going to be true, then your confidence should drop. But if you become fairly confident it's going to be false, then your confidence should spike. Thus, your probabilities should oscillate, pushing your belief so close to 80% that you're not quite sure which way the brain scanner will actually call the claim, and you think the scanner is roughly 80% likely to call it true. In response to a paradoxical claim, this is exactly how P behaves, once it's learned how the paradoxical sentences work.

Self-Trust
We've seen that logical inductors can, without paradox, have accurate beliefs about their own current beliefs. Next, we turn our attention to the question of what a logical inductor believes about its future beliefs.
The coherence conditions of classical probability theory guarantee that, though a probabilistic reasoner expects their future beliefs to change in response to new empirical observations, they don't e.g., believe that their future credence in φ is, in net expectation, lower than their current credence in φ . For example, if a reasoner Pr(−) knows that tomorrow they'll see some evidence e that will convince them that Miss Scarlet was the murderer, then they already believe that she was the murderer today: Pr(Scarlet) = Pr(Scarlet | e)Pr(e) + Pr(Scarlet | ¬e)Pr(¬e).
In colloquial terms, this says "my current beliefs are already a mixture of my expected future beliefs, weighted by the probability of the evidence that I expect to see." Logical inductors obey similar coherence conditions with respect to their future beliefs, with the difference being that a logical inductor updates its belief by gaining more knowledge about logical facts, both by observing an ongoing process of deduction and by thinking for longer periods of time.
To refer to P's expectations about its future self, we need a notion of logically uncertain variables. To avoid needless detail, suffice it to say that logically determined quantities, such as the output of a given computer program, can be represented and manipulated analogously to random variables in probability theory. We can write these variables as terms representing their value; for example, the variable written "P n (φ )" represents the probability assigned to φ by P on day n. Using the beliefs P n of P about X on day n, we can define the (approximate) expectation E n (X ).
We also need to know which future self our logical inductor will defer to: Now we can state the sense in which logical inductors don't expect, on net, their future beliefs to be wrong in any particular direction.
Theorem 5.5.2 (No Expected Net Update). Let f be a deferral function, and let φ be an e.c. sequence of sentences. Then P n (φ n ) n E n ("P f (n) (φ n )").
This theorem only says that P n doesn't expect the beliefs of P f (n) about φ to err in a particular direction. A priori, it is possible that P n nevertheless believes its future beliefs P f (n) will be grossly misguided. For example, suppose that P n is very confident that P f (n) will have sufficient time to compute the truth of φ , but will react insanely to this information: This is a priori consistent with Theorem 5.5.2 so long as P n assigns P n (φ ) = 0.5, but it clearly indicates that P n does not trust its future beliefs.
To instead formalize the idea of a reasoner Pr that trusts their own reasoning process, let us first consider a self-trust property in the setting of deductive logic: This property of deductive systems says that the system proves "If I prove φ at some point, then it is true". However, any sufficiently strong reasoner that satisfies this property for the statement φ = ⊥ is inconsistent by Gödel's second incompleteness theorem! The search for logics that place confidence in their own machinery dates at least back to Hilbert [29]. While Gödel et al. [22] dashed these hopes, it is still desirable for reasoners to trust their reasoning process relatively well, most of the time (which humans seem to do).
As discussed in Section 5.3, logical inductors trust their underlying deductive process D in a slightly weaker, finitary sense. More interestingly, it turns out that logical inductors also trust their own reasoning process as a whole, including their inductive conclusions, in a manner that we now formalize.
Instead of ⊢ φ → φ , we can replace provability with high confidence, and then ask for something like Pr now (φ | Pr later (φ ) > p) p.
Colloquially, this says that if we tell Pr that in the future they will place more than p credence in φ , then they update their current beliefs to place at least p credence. In short, Pr trusts that the outputs of their own ongoing reasoning process will be accurate. Now, in fact property 5.5 is not quite desirable as stated (and logical inductors do not satisfy it). Indeed, consider the liar sentence χ p defined by χ p := "Pr later (χ p ) < p".
A good reasoner will then satisfy Pr now (χ p | Pr later (χ p ) > p) 0, contradicting equation 5.5. The issue is that if we give Pr now high-precision access to the probabilities assigned by Pr later -for example by conditioning on them-then Pr now can outperform the (unconditioned) beliefs of Pr later , in this case by having correct opinions about the liar sentence for Pr later .
Instead, we have the following self-trust property, which only gives P n limited-precision access to the beliefs of P f (n) : Theorem 5.5.3 (Self-Trust). Let f be a deferral function, φ be an e.c. sequence of sentences, δ be an e.c. sequence of positive rational numbers, and p be an e.c. sequence of rational probabilities. Then E n "1(φ n ) · Ind δ n P f (n) (φ n ) > p n " n p n · E n "Ind δ n P f (n) (φ n ) > p n " .
The indicator variable 1(φ ) represents 1 if φ is true and 0 if φ is false. The continuous indicator variable Ind δ (X > p) is an ordinary indicator of the event X > p, except that instead of a discontinuity at X = p, the value is linear in X on a region of length δ . Thus the self-trust property gives P n only continuous (limited precision) access to the beliefs of P f (n) ; except for this subtlety, we could have written the more recognizable (but false and undesirable!) statement P n "φ n ∧ P f (n) (φ n ) > p n " n p n · P n "P f (n) (φ n ) > p n " , where the conditional P n "φ n | P f (n) (φ n ) > p n " has been rearranged to avoid a potential division by 0.

Discussion
We have proposed the logical induction criterion as a criterion on the beliefs of deductively limited reasoners, and we have described how reasoners who satisfy this criterion (logical inductors) possess many desirable properties when it comes to developing beliefs about logical statements (including statements about mathematical facts, long-running computations, and the reasoner themself). That said, there are clear drawbacks to the logical inductor we describe in [18]: it does not use its resources efficiently; it is not a decision-making algorithm (i.e., it does not "think about what to think about"); and the properties above hold either asymptotically (with poor convergence bounds) or in the limit. Further, it is unclear whether logical inductors have good beliefs about counterpossibilities, and whether they take advantage of old evidence. These are enticing directions for further research.
The authors are particularly interested in tools that help AI scientists attain novel statistical guarantees in settings where robustness and reliability guarantees are currently difficult to come by. For example, consider the task of designing an AI system that reasons about the behavior of computer programs, or that reasons about its own beliefs and its own effects on the world. While practical algorithms for achieving these feats are sure to make use of heuristics and approximations, we believe scientists will have an easier time designing robust and reliable systems if they have some way to relate those approximations to theoretical algorithms that are known to behave well in principle. Modern models of rational behavior are not up to this task: formal logic is inadequate when it comes to modeling self-reference, and probability theory is inadequate when it comes to modeling logical uncertainty. We see logical induction as a first step towards models of rational behavior that work in settings where agents must reason about themselves, while deductively limited.