Theorem: canonicalSatisfaction (Fine/SystemB/CanonicalModel.lean)

State before:
⊢ ∀ {t : Th} {f : Form}, t⊨f ↔ f ∈ ↑t
Tactic:
intros t f
State after:
t : Th
f : Form
⊢ t⊨f ↔ f ∈ ↑t

State before:
t : Th
f : Form
⊢ t⊨f ↔ f ∈ ↑t
Tactic:
cases f
State after:
case atom
t : Th
a✝ : ℕ
⊢ t⊨#a✝ ↔ #a✝ ∈ ↑t

case neg
t : Th
a✝ : Form
⊢ t⊨~a✝ ↔ ~a✝ ∈ ↑t

case and
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹&a✝ ↔ a✝¹&a✝ ∈ ↑t

case or
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹¦a✝ ↔ a✝¹¦a✝ ∈ ↑t

case impl
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹⊃a✝ ↔ a✝¹⊃a✝ ∈ ↑t

State before:
case atom
t : Th
a✝ : ℕ
⊢ t⊨#a✝ ↔ #a✝ ∈ ↑t

case neg
t : Th
a✝ : Form
⊢ t⊨~a✝ ↔ ~a✝ ∈ ↑t

case and
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹&a✝ ↔ a✝¹&a✝ ∈ ↑t

case or
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹¦a✝ ↔ a✝¹¦a✝ ∈ ↑t

case impl
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹⊃a✝ ↔ a✝¹⊃a✝ ∈ ↑t
Tactic:
all_goals apply Iff.intro <;> intros h₁
State after:
case atom.mp
t : Th
a✝ : ℕ
h₁ : t⊨#a✝
⊢ #a✝ ∈ ↑t

case atom.mpr
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ↑t
⊢ t⊨#a✝

case neg.mp
t : Th
a✝ : Form
h₁ : t⊨~a✝
⊢ ~a✝ ∈ ↑t

case neg.mpr
t : Th
a✝ : Form
h₁ : ~a✝ ∈ ↑t
⊢ t⊨~a✝

case and.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹&a✝
⊢ a✝¹&a✝ ∈ ↑t

case and.mpr
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹&a✝ ∈ ↑t
⊢ t⊨a✝¹&a✝

case or.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹¦a✝
⊢ a✝¹¦a✝ ∈ ↑t

case or.mpr
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹¦a✝ ∈ ↑t
⊢ t⊨a✝¹¦a✝

case impl.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹⊃a✝
⊢ a✝¹⊃a✝ ∈ ↑t

case impl.mpr
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ↑t
⊢ t⊨a✝¹⊃a✝

State before:
t : Th
a✝ : ℕ
h₁ : t⊨#a✝
⊢ #a✝ ∈ ↑t
Tactic:
case atom.mp => exact h₁
State after:
no goals

State before:
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ↑t
⊢ t⊨#a✝
Tactic:
case atom.mpr => exact h₁
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f&g
⊢ f&g ∈ ↑t
Tactic:
case and.mp f g => 
    have l₁ : f ∈ t := canonicalSatisfaction.mp h₁.left
    have l₂ : g ∈ t := canonicalSatisfaction.mp h₁.right
    exact t.property.mpr ⟨BProof.adj (BProof.ax l₁) (BProof.ax l₂)⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
⊢ t⊨f&g
Tactic:
case and.mpr f g =>
    have l₁ : t ⊨ f := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₁⟩
    have l₂ : t ⊨ g := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₂⟩
    exact ⟨l₁,l₂⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
⊢ f¦g ∈ ↑t
Tactic:
case or.mp f g =>
  rw [primeAnalysis]
  intros p h₂
  let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
  have l₁ := @h₁ pr h₂.right.left
  cases l₁
  case inl h₃ => 
    have l₂ := canonicalSatisfaction.mp h₃
    exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₁⟩
  case inr h₃ => 
    have l₂ := canonicalSatisfaction.mp h₃
    exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₂⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
