Betting on what is neither verifiable nor falsifiable

TL;DR

This work tackles the problem of designing prediction markets for sentences in First-Order Logic whose truth is not fixed by empirical verification. It introduces a verification-falsification (VF) game-based market that leverages constructive truth notions to price sentences expressible in the arithmetical hierarchy, beyond simple $ extit{Δ}_0$ cases. The authors prove inexploitability and convergence results and establish a constructive-truth correspondence: if a sentence is $reve{oldsymbol{A}}_s$-true, the market price limit tends to 1, and if it is false, the limit tends to 0 (via handling of $ eg P$). While the limit is not a standard probability distribution, the framework offers a principled approach to logical uncertainty and suggests avenues for latent-space betting and theory-strength assessment, with implications for logic, philosophy, and practical market design.

Abstract

Prediction markets are useful for estimating probabilities of claims whose truth will be revealed at some fixed time -- this includes questions about the values of real-world events (i.e. statistical uncertainty), and questions about the values of primitive recursive functions (i.e. logical or algorithmic uncertainty). However, they cannot be directly applied to questions without a fixed resolution criterion, and real-world applications of prediction markets to such questions often amount to predicting not whether a sentence is true, but whether it will be proven. Such questions could be represented by countable unions or intersections of more basic events, or as First-Order-Logic sentences on the Arithmetical Hierarchy (or even beyond FOL, as hyperarithmetical sentences). In this paper, we propose an approach to betting on such events via options, or equivalently as bets on the outcome of a "verification-falsification game". Our work thus acts as an alternative to the existing framework of Garrabrant induction for logical uncertainty, and relates to the stance known as constructivism in the philosophy of mathematics; furthermore it has broader implications for philosophy and mathematical logic.

Figures (3)

• Figure 1: The "arithmetical hierarchy" of FOL sentences. A $\Sigma_{n+1}$ sentence is of the form $\exists x,p(x)$ where $p$ is $\Pi_n$; a $\Pi_{n+1}$ sentence is of the form $\forall x,p(x)$ where $p$ is $\Sigma_n$. In logic, the lowest level of the arithmetical hierarchy $\Delta_0=\Sigma_0=\Pi_0$ are sentences of the form $f(n)=0$ where $f$ is a primitive recursive function, but this formalism may be extended to empirical truths that will be revealed at a fixed time.
• Figure 2: Shading $P(x,y)$ as a checkerboard, the $\Sigma_2$ sentence $\exists x,\forall y, P(x,y)$ can be interpreted as "there is an infinite black column". Left: an arbitrary example; Right: the example of $P(x,y):=x\ge y$, where the $\Sigma_2$ sentence is false, yet it is true for every "finite window".
• Figure 3: Illustration of $\varpi$'s player countering $\mu$

Theorems & Definitions (20)

• Definition 1.1: Worlds and valuations
• Definition 1.2: PC worlds
• Definition 1.3: Garrabrant induction
• Theorem 1.1: Inexploitability
• Lemma 1.2: the problem is not trivial
• proof
• Definition 2.1: Verification-Falsification game
• Definition 2.2: Prediction Market for VF games
• Definition 3.1: Exploitation
• Lemma 3.1: Inexploitabity