@@ -72,53 +72,53 @@ end Derivation
7272theorem Provable.sound {M : Type *} [s : Structure L M] [Nonempty M] {φ : Proposition L} (f : ℕ → M) :
7373 𝐋𝐊¹ ⊢ φ → φ.Evalf f := fun b ↦ by simpa using Derivation.sound f b.get
7474
75- variable {𝔖 : Schema L}
76-
77- theorem Schema.sound_proposition {M : Type *} [s : Structure L M] [Nonempty M] :
78- 𝔖 ⊢ φ → M↓[L] ⊧* ↑↑𝔖 → ∀ f : ℕ → M, φ.Evalf f := fun b H f ↦ by
79- rcases Schema.provable_iff.mp b with ⟨Γ, hΓ, ⟨b⟩⟩
80- have : φ.Evalf f ∨ ∃ ψ, ∼ψ ∈ Γ ∧ ψ.Evalf f := by simpa using b.sound f
75+ variable {T : Theory L}
76+
77+ theorem Theory.Proof.sound_proposition {M : Type *} [s : Structure L M] [Nonempty M] :
78+ T ⊢ φ → M↓[L] ⊧* T → φ.Realize M := fun b H ↦ by
79+ rcases Theory.Proof.provable_iff.mp b with ⟨Γ, hΓ, ⟨b⟩⟩
80+ have : Inhabited M := Classical.inhabited_of_nonempty inferInstance
81+ let f : ℕ → M := fun _ ↦ default
82+ have : φ.Realize M ∨ ∃ ψ, ∼ψ ∈ Sequent.embed Γ ∧ ψ.Evalf f := by simpa using b.sound f
8183 rcases this with (h | ⟨ψ, hψ, h⟩)
8284 · assumption
83- · have : ¬ψ.Evalf f := by
84- have := by simpa [models_iff] using H.models _ (φ := (∼ψ).univCl) (by grind only [Schema.mem_uniClosure])
85- exact this f
85+ · have : ∃ χ, ∼χ ∈ Γ ∧ ↑χ = ψ := by
86+ have : ∃ χ ∈ Γ, χ = ∼ψ := by simpa [Sequent.embed] using hψ
87+ rcases this with ⟨χ, hχ, e⟩
88+ refine ⟨∼χ, by simpa using hχ, by simp [e]⟩
89+ rcases this with ⟨χ, hχ, rfl⟩
90+ have : χ.Realize M := by simpa using h
91+ have : ¬χ.Realize M := by
92+ simpa [models_iff] using H.models _ (hΓ _ hχ)
8693 contradiction
8794
88- theorem Schema.sound_proposition' :
89- 𝔖 ⊢ φ → (𝔖 : Theory L) ⊨[Struc.{v, u} L] φ.univCl := fun b s hS ↦ by
95+ theorem Theory.Proof.sound {φ : Sentence L} :
96+ T ⊢ φ → T ⊨[Struc.{v, u} L] φ := fun b s hS ↦ by
9097 simpa [struc_models_iff_models (s := s), models_iff]
91- using Schema.sound_proposition b hS
92-
93- theorem Schema.sound_sentence {σ : Sentence L} :
94- 𝔖 ⊢ ↑σ → (𝔖 : Theory L) ⊨[Struc.{v, u} L] σ := fun b ↦ by
95- simpa using Schema.sound_proposition' b
98+ using Theory.Proof.sound_proposition b hS
9699
97- theorem Schema.smallSound_sentence {σ : Sentence L} : 𝔖 ⊢ ↑σ → (𝔖 : Theory L) ⊨ σ := Schema.sound_sentence
100+ theorem Theory.Proof.sound_small : T ⊢ φ → T ⊨ φ := Theory.Proof.sound
98101
99- instance sound (𝔖 : Schema L) :
100- Sound (Entailment.pullback 𝔖 ((↑·) : Sentence L → Proposition L)) (Semantics.models (Struc.{v, u} L) 𝔖) :=
101- ⟨Schema.sound_sentence⟩
102+ instance sound (T : Theory L) : Sound T (Semantics.models (Struc.{v, u} L) T) := ⟨Theory.Proof.sound⟩
102103
103- lemma models_of_subtheory {𝔖 𝔗 : Schema L} [𝔖 ⪯ 𝔗] {M : Type *} [Structure L M] [Nonempty M] : M↓[L] ⊧* ↑↑𝔗 → M↓[L] ⊧* ↑↑𝔖 :=
104- fun hM ↦ ⟨fun {σ} hσ ↦ by
105- rcases show ∃ φ ∈ 𝔖, univCl φ = σ by simpa using hσ with ⟨φ, hφ, rfl⟩
106- have : 𝔖 ⪯ 𝔗 := inferInstance
107- have : 𝔗 ⊢ φ := this.pbl (Entailment.by_axm hφ)
108- exact Schema.sound_proposition' this hM⟩
104+ lemma models_of_subtheory {T U : Theory L} [T ⪯ U] {M : Type *} [Structure L M] [Nonempty M] : M↓[L] ⊧* U → M↓[L] ⊧* T :=
105+ fun hM ↦ ⟨fun {φ} hφ ↦ by
106+ have : T ⪯ U := inferInstance
107+ have : U ⊢ φ := this.pbl (Entailment.by_axm hφ)
108+ exact Theory.Proof.sound this hM⟩
109109
110- lemma consistent_of_satisfiable (h : Semantics.Satisfiable (Struc.{v, u} L) ↑↑𝔖 ) : Entailment.Consistent 𝔖 :=
111- Entailment.Pullback.consistent <| Sound.consistent_of_satisfiable (𝓢 := Entailment.pullback 𝔖 ((↑·) : Sentence L → Proposition L)) h
110+ lemma consistent_of_satisfiable (h : Semantics.Satisfiable (Struc.{v, u} L) T ) : Entailment.Consistent T :=
111+ Sound.consistent_of_satisfiable h
112112
113- lemma consistent_of_model (𝔖 : Schema L) (M : Type *) [Structure L M] [Nonempty M] [hM : M↓[L] ⊧* ↑↑𝔖 ] :
114- Entailment.Consistent 𝔖 := consistent_of_satisfiable ⟨M↓[L], hM⟩
113+ lemma consistent_of_model (T : Theory L) (M : Type *) [Structure L M] [Nonempty M] [hM : M↓[L] ⊧* T ] :
114+ Entailment.Consistent T := consistent_of_satisfiable ⟨M↓[L], hM⟩
115115
116- lemma unprovable_of_countermodel {M : Type *} [Structure L M] [Nonempty M] [hM : M↓[L] ⊧* ↑↑𝔖 ] {σ } : M↓[L] ⊭ σ → 𝔖 ⊬ ↑σ := by
116+ lemma unprovable_of_countermodel {M : Type *} [Structure L M] [Nonempty M] [hM : M↓[L] ⊧* T ] {φ } : M↓[L] ⊭ φ → T ⊬ φ := by
117117 contrapose!; intro h
118- exact Schema.sound_sentence h hM
118+ exact Theory.Proof.sound h hM
119119
120- lemma models_of_provable {M : Type *} [Nonempty M] [Structure L M] (hT : M↓[L] ⊧* ↑↑𝔖 ) {σ : Sentence L} (h : 𝔖 ⊢ ↑σ ) :
121- M↓[L] ⊧ σ := consequence_iff.mp (Schema.sound_sentence h) M inferInstance
120+ lemma models_of_provable {M : Type *} [Nonempty M] [Structure L M] (hT : M↓[L] ⊧* ↑↑T ) {φ : Sentence L} (h : T ⊢ φ ) :
121+ M↓[L] ⊧ φ := consequence_iff.mp (Theory.Proof.sound h) M inferInstance
122122
123123end sound
124124
0 commit comments