⊢ t⊨f¦g
Tactic:
case or.mpr f g =>
  intros p h₂
  rw [primeAnalysis] at h₁
  have l₁ : f ¦ g ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
  have l₂ : f ∈ p.val.val ∨ g ∈ p.val.val := p.property l₁
  cases l₂
  case inl h₂ => exact Or.inl $ canonicalSatisfaction.mpr h₂
  case inr h₂ => exact Or.inr $ canonicalSatisfaction.mpr h₂
State after:
no goals

State before:
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ↑t
Tactic:
case neg.mp f => 
  rw [primeAnalysis]
  intros p h₂
  let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
  have l₁ := @h₁ pr h₂.right.left
  have l₂ := l₁ ∘ canonicalSatisfaction.mpr 
  apply byContradiction
  exact l₂
State after:
no goals

State before:
t : Th
f : Form
h₁ : ~f ∈ ↑t
⊢ t⊨~f
Tactic:
case neg.mpr f => 
  intros p h₂ h₃
  rw [primeAnalysis] at h₁
  have l₁ : ~f ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
  exact canonicalSatisfaction.mp h₃ l₁
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ f⊃g ∈ ↑t
Tactic:
case impl.mp f g =>
  apply byContradiction
  intros h₂
  let Δ : Th := ⟨▲{f}, generatedFormal {f}⟩
  have l₁ : ¬(g ∈ (formalApplicationFunction t Δ).val) := by
    intros h₃
    have ⟨q,⟨prf₁⟩,l₂⟩ := h₃
    have ⟨prf₂⟩ := t.property.mp l₂
    have prf₃ := BProof.mp prf₂ (BTheorem.hs prf₁.toTheorem BTheorem.taut)
    exact h₂ $ t.property.mpr ⟨prf₃⟩
  have l₂ : Δ ⊨ f := canonicalSatisfaction.mpr ⟨BProof.ax rfl⟩
  exact l₁ $ canonicalSatisfaction.mp (h₁ l₂)
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
⊢ t⊨f⊃g
Tactic:
case impl.mpr f g => 
  intros r h₂
  have l₁ := canonicalSatisfaction.mp h₂
  have l₂ : g ∈ (formalApplicationFunction t r).val := ⟨f, l₁, h₁⟩
  exact canonicalSatisfaction.mpr l₂
State after:
no goals

State before:
case impl
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹⊃a✝ ↔ a✝¹⊃a✝ ∈ ↑t
Tactic:
apply Iff.intro <;> intros h₁
State after:
case impl.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹⊃a✝
⊢ a✝¹⊃a✝ ∈ ↑t

case impl.mpr
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ↑t
⊢ t⊨a✝¹⊃a✝

State before:
t : Th
a✝ : ℕ
h₁ : t⊨#a✝
⊢ #a✝ ∈ ↑t
Tactic:
exact h₁
State after:
no goals

State before:
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ↑t
⊢ t⊨#a✝
Tactic:
exact h₁
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f&g
⊢ f&g ∈ ↑t
Tactic:
have l₁ : f ∈ t := canonicalSatisfaction.mp h₁.left
State after:
t : Th
f g : Form
h₁ : t⊨f&g
l₁ : f ∈ t
⊢ f&g ∈ ↑t

State before:
t : Th
f g : Form
h₁ : t⊨f&g
l₁ : f ∈ t
⊢ f&g ∈ ↑t
Tactic:
have l₂ : g ∈ t := canonicalSatisfaction.mp h₁.right
State after:
t : Th
f g : Form
h₁ : t⊨f&g
l₁ : f ∈ t
l₂ : g ∈ t
⊢ f&g ∈ ↑t

State before:
t : Th
f g : Form
h₁ : t⊨f&g
l₁ : f ∈ t
l₂ : g ∈ t
⊢ f&g ∈ ↑t
Tactic:
exact t.property.mpr ⟨BProof.adj (BProof.ax l₁) (BProof.ax l₂)⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
⊢ t⊨f&g
Tactic:
have l₁ : t ⊨ f := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₁⟩
State after:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
⊢ t⊨f&g

