  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.
