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 indiv