State before:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
⊢ t⊨f&g
Tactic:
have l₂ : t ⊨ g := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₂⟩
State after:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
l₂ : t⊨g
⊢ t⊨f&g

State before:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
l₂ : t⊨g
⊢ t⊨f&g
Tactic:
exact ⟨l₁,l₂⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
⊢ f¦g ∈ ↑t
Tactic:
rw [primeAnalysis]
State after:
t : Th
f g : Form
h₁ : t⊨f¦g
⊢ f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
⊢ f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
intros p h₂
State after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ f¦g ∈ p

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ f¦g ∈ p
Tactic:
let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
State after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
⊢ f¦g ∈ p

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
⊢ f¦g ∈ p
Tactic:
have l₁ := @h₁ pr h₂.right.left
State after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ↑pr⊨f ∨ ↑pr⊨g
⊢ f¦g ∈ p

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ↑pr⊨f ∨ ↑pr⊨g
⊢ f¦g ∈ p
Tactic:
cases l₁
State after:
case inl
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h✝ : ↑pr⊨f
⊢ f¦g ∈ p

case inr
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h✝ : ↑pr⊨g
⊢ f¦g ∈ p

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
⊢ f¦g ∈ p
Tactic:
case inl h₃ => 
  have l₂ := canonicalSatisfaction.mp h₃
  exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₁⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨g
⊢ f¦g ∈ p
Tactic:
case inr h₃ => 
  have l₂ := canonicalSatisfaction.mp h₃
  exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₂⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
⊢ f¦g ∈ p
Tactic:
have l₂ := canonicalSatisfaction.mp h₃
State after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
l₂ : f ∈ ↑↑pr
⊢ f¦g ∈ p

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
l₂ : f ∈ ↑↑pr
⊢ f¦g ∈ p
Tactic:
exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₁⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨g
⊢ f¦g ∈ p
Tactic:
have l₂ := canonicalSatisfaction.mp h₃
State after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨g
l₂ : g ∈ ↑↑pr
⊢ f¦g ∈ p

State before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨g
l₂ : g ∈ ↑↑pr
⊢ f¦g ∈ p
Tactic:
exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₂⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
⊢ t⊨f¦g
Tactic:
intros p h₂
State after:
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
rw [primeAnalysis] at h₁
State after:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
have l₁ : f ¦ g ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
State after:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
have l₂ : f ∈ p.val.val ∨ g ∈ p.val.val := p.property l₁
State after:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
l₂ : f ∈ ↑↑p ∨ g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
l₂ : f ∈ ↑↑p ∨ g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
cases l₂
State after:
case inl
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h✝ : f ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g

case inr
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h✝ : g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂✝ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h₂ : f ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
case inl h₂ => exact Or.inl $ canonicalSatisfaction.mpr h₂
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂✝ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h₂ : g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
case inr h₂ => exact Or.inr $ canonicalSatisfaction.mpr h₂
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂✝ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h₂ : f ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
exact Or.inl $ canonicalSatisfaction.mpr h₂
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂✝ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h₂ : g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
exact Or.inr $ canonicalSatisfaction.mpr h₂
State after:
no goals

State before:
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ↑t
Tactic:
rw [primeAnalysis]
State after:
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }

State before:
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
intros p h₂
State after:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ~f ∈ p

State before:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ~f ∈ p
Tactic:
let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
State after:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
⊢ ~f ∈ p

State before:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
⊢ ~f ∈ p
Tactic:
have l₁ := @h₁ pr h₂.right.left
State after:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
⊢ ~f ∈ p

State before:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
⊢ ~f ∈ p
Tactic:
have l₂ := l₁ ∘ canonicalSatisfaction.mpr
State after:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ~f ∈ p

