Theory Arbitrage_Probability_Correspondence
section ‹Introduction›
theory Arbitrage_Probability_Correspondence
imports
"Probability_Inequality_Completeness.Probability_Inequality_Completeness"
"HOL.Real"
begin
subsection ‹Motivation›
text ‹
Consider a ∗‹fixed-odds gambling market› where participants trade bets on arbitrary
logical propositions.
In this setting, every bet pays out exactly ‹$1› if the proposition is true and ‹$0›
otherwise. Unlike traditional prediction markets like ∗‹PredictIt› or ∗‹Polymarket›,
which usually limit trading to mutually exclusive outcomes, we assume a market that
allows bets on any combination of logical operators: ‹AND› (‹⊓›), ‹OR› (‹⊔›), and
‹NOT› (‹∼›).
To understand the relationship between market liquidity and probability logic, imagine
two events:
▪ ‹A :: "The NASDAQ will go up 1% by Friday"›
▪ ‹B :: "The S&P500 will go up 1% by Friday"›
Suppose the market order book contains the following quotes:
▪ ‹ASK› for ‹A› at ‹$0.40› (Someone is selling/offering a bet on ‹A›).
▪ ‹ASK› for ‹B› at ‹$0.50› (Someone is selling/offering a bet on ‹B›).
▪ ‹BID› for ‹A ⊓ B› at ‹$0.30› (Someone wants to buy a bet on ‹A AND B›).
▪ ‹BID› for ‹A ⊔ B› at ‹$0.70› (Someone wants to buy a bet on ‹A OR B›).
An arbitrageur can exploit these prices to guarantee a risk-free profit.
They act as a ∗‹market taker› for the ‹ASK›s (buying ‹A› and ‹B›) and as a
∗‹market maker› for the BIDs (selling ‹A AND B› and ‹A OR B›).
The initial cash flow is positive:
‹Profit = (BID(A ⊓ B) + BID(A ⊔ B)) - (ASK(A) + ASK(B))›
‹Profit = ($0.30 + $0.70) - ($0.40 + $0.50) = $1.00 - $0.90 = $0.10›
Crucially, this profit is safe regardless of the outcome. The arbitrageur holds long
positions in ‹A› and ‹B›, and short positions in ‹A ⊓ B› and ‹A ⊔ B›.
▪ If both rise (True, True): The arbitrageur wins ‹$2› on longs, pays ‹$2› on shorts.
Net: ‹$0› payout.
▪ If only one rises (True, False): The arbitrageur wins ‹$1› on longs, pays ‹$1› on
short (the ‹OR› bet). Net: ‹$0› payout.
▪ If neither rises (False, False): The arbitrageur wins ‹$0›, pay ‹$0›.
Net: ‹$0› payout.
The arbitrage exists because the market prices violate the probability identity:
‹Pr(A) + Pr(B) = Pr(A ⊓ B) + Pr(A ⊔ B)›
The central result of this work generalizes this intuition:
∗‹Every arbitrage opportunity corresponds to a probability inequality identity.›
›
subsection ‹Overview of Results›
text ‹
The central result of this work is as follows:
∗‹Proving a strategy will always yield a profit (if completely matched) in a
fixed-odds gambling market over arbitrary logical propositions corresponds to
proving an inequality identity in probability logic, and also corresponds to a
bounded MaxSAT problem.›
Such strategies are referred to as ∗‹arbitrage strategies›.
We also consider the ∗‹dual› problem of identifying if a trading strategy will never
make a profit. Strategies that will never logically yield a profit are called
∗‹incoherent›.
›
subsection ‹Prior Work›
text ‹
Two results that appear to be related at first glance are ∗‹The Fundamental Theorem(s)
of Asset Pricing› (FTAP) \<^cite>‹varianArbitragePrincipleFinancial1987› and the
∗‹Dutch Book Theorem› \<^cite>‹definettiSuiPassaggiLimite1930 and
kemenyFairBetsInductive1955 and lehmanConfirmationRationalBetting1955 and
ramseyChapterTruthProbability1931›. While the connection to FTAP is purely
superficial, the results are close in spirit to the Dutch Book tradition: we study
when a collection of fixed-odds commitments can be combined into a strategy that is
guaranteed to lose (or, dually, guaranteed to profit), and we treat such strategies
as computational objects.
The Fundamental Theorems of Asset Pricing (FTAP) connect a suitable notion of
∗‹no-arbitrage› to the existence of a pricing functional (or, in stochastic
settings, an equivalent martingale measure) in an idealized, frictionless market. In
their classical formulations, the objects being priced are standard financial assets
(e.g., securities or commodities) represented by a spot price or a price process,
and the market model abstracts away from microstructure: order placement, order
matching, bid/ask discreteness, and fixed-odds quoting are not part of the primitive
data. By contrast, we work directly with fixed-odds markets for wagers on arbitrary
logical propositions, where the microstructure of how orders compose into strategies
is central, and we connect ``no-arbitage'' strategies to the existence of some
scenario where the strategy doesn't always lose, which falls out of a certain
bounded MaxSAT calculation.
The Dutch Book literature shares more of our vocabulary. Philosophical treatments
emphasize ∗‹coherence› and the avoidance of a ∗‹bad book›: a collection of
bets that guarantees a loss. Following H\'ajek's terminology
\<^cite>‹hajekScotchingDutchBooks2005›, one may also speak of ∗‹good books›. In this
development, we adopt finance-oriented language and refer to these objects as
(loss-guaranteeing) ∗‹arbitrage strategies›, because they are assembled from posted
odds and executed mechanically once the relevant orders are matched. We also work with
possibility-style representations in the spirit of Lehman, generalized to any instance
of a \<^class>‹classical_logic›.
Our main contribution is not a normative thesis that rational agents ought to
conform their degrees of belief to probability theory. Instead, we make explicit a
three-way correspondence between:
▸ checking whether a bounded family of fixed-odds commitments is coherent (i.e.,
not loss-guaranteeing),
▸ feasibility of a bounded MaxSAT instance derived from the same commitments, and
▸ certain inequalities that hold for all probability functions over the same set
of propositions.
Operationally, we only require the first criterion: there must exist a scenario in
which the strategy does not always lose. The MaxSAT formulation supplies a concrete
decision procedure, and the coNP-hardness of the resulting feasibility questions
explains why coherence checking is not a task one should expect to perform reliably by
hand.
We also study the ∗‹dual› problem: identifying strategies that are pure
arbitrages (guaranteed nonnegative payoff with strictly positive payoff in some
outcome). Such strategies are useful not merely as pathologies, but as mechanisms
for creating market depth. Intuitively, they can match ‹BID› interest in one venue
with ‹ASK› interest in another, improving execution for multiple participants.
From a microeconomic perspective, this can increase surplus by enabling trades that
would otherwise fail to clear.
›
section ‹Fixed Odds Markets›
notation Probability_Inequality_Completeness.relative_maximals (‹ℳ›)
unbundle no funcset_syntax
subsection ‹Orders and Trading Strategies›
text ‹
In this section, we model a ∗‹fixed odds market› where each bet pays out ‹$0› or ‹$1›,
and people make and take bets. For simplicity, we consider ‹BID› and ‹ASK› limit
orders of a single unit (i.e., trades such that if they match, then they are
completely cleared). In an ordinary central limit order book, such ‹BID› and ‹ASK›
orders would have prices in the interval ‹(0,1)›, but we do not make use of this
assumption in our proofs, as it is not necessary.
›
record 'p bet_offer =
bet :: 'p
price :: real
text ‹
A trading strategy is a collection of ‹BID› and ‹ASK› orders that are to be matched
atomically.
∗‹Making› a bet is when you ∗‹ask› a bet on the market, while ∗‹taking› a bet is when
you ∗‹bid› a bet on the market.
A ∗‹market maker› is one who puts up capital and asks bets, while a ∗‹market taker› is
one who bids bets.
In a trading strategy, the market participant acts as a market maker for the ‹ASK›
orders they are willing make and as a market taker for the ‹BID› orders they are
willing to make.
›
record 'p strategy =
asks :: "('p bet_offer) list"
bids :: "('p bet_offer) list"
subsection ‹Possibility Functions›
text ‹
Possibility functions are states of affairs that determine the outcomes of bets.
They were first used in Lehman's formulation of the Dutch Book Theorem
\<^cite>‹lehmanConfirmationRationalBetting1955›. Our approach diverges from Lehman's.
Lehman uses linear programming to prove his result. Our formulation is pure
probability logic.
›
text ‹
We give our definition of a possibility function as follows:
›
definition (in classical_logic) possibility :: "('a ⇒ bool) ⇒ bool" where
[simp]: "possibility p ≡
¬ (p ⊥)
∧ (∀ φ. ⊢ φ ⟶ p φ)
∧ (∀ φ ψ . p (φ → ψ) ⟶ p φ ⟶ p ψ)
∧ (∀ φ . p φ ∨ p (∼ φ))"
text ‹
Our formulation of possibility functions generalizes Lehman's. Lehman restricts his
definition to the language of classical propositional logic formulae. We define ours
over any arbitrary classical logic satisfying the axioms of the \<^class>‹classical_logic›
class.
›
definition (in classical_logic) possibilities :: "('a ⇒ bool) set" where
[simp]: "possibilities = {p. possibility p}"
lemma (in classical_logic) possibility_negation:
assumes "possibility p"
shows "p (φ → ⊥) = (¬ p φ)"
proof
assume "p (φ → ⊥)"
show "¬ p φ"
proof
assume "p φ"
have "⊢ φ → (φ → ⊥) → ⊥"
by (simp add: double_negation_converse)
hence "p ((φ → ⊥) → ⊥)"
using ‹p φ› ‹possibility p› by auto
thus "False" using ‹p (φ → ⊥)› ‹possibility p› by auto
qed
next
show "¬ p φ ⟹ p (φ → ⊥)"
using ‹possibility p› negation_def by fastforce
qed
lemma (in classical_logic) possibilities_logical_closure:
assumes "possibility p"
and "{x. p x} ⊩ φ"
shows "p φ"
proof -
{
fix Γ
assume "set Γ ⊆ Collect p"
hence "∀ φ. Γ :⊢ φ ⟶ p φ"
proof (induct Γ)
case Nil
have "∀φ. ⊢ φ ⟶ p φ"
using ‹possibility p› by auto
then show ?case
using list_deduction_base_theory by blast
next
case (Cons γ Γ)
hence "p γ"
by simp
have "∀ φ. Γ :⊢ γ → φ ⟶ p (γ → φ)"
using Cons.hyps Cons.prems by auto
then show ?case
by (meson
‹p γ›
‹possibility p›
list_deduction_theorem
possibility_def)
qed
}
thus ?thesis
using ‹Collect p ⊩ φ› set_deduction_def by auto
qed
text ‹
The next two lemmas establish that possibility functions are equivalent to maximally
consistent sets.
›
lemma (in classical_logic) possibilities_are_MCS:
assumes "possibility p"
shows "MCS {x. p x}"
using assms
by (metis
(mono_tags, lifting)
formula_consistent_def
formula_maximally_consistent_set_def_def
maximally_consistent_set_def
possibilities_logical_closure
possibility_def
mem_Collect_eq
negation_def)
lemma (in classical_logic) MCSs_are_possibilities:
assumes "MCS s"
shows "possibility (λ x. x ∈ s)"
proof -
have "⊥ ∉ s"
using ‹MCS s›
formula_consistent_def
formula_maximally_consistent_set_def_def
maximally_consistent_set_def
set_deduction_reflection
by blast
moreover have "∀ φ. ⊢ φ ⟶ φ ∈ s"
using ‹MCS s›
formula_maximally_consistent_set_def_reflection
maximally_consistent_set_def
set_deduction_weaken
by blast
moreover have "∀ φ ψ. (φ → ψ) ∈ s ⟶ φ ∈ s ⟶ ψ ∈ s"
using ‹MCS s›
formula_maximal_consistency
formula_maximally_consistent_set_def_implication
by blast
moreover have "∀ φ. φ ∈ s ∨ (φ → ⊥) ∈ s"
using assms
formula_maximally_consistent_set_def_implication
maximally_consistent_set_def
by blast
ultimately show ?thesis by (simp add: negation_def)
qed
subsection ‹Payoff Functions›
text ‹
Given a market strategy and a possibility function, we can define the ∗‹payoff› of
that strategy if all the bet positions in that strategy were matched and settled at
the particular state of affairs given by the possibility function.
Recall that in a trading strategy, we act as a market ∗‹maker› for ask positions,
meaning we payout if the proposition behind the bet we are asking evaluates to
∗‹true›.
Payoff is revenue from won bets minus costs of the ‹BID›s for those bets, plus revenue
from sold ‹ASK› bets minus payouts from bets lost.
›
definition payoff :: "('p ⇒ bool) ⇒ 'p strategy ⇒ real" ("π") where
[simp]: "π s strategy ≡
(∑ i ← bids strategy. (if s (bet i) then 1 else 0) - price i)
+ (∑ i ← asks strategy. price i - (if s (bet i) then 1 else 0))"
text ‹
Alternate definitions of the payout function \<^term>‹π› are to use the notion of
∗‹settling› bets given a state of affairs. Settling is just paying out those bets that
came true.
›
definition settle_bet :: "('p ⇒ bool) ⇒ 'p ⇒ real" where
"settle_bet s φ ≡ if (s φ) then 1 else 0"
lemma payoff_alt_def1:
"π s strategy =
(∑ i ← bids strategy. settle_bet s (bet i) - price i)
+ (∑ i ← asks strategy. price i - settle_bet s (bet i))"
unfolding settle_bet_def
by simp
definition settle :: "('p ⇒ bool) ⇒ 'p bet_offer list ⇒ real" where
"settle s bets ≡ ∑ b ← bets. settle_bet s (bet b)"
lemma settle_alt_def:
"settle q bets = length [φ ← [ bet b . b ← bets ] . q φ]"
unfolding settle_def settle_bet_def
by (induct bets, simp+)
definition total_price :: "('p bet_offer) list ⇒ real" where
"total_price offers ≡ ∑ i ← offers. price i"
lemma payoff_alt_def2:
"π s strategy = settle s (bids strategy)
- settle s (asks strategy)
+ total_price (asks strategy)
- total_price (bids strategy)"
unfolding payoff_alt_def1 total_price_def settle_def
by (simp add: sum_list_subtractf)
subsection ‹Revenue Equivalence›
text ‹
When evaluating a payout function, we can essentially convert ‹BID› orders to ‹ASK›
orders in a strategy, provided we properly account for locked capital when
calculating the effective prices for the new ‹ASK› positions.
›
definition (in classical_logic) negate_bets ("_⇧∼") where
"bets⇧∼ = [b ⦇ bet := ∼ (bet b) ⦈. b ← bets]"
lemma (in classical_logic) ask_revenue_equivalence:
assumes "possibility p"
shows " π p ⦇ asks = asks', bids = bids' ⦈
= - settle p (bids'⇧∼ @ asks')
+ total_price asks'
+ length bids'
- total_price bids'"
proof (induct bids')
case Nil
then show ?case
unfolding
payoff_alt_def2
negate_bets_def
total_price_def
settle_def
by simp
next
case (Cons bid' bids')
have "p (∼ (bet bid')) = (¬ (p (bet bid')))"
using assms negation_def by auto
moreover have
"total_price ((bid' # bids') @ asks')
= price bid' + total_price bids' + total_price asks'"
unfolding total_price_def
by (induct asks', induct bids', auto)
ultimately show ?case
using Cons
unfolding payoff_alt_def2 negate_bets_def settle_def settle_bet_def
by simp
qed
text ‹
The dual is also true: when evaluating a payout function, we can, in a sense, treat
‹ASK› as ‹BID› positions with proper accounting.
›
lemma (in classical_logic) bid_revenue_equivalence:
assumes "possibility p"
shows " π p ⦇ asks = asks', bids = bids' ⦈
= settle p (asks'⇧∼ @ bids')
+ total_price asks'
- total_price bids'
- length asks'"
proof (induct asks')
case Nil
then show ?case
unfolding
payoff_alt_def2
negate_bets_def
total_price_def
settle_def
settle_bet_def
by simp
next
case (Cons s asks')
have "p (∼ (bet s)) = (¬ (p (bet s)))" using assms negation_def by auto
moreover have " total_price ((s # asks') @ bids')
= price s + total_price asks' + total_price bids'"
unfolding total_price_def
by (induct bids', induct asks', auto)
ultimately show ?case
using Cons
unfolding payoff_alt_def2 negate_bets_def settle_def settle_bet_def
by simp
qed
section ‹Arbitrage Strategies›
subsection ‹Introduction›
text ‹
In this section, we consider the problem of computing whether a strategy will always
yield a profit. Such strategies are referred to as ∗‹arbitrage strategies›.
›
subsection ‹Minimum Payoff›
text ‹
When computing whether a strategy is suited to arbitrage trading, we need to know the
∗‹minimum payoff› of that strategy given every possible scenario.
›
definition (in consistent_classical_logic)
minimum_payoff :: "'a strategy ⇒ real" ("π⇩m⇩i⇩n") where
"π⇩m⇩i⇩n b ≡ THE x. (∃ p ∈ possibilities. π p b = x)
∧ (∀ q ∈ possibilities. x ≤ π q b)"
text ‹
Since our definition of \<^term>‹π⇩m⇩i⇩n› relies on a definite descriptor, we need the
following theorem to prove it is well-defined.
›
lemma (in consistent_classical_logic) minimum_payoff_existence:
"∃! x. (∃ p ∈ possibilities. π p bets = x) ∧ (∀ q ∈ possibilities. x ≤ π q bets)"
proof (rule ex_ex1I)
show "∃x. (∃p∈possibilities. π p bets = x) ∧ (∀q∈possibilities. x ≤ π q bets)"
proof (rule ccontr)
obtain bids' asks' where "bets = ⦇ asks = asks', bids = bids' ⦈"
by (metis strategy.cases)
assume "∄x. (∃ p ∈ possibilities. π p bets = x) ∧ (∀ q ∈ possibilities. x ≤ π q bets)"
hence "∀x. (∃ p ∈ possibilities. π p bets = x) ⟶ (∃ q ∈ possibilities. π q bets < x)"
by (meson le_less_linear)
hence ⋆: "∀p ∈ possibilities. ∃ q ∈ possibilities. π q bets < π p bets"
by blast
have ◊: "∀ p ∈ possibilities. ∃ q ∈ possibilities.
settle q (asks'⇧∼ @ bids') < settle p (asks'⇧∼ @ bids')"
proof
fix p
assume "p ∈ possibilities"
from this obtain q where "q ∈ possibilities" and "π q bets < π p bets"
using ⋆ by blast
hence
" settle q (asks'⇧∼ @ bids')
+ total_price asks'
- total_price bids'
- length asks'
< settle p (asks'⇧∼ @ bids')
+ total_price asks'
- total_price bids'
- length asks'"
by (metis ‹π q bets < π p bets›
‹bets = ⦇asks = asks', bids = bids'⦈›
‹p ∈ possibilities›
possibilities_def
bid_revenue_equivalence
mem_Collect_eq)
hence "settle q (asks'⇧∼ @ bids') < settle p (asks'⇧∼ @ bids')"
by simp
thus "∃q∈possibilities. settle q (asks'⇧∼ @ bids') < settle p (asks'⇧∼ @ bids')"
using ‹q ∈ possibilities› by blast
qed
{
fix bets :: "('a bet_offer) list"
fix s :: "'a ⇒ bool"
have "∃ n ∈ ℕ. settle s bets = real n"
unfolding settle_def settle_bet_def
by (induct bets, auto, metis Nats_1 Nats_add Suc_eq_plus1_left of_nat_Suc)
} note † = this
{
fix n :: "nat"
have " (∃ p ∈ possibilities. settle p (asks'⇧∼ @ bids') ≤ n)
⟶ (∃ q ∈ possibilities. settle q (asks'⇧∼ @ bids') < 0)"
(is "_ ⟶ ?consequent")
proof (induct n)
case 0
{
fix p :: "'a ⇒ bool"
assume "p ∈ possibilities" and "settle p (asks'⇧∼ @ bids') ≤ 0"
from this obtain q where
"q ∈ possibilities"
"settle q (asks'⇧∼ @ bids') < settle p (asks'⇧∼ @ bids')"
using ◊ by blast
hence ?consequent
by (metis
†
‹settle p (asks'⇧∼ @ bids') ≤ 0›
of_nat_0_eq_iff
of_nat_le_0_iff)
}
then show ?case by auto
next
case (Suc n)
{
fix p :: "'a ⇒ bool"
assume"p ∈ possibilities" and "settle p (asks'⇧∼ @ bids') ≤ Suc n"
from this obtain q⇩1 where
"q⇩1 ∈ possibilities"
"settle q⇩1 (asks'⇧∼ @ bids') < Suc n"
by (metis ◊ antisym_conv not_less)
from this obtain q⇩2 where
"q⇩2 ∈ possibilities"
"settle q⇩2 (asks'⇧∼ @ bids') < n"
using ◊
by (metis
†
add.commute
nat_le_real_less
nat_less_le
of_nat_Suc
of_nat_less_iff)
hence ?consequent
by (metis † Suc.hyps nat_less_le of_nat_le_iff of_nat_less_iff)
}
then show ?case by auto
qed
}
hence "∄ p. p ∈ possibilities"
by (metis † not_less0 of_nat_0 of_nat_less_iff order_refl)
moreover
have "¬ {} ⊩ ⊥"
using consistency set_deduction_base_theory by auto
from this obtain Γ where "MCS Γ"
by (meson formula_consistent_def
formula_maximal_consistency
formula_maximally_consistent_extension)
hence "(λ γ. γ ∈ Γ) ∈ possibilities"
using MCSs_are_possibilities possibilities_def by blast
ultimately show False
by blast
qed
next
fix x y
assume A: "(∃p ∈ possibilities. π p bets = x) ∧ (∀q ∈ possibilities. x ≤ π q bets)"
and B: "(∃p ∈ possibilities. π p bets = y) ∧ (∀q ∈ possibilities. y ≤ π q bets)"
from this obtain p⇩x p⇩y where
"p⇩x ∈ possibilities"
"p⇩y ∈ possibilities"
"π p⇩x bets = x"
"π p⇩y bets = y"
by blast
with A B have "x ≤ y" "y ≤ x"
by blast+
thus "x = y" by linarith
qed
subsection ‹Bounding Minimum Payoffs Below Using MaxSAT›
text ‹
Below, we present our second major theorem: computing a lower bound to a strategy's
minimum payoff is equivalent to checking a bounded MaxSAT problem.
A concrete implementation of this algorithm would enable software search for trading
strategies that can convert orders from one central limit order book to another.
As in the previous section, we prove our theorem in the general case of an arbitrary
‹k›, but in practice users will want to set ‹k = 0› to check if their strategy is an
arbitrage strategy.
›
theorem (in consistent_classical_logic) arbitrageur_maxsat:
" ((k :: real) ≤ π⇩m⇩i⇩n ⦇ asks = asks', bids = bids' ⦈)
= ( MaxSAT [bet b . b ← bids'⇧∼ @ asks']
≤ total_price asks' + length bids' - total_price bids' - k )"
(is "(k ≤ π⇩m⇩i⇩n ?bets) = (MaxSAT ?props ≤ total_price _ + _ - _ - _)")
proof
assume "k ≤ π⇩m⇩i⇩n ?bets"
let ?P = "λ x . (∃ p ∈ possibilities. π p ?bets = x)
∧ (∀ q ∈ possibilities. x ≤ π q ?bets)"
obtain p where
"possibility p" and
"∀ q ∈ possibilities. π p ?bets ≤ π q ?bets"
using ‹k ≤ π⇩m⇩i⇩n ?bets›
minimum_payoff_existence [of ?bets]
by (metis possibilities_def mem_Collect_eq)
hence "?P (π p ?bets)"
using possibilities_def by blast
hence "π⇩m⇩i⇩n ?bets = π p ?bets"
unfolding minimum_payoff_def
using minimum_payoff_existence [of ?bets]
the1_equality [where P = ?P and a = "π p ?bets"]
by blast
let ?Φ = "[φ ← ?props. p φ]"
have "mset ?Φ ⊆# mset ?props"
by(induct ?props,
auto,
simp add: subset_mset.add_mono)
moreover
have "¬ (?Φ :⊢ ⊥)"
proof -
have "set ?Φ ⊆ {x. p x}"
by auto
hence "¬ (set ?Φ ⊩ ⊥)"
by (meson ‹possibility p›
possibilities_are_MCS [of p]
formula_consistent_def
formula_maximally_consistent_set_def_def
maximally_consistent_set_def
list_deduction_monotonic
set_deduction_def)
thus ?thesis
using set_deduction_def by blast
qed
moreover
{
fix Ψ
assume "mset Ψ ⊆# mset ?props" and "¬ Ψ :⊢ ⊥"
from this obtain Ω⇩Ψ where "MCS Ω⇩Ψ" and "set Ψ ⊆ Ω⇩Ψ"
by (meson formula_consistent_def
formula_maximal_consistency
formula_maximally_consistent_extension
list_deduction_monotonic
set_deduction_def)
let ?q = "λφ . φ ∈ Ω⇩Ψ"
have "possibility ?q"
using ‹MCS Ω⇩Ψ› MCSs_are_possibilities by blast
hence "π p ?bets ≤ π ?q ?bets"
using ‹∀q∈possibilities. π p ?bets ≤ π q ?bets›
possibilities_def
by blast
let ?c = "total_price asks' + length bids' - total_price bids'"
have "- settle p (bids'⇧∼ @ asks') + ?c ≤ - settle ?q (bids'⇧∼ @ asks') + ?c"
using ‹π p ?bets ≤ π ?q ?bets›
‹possibility p›
ask_revenue_equivalence [of p asks' bids']
‹possibility ?q›
ask_revenue_equivalence [of ?q asks' bids']
by linarith
hence "settle ?q (bids'⇧∼ @ asks') ≤ settle p (bids'⇧∼ @ asks')"
by linarith
let ?Ψ' = "[φ ← ?props. ?q φ]"
have "length ?Ψ' ≤ length ?Φ"
using ‹settle ?q (bids'⇧∼ @ asks') ≤ settle p (bids'⇧∼ @ asks')›
unfolding settle_alt_def
by simp
moreover
have "length Ψ ≤ length ?Ψ'"
proof -
have "mset [ψ ← Ψ. ?q ψ] ⊆# mset ?Ψ'"
proof -
{
fix props :: "'a list"
have "∀ Ψ. ∀ Ω. mset Ψ ⊆# mset props ⟶
mset [ψ ← Ψ. ψ ∈ Ω] ⊆# mset [φ ← props. φ ∈ Ω]"
by (simp add: multiset_filter_mono)
}
thus ?thesis
using ‹mset Ψ ⊆# mset ?props› by blast
qed
hence "length [ψ ← Ψ. ?q ψ] ≤ length ?Ψ'"
by (metis (no_types, lifting) length_sub_mset mset_eq_length nat_less_le not_le)
moreover have "length Ψ = length [ψ ← Ψ. ?q ψ]"
using ‹set Ψ ⊆ Ω⇩Ψ›
by (induct Ψ, simp+)
ultimately show ?thesis by linarith
qed
ultimately have "length Ψ ≤ length ?Φ" by linarith
}
ultimately have "?Φ ∈ ℳ ?props ⊥"
unfolding relative_maximals_def
by blast
hence "MaxSAT ?props = length ?Φ"
using relative_MaxSAT_intro by presburger
hence "MaxSAT ?props = settle p (bids'⇧∼ @ asks')"
unfolding settle_alt_def
by simp
thus "MaxSAT ?props ≤ total_price asks' + length bids' - total_price bids' - k"
using ask_revenue_equivalence [of p asks' bids']
‹k ≤ π⇩m⇩i⇩n ?bets›
‹π⇩m⇩i⇩n ?bets = π p ?bets›
‹possibility p›
by linarith
next
let ?c = "total_price asks' + length bids' - total_price bids'"
assume "MaxSAT ?props ≤ total_price asks' + length bids' - total_price bids' - k"
from this obtain Φ where "Φ ∈ ℳ ?props ⊥" and "length Φ + k ≤ ?c"
using
consistency
relative_MaxSAT_intro
relative_maximals_existence
by fastforce
hence "¬ Φ :⊢ ⊥"
using relative_maximals_def by blast
from this obtain Ω⇩Φ where "MCS Ω⇩Φ" and "set Φ ⊆ Ω⇩Φ"
by (meson formula_consistent_def
formula_maximal_consistency
formula_maximally_consistent_extension
list_deduction_monotonic
set_deduction_def)
let ?p = "λφ . φ ∈ Ω⇩Φ"
have "possibility ?p"
using ‹MCS Ω⇩Φ› MCSs_are_possibilities by blast
have "mset Φ ⊆# mset ?props"
using ‹Φ ∈ ℳ ?props ⊥› relative_maximals_def by blast
have "mset Φ ⊆# mset [ b ← ?props. ?p b]"
by (metis ‹mset Φ ⊆# mset ?props›
‹set Φ ⊆ Ω⇩Φ›
filter_True
mset_filter
multiset_filter_mono
subset_code(1))
have "mset Φ = mset [ b ← ?props. ?p b]"
proof (rule ccontr)
assume "mset Φ ≠ mset [ b ← ?props. ?p b]"
hence "length Φ < length [ b ← ?props. ?p b]"
using
‹mset Φ ⊆# mset [ b ← ?props. ?p b]›
length_sub_mset not_less
by blast
moreover
have "¬ [ b ← ?props. ?p b] :⊢ ⊥"
by (metis
IntE
‹MCS Ω⇩Φ›
inter_set_filter
formula_consistent_def
formula_maximally_consistent_set_def_def
maximally_consistent_set_def
set_deduction_def
subsetI)
hence "length [ b ← ?props. ?p b] ≤ length Φ"
by (metis
(mono_tags, lifting)
‹Φ ∈ ℳ ?props ⊥›
relative_maximals_def [of ?props ⊥]
mem_Collect_eq
mset_filter
multiset_filter_subset)
ultimately show "False"
using not_le by blast
qed
hence "length Φ = settle ?p (bids'⇧∼ @ asks')"
unfolding settle_alt_def
using mset_eq_length
by metis
hence "k ≤ settle ?p (bids'⇧∼ @ asks')
+ total_price asks' + length bids' - total_price bids'"
using ‹length Φ + k ≤ ?c› by linarith
hence "k ≤ π ?p ?bets"
using ‹possibility ?p›
ask_revenue_equivalence [of ?p asks' bids']
‹length Φ + k ≤ ?c›
‹length Φ = settle ?p (bids'⇧∼ @ asks')›
by linarith
have "∀ q ∈ possibilities. π ?p ?bets ≤ π q ?bets"
proof
{
fix x :: 'a
fix P A
have "x ∈ Set.filter P A ⟷ x ∈ A ∧ P x"
by (simp add: filter_def)
}
note member_filter = this
fix q
assume "q ∈ possibilities"
hence "¬ [ b ← ?props. q b] :⊢ ⊥"
unfolding possibilities_def
by (metis filter_set
possibilities_logical_closure
possibility_def
set_deduction_def
mem_Collect_eq
member_filter
subsetI)
hence "length [ b ← ?props. q b] ≤ length Φ"
by (metis (mono_tags, lifting)
‹Φ ∈ ℳ ?props ⊥›
relative_maximals_def
mem_Collect_eq
mset_filter
multiset_filter_subset)
hence
" - settle ?p (bids'⇧∼ @ asks')
+ total_price asks'
+ length bids'
- total_price bids'
≤ - settle q (bids'⇧∼ @ asks')
+ total_price asks'
+ length bids'
- total_price bids'"
using ‹length Φ = settle ?p (bids'⇧∼ @ asks')›
settle_alt_def [of q "bids'⇧∼ @ asks'"]
by linarith
thus "π ?p ?bets ≤ π q ?bets"
using ask_revenue_equivalence [of ?p asks' bids']
ask_revenue_equivalence [of q asks' bids']
‹possibility ?p›
‹q ∈ possibilities›
unfolding possibilities_def
by (metis mem_Collect_eq)
qed
have "π⇩m⇩i⇩n ?bets = π ?p ?bets"
unfolding minimum_payoff_def
proof
show "(∃p∈possibilities. π p ?bets = π ?p ?bets)
∧ (∀q∈possibilities. π ?p ?bets ≤ π q ?bets)"
using ‹∀ q ∈ possibilities. π ?p ?bets ≤ π q ?bets›
‹possibility ?p›
unfolding possibilities_def
by blast
next
fix n
assume ⋆: "(∃p∈possibilities. π p ?bets = n) ∧ (∀q∈possibilities. n ≤ π q ?bets)"
from this obtain p where "π p ?bets = n" and "possibility p"
using possibilities_def by blast
hence "π p ?bets ≤ π ?p ?bets"
using ⋆ ‹possibility ?p›
unfolding possibilities_def
by blast
moreover have "π ?p ?bets ≤ π p ?bets"
using ‹∀ q ∈ possibilities. π ?p ?bets ≤ π q ?bets›
‹possibility p›
unfolding possibilities_def
by blast
ultimately show "n = π ?p ?bets" using ‹π p ?bets = n› by linarith
qed
thus "k ≤ π⇩m⇩i⇩n ?bets"
using ‹k ≤ π ?p ?bets›
by auto
qed
section ‹Coherence Checking›
subsection ‹Introduction›
text ‹
In this section, we give an abstract algorithm for traders to use to detect if a
strategy they want to employ will ∗‹always lose›, i.e., is ∗‹incoherent›.
›
subsection ‹Maximum Payoff›
text ‹
The key to figuring out if a trading strategy will not always lose is computing the
strategy's ∗‹maximum payoff›.
Below, we define the maximum payoff using a definite description.
›
definition (in consistent_classical_logic)
maximum_payoff :: "'a strategy ⇒ real" ("π⇩m⇩a⇩x") where
"π⇩m⇩a⇩x b ≡ THE x. (∃ p ∈ possibilities. π p b = x)
∧ (∀ q ∈ possibilities. π q b ≤ x)"
text ‹
The following lemma establishes that our definition of \<^term>‹π⇩m⇩a⇩x› is well-defined.
›
lemma (in consistent_classical_logic) maximum_payoff_existence:
"∃! x. (∃ p ∈ possibilities. π p bets = x)
∧ (∀ q ∈ possibilities. π q bets ≤ x)"
proof (rule ex_ex1I)
show "∃x. (∃ p ∈possibilities. π p bets = x)
∧ (∀ q ∈ possibilities. π q bets ≤ x)"
proof (rule ccontr)
obtain bids' asks' where "bets = ⦇ asks = asks', bids = bids' ⦈"
by (metis strategy.cases)
assume "∄x. (∃p∈possibilities. π p bets = x)
∧ (∀q∈possibilities. π q bets ≤ x)"
hence "∀x. (∃ p ∈ possibilities. π p bets = x)
⟶ (∃ q ∈ possibilities. x < π q bets)"
by (meson le_less_linear)
hence ⋆: "∀p ∈ possibilities. ∃ q ∈ possibilities. π p bets < π q bets"
by blast
have ◊: "∀ p ∈ possibilities. ∃ q ∈ possibilities.
settle p (asks'⇧∼ @ bids') < settle q (asks'⇧∼ @ bids')"
proof
fix p
assume "p ∈ possibilities"
from this obtain q where "q ∈ possibilities" and "π p bets < π q bets"
using ⋆ by blast
hence
" settle p (asks'⇧∼ @ bids')
+ total_price asks'
- total_price bids'
- length asks'
< settle q (asks'⇧∼ @ bids')
+ total_price asks'
- total_price bids'
- length asks'"
by (metis ‹π p bets < π q bets›
‹bets = ⦇asks = asks', bids = bids'⦈›
‹p ∈ possibilities›
possibilities_def
bid_revenue_equivalence
mem_Collect_eq)
hence "settle p (asks'⇧∼ @ bids') < settle q (asks'⇧∼ @ bids')"
by simp
thus "∃q∈possibilities. settle p (asks'⇧∼ @ bids')
< settle q (asks'⇧∼ @ bids')"
using ‹q ∈ possibilities› by blast
qed
{
fix bets :: "('a bet_offer) list"
fix s :: "'a ⇒ bool"
have "∃ n ∈ ℕ. settle s bets = real n"
unfolding settle_def settle_bet_def
by (induct bets,
auto,
metis
Nats_1
Nats_add
Suc_eq_plus1_left of_nat_Suc)
} note † = this
{
fix n :: "nat"
have "∃ q ∈ possibilities. n ≤ settle q (asks'⇧∼ @ bids')"
by (induct n,
metis
†
MCSs_are_possibilities
consistency
formula_consistent_def
formula_maximal_consistency
formula_maximally_consistent_extension
possibilities_def
set_deduction_base_theory
mem_Collect_eq
of_nat_0
of_nat_0_le_iff,
metis ◊ † le_antisym not_less not_less_eq_eq of_nat_less_iff)
}
moreover
{
fix bets :: "('a bet_offer) list"
fix s :: "'a ⇒ bool"
have "settle s bets ≤ length bets"
unfolding settle_def settle_bet_def
by (induct bets, auto)
}
ultimately show False
by (metis † not_less_eq_eq of_nat_le_iff)
qed
next
fix x y
assume A: "(∃p∈possibilities. π p bets = x) ∧ (∀q∈possibilities. π q bets ≤ x)"
and B: "(∃p∈possibilities. π p bets = y) ∧ (∀q∈possibilities. π q bets ≤ y)"
from this obtain p⇩x p⇩y where
"p⇩x ∈ possibilities"
"p⇩y ∈ possibilities"
"π p⇩x bets = x"
"π p⇩y bets = y"
by blast
with A B have "x ≤ y" "y ≤ x"
by blast+
thus "x = y" by linarith
qed
subsection ‹Bounding Maximum Payoffs Above Using MaxSAT›
text ‹
Below, we present our first major theorem: computing an upper bound to a strategy's
maximum payoff is equivalent to a bounded MaxSAT problem.
Given a software MaxSAT implementation, a trader can use this equivalence to run a
program to check whether the way they arrive at their strategies has a bug.
Note that while the theorem below is formulated using an arbitrary ‹k› constant, in
practice users will want to check their strategies are safe by using ‹k = 0›.
›
theorem (in consistent_classical_logic) coherence_maxsat:
" (π⇩m⇩a⇩x ⦇ asks = asks', bids = bids' ⦈ ≤ (k :: real))
= (MaxSAT [bet b . b ← asks'⇧∼ @ bids']
≤ k - total_price asks' + total_price bids' + length asks')"
(is "(π⇩m⇩a⇩x ?bets ≤ k) = (MaxSAT ?props ≤ _ - total_price _ + _ + _)")
proof
assume "π⇩m⇩a⇩x ?bets ≤ k"
let ?P = "λ x . (∃ p ∈ possibilities. π p ?bets = x)
∧ (∀ q ∈ possibilities. π q ?bets ≤ x)"
obtain p where
"possibility p" and
"∀ q ∈ possibilities. π q ?bets ≤ π p ?bets"
using ‹π⇩m⇩a⇩x ?bets ≤ k›
maximum_payoff_existence [of ?bets]
by (metis possibilities_def mem_Collect_eq)
hence "?P (π p ?bets)"
using possibilities_def by blast
hence "π⇩m⇩a⇩x ?bets = π p ?bets"
unfolding maximum_payoff_def
using maximum_payoff_existence [of ?bets]
the1_equality [where P = ?P and a = "π p ?bets"]
by blast
let ?Φ = "[φ ← ?props. p φ]"
have "mset ?Φ ⊆# mset ?props"
by(induct ?props,
auto,
simp add: subset_mset.add_mono)
moreover
have "¬ (?Φ :⊢ ⊥)"
proof -
have "set ?Φ ⊆ {x. p x}"
by auto
hence "¬ (set ?Φ ⊩ ⊥)"
by (meson
‹possibility p›
possibilities_are_MCS [of p]
formula_consistent_def
formula_maximally_consistent_set_def_def
maximally_consistent_set_def
list_deduction_monotonic
set_deduction_def)
thus ?thesis
using set_deduction_def by blast
qed
moreover
{
fix Ψ
assume "mset Ψ ⊆# mset ?props" and "¬ Ψ :⊢ ⊥"
from this obtain Ω⇩Ψ where "MCS Ω⇩Ψ" and "set Ψ ⊆ Ω⇩Ψ"
by (meson
formula_consistent_def
formula_maximal_consistency
formula_maximally_consistent_extension
list_deduction_monotonic
set_deduction_def)
let ?q = "λφ . φ ∈ Ω⇩Ψ"
have "possibility ?q"
using ‹MCS Ω⇩Ψ› MCSs_are_possibilities by blast
hence "π ?q ?bets ≤ π p ?bets"
using ‹∀q∈possibilities. π q ?bets ≤ π p ?bets›
possibilities_def
by blast
let ?c = "total_price asks' - total_price bids' - length asks'"
have "settle ?q (asks'⇧∼ @ bids') + ?c ≤ settle p (asks'⇧∼ @ bids') + ?c"
using ‹π ?q ?bets ≤ π p ?bets›
‹possibility p›
bid_revenue_equivalence [of p asks' bids']
‹possibility ?q›
bid_revenue_equivalence [of ?q asks' bids']
by linarith
hence "settle ?q (asks'⇧∼ @ bids') ≤ settle p (asks'⇧∼ @ bids')"
by linarith
let ?Ψ' = "[φ ← ?props. ?q φ]"
have "length ?Ψ' ≤ length ?Φ"
using ‹settle ?q (asks'⇧∼ @ bids') ≤ settle p (asks'⇧∼ @ bids')›
unfolding settle_alt_def
by simp
moreover
have "length Ψ ≤ length ?Ψ'"
proof -
have "mset [ψ ← Ψ. ?q ψ] ⊆# mset ?Ψ'"
proof -
{
fix props :: "'a list"
have "∀ Ψ. ∀ Ω.
mset Ψ ⊆# mset props
⟶ mset [ψ ← Ψ. ψ ∈ Ω] ⊆# mset [φ ← props. φ ∈ Ω]"
by (simp add: multiset_filter_mono)
}
thus ?thesis
using ‹mset Ψ ⊆# mset ?props› by blast
qed
hence "length [ψ ← Ψ. ?q ψ] ≤ length ?Ψ'"
by (metis
(no_types, lifting)
length_sub_mset
mset_eq_length
nat_less_le
not_le)
moreover have "length Ψ = length [ψ ← Ψ. ?q ψ]"
using ‹set Ψ ⊆ Ω⇩Ψ›
by (induct Ψ, simp+)
ultimately show ?thesis by linarith
qed
ultimately have "length Ψ ≤ length ?Φ" by linarith
}
ultimately have "?Φ ∈ ℳ ?props ⊥"
unfolding relative_maximals_def
by blast
hence "MaxSAT ?props = length ?Φ"
using relative_MaxSAT_intro by presburger
hence "MaxSAT ?props = settle p (asks'⇧∼ @ bids')"
unfolding settle_alt_def
by simp
thus "MaxSAT ?props
≤ k - total_price asks' + total_price bids' + length asks'"
using bid_revenue_equivalence [of p asks' bids']
‹π⇩m⇩a⇩x ?bets ≤ k›
‹π⇩m⇩a⇩x ?bets = π p ?bets›
‹possibility p›
by linarith
next
let ?c = "- total_price asks' + total_price bids' + length asks'"
assume "MaxSAT ?props
≤ k - total_price asks' + total_price bids' + length asks'"
from this obtain Φ where "Φ ∈ ℳ ?props ⊥" and "length Φ ≤ k + ?c"
using
consistency
relative_MaxSAT_intro
relative_maximals_existence
by fastforce
hence "¬ Φ :⊢ ⊥"
using relative_maximals_def by blast
from this obtain Ω⇩Φ where "MCS Ω⇩Φ" and "set Φ ⊆ Ω⇩Φ"
by (meson
formula_consistent_def
formula_maximal_consistency
formula_maximally_consistent_extension
list_deduction_monotonic
set_deduction_def)
let ?p = "λφ . φ ∈ Ω⇩Φ"
have "possibility ?p"
using ‹MCS Ω⇩Φ› MCSs_are_possibilities by blast
have "mset Φ ⊆# mset ?props"
using ‹Φ ∈ ℳ ?props ⊥› relative_maximals_def by blast
have "mset Φ ⊆# mset [ b ← ?props. ?p b]"
by (metis
‹mset Φ ⊆# mset ?props›
‹set Φ ⊆ Ω⇩Φ›
filter_True
mset_filter
multiset_filter_mono
subset_code(1))
have "mset Φ = mset [ b ← ?props. ?p b]"
proof (rule ccontr)
assume "mset Φ ≠ mset [ b ← ?props. ?p b]"
hence "length Φ < length [ b ← ?props. ?p b]"
using
‹mset Φ ⊆# mset [ b ← ?props. ?p b]›
length_sub_mset not_less
by blast
moreover
have "¬ [ b ← ?props. ?p b] :⊢ ⊥"
by (metis
IntE
‹MCS Ω⇩Φ›
inter_set_filter
formula_consistent_def
formula_maximally_consistent_set_def_def
maximally_consistent_set_def
set_deduction_def
subsetI)
hence "length [ b ← ?props. ?p b] ≤ length Φ"
by (metis
(mono_tags, lifting)
‹Φ ∈ ℳ ?props ⊥›
relative_maximals_def [of ?props ⊥]
mem_Collect_eq
mset_filter
multiset_filter_subset)
ultimately show "False"
using not_le by blast
qed
hence "length Φ = settle ?p (asks'⇧∼ @ bids')"
unfolding settle_alt_def
using mset_eq_length
by metis
hence "settle ?p (asks'⇧∼ @ bids') ≤ k + ?c"
using ‹length Φ ≤ k + ?c› by linarith
hence "π ?p ?bets ≤ k"
using ‹possibility ?p›
bid_revenue_equivalence [of ?p asks' bids']
‹length Φ ≤ k + ?c›
‹length Φ = settle ?p (asks'⇧∼ @ bids')›
by linarith
have "∀ q ∈ possibilities. π q ?bets ≤ π ?p ?bets"
proof
{
fix x :: 'a
fix P A
have "x ∈ Set.filter P A ⟷ x ∈ A ∧ P x"
by (simp add: filter_def)
}
note member_filter = this
fix q
assume "q ∈ possibilities"
hence "possibility q" unfolding possibilities_def by auto
hence "¬ [ b ← ?props. q b] :⊢ ⊥"
by (metis filter_set
possibilities_logical_closure
possibility_def
set_deduction_def
mem_Collect_eq
member_filter
subsetI)
hence "length [ b ← ?props. q b] ≤ length Φ"
by (metis (mono_tags, lifting)
‹Φ ∈ ℳ ?props ⊥›
relative_maximals_def
mem_Collect_eq
mset_filter
multiset_filter_subset)
hence "settle q (asks'⇧∼ @ bids') ≤ length Φ"
by (metis of_nat_le_iff settle_alt_def)
thus "π q ?bets ≤ π ?p ?bets"
using bid_revenue_equivalence [OF ‹possibility ?p›]
bid_revenue_equivalence [OF ‹possibility q›]
‹length Φ = settle ?p (asks'⇧∼ @ bids')›
by force
qed
have "π⇩m⇩a⇩x ?bets = π ?p ?bets"
unfolding maximum_payoff_def
proof
show "(∃p∈possibilities. π p ?bets = π ?p ?bets)
∧ (∀q∈possibilities. π q ?bets ≤ π ?p ?bets)"
using ‹∀ q ∈ possibilities. π q ?bets ≤ π ?p ?bets›
‹possibility ?p›
unfolding possibilities_def
by blast
next
fix n
assume ⋆: "(∃p∈possibilities. π p ?bets = n)
∧ (∀q∈possibilities. π q ?bets ≤ n)"
from this obtain p where "π p ?bets = n" and "possibility p"
using possibilities_def by blast
hence "π ?p ?bets ≤ π p ?bets"
using ⋆ ‹possibility ?p›
unfolding possibilities_def
by blast
moreover have "π p ?bets ≤ π ?p ?bets"
using ‹∀ q ∈ possibilities. π q ?bets ≤ π ?p ?bets›
‹possibility p›
unfolding possibilities_def
by blast
ultimately show "n = π ?p ?bets" using ‹π p ?bets = n› by linarith
qed
thus "π⇩m⇩a⇩x ?bets ≤ k"
using ‹π ?p ?bets ≤ k›
by auto
qed
section ‹Probability Inequality Identity Correspondence›
subsection ‹Introduction›
text ‹
In this section, we prove two forms of the probability inequality identity
correspondence theorem.
The two forms relate to \<^term>‹π⇩m⇩i⇩n› (i.e., arbitrage strategy determination) and
\<^term>‹π⇩m⇩a⇩x› (i.e., coherence testing).
In each case, the form follows from the reduction to bounded MaxSAT previously
presented, and the reduction of bounded MaxSAT to probability logic, we
established in
\<^theory>‹Probability_Inequality_Completeness.Probability_Inequality_Completeness›.
›
subsection ‹Arbitrage Strategies and Minimum Payoff›
text ‹
First, we connect checking if a strategy is an arbitrage strategy and probability
identities.
›
lemma (in consistent_classical_logic) arbitrageur_nonstrict_correspondence:
" (k ≤ π⇩m⇩i⇩n ⦇ asks = asks', bids = bids' ⦈)
= (∀ 𝒫 ∈ probabilities.
(∑b←asks'. 𝒫 (bet b)) + total_price bids' + k
≤ (∑s←bids'. 𝒫 (bet s)) + total_price asks')"
(is "?lhs = _")
proof -
let ?tot_bs = "total_price bids'" and ?tot_ss = "total_price asks'"
let ?c = "?tot_bs - ?tot_ss + k"
have "[bet b . b ← bids'⇧∼ @ asks'] = ❙∼ [bet s. s ← bids'] @ [bet b. b ← asks']"
(is "_ = ❙∼ ?bid_φs @ ?ask_φs")
unfolding negate_bets_def
by (induct bids', simp+)
hence
"?lhs = (∀ 𝒫 ∈ dirac_measures. (∑φ←?ask_φs. 𝒫 φ) + ?c ≤ (∑γ←?bid_φs. 𝒫 γ))"
using
dirac_inequality_equiv [of ?ask_φs ?c ?bid_φs]
arbitrageur_maxsat [of k asks' bids']
by force
moreover
{
fix 𝒫 :: "'a ⇒ real"
have "(∑φ←?ask_φs. 𝒫 φ) = (∑b←asks'. 𝒫 (bet b))"
"(∑γ←?bid_φs. 𝒫 γ) = (∑s←bids'. 𝒫 (bet s))"
by (simp add: comp_def)+
hence " ((∑φ←?ask_φs. 𝒫 φ) + ?c ≤ (∑γ←?bid_φs. 𝒫 γ))
= ( (∑b←asks'. 𝒫 (bet b)) + ?tot_bs + k
≤ (∑s←bids'. 𝒫 (bet s)) + ?tot_ss)"
by linarith
}
ultimately show ?thesis
by (meson dirac_measures_subset dirac_ceiling dirac_collapse subset_eq)
qed
lemma (in consistent_classical_logic) arbitrageur_strict_correspondence:
" (k < π⇩m⇩i⇩n ⦇ asks = asks', bids = bids' ⦈)
= (∀ 𝒫 ∈ probabilities.
(∑b←asks'. 𝒫 (bet b)) + total_price bids' + k
< (∑s←bids'. 𝒫 (bet s)) + total_price asks')"
(is "?lhs = ?rhs")
proof
assume ?lhs
from this obtain ε where "0 < ε" "k + ε ≤ π⇩m⇩i⇩n ⦇asks = asks', bids = bids'⦈"
using less_diff_eq by fastforce
hence "∀𝒫 ∈ probabilities.
(∑b←asks'. 𝒫 (bet b)) + total_price bids' + (k + ε)
≤ (∑s←bids'. 𝒫 (bet s)) + total_price asks'"
using arbitrageur_nonstrict_correspondence [of "k + ε" asks' bids'] by auto
thus ?rhs
using ‹0 < ε› by auto
next
have "[bet b . b ← bids'⇧∼ @ asks'] = ❙∼ [bet s. s ← bids'] @ [bet b. b ← asks']"
(is "_ = ❙∼ ?bid_φs @ ?ask_φs")
unfolding negate_bets_def
by (induct bids', simp+)
{
fix 𝒫 :: "'a ⇒ real"
have "(∑b←asks'. 𝒫 (bet b)) = (∑φ←?ask_φs. 𝒫 φ)"
"(∑b←bids'. 𝒫 (bet b)) = (∑φ←?bid_φs. 𝒫 φ)"
by (induct asks', auto, induct bids', auto)
}
note ⋆ = this
let ?tot_bs = "total_price bids'" and ?tot_ss = "total_price asks'"
let ?c = "?tot_bs + k - ?tot_ss"
assume ?rhs
have "∀ 𝒫 ∈ probabilities. (∑b←asks'. 𝒫 (bet b)) + ?c < (∑s←bids'. 𝒫 (bet s))"
using ‹?rhs› by fastforce
hence "∀ 𝒫 ∈ probabilities. (∑φ←?ask_φs. 𝒫 φ) + ?c < (∑φ←?bid_φs. 𝒫 φ)"
using ⋆ by auto
hence "∀ 𝒫 ∈ dirac_measures. (∑φ←?ask_φs. 𝒫 φ) + (⌊?c⌋ + 1) ≤ (∑φ←?bid_φs. 𝒫 φ)"
using strict_dirac_collapse [of ?ask_φs ?c ?bid_φs]
by auto
hence "MaxSAT (❙∼ ?bid_φs @ ?ask_φs) + (⌊?c⌋ + 1) ≤ length ?bid_φs"
by (metis floor_add_int floor_mono floor_of_nat dirac_inequality_equiv)
hence "MaxSAT (❙∼ ?bid_φs @ ?ask_φs) + ?c < length ?bid_φs"
by linarith
from this obtain ε :: real where
"0 < ε"
"MaxSAT (❙∼ ?bid_φs @ ?ask_φs) + (k + ε) ≤ ?tot_ss + length bids' - ?tot_bs"
using less_diff_eq by fastforce
hence "k + ε ≤ π⇩m⇩i⇩n ⦇asks = asks', bids = bids'⦈"
using ‹[bet b . b ← bids'⇧∼ @ asks'] = ❙∼ ?bid_φs @ ?ask_φs›
arbitrageur_maxsat [of "k + ε" asks' bids']
by simp
thus ?lhs
using ‹0 < ε› by linarith
qed
text ‹
Below is our central result regarding checking if a strategy is an arbitrage strategy:
∗‹A strategy is an arbitrage strategy if and only if there is a corresponding identity
in probability theory that reflects it.›
›
theorem (in consistent_classical_logic) arbitrageur_correspondence:
" (0 < π⇩m⇩i⇩n ⦇ asks = asks', bids = bids' ⦈)
= (∀ 𝒫 ∈ probabilities.
(∑b←asks'. 𝒫 (bet b)) + total_price bids'
< (∑s←bids'. 𝒫 (bet s)) + total_price asks')"
by (simp add: arbitrageur_strict_correspondence)
subsection ‹Coherence Checking and Maximum Payoff›
text ‹
Finally, we show the connection between coherence checking and probability identities.
›
lemma (in consistent_classical_logic) coherence_nonstrict_correspondence:
" (π⇩m⇩a⇩x ⦇ asks = asks', bids = bids' ⦈ ≤ k)
= (∀ 𝒫 ∈ probabilities.
(∑b←bids'. 𝒫 (bet b)) + total_price asks'
≤ (∑s←asks'. 𝒫 (bet s)) + total_price bids' + k)"
(is "?lhs = _")
proof -
let ?tot_bs = "total_price bids'" and ?tot_ss = "total_price asks'"
let ?c = "?tot_ss - ?tot_bs - k"
have "[bet b . b ← asks'⇧∼ @ bids'] = ❙∼ [bet s. s ← asks'] @ [bet b. b ← bids']"
(is "_ = ❙∼ ?ask_φs @ ?bid_φs")
unfolding negate_bets_def
by (induct bids', simp+)
hence
"?lhs = (∀ 𝒫 ∈ dirac_measures. (∑φ←?bid_φs. 𝒫 φ) + ?c ≤ (∑γ←?ask_φs. 𝒫 γ))"
using
dirac_inequality_equiv [of ?bid_φs ?c ?ask_φs]
coherence_maxsat [of asks' bids' k]
by force
moreover
{
fix 𝒫 :: "'a ⇒ real"
have "(∑φ←?ask_φs. 𝒫 φ) = (∑b←asks'. 𝒫 (bet b))"
"(∑γ←?bid_φs. 𝒫 γ) = (∑s←bids'. 𝒫 (bet s))"
by (simp add: comp_def)+
hence " ((∑φ←?bid_φs. 𝒫 φ) + ?c ≤ (∑γ←?ask_φs. 𝒫 γ))
= ((∑b←bids'. 𝒫 (bet b)) + ?tot_ss
≤ (∑s←asks'. 𝒫 (bet s)) + ?tot_bs + k)"
by linarith
}
ultimately show ?thesis
by (meson dirac_measures_subset dirac_ceiling dirac_collapse subset_eq)
qed
lemma (in consistent_classical_logic) coherence_strict_correspondence:
" (π⇩m⇩a⇩x ⦇ asks = asks', bids = bids' ⦈ < k)
= (∀ 𝒫 ∈ probabilities.
(∑b←bids'. 𝒫 (bet b)) + total_price asks'
< (∑s←asks'. 𝒫 (bet s)) + total_price bids' + k)"
(is "?lhs = ?rhs")
proof
assume ?lhs
from this obtain ε where "0 < ε" "π⇩m⇩a⇩x ⦇asks = asks', bids = bids'⦈ + ε ≤ k"
using less_diff_eq by fastforce
hence "∀𝒫 ∈ probabilities.
(∑b←bids'. 𝒫 (bet b)) + total_price asks' + ε
≤ (∑s←asks'. 𝒫 (bet s)) + total_price bids' + k"
using coherence_nonstrict_correspondence [of asks' bids' "k - ε"] by auto
thus ?rhs
using ‹0 < ε› by auto
next
have "[bet b . b ← asks'⇧∼ @ bids'] = ❙∼ [bet s. s ← asks'] @ [bet b. b ← bids']"
(is "_ = ❙∼ ?ask_φs @ ?bid_φs")
unfolding negate_bets_def
by (induct bids', simp+)
{
fix 𝒫 :: "'a ⇒ real"
have "(∑b←asks'. 𝒫 (bet b)) = (∑φ←?ask_φs. 𝒫 φ)"
"(∑b←bids'. 𝒫 (bet b)) = (∑φ←?bid_φs. 𝒫 φ)"
by (induct asks', auto, induct bids', auto)
}
note ⋆ = this
let ?tot_bs = "total_price bids'" and ?tot_ss = "total_price asks'"
let ?c = "?tot_ss - ?tot_bs - k"
assume ?rhs
have "∀ 𝒫 ∈ probabilities. (∑b←bids'. 𝒫 (bet b)) + ?c < (∑s←asks'. 𝒫 (bet s))"
using ‹?rhs› by fastforce
hence "∀ 𝒫 ∈ probabilities. (∑φ←?bid_φs. 𝒫 φ) + ?c < (∑φ←?ask_φs. 𝒫 φ)"
using ⋆ by auto
hence "∀ 𝒫 ∈ dirac_measures. (∑φ←?bid_φs. 𝒫 φ) + (⌊?c⌋ + 1) ≤ (∑φ←?ask_φs. 𝒫 φ)"
using strict_dirac_collapse [of ?bid_φs ?c ?ask_φs]
by auto
hence "MaxSAT (❙∼ ?ask_φs @ ?bid_φs) + (⌊?c⌋ + 1) ≤ length ?ask_φs"
by (metis floor_add_int floor_mono floor_of_nat dirac_inequality_equiv)
hence "MaxSAT (❙∼ ?ask_φs @ ?bid_φs) + ?c < length ?ask_φs"
by linarith
from this obtain ε :: real where
"0 < ε"
"MaxSAT (❙∼ ?ask_φs @ ?bid_φs) + ?c + ε ≤ length asks'"
using less_diff_eq by fastforce
hence "π⇩m⇩a⇩x ⦇asks = asks', bids = bids'⦈ ≤ k - ε "
using ‹[bet b . b ← asks'⇧∼ @ bids'] = ❙∼ ?ask_φs @ ?bid_φs›
coherence_maxsat [of asks' bids' "k - ε"]
by auto
thus ?lhs using ‹0 < ε› by linarith
qed
text ‹
Below is our central result regarding coherence testing:
∗‹A strategy is incoherent if and only if there is a corresponding identity in
probability theory that reflects it.›
›
theorem (in consistent_classical_logic) coherence_correspondence:
" (π⇩m⇩a⇩x ⦇ asks = asks', bids = bids' ⦈ < 0)
= (∀ 𝒫 ∈ probabilities.
(∑b←bids'. 𝒫 (bet b)) + total_price asks'
< (∑s←asks'. 𝒫 (bet s)) + total_price bids')"
using coherence_strict_correspondence by force
no_notation Probability_Inequality_Completeness.relative_maximals (‹ℳ›)
end