Skip to content

Commit 0c8f6eb

Browse files
awainverseawainverse
committed
chore(ModelTheory/Complexity): move quantifier complexity into a new file (#15275)
Several important files in the model theory library touch on quantifier complexity of formulas, an idea that is not yet used for anything else in `mathlib`. This PR moves all quantifier complexity content to a new file, `ModelTheory/Complexity` and improves the documentation of these concepts. This will hopefully make these basic files more legible and easier to refactor. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
1 parent 4235d67 commit 0c8f6eb

File tree

5 files changed

+326
-282
lines changed

5 files changed

+326
-282
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3257,6 +3257,7 @@ import Mathlib.ModelTheory.Algebra.Ring.Basic
32573257
import Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
32583258
import Mathlib.ModelTheory.Basic
32593259
import Mathlib.ModelTheory.Bundled
3260+
import Mathlib.ModelTheory.Complexity
32603261
import Mathlib.ModelTheory.Definability
32613262
import Mathlib.ModelTheory.DirectLimit
32623263
import Mathlib.ModelTheory.ElementaryMaps

‎Mathlib/ModelTheory/Complexity.lean‎

Lines changed: 325 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,325 @@
1+
/-
2+
Copyright (c) 2021 Aaron Anderson. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Aaron Anderson
5+
-/
6+
import Mathlib.ModelTheory.Satisfiability
7+
8+
/-!
9+
# Quantifier Complexity
10+
11+
This file defines quantifier complexity of first-order formulas, and constructs prenex normal forms.
12+
13+
## Main Definitions
14+
15+
* `FirstOrder.Language.BoundedFormula.IsAtomic` defines atomic formulas - those which are
16+
constructed only from terms and relations.
17+
* `FirstOrder.Language.BoundedFormula.IsQF` defines quantifier-free formulas - those which are
18+
constructed only from atomic formulas and boolean operations.
19+
* `FirstOrder.Language.BoundedFormula.IsPrenex` defines when a formula is in prenex normal form -
20+
when it consists of a series of quantifiers applied to a quantifier-free formula.
21+
* `FirstOrder.Language.BoundedFormula.toPrenex` constructs a prenex normal form of a given formula.
22+
23+
24+
## Main Results
25+
26+
* `FirstOrder.Language.BoundedFormula.realize_toPrenex` shows that the prenex normal form of a
27+
formula has the same realization as the original formula.
28+
29+
-/
30+
31+
universe u v w u' v'
32+
33+
namespace FirstOrder
34+
35+
namespace Language
36+
37+
variable {L : Language.{u, v}} {L' : Language}
38+
variable {M : Type w} {N P : Type*} [L.Structure M] [L.Structure N] [L.Structure P]
39+
variable {α : Type u'} {β : Type v'} {γ : Type*}
40+
variable {n l : ℕ} {φ ψ : L.BoundedFormula α l} {θ : L.BoundedFormula α l.succ}
41+
variable {v : α → M} {xs : Fin l → M}
42+
43+
open FirstOrder Structure Fin
44+
45+
namespace BoundedFormula
46+
47+
/-- An atomic formula is either equality or a relation symbol applied to terms.
48+
Note that `⊥` and `⊤` are not considered atomic in this convention. -/
49+
inductive IsAtomic : L.BoundedFormula α n → Prop
50+
| equal (t₁ t₂ : L.Term (α ⊕ (Fin n))) : IsAtomic (t₁.bdEqual t₂)
51+
| rel {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ (Fin n))) :
52+
IsAtomic (R.boundedFormula ts)
53+
54+
theorem not_all_isAtomic (φ : L.BoundedFormula α (n + 1)) : ¬φ.all.IsAtomic := fun con => by
55+
cases con
56+
57+
theorem not_ex_isAtomic (φ : L.BoundedFormula α (n + 1)) : ¬φ.ex.IsAtomic := fun con => by cases con
58+
59+
theorem IsAtomic.relabel {m : ℕ} {φ : L.BoundedFormula α m} (h : φ.IsAtomic)
60+
(f : α → β ⊕ (Fin n)) : (φ.relabel f).IsAtomic :=
61+
IsAtomic.recOn h (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _
62+
63+
theorem IsAtomic.liftAt {k m : ℕ} (h : IsAtomic φ) : (φ.liftAt k m).IsAtomic :=
64+
IsAtomic.recOn h (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _
65+
66+
theorem IsAtomic.castLE {h : l ≤ n} (hφ : IsAtomic φ) : (φ.castLE h).IsAtomic :=
67+
IsAtomic.recOn hφ (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _
68+
69+
/-- A quantifier-free formula is a formula defined without quantifiers. These are all equivalent
70+
to boolean combinations of atomic formulas. -/
71+
inductive IsQF : L.BoundedFormula α n → Prop
72+
| falsum : IsQF falsum
73+
| of_isAtomic {φ} (h : IsAtomic φ) : IsQF φ
74+
| imp {φ₁ φ₂} (h₁ : IsQF φ₁) (h₂ : IsQF φ₂) : IsQF (φ₁.imp φ₂)
75+
76+
theorem IsAtomic.isQF {φ : L.BoundedFormula α n} : IsAtomic φ → IsQF φ :=
77+
IsQF.of_isAtomic
78+
79+
theorem isQF_bot : IsQF (⊥ : L.BoundedFormula α n) :=
80+
IsQF.falsum
81+
82+
theorem IsQF.not {φ : L.BoundedFormula α n} (h : IsQF φ) : IsQF φ.not :=
83+
h.imp isQF_bot
84+
85+
theorem IsQF.relabel {m : ℕ} {φ : L.BoundedFormula α m} (h : φ.IsQF) (f : α → β ⊕ (Fin n)) :
86+
(φ.relabel f).IsQF :=
87+
IsQF.recOn h isQF_bot (fun h => (h.relabel f).isQF) fun _ _ h1 h2 => h1.imp h2
88+
89+
theorem IsQF.liftAt {k m : ℕ} (h : IsQF φ) : (φ.liftAt k m).IsQF :=
90+
IsQF.recOn h isQF_bot (fun ih => ih.liftAt.isQF) fun _ _ ih1 ih2 => ih1.imp ih2
91+
92+
theorem IsQF.castLE {h : l ≤ n} (hφ : IsQF φ) : (φ.castLE h).IsQF :=
93+
IsQF.recOn hφ isQF_bot (fun ih => ih.castLE.isQF) fun _ _ ih1 ih2 => ih1.imp ih2
94+
95+
theorem not_all_isQF (φ : L.BoundedFormula α (n + 1)) : ¬φ.all.IsQF := fun con => by
96+
cases' con with _ con
97+
exact φ.not_all_isAtomic con
98+
99+
theorem not_ex_isQF (φ : L.BoundedFormula α (n + 1)) : ¬φ.ex.IsQF := fun con => by
100+
cases' con with _ con _ _ con
101+
· exact φ.not_ex_isAtomic con
102+
· exact not_all_isQF _ con
103+
104+
/-- Indicates that a bounded formula is in prenex normal form - that is, it consists of quantifiers
105+
applied to a quantifier-free formula. -/
106+
inductive IsPrenex : ∀ {n}, L.BoundedFormula α n → Prop
107+
| of_isQF {n} {φ : L.BoundedFormula α n} (h : IsQF φ) : IsPrenex φ
108+
| all {n} {φ : L.BoundedFormula α (n + 1)} (h : IsPrenex φ) : IsPrenex φ.all
109+
| ex {n} {φ : L.BoundedFormula α (n + 1)} (h : IsPrenex φ) : IsPrenex φ.ex
110+
111+
theorem IsQF.isPrenex {φ : L.BoundedFormula α n} : IsQF φ → IsPrenex φ :=
112+
IsPrenex.of_isQF
113+
114+
theorem IsAtomic.isPrenex {φ : L.BoundedFormula α n} (h : IsAtomic φ) : IsPrenex φ :=
115+
h.isQF.isPrenex
116+
117+
theorem IsPrenex.induction_on_all_not {P : ∀ {n}, L.BoundedFormula α n → Prop}
118+
{φ : L.BoundedFormula α n} (h : IsPrenex φ)
119+
(hq : ∀ {m} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ)
120+
(ha : ∀ {m} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all)
121+
(hn : ∀ {m} {ψ : L.BoundedFormula α m}, P ψ → P ψ.not) : P φ :=
122+
IsPrenex.recOn h hq (fun _ => ha) fun _ ih => hn (ha (hn ih))
123+
124+
theorem IsPrenex.relabel {m : ℕ} {φ : L.BoundedFormula α m} (h : φ.IsPrenex)
125+
(f : α → β ⊕ (Fin n)) : (φ.relabel f).IsPrenex :=
126+
IsPrenex.recOn h (fun h => (h.relabel f).isPrenex) (fun _ h => by simp [h.all])
127+
fun _ h => by simp [h.ex]
128+
129+
theorem IsPrenex.castLE (hφ : IsPrenex φ) : ∀ {n} {h : l ≤ n}, (φ.castLE h).IsPrenex :=
130+
IsPrenex.recOn (motive := @fun l φ _ => ∀ (n : ℕ) (h : l ≤ n), (φ.castLE h).IsPrenex) hφ
131+
(@fun _ _ ih _ _ => ih.castLE.isPrenex)
132+
(@fun _ _ _ ih _ _ => (ih _ _).all)
133+
(@fun _ _ _ ih _ _ => (ih _ _).ex) _ _
134+
135+
theorem IsPrenex.liftAt {k m : ℕ} (h : IsPrenex φ) : (φ.liftAt k m).IsPrenex :=
136+
IsPrenex.recOn h (fun ih => ih.liftAt.isPrenex) (fun _ ih => ih.castLE.all)
137+
fun _ ih => ih.castLE.ex
138+
139+
-- Porting note: universes in different order
140+
/-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`.
141+
If `φ` is quantifier-free and `ψ` is in prenex normal form, then `φ.toPrenexImpRight ψ`
142+
is a prenex normal form for `φ.imp ψ`. -/
143+
def toPrenexImpRight : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
144+
| n, φ, BoundedFormula.ex ψ => ((φ.liftAt 1 n).toPrenexImpRight ψ).ex
145+
| n, φ, all ψ => ((φ.liftAt 1 n).toPrenexImpRight ψ).all
146+
| _n, φ, ψ => φ.imp ψ
147+
148+
theorem IsQF.toPrenexImpRight {φ : L.BoundedFormula α n} :
149+
∀ {ψ : L.BoundedFormula α n}, IsQF ψ → φ.toPrenexImpRight ψ = φ.imp ψ
150+
| _, IsQF.falsum => rfl
151+
| _, IsQF.of_isAtomic (IsAtomic.equal _ _) => rfl
152+
| _, IsQF.of_isAtomic (IsAtomic.rel _ _) => rfl
153+
| _, IsQF.imp IsQF.falsum _ => rfl
154+
| _, IsQF.imp (IsQF.of_isAtomic (IsAtomic.equal _ _)) _ => rfl
155+
| _, IsQF.imp (IsQF.of_isAtomic (IsAtomic.rel _ _)) _ => rfl
156+
| _, IsQF.imp (IsQF.imp _ _) _ => rfl
157+
158+
theorem isPrenex_toPrenexImpRight {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ) (hψ : IsPrenex ψ) :
159+
IsPrenex (φ.toPrenexImpRight ψ) := by
160+
induction' hψ with _ _ hψ _ _ _ ih1 _ _ _ ih2
161+
· rw [hψ.toPrenexImpRight]
162+
exact (hφ.imp hψ).isPrenex
163+
· exact (ih1 hφ.liftAt).all
164+
· exact (ih2 hφ.liftAt).ex
165+
166+
-- Porting note: universes in different order
167+
/-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`.
168+
If `φ` and `ψ` are in prenex normal form, then `φ.toPrenexImp ψ`
169+
is a prenex normal form for `φ.imp ψ`. -/
170+
def toPrenexImp : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
171+
| n, BoundedFormula.ex φ, ψ => (φ.toPrenexImp (ψ.liftAt 1 n)).all
172+
| n, all φ, ψ => (φ.toPrenexImp (ψ.liftAt 1 n)).ex
173+
| _, φ, ψ => φ.toPrenexImpRight ψ
174+
175+
theorem IsQF.toPrenexImp :
176+
∀ {φ ψ : L.BoundedFormula α n}, φ.IsQF → φ.toPrenexImp ψ = φ.toPrenexImpRight ψ
177+
| _, _, IsQF.falsum => rfl
178+
| _, _, IsQF.of_isAtomic (IsAtomic.equal _ _) => rfl
179+
| _, _, IsQF.of_isAtomic (IsAtomic.rel _ _) => rfl
180+
| _, _, IsQF.imp IsQF.falsum _ => rfl
181+
| _, _, IsQF.imp (IsQF.of_isAtomic (IsAtomic.equal _ _)) _ => rfl
182+
| _, _, IsQF.imp (IsQF.of_isAtomic (IsAtomic.rel _ _)) _ => rfl
183+
| _, _, IsQF.imp (IsQF.imp _ _) _ => rfl
184+
185+
theorem isPrenex_toPrenexImp {φ ψ : L.BoundedFormula α n} (hφ : IsPrenex φ) (hψ : IsPrenex ψ) :
186+
IsPrenex (φ.toPrenexImp ψ) := by
187+
induction' hφ with _ _ hφ _ _ _ ih1 _ _ _ ih2
188+
· rw [hφ.toPrenexImp]
189+
exact isPrenex_toPrenexImpRight hφ hψ
190+
· exact (ih1 hψ.liftAt).ex
191+
· exact (ih2 hψ.liftAt).all
192+
193+
-- Porting note: universes in different order
194+
/-- For any bounded formula `φ`, `φ.toPrenex` is a semantically-equivalent formula in prenex normal
195+
form. -/
196+
def toPrenex : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n
197+
| _, falsum => ⊥
198+
| _, equal t₁ t₂ => t₁.bdEqual t₂
199+
| _, rel R ts => rel R ts
200+
| _, imp f₁ f₂ => f₁.toPrenex.toPrenexImp f₂.toPrenex
201+
| _, all f => f.toPrenex.all
202+
203+
theorem toPrenex_isPrenex (φ : L.BoundedFormula α n) : φ.toPrenex.IsPrenex :=
204+
BoundedFormula.recOn φ isQF_bot.isPrenex (fun _ _ => (IsAtomic.equal _ _).isPrenex)
205+
(fun _ _ => (IsAtomic.rel _ _).isPrenex) (fun _ _ h1 h2 => isPrenex_toPrenexImp h1 h2)
206+
fun _ => IsPrenex.all
207+
208+
variable [Nonempty M]
209+
210+
theorem realize_toPrenexImpRight {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ) (hψ : IsPrenex ψ)
211+
{v : α → M} {xs : Fin n → M} :
212+
(φ.toPrenexImpRight ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs := by
213+
induction' hψ with _ _ hψ _ _ _hψ ih _ _ _hψ ih
214+
· rw [hψ.toPrenexImpRight]
215+
· refine _root_.trans (forall_congr' fun _ => ih hφ.liftAt) ?_
216+
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
217+
exact ⟨fun h1 a h2 => h1 h2 a, fun h1 h2 a => h1 a h2⟩
218+
· unfold toPrenexImpRight
219+
rw [realize_ex]
220+
refine _root_.trans (exists_congr fun _ => ih hφ.liftAt) ?_
221+
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_ex]
222+
refine ⟨?_, fun h' => ?_⟩
223+
· rintro ⟨a, ha⟩ h
224+
exact ⟨a, ha h⟩
225+
· by_cases h : φ.Realize v xs
226+
· obtain ⟨a, ha⟩ := h' h
227+
exact ⟨a, fun _ => ha⟩
228+
· inhabit M
229+
exact ⟨default, fun h'' => (h h'').elim⟩
230+
231+
theorem realize_toPrenexImp {φ ψ : L.BoundedFormula α n} (hφ : IsPrenex φ) (hψ : IsPrenex ψ)
232+
{v : α → M} {xs : Fin n → M} : (φ.toPrenexImp ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs := by
233+
revert ψ
234+
induction' hφ with _ _ hφ _ _ _hφ ih _ _ _hφ ih <;> intro ψ hψ
235+
· rw [hφ.toPrenexImp]
236+
exact realize_toPrenexImpRight hφ hψ
237+
· unfold toPrenexImp
238+
rw [realize_ex]
239+
refine _root_.trans (exists_congr fun _ => ih hψ.liftAt) ?_
240+
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
241+
refine ⟨?_, fun h' => ?_⟩
242+
· rintro ⟨a, ha⟩ h
243+
exact ha (h a)
244+
· by_cases h : ψ.Realize v xs
245+
· inhabit M
246+
exact ⟨default, fun _h'' => h⟩
247+
· obtain ⟨a, ha⟩ := not_forall.1 (h ∘ h')
248+
exact ⟨a, fun h => (ha h).elim⟩
249+
· refine _root_.trans (forall_congr' fun _ => ih hψ.liftAt) ?_
250+
simp
251+
252+
@[simp]
253+
theorem realize_toPrenex (φ : L.BoundedFormula α n) {v : α → M} :
254+
∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs := by
255+
induction' φ with _ _ _ _ _ _ _ _ _ f1 f2 h1 h2 _ _ h
256+
· exact Iff.rfl
257+
· exact Iff.rfl
258+
· exact Iff.rfl
259+
· intros
260+
rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
261+
realize_imp, h1, h2]
262+
· intros
263+
rw [realize_all, toPrenex, realize_all]
264+
exact forall_congr' fun a => h
265+
266+
theorem IsQF.induction_on_sup_not {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n}
267+
(h : IsQF φ) (hf : P (⊥ : L.BoundedFormula α n))
268+
(ha : ∀ ψ : L.BoundedFormula α n, IsAtomic ψ → P ψ)
269+
(hsup : ∀ {φ₁ φ₂}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)) (hnot : ∀ {φ}, P φ → P φ.not)
270+
(hse :
271+
∀ {φ₁ φ₂ : L.BoundedFormula α n}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :
272+
P φ :=
273+
IsQF.recOn h hf @(ha) fun {φ₁ φ₂} _ _ h1 h2 =>
274+
(hse (φ₁.imp_semanticallyEquivalent_not_sup φ₂)).2 (hsup (hnot h1) h2)
275+
276+
theorem IsQF.induction_on_inf_not {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n}
277+
(h : IsQF φ) (hf : P (⊥ : L.BoundedFormula α n))
278+
(ha : ∀ ψ : L.BoundedFormula α n, IsAtomic ψ → P ψ)
279+
(hinf : ∀ {φ₁ φ₂}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)) (hnot : ∀ {φ}, P φ → P φ.not)
280+
(hse :
281+
∀ {φ₁ φ₂ : L.BoundedFormula α n}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :
282+
P φ :=
283+
h.induction_on_sup_not hf ha
284+
(fun {φ₁ φ₂} h1 h2 =>
285+
(hse (φ₁.sup_semanticallyEquivalent_not_inf_not φ₂)).2 (hnot (hinf (hnot h1) (hnot h2))))
286+
(fun {_} => hnot) fun {_ _} => hse
287+
288+
theorem semanticallyEquivalent_toPrenex (φ : L.BoundedFormula α n) :
289+
(∅ : L.Theory).SemanticallyEquivalent φ φ.toPrenex := fun M v xs => by
290+
rw [realize_iff, realize_toPrenex]
291+
292+
theorem induction_on_all_ex {P : ∀ {m}, L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n)
293+
(hqf : ∀ {m} {ψ : L.BoundedFormula α m}, IsQF ψ → P ψ)
294+
(hall : ∀ {m} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all)
295+
(hex : ∀ {m} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex)
296+
(hse : ∀ {m} {φ₁ φ₂ : L.BoundedFormula α m},
297+
Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :
298+
P φ := by
299+
suffices h' : ∀ {m} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ from
300+
(hse φ.semanticallyEquivalent_toPrenex).2 (h' φ.toPrenex_isPrenex)
301+
intro m φ hφ
302+
induction' hφ with _ _ hφ _ _ _ hφ _ _ _ hφ
303+
· exact hqf hφ
304+
· exact hall hφ
305+
· exact hex hφ
306+
307+
theorem induction_on_exists_not {P : ∀ {m}, L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n)
308+
(hqf : ∀ {m} {ψ : L.BoundedFormula α m}, IsQF ψ → P ψ)
309+
(hnot : ∀ {m} {φ : L.BoundedFormula α m}, P φ → P φ.not)
310+
(hex : ∀ {m} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex)
311+
(hse : ∀ {m} {φ₁ φ₂ : L.BoundedFormula α m},
312+
Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :
313+
P φ :=
314+
φ.induction_on_all_ex (fun {_ _} => hqf)
315+
(fun {_ φ} hφ => (hse φ.all_semanticallyEquivalent_not_ex_not).2 (hnot (hex (hnot hφ))))
316+
(fun {_ _} => hex) fun {_ _ _} => hse
317+
318+
end BoundedFormula
319+
320+
theorem Formula.isAtomic_graph (f : L.Functions n) : (Formula.graph f).IsAtomic :=
321+
BoundedFormula.IsAtomic.equal _ _
322+
323+
end Language
324+
325+
end FirstOrder

‎Mathlib/ModelTheory/Satisfiability.lean‎

Lines changed: 0 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -536,62 +536,6 @@ theorem inf_semanticallyEquivalent_not_sup_not :
536536

537537
end Formula
538538

539-
namespace BoundedFormula
540-
541-
theorem IsQF.induction_on_sup_not {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n}
542-
(h : IsQF φ) (hf : P (⊥ : L.BoundedFormula α n))
543-
(ha : ∀ ψ : L.BoundedFormula α n, IsAtomic ψ → P ψ)
544-
(hsup : ∀ {φ₁ φ₂}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)) (hnot : ∀ {φ}, P φ → P φ.not)
545-
(hse :
546-
∀ {φ₁ φ₂ : L.BoundedFormula α n}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :
547-
P φ :=
548-
IsQF.recOn h hf @(ha) fun {φ₁ φ₂} _ _ h1 h2 =>
549-
(hse (φ₁.imp_semanticallyEquivalent_not_sup φ₂)).2 (hsup (hnot h1) h2)
550-
551-
theorem IsQF.induction_on_inf_not {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n}
552-
(h : IsQF φ) (hf : P (⊥ : L.BoundedFormula α n))
553-
(ha : ∀ ψ : L.BoundedFormula α n, IsAtomic ψ → P ψ)
554-
(hinf : ∀ {φ₁ φ₂}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)) (hnot : ∀ {φ}, P φ → P φ.not)
555-
(hse :
556-
∀ {φ₁ φ₂ : L.BoundedFormula α n}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :
557-
P φ :=
558-
h.induction_on_sup_not hf ha
559-
(fun {φ₁ φ₂} h1 h2 =>
560-
(hse (φ₁.sup_semanticallyEquivalent_not_inf_not φ₂)).2 (hnot (hinf (hnot h1) (hnot h2))))
561-
(fun {_} => hnot) fun {_ _} => hse
562-
563-
theorem semanticallyEquivalent_toPrenex (φ : L.BoundedFormula α n) :
564-
(∅ : L.Theory).SemanticallyEquivalent φ φ.toPrenex := fun M v xs => by
565-
rw [realize_iff, realize_toPrenex]
566-
567-
theorem induction_on_all_ex {P : ∀ {m}, L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n)
568-
(hqf : ∀ {m} {ψ : L.BoundedFormula α m}, IsQF ψ → P ψ)
569-
(hall : ∀ {m} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all)
570-
(hex : ∀ {m} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex)
571-
(hse : ∀ {m} {φ₁ φ₂ : L.BoundedFormula α m},
572-
Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :
573-
P φ := by
574-
suffices h' : ∀ {m} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ from
575-
(hse φ.semanticallyEquivalent_toPrenex).2 (h' φ.toPrenex_isPrenex)
576-
intro m φ hφ
577-
induction' hφ with _ _ hφ _ _ _ hφ _ _ _ hφ
578-
· exact hqf hφ
579-
· exact hall hφ
580-
· exact hex hφ
581-
582-
theorem induction_on_exists_not {P : ∀ {m}, L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n)
583-
(hqf : ∀ {m} {ψ : L.BoundedFormula α m}, IsQF ψ → P ψ)
584-
(hnot : ∀ {m} {φ : L.BoundedFormula α m}, P φ → P φ.not)
585-
(hex : ∀ {m} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex)
586-
(hse : ∀ {m} {φ₁ φ₂ : L.BoundedFormula α m},
587-
Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :
588-
P φ :=
589-
φ.induction_on_all_ex (fun {_ _} => hqf)
590-
(fun {_ φ} hφ => (hse φ.all_semanticallyEquivalent_not_ex_not).2 (hnot (hex (hnot hφ))))
591-
(fun {_ _} => hex) fun {_ _ _} => hse
592-
593-
end BoundedFormula
594-
595539
end Language
596540

597541
end FirstOrder

0 commit comments

Comments
 (0)