State before:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ~f ∈ p
Tactic:
apply byContradiction
State after:
case h
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ¬~f ∈ p → False

State before:
case h
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ¬~f ∈ p → False
Tactic:
exact l₂
State after:
no goals

State before:
t : Th
f : Form
h₁ : ~f ∈ ↑t
⊢ t⊨~f
Tactic:
intros p h₂ h₃
State after:
t : Th
f : Form
h₁ : ~f ∈ ↑t
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False

State before:
t : Th
f : Form
h₁ : ~f ∈ ↑t
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Tactic:
rw [primeAnalysis] at h₁
State after:
t : Th
f : Form
h₁ : ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False

State before:
t : Th
f : Form
h₁ : ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Tactic:
have l₁ : ~f ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
State after:
t : Th
f : Form
h₁ : ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
l₁ : ~f ∈ ↑↑p
⊢ False

State before:
t : Th
f : Form
h₁ : ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
l₁ : ~f ∈ ↑↑p
⊢ False
Tactic:
exact canonicalSatisfaction.mp h₃ l₁
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ f⊃g ∈ ↑t
Tactic:
apply byContradiction
State after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ ¬f⊃g ∈ ↑t → False

State before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ ¬f⊃g ∈ ↑t → False
Tactic:
intros h₂
State after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
⊢ False

State before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
⊢ False
Tactic:
let Δ : Th := ⟨▲{f}, generatedFormal {f}⟩
State after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
⊢ False

State before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
⊢ False
Tactic:
have l₁ : ¬(g ∈ (formalApplicationFunction t Δ).val) := by
  intros h₃
  have ⟨q,⟨prf₁⟩,l₂⟩ := h₃
  have ⟨prf₂⟩ := t.property.mp l₂
  have prf₃ := BProof.mp prf₂ (BTheorem.hs prf₁.toTheorem BTheorem.taut)
  exact h₂ $ t.property.mpr ⟨prf₃⟩
State after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
⊢ False

State before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
⊢ False
Tactic:
have l₂ : Δ ⊨ f := canonicalSatisfaction.mpr ⟨BProof.ax rfl⟩
State after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
l₂ : Δ⊨f
⊢ False

State before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
l₂ : Δ⊨f
⊢ False
Tactic:
exact l₁ $ canonicalSatisfaction.mp (h₁ l₂)
State after:
no goals

State before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
⊢ ¬g ∈ ↑(formalApplicationFunction t Δ)
Tactic:
intros h₃
State after:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
⊢ False

State before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
⊢ False
Tactic:
have ⟨q,⟨prf₁⟩,l₂⟩ := h₃
State after:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
⊢ False

State before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
⊢ False
Tactic:
have ⟨prf₂⟩ := t.property.mp l₂
State after:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
⊢ False

State before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
⊢ False
Tactic:
have prf₃ := BProof.mp prf₂ (BTheorem.hs prf₁.toTheorem BTheorem.taut)
State after:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
prf₃ : BProof (↑t) (f⊃g)
⊢ False

State before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
prf₃ : BProof (↑t) (f⊃g)
⊢ False
Tactic:
exact h₂ $ t.property.mpr ⟨prf₃⟩
State after:
no goals

State before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
⊢ t⊨f⊃g
Tactic:
intros r h₂
State after:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
⊢ t∙r⊨g

State before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
⊢ t∙r⊨g
Tactic:
have l₁ := canonicalSatisfaction.mp h₂
State after:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
⊢ t∙r⊨g

State before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
⊢ t∙r⊨g
Tactic:
have l₂ : g ∈ (formalApplicationFunction t r).val := ⟨f, l₁, h₁⟩
State after:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
l₂ : g ∈ ↑(formalApplicationFunction t r)
⊢ t∙r⊨g

State before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
l₂ : g ∈ ↑(formalApplicationFunction t r)
⊢ t∙r⊨g
Tactic:
exact canonicalSatisfaction.mpr l₂
State after:
no goals