diff --git a/Incompleteness.lean b/Incompleteness.lean index ad637f5..428b23e 100644 --- a/Incompleteness.lean +++ b/Incompleteness.lean @@ -7,4 +7,5 @@ import Incompleteness.Arith.Second import Incompleteness.Arith.DC import Incompleteness.DC.Basic -import Incompleteness.ProvabilityLogic.Basic +import Incompleteness.ProvabilityLogic.Soundness +import Incompleteness.ProvabilityLogic.GL.Completeness diff --git a/Incompleteness/ProvabilityLogic/Basic.lean b/Incompleteness/ProvabilityLogic/Basic.lean index f587ab9..93f302c 100644 --- a/Incompleteness/ProvabilityLogic/Basic.lean +++ b/Incompleteness/ProvabilityLogic/Basic.lean @@ -16,17 +16,35 @@ variable [Semiterm.Operator.GoedelNumber L (Sentence L)] namespace ProvabilityLogic /-- Mapping modal prop vars to first-order sentence -/ -def Realization (α : Type u) (L) := α → FirstOrder.Sentence L +def Realization (α L) := α → FirstOrder.Sentence L + + +namespace Realization + +variable {T U : FirstOrder.Theory L} {𝔅 : ProvabilityPredicate T U} /-- Mapping modal formulae to first-order sentence -/ -def Realization.interpret - {T U : FirstOrder.Theory L} - (f : Realization α L) (𝔅 : ProvabilityPredicate T U) : Formula α → FirstOrder.Sentence L +def interpret (f : Realization α L) (𝔅 : ProvabilityPredicate T U) : Formula α → FirstOrder.Sentence L | .atom a => f a | □φ => 𝔅 (f.interpret 𝔅 φ) | ⊥ => ⊥ | φ ➝ ψ => (f.interpret 𝔅 φ) ➝ (f.interpret 𝔅 ψ) +variable {f : Realization α L} + +lemma unbox_bot (soundness : ∀ k, T ⊢!. 𝔅 (f.interpret 𝔅 (□^[k]⊥)) → T ⊢!. f.interpret 𝔅 (□^[k]⊥)) : T ⊢!. f.interpret 𝔅 (□^[n]⊥) → T ⊢!. ⊥ := by + induction n with + | zero => simp [Realization.interpret]; + | succ n ih => + intro h; + apply ih; + apply soundness n; + simpa [Realization.interpret] using h; + +end Realization + +section + variable [Semiterm.Operator.GoedelNumber L (Sentence L)] class ArithmeticalSound (Λ : Hilbert α) (𝔅 : ProvabilityPredicate T U) where @@ -35,48 +53,6 @@ class ArithmeticalSound (Λ : Hilbert α) (𝔅 : ProvabilityPredicate T U) wher class ArithmeticalComplete (Λ : Hilbert α) (𝔅 : ProvabilityPredicate T U) where complete : ∀ {φ}, (∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ)) → (Λ ⊢! φ) - -section ArithmeticalSoundness - -open System -open ProvabilityPredicate - -variable {L : FirstOrder.Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] - [L.DecidableEq] - {T U : FirstOrder.Theory L} [T ≼ U] - {𝔅 : ProvabilityPredicate T U} - -lemma arithmetical_soundness_N (h : (Hilbert.N α) ⊢! φ) : ∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ) := by - intro f; - induction h using Deduction.inducition_with_necOnly! with - | hMaxm hp => simp at hp; - | hNec ihp => exact D1_shift ihp; - | hMdp ihpq ihp => exact ihpq ⨀ ihp; - | hImply₁ => exact imply₁!; - | hImply₂ => exact imply₂!; - | hElimContra => exact elim_contra_neg!; - - -lemma arithmetical_soundness_GL [Diagonalization T] [𝔅.HBL] (h : (Hilbert.GL α) ⊢! φ) : ∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ) := by - intro f; - induction h using Deduction.inducition_with_necOnly! with - | hMaxm hp => - rcases hp with (⟨_, _, rfl⟩ | ⟨_, rfl⟩) - . exact D2_shift; - . exact FLT_shift; - | hNec ihp => exact D1_shift ihp; - | hMdp ihpq ihp => exact ihpq ⨀ ihp; - | hImply₁ => exact imply₁!; - | hImply₂ => exact imply₂!; - | hElimContra => exact elim_contra_neg!; - -end ArithmeticalSoundness - - -section - -instance (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : ArithmeticalSound (Hilbert.GL α) (T.standardDP T) := ⟨arithmetical_soundness_GL⟩ - end diff --git a/Incompleteness/ProvabilityLogic/GL/Completeness.lean b/Incompleteness/ProvabilityLogic/GL/Completeness.lean new file mode 100644 index 0000000..d137f9d --- /dev/null +++ b/Incompleteness/ProvabilityLogic/GL/Completeness.lean @@ -0,0 +1,36 @@ +import Incompleteness.ProvabilityLogic.GL.SolovaySentences + +namespace LO + +open Classical + +open System (Consistent) +open Modal +open FirstOrder.DerivabilityCondition +open ProvabilityLogic + + +variable {T : FirstOrder.Theory ℒₒᵣ} [𝐑₀ ≼ T] [𝐈𝚺₁ ≼ T] [System.Consistent T] [T.Delta1Definable] [ℕ ⊧ₘ* T] + +namespace Modal.Hilbert.GL + +open FirstOrder.Theory (standardDP) + +theorem arithmetical_completeness : (∀ {f : Realization _ _}, T ⊢!. f.interpret (standardDP T T) A) → (Hilbert.GL ℕ) ⊢! A := by + contrapose; + intro h; + obtain ⟨M, h⟩ := @Hilbert.GL.Kripke.unprovable_iff_exists_unsatisfies_at_root_on_FiniteTransitiveTree A |>.mp h; + letI Φ := M↧.solovaySentences (standardDP T T); + push_neg; + use Φ.realization; + refine SolovaySentences.lemma3 Φ h ?_; + . intro k hk; + apply FirstOrder.Arith.provableₐ_sound (T := T) (U := T); + exact hk; + +instance : ArithmeticalComplete (Hilbert.GL ℕ) (standardDP T T) := ⟨arithmetical_completeness⟩ + +end Modal.Hilbert.GL + + +end LO diff --git a/Incompleteness/ProvabilityLogic/GL/Preface.lean b/Incompleteness/ProvabilityLogic/GL/Preface.lean new file mode 100644 index 0000000..1c7ad6e --- /dev/null +++ b/Incompleteness/ProvabilityLogic/GL/Preface.lean @@ -0,0 +1,188 @@ +import Foundation.Modal.Kripke.GL.Tree +import Incompleteness.ProvabilityLogic.Basic +import Mathlib.Data.Finite.Card + + +section + +lemma _root_.Nat.lt_succ_sub {i : ℕ} (hi : i ≠ 0) : i < n + 1 → i - 1 < n := by induction i <;> simp_all; + +end + + +namespace LO.System + +open FiniteContext + +variable {F : Type*} [LogicalConnective F] [DecidableEq F] + {S : Type*} [System F S] + {𝓢 : S} [System.Classical 𝓢] + {p q r : F} + {Γ Δ : List F} + +lemma conj_disj_demorgan₂'! (h : 𝓢 ⊢! ⋀Γ.map (∼·)) : 𝓢 ⊢! ∼⋁Γ := by + induction Γ using List.induction_with_singleton with + | hnil => simp; + | hsingle q => simp_all; + | hcons q Γ hΓ ih => + replace h : 𝓢 ⊢! ∼q ⋏ (⋀Γ.map (∼·)) := by + have e := List.conj₂_cons_nonempty (a := ∼q) (as := Γ.map (∼·)) (by simpa using hΓ); + simpa [←e] using h; + simp [List.disj₂_cons_nonempty (a := q) hΓ]; + apply demorgan₂'!; + apply and₃'!; + . exact and₁'! h; + . exact ih $ and₂'! h + +lemma conj_disj_demorgan₂_suppl'! (h : 𝓢 ⊢! p ➝ ⋀Γ.map (∼·)) : 𝓢 ⊢! p ➝ ∼⋁Γ := + deduct'! $ conj_disj_demorgan₂'! $ (of'! h) ⨀ by_axm! + +omit [DecidableEq F] in +lemma disj_mem! (h : p ∈ Γ) : 𝓢 ⊢! p ➝ ⋁Γ := by + induction Γ using List.induction_with_singleton with + | hnil => simp at h; + | hsingle q => + replace h : p = q := by simpa using h; + subst h; + simp; + | hcons q Γ hΓ ih => + replace h : p = q ∨ p ∈ Γ := by simpa using h; + simp [List.disj₂_cons_nonempty (a := q) hΓ]; + rcases h with (rfl | h); + . exact or₁!; + . exact imply_right_or'! $ ih h + +lemma not_imply_prem''! (hpq : 𝓢 ⊢! p ➝ q) (hpnr : 𝓢 ⊢! p ➝ ∼(r)) : 𝓢 ⊢! p ➝ ∼(q ➝ r) := + deduct'! $ (contra₀'! $ not_or_of_imply!) ⨀ (demorgan₂'! $ and₃'! (dni'! $ of'! hpq ⨀ (by_axm!)) (of'! hpnr ⨀ (by_axm!))) + +lemma disj_intro! (h : ∀ q ∈ Γ, 𝓢 ⊢! q ➝ p) : 𝓢 ⊢! ⋁Γ ➝ p := by + induction Γ using List.induction_with_singleton with + | hnil => simp; + | hsingle q => simp_all; + | hcons q Γ hΓ ih => + simp [List.disj₂_cons_nonempty (a := q) hΓ]; + obtain ⟨h₁, h₂⟩ := by simpa using h; + replace h₂ := ih h₂; + exact or₃''! h₁ h₂; + +lemma disj_outro! [System.Consistent 𝓢] + (h₁ : 𝓢 ⊢! ⋁Γ) (h₂ : ∀ q ∈ Γ, 𝓢 ⊢! q ➝ p) : 𝓢 ⊢! p := by + induction Γ using List.induction_with_singleton with + | hnil => + obtain ⟨f, hf⟩ := Consistent.exists_unprovable (𝓢 := 𝓢) (by assumption); + have : 𝓢 ⊢! f := efq'! $ by simpa using h₁; + contradiction; + | hsingle r => + simp_all; + exact h₂ ⨀ h₁; + | hcons q Γ hΓ ih => + simp_all; + have ⟨h₂₁, h₂₂⟩ := h₂; + apply or₃'''! (d₃ := h₁); + . exact h₂₁; + . apply disj_intro!; + exact h₂₂; + + +/- +section + +-- TODO: cancel class + +lemma cancel_or_left! (cancel : ∀ {p}, 𝓢 ⊬ p → 𝓢 ⊢! ∼p) (hpq : 𝓢 ⊢! p ⋎ q) (hp : 𝓢 ⊬ p) : 𝓢 ⊢! q := by + apply or₃'''! (𝓢 := 𝓢) (φ := p) (ψ := q) (χ := q); + . apply imply_of_not_or'!; + apply or₁'!; + apply cancel hp; + . simp; + . assumption; + +lemma cancel_or_right! (cancel : ∀ {p}, 𝓢 ⊬ p → 𝓢 ⊢! ∼p) (hpq : 𝓢 ⊢! p ⋎ q) (hq : 𝓢 ⊬ q) : 𝓢 ⊢! p := by + apply cancel_or_left! (p := q) (q := p) cancel; + . exact or_comm'! hpq; + . exact hq; + +lemma disj_tail! (cancel : ∀ {p}, 𝓢 ⊬ p → 𝓢 ⊢! ∼p) (Γ_nil : Γ.length > 0) (h₁ : 𝓢 ⊢! ⋁Γ) (h₂ : 𝓢 ⊬ Γ[0]) : 𝓢 ⊢! ⋁(Γ.tail) := by + induction Γ using List.induction_with_singleton with + | hnil => simp at Γ_nil; + | hsingle q => simp_all; + | hcons q Γ hΓ ih => + simp_all; + exact cancel_or_left! cancel h₁ h₂; + +end +-/ + +lemma cancel_or_left! (hpq : 𝓢 ⊢! p ⋎ q) (hp : 𝓢 ⊢! ∼p) : 𝓢 ⊢! q := by + apply or₃'''! (𝓢 := 𝓢) (φ := p) (ψ := q) (χ := q); + . apply imply_of_not_or'!; + apply or₁'!; + apply hp; + . simp; + . assumption; + +lemma cancel_or_right! (hpq : 𝓢 ⊢! p ⋎ q) (hq : 𝓢 ⊢! ∼q) : 𝓢 ⊢! p := by + apply cancel_or_left! (p := q) (q := p); + . exact or_comm'! hpq; + . exact hq; + +lemma disj_tail! (Γ_nil : Γ.length > 0) (h₁ : 𝓢 ⊢! ⋁Γ) (h₂ : 𝓢 ⊢! ∼Γ[0]) : 𝓢 ⊢! ⋁(Γ.tail) := by + induction Γ using List.induction_with_singleton with + | hnil => simp at Γ_nil; + | hsingle q => + simp at h₁ h₂; + replace h₂ := neg_equiv'!.mp h₂; + exact efq'! $ h₂ ⨀ h₁ + | hcons q Γ hΓ ih => + simp_all; + exact cancel_or_left! h₁ h₂; + +end LO.System + + + +namespace LO.Modal.Kripke + +open Modal.Formula.Kripke + +namespace FiniteTransitiveTree + +variable {F : FiniteTransitiveTree} + +noncomputable def size (F : FiniteTransitiveTree) : ℕ := Nat.card F.World + +@[simp] lemma size_le_0 : 0 < F.size := Finite.card_pos + +def world_selector (F : FiniteTransitiveTree) : Fin F.size → F.World := by sorry + +lemma world_selector.bijective : (Function.Bijective F.world_selector) := by sorry + +lemma world_selector.zero : F.world_selector ⟨0, by simp⟩ = F.root := by sorry; + + +noncomputable def get_world (F : FiniteTransitiveTree) (i : Fin F.size) : F.World := F.world_selector i + +lemma get_world_zero_root : F.get_world ⟨0, by simp⟩ = F.root := world_selector.zero + +noncomputable def get_index (F : FiniteTransitiveTree) (w : F.World) : Fin F.size := world_selector.bijective.2 w |>.choose + +lemma get_index_get_world : F.get_index (F.get_world i) = i := by sorry; + +set_option pp.proofs true in +@[simp] +lemma get_world_get_index : F.get_world (F.get_index wi) = wi := by + simp [get_world, get_index]; + sorry; + +@[simp] +lemma cannotback_zero : ¬(x ≺ F.get_world ⟨0, by simp⟩) := by + rw [get_world_zero_root]; + sorry; + +end FiniteTransitiveTree + + +instance {M : FiniteTransitiveTreeModel} : Semantics (Modal.Formula ℕ) (M.World) := ⟨λ b a => Satisfies M.toModel b a⟩ + + +end LO.Modal.Kripke diff --git a/Incompleteness/ProvabilityLogic/GL/SolovaySentences.lean b/Incompleteness/ProvabilityLogic/GL/SolovaySentences.lean new file mode 100644 index 0000000..4da964f --- /dev/null +++ b/Incompleteness/ProvabilityLogic/GL/SolovaySentences.lean @@ -0,0 +1,188 @@ +import Incompleteness.ProvabilityLogic.GL.Preface + +namespace LO.ProvabilityLogic + +open Classical + +open System System.FiniteContext +open Modal +open Modal.Formula +open Modal.Formula.Kripke +open Modal.Kripke +open FirstOrder.DerivabilityCondition +open FirstOrder.DerivabilityCondition.ProvabilityPredicate + +variable {T U : FirstOrder.Theory ℒₒᵣ} {𝔅 : ProvabilityPredicate T T} [𝔅.HBL] +variable {M : FiniteTransitiveTreeModel} + +structure SolovaySentences + {T U : FirstOrder.Theory ℒₒᵣ} + (𝔅 : ProvabilityPredicate T U) [𝔅.HBL] + (M : FiniteTransitiveTreeModel) + where + Φ : List (FirstOrder.Sentence ℒₒᵣ) + eq_length_model_size : Φ.length = M.size + 1 + S1 : T ⊢!. ⋁Φ + S2 : ∀ i : Fin Φ.length, ∀ j : Fin Φ.length, i ≠ j → T ⊢!. Φ[i] ➝ ∼Φ[j] + S3 : + ∀ i : Fin Φ.length, (hi : i ≠ ⟨0, by omega⟩) → + letI Φ' := List.finRange Φ.length + |>.filter (λ j => + letI wi : M.World := M.get_world ⟨i.1 - 1, by omega⟩ + letI wj : M.World := M.get_world ⟨j.1 - 1, by omega⟩ + wi ≺ wj + ) + |>.map (λ j => Φ[j]); + T ⊢!. Φ[i] ➝ 𝔅 (⋁Φ') + S4 : + ∀ i : Fin Φ.length, + ∀ j : Fin Φ.length, (hj : j ≠ ⟨0, by omega⟩) → + letI wi : M.World := M.get_world ⟨i.1 - 1, by omega⟩; + letI wj : M.World := M.get_world ⟨j.1 - 1, by omega⟩; + wi ≺ wj → + T ⊢!. 𝔅 (∼Φ[j]) ➝ ∼Φ[i] + +namespace SolovaySentences + +-- instance : CoeSort (SolovaySentences M 𝔅) (List (Sentence ℒₒᵣ)) := ⟨λ Φ => Φ.Φ⟩ + +attribute [simp] eq_length_model_size + +variable {Φ : SolovaySentences 𝔅 M} + +abbrev length (Φ : SolovaySentences 𝔅 M) : ℕ := Φ.Φ.length + +@[simp] +lemma ln_zero : 0 < Φ.length := by + rw [length, Φ.eq_length_model_size]; + simp; + +lemma ln_M_size {i : Fin Φ.length} (hi : i ≠ ⟨0, ln_zero⟩ := by assumption) : i - 1 < M.size := by + have := i.2; + simp only [eq_length_model_size] at this; + exact Nat.lt_succ_sub ((Fin.ne_iff_vne i ⟨0, by simp⟩).mp hi) this; + +noncomputable def realization (Φ : SolovaySentences 𝔅 M) : Realization ℕ ℒₒᵣ := λ a => + letI Φ' := List.finRange Φ.length + |>.filter (λ i => + if hi : i = ⟨0, ln_zero⟩ then False + else Kripke.Satisfies M.toModel (M.get_world ⟨i.1 - 1, ln_M_size⟩) a + ) + |>.map (λ i => Φ.Φ[i]); + ⋁Φ' + + +lemma lemma1 + (Φ : SolovaySentences 𝔅 M) (i : Fin Φ.length) (hi : i ≠ ⟨0, by simp⟩) + (A : Modal.Formula ℕ) : + let wi : M.World := M.get_world ⟨i - 1, SolovaySentences.ln_M_size hi⟩ + (wi ⊧ A → T ⊢!. Φ.Φ[i] ➝ (Φ.realization.interpret 𝔅 A)) ∧ (¬(wi ⊧ A) → T ⊢!. Φ.Φ[i] ➝ ∼(Φ.realization.interpret 𝔅 A)) + := by + intro wi; + induction A using Modal.Formula.rec' generalizing i with + | hfalsum => simp [Realization.interpret, Semantics.Realize, Satisfies]; + | hatom a => + simp only [Realization.interpret, SolovaySentences.realization]; + constructor; + . intro h; + apply disj_mem!; + simp; + use i; + constructor; + . split; + . contradiction; + . simpa; + . rfl; + . intro h; + apply conj_disj_demorgan₂_suppl'!; + have : T ⊢!. Φ.Φ[i] ➝ ⋀(List.finRange Φ.length |>.filter (i ≠ ·) |>.map (λ j => ∼Φ.Φ[j])) := by + apply deduct'!; + apply iff_provable_list_conj.mpr; + intro q hq; + obtain ⟨j, hj, rfl⟩ := List.mem_map.mp hq; + exact deductInv'! $ Φ.S2 i j (by simpa using List.of_mem_filter hj); + exact imp_trans''! this $ conjconj_subset! $ by + simp; + intro j hj; + use j; + constructor; + . rintro rfl; + have : wi ⊧ (atom a) := by simpa [hi] using hj; + contradiction; + . rfl; + | himp A B ihA ihB => + simp only [Realization.interpret]; + constructor; + . intro h; + rcases (not_or_of_imp $ Satisfies.imp_def.mp h) with (hp | hq); + . apply deduct'!; + exact efq_imply_not₁! ⨀ (deductInv'! $ ihA i hi |>.2 hp) + . apply deduct'!; + exact imply₁'! $ deductInv'! $ ihB i hi |>.1 hq; + . intro h; + have := Satisfies.imp_def.not.mp h; push_neg at this; + replace ⟨hp, hq⟩ := this; + have hp := ihA i hi |>.1 hp; + have hq := ihB i hi |>.2 hq; + exact not_imply_prem''! hp hq; + | hbox A ihA => + simp only [Realization.interpret]; + constructor; + . intro h; + apply imp_trans''! (Φ.S3 i hi) ?_; + apply prov_distribute_imply; + apply disj_intro!; + intro j hj; + simp at hj; + obtain ⟨j, ⟨hj₂, rfl⟩⟩ := hj; + apply ihA j (by rintro rfl; simp at hj₂) |>.1; + apply h; + exact hj₂; + . intro h; + have := Satisfies.box_def.not.mp h; push_neg at this; + obtain ⟨wj, hwj, hwj'⟩ := this; + let j := M.get_index wj; + have : T ⊢!. Φ.Φ[↑j + 1] ➝ ∼Φ.realization.interpret 𝔅 A := ihA ⟨j.1 + 1, by simp⟩ (by simp) |>.2 (by convert hwj'; simp [j]); + have h₁ := 𝔅.prov_distribute_imply $ contra₁'! this; + have h₂ := Φ.S4 i ⟨j.1 + 1, by simp⟩ (by simp) (by convert hwj; simp [j]); + exact contra₁'! $ imp_trans''! h₁ h₂; + +lemma lemma2 {Φ : SolovaySentences 𝔅 M} (h : ¬M.root ⊧ A) : T ⊢!. Φ.Φ[1] ➝ ∼(Φ.realization.interpret 𝔅 A) := by + apply lemma1 Φ ⟨1, by simp⟩ (by simp) A |>.2; + convert h; + exact FiniteTransitiveTree.get_world_zero_root; + +instance [h : Consistent T] : Consistent T.alt := by sorry + +lemma lemma3 [Consistent T] (Φ : SolovaySentences 𝔅 M↧) (h : ¬M.root ⊧ A) + (soundness : ∀ k, T ⊢!. 𝔅 (Φ.realization.interpret 𝔅 (□^[k]⊥)) → T ⊢!. Φ.realization.interpret 𝔅 (□^[k]⊥)) + : T ⊬. Φ.realization.interpret 𝔅 A := by + by_contra hC; + suffices T ⊢!. ⊥ by + have : ¬Consistent T := consistent_iff_unprovable_bot.not.mpr $ by simpa using this; + contradiction; + have : T ⊢!. Φ.Φ[1] ➝ ∼Φ.realization.interpret 𝔅 A := lemma2 $ by + have := @FiniteTransitiveTreeModel.SimpleExtension.modal_equivalence_original_world M M.root A |>.not.mp h; + suffices ¬(Satisfies M↧.toModel (Sum.inr M.root) A) by sorry; + exact this; + have : T ⊢!. ∼Φ.Φ[1] := contra₁'! this ⨀ hC; + have : T ⊢!. (𝔅 (∼Φ.Φ[1])) := D1_shift this; + have : T ⊢!. ∼Φ.Φ[0] := Φ.S4 ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp) (by sorry) ⨀ this; + have : T ⊢!. ⋁Φ.Φ.tail := disj_tail! (by simp) Φ.S1 (by assumption); + have : T ⊢!. Φ.realization.interpret 𝔅 (□^[7]⊥) := disj_outro! this $ by + intro j hj; + convert @lemma1 T 𝔅 _ (Φ := Φ) _ ⟨Φ.Φ.indexOf j, ?_⟩ ?_ _ |>.1 ?_; + . simp; + . apply List.indexOf_lt_length.mpr; + exact List.mem_of_mem_tail hj; + . sorry; + . sorry; + exact Realization.unbox_bot soundness this; + +end SolovaySentences + + +noncomputable def _root_.LO.Modal.Kripke.FiniteTransitiveTreeModel.solovaySentences (M : FiniteTransitiveTreeModel) (𝔅 : ProvabilityPredicate T T) [𝔅.HBL] : SolovaySentences 𝔅 M := by sorry; + + +end LO.ProvabilityLogic diff --git a/Incompleteness/ProvabilityLogic/Soundness.lean b/Incompleteness/ProvabilityLogic/Soundness.lean new file mode 100644 index 0000000..cc9a5f9 --- /dev/null +++ b/Incompleteness/ProvabilityLogic/Soundness.lean @@ -0,0 +1,56 @@ +import Incompleteness.ProvabilityLogic.Basic + +namespace LO + +open FirstOrder FirstOrder.DerivabilityCondition +open Modal +open Modal.Hilbert +open ProvabilityPredicate +open System +open ProvabilityLogic + +variable {L : FirstOrder.Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] + [L.DecidableEq] + {T U : FirstOrder.Theory L} [T ≼ U] + {𝔅 : ProvabilityPredicate T U} + +namespace Modal.Hilbert + +namespace N + +theorem arithmetical_soundness (h : (Hilbert.N α) ⊢! φ) : ∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ) := by + intro f; + induction h using Deduction.inducition_with_necOnly! with + | hMaxm hp => simp at hp; + | hNec ihp => exact D1_shift ihp; + | hMdp ihpq ihp => exact ihpq ⨀ ihp; + | hImply₁ => exact imply₁!; + | hImply₂ => exact imply₂!; + | hElimContra => exact elim_contra_neg!; + +end N + + +namespace GL + +theorem arithmetical_soundness [Diagonalization T] [𝔅.HBL] (h : (Hilbert.GL α) ⊢! φ) : ∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ) := by + intro f; + induction h using Deduction.inducition_with_necOnly! with + | hMaxm hp => + rcases hp with (⟨_, _, rfl⟩ | ⟨_, rfl⟩) + . exact D2_shift; + . exact FLT_shift; + | hNec ihp => exact D1_shift ihp; + | hMdp ihpq ihp => exact ihpq ⨀ ihp; + | hImply₁ => exact imply₁!; + | hImply₂ => exact imply₂!; + | hElimContra => exact elim_contra_neg!; + +instance {T : FirstOrder.Theory ℒₒᵣ} [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : ArithmeticalSound (Hilbert.GL α) (T.standardDP T) := ⟨arithmetical_soundness⟩ + +end GL + +end Modal.Hilbert + + +end LO diff --git a/lake-manifest.json b/lake-manifest.json index 7e858c9..615db95 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,52 +1,52 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/FormalizedFormalLogic/Arithmetization", + [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "FormalizedFormalLogic", - "rev": "fe2c1952fc091a965b64e2aa5dbcc4581e7497a6", - "name": "arithmetization", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/FormalizedFormalLogic/Foundation", - "type": "git", - "subDir": null, - "scope": "FormalizedFormalLogic", - "rev": "a1bfd1fa480026f05e476050030c0b2d17983bb0", - "name": "foundation", + "scope": "leanprover-community", + "rev": "0dc51ac7947ff6aa2c16bcffb64c46c7149d1276", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4", + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3ece930d0a4a55679efa52b1a825ac93b2469a06", - "name": "mathlib", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", - "name": "plausible", + "rev": "de91b59101763419997026c35a41432ac8691f15", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", - "name": "LeanSearchClient", + "rev": "1383e72b40dd62a566896a6e348ffe868801b172", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.46", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", + "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -61,55 +61,55 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1383e72b40dd62a566896a6e348ffe868801b172", - "name": "proofwidgets", + "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.46", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "de91b59101763419997026c35a41432ac8691f15", - "name": "aesop", + "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", - "name": "Qq", + "rev": "3ece930d0a4a55679efa52b1a825ac93b2469a06", + "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/batteries", + {"url": "https://github.com/FormalizedFormalLogic/Foundation", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "0dc51ac7947ff6aa2c16bcffb64c46c7149d1276", - "name": "batteries", + "scope": "FormalizedFormalLogic", + "rev": "a1bfd1fa480026f05e476050030c0b2d17983bb0", + "name": "foundation", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/FormalizedFormalLogic/Arithmetization", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", - "name": "Cli", + "scope": "FormalizedFormalLogic", + "rev": "f9bc733f6cb954b99c76c698a3e4d191a8a667d5", + "name": "arithmetization", "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}], + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}], "name": "incompleteness", "lakeDir": ".lake"}