internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
⊢ (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r) →
    ∀ (e_1 : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
        (Eval s e_1 Empty.elim) (ι.rel r)
Tactic:
intro h
Proof state after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
⊢ ∀ (e_1 : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
      (Eval s e_1 Empty.elim) (ι.rel r)
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
⊢ ∀ (e_1 : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
      (Eval s e_1 Empty.elim) (ι.rel r)
Tactic:
intro l H
Proof state after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ (Eval s l Empty.elim) (ι.rel r)
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ (Eval s l Empty.elim) (ι.rel r)
Tactic:
have : l = fun i ↦ (Semiterm.valbm (ι.Sub M) e (v i)).val := funext fun i ↦ by
  let z : ι.Sub M := ⟨l i, (H i).1⟩
  have : Evalbm M (z :> fun i ↦ e i) (ι.varEquals (v i)) := (H i).2
  exact congr_arg Subtype.val (eval_varEquals_iff.mp this)
Proof state after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
this : l = fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))
⊢ (Eval s l Empty.elim) (ι.rel r)
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
this : l = fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))
⊢ (Eval s l Empty.elim) (ι.rel r)
Tactic:
rcases this
Proof state after:
case mpr.refl
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
H :
  ∀ (i : Fin k),
    (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i]) ι.domain ∧
      (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ (Eval s (fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) Empty.elim) (ι.rel r)
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
case mpr.refl
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
H :
  ∀ (i : Fin k),
    (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i]) ι.domain ∧
      (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ (Eval s (fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) Empty.elim) (ι.rel r)
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
Tactic:
let z : ι.Sub M := ⟨l i, (H i).1⟩
Proof state after:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
Tactic:
have : Evalbm M (z :> fun i ↦ e i) (ι.varEquals (v i)) := (H i).2
Proof state after:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
this : (Evalbm M (↑z :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
this : (Evalbm M (↑z :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
Tactic:
exact congr_arg Subtype.val (eval_varEquals_iff.mp this)
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
p : Semisentence L' n
e : Fin n → ι.Sub M
⊢ (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
Tactic:
induction p using Semiformula.rec'
  <;> simp [*, Matrix.constant_eq_singleton, eval_substs, eval_translationRel_iff, eval_rel, eval_nrel]
Proof state after:
case hall
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n n✝ : ℕ
p✝ : Semiformula L' Empty (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p✝) ↔ (Evalbm (ι.Sub M) e) p✝
e : Fin n✝ → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p✝)) ↔
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p✝

case hex
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n n✝ : ℕ
p✝ : Semiformula L' Empty (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p✝) ↔ (Evalbm (ι.Sub M) e) p✝
e : Fin n✝ → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p✝)) ↔
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p✝
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) ↔
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Tactic:
constructor
Proof state after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) →
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p

case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p) →
    ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) →
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Tactic:
intro h x hx
Proof state after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
x : M
hx : ι.Dom x
⊢ (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
x : M
hx : ι.Dom x
⊢ (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
Tactic:
exact ih.mp (by simpa [Matrix.comp_vecCons'] using h x hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
x : M
hx : ι.Dom x
⊢ (Evalbm M fun i => ↑((⟨x, hx⟩ :> e) i)) (ι.translation p)
Tactic:
simpa [Matrix.comp_vecCons'] using h x hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p) →
    ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
intro h x hx
Proof state after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
⊢ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
⊢ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
simpa [Matrix.comp_vecCons'] using ih.mpr (h x hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) ↔
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Tactic:
constructor
Proof state after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) →
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p

case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p) →
    ∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) →
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Tactic:
rintro ⟨x, hx, h⟩
Proof state after:
case mp.intro.intro
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
h : (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
⊢ ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
case mp.intro.intro
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
h : (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
⊢ ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Tactic:
refine ⟨x, hx, ih.mp (by simpa [Matrix.comp_vecCons'] using h)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
h : (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
⊢ (Evalbm M fun i => ↑((⟨x, hx⟩ :> e) i)) (ι.translation p)
Tactic:
simpa [Matrix.comp_vecCons'] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p) →
    ∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
intro ⟨x, hx, h⟩
Proof state after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : ι.Dom x
h : (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
⊢ ∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : ι.Dom x
h : (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
⊢ ∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
refine ⟨x, hx, by simpa [Matrix.comp_vecCons'] using ih.mpr h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translation_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : ι.Dom x
h : (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
⊢ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
simpa [Matrix.comp_vecCons'] using ih.mpr h
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.models_translation_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
σ : Sentence L'
⊢ M ⊧ₘ ι.translation σ ↔ ι.Sub M ⊧ₘ σ
Tactic:
simp [models_iff, ←eval_translation_iff, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.provable_iff_of_consistent_of_complete
Proof state before:
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
⊢ T ⊢! σ → ¬T ⊢! ~σ
Tactic:
rintro ⟨b₁⟩ ⟨b₂⟩
Proof state after:
case intro.intro
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
b₁ : T ⊢ σ
b₂ : T ⊢ ~σ
⊢ False
Theorem: LO.FirstOrder.provable_iff_of_consistent_of_complete
Proof state before:
case intro.intro
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
b₁ : T ⊢ σ
b₂ : T ⊢ ~σ
⊢ False
Tactic:
exact (Gentzen.inconsistent_of_provable_and_refutable b₁ b₂).not_con consis
Proof state after:
no goals
Theorem: LO.FirstOrder.provable_iff_of_consistent_of_complete
Proof state before:
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
⊢ ¬T ⊢! ~σ → T ⊢! σ
Tactic:
intro h
Proof state after:
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
h : ¬T ⊢! ~σ
⊢ T ⊢! σ