Completeness of natural deduction for BSML #
The natural deduction system Derives of NaturalDeduction.lean is complete: a consequence that
holds on every model is derivable from finitely many premises. The proof follows the normal-form
strategy of Aloni, Anttila and Yang. The world types of Characteristic.lean are the worlds of one
universal model, and each type's Hintikka formula holds exactly at it there. A set of
types T has the strong Hintikka formula θ_T, the disjunction of the formulas χ_τ ∧ NE, which
derives every formula the team T supports. Conversely, the ⊥NE-translation rules split every
formula into the cases θ_T for the teams supporting it.
Main definitions #
Main results #
derives_of_support: a strong Hintikka formula derives what its team supports.derives_bigDisj_hintikka: every world has a type of each depth.derives_bigDisj_realize: a classical formula derives the disjunction of its types.splits_fill: every formula splits into the strong Hintikka formulas of its teams.completeness,derives_iff: completeness for finite premise sets.
Implementation notes #
Successor sets are finite, so completeness holds for finite premise sets only. No team supports
{◇pₙ | n ∈ ℕ} ∪ {□¬(pᵢ ∧ pⱼ) | i ≠ j} ∪ {NE}, yet each of its finite subsets is satisfiable.
The first sections derive general rules of the system.
References #
- [AAY24] Aloni, Anttila and Yang, State-based Modal Logics for Free Choice
Derived propositional rules #
theorem
BSML.Derives.disj_falsum
{Atom : Type u_1}
[Inhabited Atom]
{Γ : Set (Formula Atom)}
{φ : Formula Atom}
(h : Derives Γ (φ.disj Formula.falsum))
:
Derives Γ φ
theorem
BSML.Derives.of_falsum
{Atom : Type u_1}
[Inhabited Atom]
{Γ : Set (Formula Atom)}
{α : Formula Atom}
(h : Derives Γ Formula.falsum)
(hα : α.NEFree)
:
Derives Γ α
Modal combinations #
theorem
BSML.Derives.poss_of_falsum
{Atom : Type u_1}
[Inhabited Atom]
{Γ : Set (Formula Atom)}
{φ : Formula Atom}
(h : Derives Γ Formula.falsum)
:
The empty team supports every possibility.
theorem
BSML.Derives.nec_of_falsum
{Atom : Type u_1}
[Inhabited Atom]
{Γ : Set (Formula Atom)}
{φ : Formula Atom}
(h : Derives Γ Formula.falsum)
:
The empty team supports every necessity.
theorem
BSML.Derives.nec_disj_conj_ne
{Atom : Type u_1}
[Inhabited Atom]
{Γ : Set (Formula Atom)}
{φ ψ : Formula Atom}
(h : Derives Γ (φ.disj ψ).nec)
(h' : Derives Γ φ.poss)
:
Derives Γ ((φ.conj Formula.ne).disj ψ).nec
With ◇φ, a necessary disjunction □(φ ∨ ψ) conjoins NE to φ
([AAY24] Lemma 4.22 (ii), right to left).
theorem
BSML.Derives.nec_bigDisjNE
{Atom : Type u_1}
[Inhabited Atom]
{Γ : Set (Formula Atom)}
{L : List (Formula Atom)}
(h : Derives Γ (bigDisj L).nec)
(hL : ∀ x ∈ L, Derives Γ x.poss)
:
With the possibility of each disjunct, a necessary disjunction conjoins NE to every
disjunct ([AAY24] Lemma 4.23 (ii), right to left).
The universal model #
noncomputable def
BSML.univModel
{Atom : Type u_1}
{n : ℕ}
(e : Fin n → Atom)
:
ModalLogic.KripkeModel ((k : ℕ) × WorldType n k) Atom
In the universal model each type is a world, whose successors are its successor types.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
noncomputable instance
BSML.instDecidableRelSigmaNatWorldTypeValUnivModel
{Atom : Type u_1}
{n : ℕ}
(e : Fin n → Atom)
:
Equations
- BSML.instDecidableRelSigmaNatWorldTypeValUnivModel e x✝¹ x✝ = Classical.dec ((BSML.univModel e).val x✝¹ x✝)
world k τ is the type τ as a world of the universal model.
Equations
- BSML.WorldType.world k τ = ⟨k, τ⟩
Instances For
theorem
BSML.univModel_access_succ
{Atom : Type u_1}
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
(τ : WorldType n (k + 1))
:
(univModel e).access (WorldType.world (k + 1) τ) = Finset.image (WorldType.world k) τ.2
theorem
BSML.worldType_univModel
{Atom : Type u_1}
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
(k : ℕ)
(τ : WorldType n k)
:
worldType e (univModel e) k (WorldType.world k τ) = τ
theorem
BSML.realize_hintikka
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
(k : ℕ)
(τ τ' : WorldType n k)
:
Realize (univModel e) (hintikka e k τ) (WorldType.world k τ') ↔ τ' = τ
The Hintikka formula of τ holds exactly at τ.
Teams of types #
The atoms occurring in a formula all lie in S.
Equations
- BSML.Formula.AtomsIn S (BSML.Formula.atom p) = (p ∈ S)
- BSML.Formula.AtomsIn S BSML.Formula.ne = True
- BSML.Formula.AtomsIn S φ.neg = BSML.Formula.AtomsIn S φ
- BSML.Formula.AtomsIn S φ.poss = BSML.Formula.AtomsIn S φ
- BSML.Formula.AtomsIn S (φ.conj ψ) = (BSML.Formula.AtomsIn S φ ∧ BSML.Formula.AtomsIn S ψ)
- BSML.Formula.AtomsIn S (φ.disj ψ) = (BSML.Formula.AtomsIn S φ ∧ BSML.Formula.AtomsIn S ψ)
Instances For
theorem
BSML.support_image_iff
{Atom : Type u_1}
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
{φ : Formula Atom}
(hφ : φ.NEFree)
(T : Finset (WorldType n k))
:
support (univModel e) φ (Finset.image (WorldType.world k) T) ↔ ∀ τ ∈ T, Realize (univModel e) φ (WorldType.world k τ)
theorem
BSML.support_strongHintikka
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
{k : ℕ}
(T T' : Finset (WorldType n k))
:
support (univModel e) (strongHintikka e T) (Finset.image (WorldType.world k) T') ↔ T' = T
The strong Hintikka formula of T is supported exactly by the team of the types in T.
Derivations from Hintikka formulas #
theorem
BSML.hintikka_derives_nec
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
(τ : WorldType n (k + 1))
:
Derives {hintikka e (k + 1) τ} (strongHintikka e τ.2).nec
theorem
BSML.Derives.strongHintikka_elim
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
{T : Finset (WorldType n k)}
{Γ : Set (Formula Atom)}
{χ : Formula Atom}
(h : Derives Γ (strongHintikka e T))
(hT : ∀ τ ∈ T, Derives {(hintikka e k τ).conj Formula.ne} χ)
(h₀ : Derives {Formula.falsum} χ)
:
Derives Γ χ
theorem
BSML.strongHintikka_union_derives
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
(T₁ T₂ : Finset (WorldType n k))
:
Derives {strongHintikka e (T₁ ∪ T₂)} ((strongHintikka e T₁).disj (strongHintikka e T₂))
theorem
BSML.disj_strongHintikka_derives
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
(T₁ T₂ : Finset (WorldType n k))
:
Derives {(strongHintikka e T₁).disj (strongHintikka e T₂)} (strongHintikka e (T₁ ∪ T₂))
Strong Hintikka formulas derive what their teams support #
theorem
BSML.derives_of_support
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
(φ : Formula Atom)
{k : ℕ}
:
φ.modalDepth ≤ k →
Formula.AtomsIn (Set.range e) φ →
∀ (T : Finset (WorldType n k)),
(support (univModel e) φ (Finset.image (WorldType.world k) T) → Derives {strongHintikka e T} φ) ∧ (antiSupport (univModel e) φ (Finset.image (WorldType.world k) T) → Derives {strongHintikka e T} φ.neg)
A strong Hintikka formula derives every formula its team supports, and the negation of every formula its team anti-supports.
Exhaustiveness of the types #
noncomputable def
BSML.succLit
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
(e : Fin n → Atom)
{k : ℕ}
(S : Finset (WorldType n k))
(σ : WorldType n k)
:
Formula Atom
succLit e S σ says whether σ is a successor type in S.
Equations
- BSML.succLit e S σ = if σ ∈ S then (BSML.hintikka e k σ).poss else (BSML.hintikka e k σ).poss.neg
Instances For
noncomputable def
BSML.succPart
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
(e : Fin n → Atom)
{k : ℕ}
(S : Finset (WorldType n k))
:
Formula Atom
succPart e S is the modal part of the Hintikka formula of a type with successor
types S.
Equations
- BSML.succPart e S = (BSML.bigConj (List.map (fun (σ : BSML.WorldType n k) => (BSML.hintikka e k σ).poss) S.toList)).conj (BSML.bigDisj (List.map (BSML.hintikka e k) S.toList)).nec
Instances For
Classical normal forms #
theorem
BSML.Derives.of_conj_ne
{Atom : Type u_1}
[Inhabited Atom]
{φ β : Formula Atom}
(hβ : β.NEFree)
(h : Derives {φ.conj Formula.ne} β)
:
Derives {φ} β
A classical consequence of φ ∧ NE follows from φ, since the ⊥-case of ⊥NETrs is ex
falso.
theorem
BSML.strongHintikka_singleton
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
(τ : WorldType n k)
:
Derives {(hintikka e k τ).conj Formula.ne} (strongHintikka e {τ})
theorem
BSML.hintikka_derives
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
{β : Formula Atom}
(hβ : β.NEFree)
{k : ℕ}
(hk : β.modalDepth ≤ k)
(hA : Formula.AtomsIn (Set.range e) β)
(τ : WorldType n k)
:
A Hintikka formula derives the classical formulas true at its type, and the negations of those false there.
theorem
BSML.derives_bigDisj_realize
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
{β : Formula Atom}
(hβ : β.NEFree)
{k : ℕ}
(hk : β.modalDepth ≤ k)
(hA : Formula.AtomsIn (Set.range e) β)
:
Classical normal form. A classical formula derives the disjunction of the Hintikka formulas of the types at which it is true.
Splitting into cases #
A splits into the cases S when whatever follows from each case follows from A.
Equations
- BSML.Splits A S = ∀ (χ : BSML.Formula Atom), (∀ σ ∈ S, BSML.Derives {σ} χ) → BSML.Derives {A} χ
Instances For
Splittable contexts #
C.comp D places D in the hole of C.
Equations
- BSML.Formula.Context.hole.comp x✝ = x✝
- (C.conjLeft ψ).comp x✝ = (C.comp x✝).conjLeft ψ
- (BSML.Formula.Context.conjRight φ C).comp x✝ = BSML.Formula.Context.conjRight φ (C.comp x✝)
- (C.disjLeft ψ).comp x✝ = (C.comp x✝).disjLeft ψ
- (BSML.Formula.Context.disjRight φ C).comp x✝ = BSML.Formula.Context.disjRight φ (C.comp x✝)
- C.poss.comp x✝ = (C.comp x✝).poss
- C.nec.comp x✝ = (C.comp x✝).nec
Instances For
theorem
BSML.Formula.Context.Distributive.comp
{Atom : Type u_1}
{C D : Context Atom}
(hC : C.Distributive)
(hD : D.Distributive)
:
(C.comp D).Distributive
A context is splittable when it is distributive below at most one modality at its top.
Equations
- C.poss.Splittable = C.Distributive
- C.nec.Splittable = C.Distributive
- x✝.Splittable = x✝.Distributive
Instances For
theorem
BSML.Formula.Context.Distributive.splittable
{Atom : Type u_1}
{C : Context Atom}
(hC : C.Distributive)
:
theorem
BSML.Formula.Context.Splittable.comp
{Atom : Type u_1}
{C D : Context Atom}
(hC : C.Splittable)
(hD : D.Distributive)
:
(C.comp D).Splittable
A context with a modality on top adds the case of the empty team.
Equations
- C.poss.extra = {BSML.Formula.falsum}
- C.nec.extra = {BSML.Formula.falsum}
- x✝.extra = ∅
Instances For
theorem
BSML.Formula.Context.extra_comp
{Atom : Type u_1}
[Inhabited Atom]
{C D : Context Atom}
(hD : D.Distributive)
:
theorem
BSML.Splits.fill_split
{Atom : Type u_1}
[Inhabited Atom]
{C : Formula.Context Atom}
(hC : C.Splittable)
(ψ : Formula Atom)
:
Splits (C.fill ψ) {C.fill (ψ.conj Formula.ne), C.fill (ψ.conj Formula.falsum)}
The ⊥NE-translation rules split a splittable context.
theorem
BSML.Splits.fill_strongFalsum
{Atom : Type u_1}
[Inhabited Atom]
{C : Formula.Context Atom}
(hC : C.Splittable)
:
Splits (C.fill Formula.strongFalsum) C.extra
A strong contradiction in a splittable context leaves only the context's extra case.
theorem
BSML.conj_ne_disj_strongHintikka_derives
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
(τ : WorldType n k)
(T : Finset (WorldType n k))
:
Derives {((hintikka e k τ).conj Formula.ne).disj (strongHintikka e T)} (strongHintikka e (insert τ T))
theorem
BSML.splits_bigDisj_hintikka
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
{k : ℕ}
(L : List (WorldType n k))
{C : Formula.Context Atom}
:
C.Splittable →
Splits (C.fill (bigDisj (List.map (hintikka e k) L)))
((fun (T : Finset (WorldType n k)) => C.fill (strongHintikka e T)) '' {T : Finset (WorldType n k) | T ⊆ L.toFinset})
A disjunction of Hintikka formulas in a splittable context splits into the strong Hintikka formulas of its subsets.
Depth and atoms of the Hintikka formulas #
theorem
BSML.atomsIn_bigConj
{Atom : Type u_1}
[Inhabited Atom]
{S : Set Atom}
(hd : default ∈ S)
{L : List (Formula Atom)}
(hL : ∀ x ∈ L, Formula.AtomsIn S x)
:
Formula.AtomsIn S (bigConj L)
theorem
BSML.atomsIn_bigDisj
{Atom : Type u_1}
[Inhabited Atom]
{S : Set Atom}
(hd : default ∈ S)
{L : List (Formula Atom)}
(hL : ∀ x ∈ L, Formula.AtomsIn S x)
:
Formula.AtomsIn S (bigDisj L)
theorem
BSML.atomsIn_literals
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(hd : default ∈ Set.range e)
(a : Fin n → Bool)
:
Formula.AtomsIn (Set.range e) (literals e a)
theorem
BSML.atomsIn_hintikka
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(hd : default ∈ Set.range e)
(k : ℕ)
(τ : WorldType n k)
:
Formula.AtomsIn (Set.range e) (hintikka e k τ)
Distinct strong Hintikka formulas contradict #
theorem
BSML.conj_ne_disj_derives_strongFalsum
{Atom : Type u_1}
[Inhabited Atom]
{φ α : Formula Atom}
(hα : α.NEFree)
:
Derives {α.neg.conj ((α.conj Formula.ne).disj φ)} Formula.strongFalsum
A disjunction with a disjunct α ∧ NE contradicts ¬α
([AAY24] Lemma 4.13).
theorem
BSML.strongHintikka_conj_derives
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
(hd : default ∈ Set.range e)
{k : ℕ}
{T₁ T₂ : Finset (WorldType n k)}
(hT : T₁ ≠ T₂)
:
Derives {(strongHintikka e T₁).conj (strongHintikka e T₂)} Formula.strongFalsum
Distinct strong Hintikka formulas contradict each other ([AAY24] Lemma 4.11).
Splitting every formula into strong Hintikka cases #
theorem
BSML.realize_bigConj_poss_hintikka
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
{k : ℕ}
(U : Finset (WorldType n k))
(τ : WorldType n (k + 1))
:
theorem
BSML.realize_nec_bigDisj_hintikka
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
{k : ℕ}
(U : Finset (WorldType n k))
(τ : WorldType n (k + 1))
:
theorem
BSML.splits_of_derives_bigDisj
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
{A : Formula Atom}
{k : ℕ}
{L : List (WorldType n k)}
{P : Set (Finset (WorldType n k))}
(h : Derives {A} (bigDisj (List.map (hintikka e k) L)))
(hP : ∀ T ⊆ L.toFinset, T ∈ P)
{C : Formula.Context Atom}
(hC : C.Splittable)
:
theorem
BSML.splits_fill_of_neFree
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
{β : Formula Atom}
(hβ : β.NEFree)
{k : ℕ}
(hk : β.modalDepth ≤ k)
(hA : Formula.AtomsIn (Set.range e) β)
{C : Formula.Context Atom}
(hC : C.Splittable)
:
Splits (C.fill β)
((fun (T : Finset (WorldType n k)) => C.fill (strongHintikka e T)) '' {T : Finset (WorldType n k) | support (univModel e) β (Finset.image (WorldType.world k) T)} ∪ C.extra)
theorem
BSML.splits_fill
{Atom : Type u_1}
[Inhabited Atom]
{n : ℕ}
{e : Fin n → Atom}
(he : Function.Injective e)
(hd : default ∈ Set.range e)
(φ : Formula Atom)
{k : ℕ}
:
φ.modalDepth ≤ k →
Formula.AtomsIn (Set.range e) φ →
∀ {C : Formula.Context Atom},
C.Splittable →
Splits (C.fill φ)
((fun (T : Finset (WorldType n k)) => C.fill (strongHintikka e T)) '' {T : Finset (WorldType n k) | support (univModel e) φ (Finset.image (WorldType.world k) T)} ∪ C.extra) ∧ Splits (C.fill φ.neg)
((fun (T : Finset (WorldType n k)) => C.fill (strongHintikka e T)) '' {T : Finset (WorldType n k) | antiSupport (univModel e) φ (Finset.image (WorldType.world k) T)} ∪ C.extra)
In a splittable context, a formula splits into the strong Hintikka formulas of the teams supporting it, and its negation into those of the teams anti-supporting it, together with the context's extra case.
Completeness #
theorem
BSML.completeness
{Atom : Type u_1}
[Inhabited Atom]
{Γ : Finset (Formula Atom)}
{φ : Formula Atom}
(h :
∀ (W : Type) [inst : DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (s : Finset W),
(∀ γ ∈ Γ, support M γ s) → support M φ s)
:
Derives (↑Γ) φ
Completeness ([AAY24] Theorem 4.43) for finite premise sets. A consequence that holds on every model is derivable.
theorem
BSML.derives_iff
{Atom : Type u_1}
[Inhabited Atom]
{Γ : Finset (Formula Atom)}
{φ : Formula Atom}
:
Derives (↑Γ) φ ↔ ∀ (W : Type) [inst : DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (s : Finset W),
(∀ γ ∈ Γ, support M γ s) → support M φ s
For finite premise sets, derivability is consequence on every model.