Logical Inductors as Proof Search
Logical Inductors rely on a robust interplay between markets and individual traders betting on the eventual output of logical computations, to develop accurate beliefs identifying features long ahead of a standard deductive process. Interestingly, inductors also identify constraints-between / properties-about logical variables (ex: “is the asymptotic distribution of primes n/log(n)?”) before concrete statements (ex: ”is this particular large X prime?”). This decomposition of a difficult statement into the total of (entropically) smaller properties is reminiscent of a yoneda embedding. This is in stark contrast with most proof search, which works towards (or backwards from) a specific goal proposition.
Meanwhile, polarized linear logic has a family of proof-net-search methods operating dually on both potentially-provable propositions and potentially-refutable properties. Such methods describe a concurrent deductive phase analogous to individual traders, alongside a synchronous resolution phase analogous to the market maker determining fair prices for the entirety of the remaining market.
I suspect there is a generalization of logical induction which amounts to a proof search in a substructural logic, and which may handle both logical (trader-level) and empirical (market-level) uncertainty, by embedding empirical properties of the market into logical propositions embodied by a market maker. Regardless of the exact form, reinterpreting logical induction as a proof search would fortify its epistemic motivation, improve reflective capabilities, and pave the way for an efficient implementation of logical induction.
The main high-level questions I see are as follows:
-
what’s the strongest generalization of a trader, and of a market/market-maker?
-
what’s the most natural type of “belief’ for each to work on?
-
what formal claims can we make about the “knowledge” held by the market, which cannot be explicitly encoded as individual efficient traders - ie. what is the natural logic of markets, as distinct from the base logic of traders?