Repository navigation
Logical Induction and Deference
How can a bounded reasoner form rational beliefs about a computation it has not yet finished? Logical Induction models a sequence of prices for logical sentences. Efficiently computable traders may trade contracts at those prices; the criterion prevents any such trader from achieving unbounded upside with bounded downside. This gives a framework for bounded beliefs about logical facts before deduction has settled them. See Garrabrant et al. in Sources.
A present sentence can name a later quote or recommendation without making that future value legally available as a present price-responsive coefficient. This distinction lets the deference line ask about a present market's opinions over a later process while keeping explicit which admissibility and resource-separation assumptions are still owed.
Logical Induction supplies prices, expectations, self-trust phenomena, and no-exploitation constraints. It does not supply an action type, controller, authorization relation, practical authority, capability, or efficacy. Those are additional structures, not interpretations smuggled into a price.
Deference Done Better begins from epistemic modesty. An expert may be worth consulting without being certain of its own worthiness. Strong reflection can be too demanding, while weak reflection can count apparent deference to an anti-expert. Dorst, Levinstein, Salow, Husic, and Fitelson propose comparing the decisions made from the expert's opinions with decisions made from one's own. See Sources.
The repository inherits that target shape rather than a finished theorem: connect epistemic deference to a decision comparison, then ask when a bounded process may rationally use a later or better-informed process. Total Trust, Value, and tower-style expectations are candidate mathematical faces of the connection.
The current corpus audit retains a two-option finite exact identity connecting Value and Total Trust, and it keeps a soft asymptotic route as conditional source evidence. It treats varying-question results as strengthening the forward epistemic relation rather than creating a separate research line.
The audit also keeps distinctions that limit the claim. A hard-selector inference from a tower condition to Value fails on selection-referencing punishment menus. That does not refute the soft construction. Conversely, the workspace's vanishing-gap mixture and the source's fixed-margin hedge have not been shown to carry the same hypothesis package.
Open / unregistered research. The finite identities, soft route, and Logical-Induction-native forcing chain have not been promoted. Cross-process calibration, admissibility, world assumptions, and resource-indexed separation remain explicit debts.
Even a successful epistemic-deference theorem would not confer practical authority. A favorable prediction or decision comparison does not say who is authorized to act, who retains a corrective capability, or whether a demand is efficacious in a transition model.
The bridge to accountable claims. Logical Induction predicts; the learning layer
that allocates realized experiments among temporally extended continuations is
Continuation BRIA, which scores accountable claims on realized block
outcomes only. A deferential value prediction — the activated future evaluation of the
legitimate-deference stack, or an LI price of it — can potentially be the claim a
continuation hypothesis is held to, and if such claims are near-tight for the
continuation's realized value (the SLACK bridge) continuation competence becomes
competence against that value. This is an interface with a named open realization, not
a theorem; the two wealth accounts stay semantically distinct.
The Corrigibility nucleus uses one Logical-Induction theorem, at its
exact statement: Expectation Provability Induction. The corrigibilization inequality
between the activated securities of a raw continuation and its corrigibilized
counterpart, with the mediation discrepancy, the decline regret and the directional
activation mismatch as its explicit costs, compiles into a bounded combination of gated
logically uncertain variables whose generability certificate is constructed at the
pinned interface; if the architecture's specification makes that combination
nonpositive in every world consistent with the inductor's theory, the inductor's own
expectations respect it asymptotically — before any instance is proved, with no
calibration hypothesis, and uniformly over any polynomial-size efficiently generated
menu through a continuous near-argmax weighting, since a hard argmax is not an
expressible feature. Logical Induction contributes the passage from validity in every
world to the market's expectations and the uniformity; it contributes no rate, no
smallness of the costs, and nothing about non-settling quantities. Expectation
Unbiasedness from Feedback is a boundary statement: it applies only to comparisons the
theory determines — a sequenced-settlement pair with an explicit finite horizon — and
genuinely empirical logs need an oracle-relativized inductor, which the paper's
computable deductive process does not provide. The deliberative half uses the same theorem once more: the trace-steering package
supplies the compiled pair's validity verbatim, a gated family bounded in every
consistent world has expectation at most the bound (a degenerate pair fed to the same
compiled theorem, constants removed by single-variable Expectation Provability
Induction), and the chain through the discovered comparator adds, so the inductor
learns 𝔼ₙ(U_T) − 𝔼ₙ(U_full) ≲ₙ L·(α + β) with the service and discovery residuals
certified as computations on the docket and the declared hypothesis space
(li_steering_le, li_gated_le, li_noncapture, li_noncapture_chain). Register:
LI_TRANSFER.md,
COMPOSITION.md,
DISCOVERY_COMPOSITION.md,
LI_CORRIGIBILITY.md,
FEEDBACK_BOUNDARY.md.