internlm/Lean-Github huggingface dataset:
Theorem: LO.Compact.compact_cumulative
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
⊢ Semantics.Satisfiable M (⋃ s, T s)
Tactic:
apply compact.mpr
Proof state after:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
⊢ ∀ (u : Finset F), ↑u ⊆ ⋃ s, T s → Semantics.Satisfiable M ↑u
Theorem: LO.Compact.compact_cumulative
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
⊢ ∀ (u : Finset F), ↑u ⊆ ⋃ s, T s → Semantics.Satisfiable M ↑u
Tactic:
intro u hu
Proof state after:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
⊢ Semantics.Satisfiable M ↑u
Theorem: LO.Compact.compact_cumulative
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
⊢ Semantics.Satisfiable M ↑u
Tactic:
rcases hT.finset_mem hu with ⟨s, hs⟩
Proof state after:
case intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ Semantics.Satisfiable M ↑u
Theorem: LO.Compact.compact_cumulative
Proof state before:
case intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ Semantics.Satisfiable M ↑u
Tactic:
exact (H s).of_subset hs
Proof state after:
no goals
Theorem: LO.System.unprovable_iff_isEmpty
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
f : F
⊢ 𝓢 ⊬! f ↔ IsEmpty (𝓢 ⊢ f)
Tactic:
simp [Provable, Unprovable]
Proof state after:
no goals
Theorem: LO.System.provableSet_iff
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
s : Set F
⊢ 𝓢 ⊢!* s ↔ Nonempty (𝓢 ⊢* s)
Tactic:
simp [ProvableSet, PrfSet, Provable, Classical.nonempty_pi, ←imp_iff_not_or]
Proof state after:
no goals
Theorem: LO.System.not_reducible_iff
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ ¬𝓢 ≤ₛ 𝓣 ↔ ∃ f, 𝓢 ⊢! f ∧ 𝓣 ⊬! f
Tactic:
simp [reducible_iff, Unprovable]
Proof state after:
no goals
Theorem: LO.System.strictReducible_iff
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ 𝓢 <ₛ 𝓣 ↔ (∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f) ∧ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f
Tactic:
simp [StrictReducible, reducible_iff]
Proof state after:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ (∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f) → ((∃ x, 𝓣 ⊢! x ∧ ¬𝓢 ⊢! x) ↔ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f)
Theorem: LO.System.strictReducible_iff
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ (∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f) → ((∃ x, 𝓣 ⊢! x ∧ ¬𝓢 ⊢! x) ↔ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f)
Tactic:
intro _
Proof state after:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
a✝ : ∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f
⊢ (∃ x, 𝓣 ⊢! x ∧ ¬𝓢 ⊢! x) ↔ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f
Theorem: LO.System.strictReducible_iff
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
a✝ : ∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f
⊢ (∃ x, 𝓣 ⊢! x ∧ ¬𝓢 ⊢! x) ↔ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f
Tactic:
exact exists_congr (fun _ ↦ by simp [and_comm])
Proof state after:
no goals
Theorem: LO.System.strictReducible_iff
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
a✝ : ∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f
x✝ : F
⊢ 𝓣 ⊢! x✝ ∧ ¬𝓢 ⊢! x✝ ↔ 𝓢 ⊬! x✝ ∧ 𝓣 ⊢! x✝
Tactic:
simp [and_comm]
Proof state after:
no goals
Theorem: LO.System.Equiv.iff
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ 𝓢 =ₛ 𝓣 ↔ ∀ (f : F), 𝓢 ⊢! f ↔ 𝓣 ⊢! f
Tactic:
simp [Equiv, Set.ext_iff, theory]
Proof state after:
no goals
Theorem: LO.System.Equiv.le
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ 𝓢 =ₛ 𝓣 → 𝓢 ≤ₛ 𝓣
Tactic:
simp [Equiv, Reducible]
Proof state after:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ theory 𝓢 = theory 𝓣 → theory 𝓢 ⊆ theory 𝓣
Theorem: LO.System.Equiv.le
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ theory 𝓢 = theory 𝓣 → theory 𝓢 ⊆ theory 𝓣
Tactic:
intro e
Proof state after:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
e : theory 𝓢 = theory 𝓣
⊢ theory 𝓢 ⊆ theory 𝓣
Theorem: LO.System.Equiv.le
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
e : theory 𝓢 = theory 𝓣
⊢ theory 𝓢 ⊆ theory 𝓣
Tactic:
rw [e]
Proof state after:
no goals
Theorem: LO.System.inconsistent_def
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
⊢ Inconsistent 𝓢 ↔ ∀ (f : F), 𝓢 ⊢! f
Tactic:
simp [Inconsistent]
Proof state after:
no goals
Theorem: LO.System.inconsistent_iff_theory_eq
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
⊢ Inconsistent 𝓢 ↔ theory 𝓢 = Set.univ
Tactic:
simp [Inconsistent, Set.ext_iff, theory]
Proof state after:
no goals
Theorem: LO.System.not_inconsistent_iff_consistent
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
⊢ Consistent 𝓢 → ¬Inconsistent 𝓢
Tactic:
rintro ⟨h⟩
Proof state after:
case mk
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
h : ¬Inconsistent 𝓢
⊢ ¬Inconsistent 𝓢
Theorem: LO.System.not_inconsistent_iff_consistent
Proof state before:
case mk
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
h : ¬Inconsistent 𝓢
⊢ ¬Inconsistent 𝓢
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.System.not_consistent_iff_inconsistent
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
⊢ ¬Consistent 𝓢 ↔ Inconsistent 𝓢
Tactic:
simp [←not_inconsistent_iff_consistent]
Proof state after:
no goals
Theorem: LO.System.consistent_iff_exists_unprovable
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
⊢ Consistent 𝓢 ↔ ∃ f, 𝓢 ⊬! f
Tactic:
simp [←not_inconsistent_iff_consistent, inconsistent_def]
Proof state after:
no goals
Theorem: LO.System.inconsistent_iff_theory_eq_univ
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
⊢ Inconsistent 𝓢 ↔ theory 𝓢 = Set.univ
Tactic:
simp [inconsistent_def, theory, Set.ext_iff]
Proof state after:
no goals
Theorem: LO.System.Inconsistent.equiv
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 𝓣 : S
h : Inconsistent 𝓢
h' : Inconsistent 𝓣
f : F
⊢ f ∈ theory 𝓢 ↔ f ∈ theory 𝓣
Tactic:
simp [h.theory_eq, h'.theory_eq]
Proof state after:
no goals
Theorem: LO.System.incomplete_iff_exists_undecidable
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝³ : System F S
inst✝² : System F T
inst✝¹ : System F U
inst✝ : LogicalConnective F
𝓢 : S
⊢ ¬Complete 𝓢 ↔ ∃ f, Undecidable 𝓢 f
Tactic:
simp [Complete, Undecidable, not_or]
Proof state after:
no goals
Theorem: LO.System.Axiomatized.le_of_subset
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
⊢ 𝓢 ≤ₛ 𝓣
Tactic:
rintro f ⟨b⟩
Proof state after:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
f : F
b : 𝓢 ⊢ f
⊢ f ∈ theory 𝓣
Theorem: LO.System.Axiomatized.le_of_subset
Proof state before:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
f : F
b : 𝓢 ⊢ f
⊢ f ∈ theory 𝓣
Tactic:
exact ⟨weakening h b⟩
Proof state after:
no goals
Theorem: LO.System.Axiomatized.weakening!
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
f : F
⊢ 𝓢 ⊢! f → 𝓣 ⊢! f
Tactic:
rintro ⟨b⟩
Proof state after:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
f : F
b : 𝓢 ⊢ f
⊢ 𝓣 ⊢! f
Theorem: LO.System.Axiomatized.weakening!
Proof state before:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
f : F
b : 𝓢 ⊢ f
⊢ 𝓣 ⊢! f
Tactic:
exact ⟨weakening h b⟩
Proof state after:
no goals
Theorem: LO.System.StrongCut.cut!
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : StrongCut S T
𝓢 : S
𝓣 : T
p : F
H : 𝓢 ⊢!* Collection.set 𝓣
hp : 𝓣 ⊢! p
⊢ 𝓢 ⊢! p
Tactic:
rcases hp with ⟨b⟩
Proof state after:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : StrongCut S T
𝓢 : S
𝓣 : T
p : F
H : 𝓢 ⊢!* Collection.set 𝓣
b : 𝓣 ⊢ p
⊢ 𝓢 ⊢! p
Theorem: LO.System.StrongCut.cut!
Proof state before:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : StrongCut S T
𝓢 : S
𝓣 : T
p : F
H : 𝓢 ⊢!* Collection.set 𝓣
b : 𝓣 ⊢ p
⊢ 𝓢 ⊢! p
Tactic:
exact ⟨StrongCut.cut H.get b⟩
Proof state after:
no goals
Theorem: LO.System.Compact.finite_provable
Proof state before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : Compact S
f : F
𝓢 : S
h : 𝓢 ⊢! f
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ 𝓕 ⊢! f
Tactic:
rcases h with ⟨b⟩
Proof state after:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : Compact S
f : F
𝓢 : S
b : 𝓢 ⊢ f
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ 𝓕 ⊢! f
Theorem: LO.System.Compact.finite_provable
Proof state before:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : Compact S
f : F
𝓢 : S
b : 𝓢 ⊢ f
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ 𝓕 ⊢! f
Tactic:
exact ⟨φ b, φ_subset b, φ_finite b, ⟨φPrf b⟩⟩
Proof state after:
no goals
Theorem: LO.System.consistent_iff_unprovable_bot
Proof state before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
inst✝ : DeductiveExplosion S
𝓢 : S
⊢ Consistent 𝓢 ↔ 𝓢 ⊬! ⊥
Tactic:
simp [inconsistent_iff_provable_bot, ←not_inconsistent_iff_consistent]
Proof state after:
no goals
Theorem: LO.System.inconsistent_compact
Proof state before:
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
H : Inconsistent 𝓢
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕
Tactic:
rcases Compact.finite_provable (H ⊥) with ⟨𝓕, h𝓕, fin, h⟩
Proof state after:
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
H : Inconsistent 𝓢
𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
fin : Collection.Finite 𝓕
h : 𝓕 ⊢! ⊥
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕
Theorem: LO.System.inconsistent_compact
Proof state before:
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
H : Inconsistent 𝓢
𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
fin : Collection.Finite 𝓕
h : 𝓕 ⊢! ⊥
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕
Tactic:
exact ⟨𝓕, h𝓕, fin, inconsistent_of_provable h⟩
Proof state after:
no goals
Theorem: LO.System.inconsistent_compact
Proof state before:
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
⊢ (∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕) → Inconsistent 𝓢
Tactic:
rintro ⟨𝓕, h𝓕, _, H⟩
Proof state after:
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
left✝ : Collection.Finite 𝓕
H : Inconsistent 𝓕
⊢ Inconsistent 𝓢
Theorem: LO.System.inconsistent_compact
Proof state before:
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
left✝ : Collection.Finite 𝓕
H : Inconsistent 𝓕
⊢ Inconsistent 𝓢
Tactic:
exact H.of_supset h𝓕
Proof state after:
no goals
Theorem: LO.System.consistent_compact
Proof state before:
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
⊢ Consistent 𝓢 ↔ ∀ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 → Consistent 𝓕
Tactic:
simp [←not_inconsistent_iff_consistent, inconsistent_compact (𝓢 := 𝓢)]
Proof state after:
no goals
Theorem: LO.System.Deduction.of_insert!
Proof state before:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
h : cons p 𝓢 ⊢! q
⊢ 𝓢 ⊢! p ⟶ q
Tactic:
rcases h with ⟨b⟩
Proof state after:
case intro
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
b : cons p 𝓢 ⊢ q
⊢ 𝓢 ⊢! p ⟶ q
Theorem: LO.System.Deduction.of_insert!
Proof state before:
case intro
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
b : cons p 𝓢 ⊢ q
⊢ 𝓢 ⊢! p ⟶ q
Tactic:
exact ⟨Deduction.ofInsert b⟩
Proof state after:
no goals
Theorem: LO.System.Deduction.inv!
Proof state before:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
h : 𝓢 ⊢! p ⟶ q
⊢ cons p 𝓢 ⊢! q
Tactic:
rcases h with ⟨b⟩
Proof state after:
case intro
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
b : 𝓢 ⊢ p ⟶ q
⊢ cons p 𝓢 ⊢! q
Theorem: LO.System.Deduction.inv!
Proof state before:
case intro
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
b : 𝓢 ⊢ p ⟶ q
⊢ cons p 𝓢 ⊢! q
Tactic:
exact ⟨Deduction.inv b⟩
Proof state after:
no goals
Theorem: LO.Sound.consistent_of_meaningful
Proof state before:
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
𝓢 𝓣 : S
𝓜 𝓝 : M
inst✝¹ : Sound 𝓢 𝓜
inst✝ : Sound 𝓣 𝓝
H : Semantics.Meaningful 𝓜
h : System.Inconsistent 𝓢
⊢ False
Tactic:
rcases H with ⟨f, hf⟩
Proof state after:
case mk.intro
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
𝓢 𝓣 : S
𝓜 𝓝 : M
inst✝¹ : Sound 𝓢 𝓜
inst✝ : Sound 𝓣 𝓝
h : System.Inconsistent 𝓢
f : F
hf : ¬𝓜 ⊧ f
⊢ False
Theorem: LO.Sound.consistent_of_meaningful
Proof state before:
case mk.intro
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
𝓢 𝓣 : S
𝓜 𝓝 : M
inst✝¹ : Sound 𝓢 𝓜
inst✝ : Sound 𝓣 𝓝
h : System.Inconsistent 𝓢
f : F
hf : ¬𝓜 ⊧ f
⊢ False
Tactic:
exact hf (Sound.sound (h f))
Proof state after:
no goals
Theorem: LO.Complete.meaningful_of_consistent
Proof state before:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
⊢ System.Consistent 𝓢 → Semantics.Meaningful 𝓜
Tactic:
contrapose
Proof state after:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
⊢ ¬Semantics.Meaningful 𝓜 → ¬System.Consistent 𝓢
Theorem: LO.Complete.meaningful_of_consistent
Proof state before:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
⊢ ¬Semantics.Meaningful 𝓜 → ¬System.Consistent 𝓢
Tactic:
intro h
Proof state after:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
h : ¬Semantics.Meaningful 𝓜
⊢ ¬System.Consistent 𝓢
Theorem: LO.Complete.meaningful_of_consistent
Proof state before:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
h : ¬Semantics.Meaningful 𝓜
⊢ ¬System.Consistent 𝓢
Tactic:
simp [Semantics.not_meaningful_iff, System.not_consistent_iff_inconsistent] at h ⊢
Proof state after:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
h : ∀ (f : F), 𝓜 ⊧ f
⊢ System.Inconsistent 𝓢
Theorem: LO.Complete.meaningful_of_consistent
Proof state before:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
h : ∀ (f : F), 𝓜 ⊧ f
⊢ System.Inconsistent 𝓢
Tactic:
intro f
Proof state after:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
h : ∀ (f : F), 𝓜 ⊧ f
f : F
⊢ 𝓢 ⊢! f
Theorem: LO.Complete.meaningful_of_consistent
Proof state before:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
M : Type u_3
inst✝¹ : Semantics F M
𝓢 : S
𝓜 : M
inst✝ : Complete 𝓢 𝓜
h : ∀ (f : F), 𝓜 ⊧ f
f : F
⊢ 𝓢 ⊢! f
Tactic:
exact Complete.complete (h f)
Proof state after:
no goals
Theorem: LO.Complete.inconsistent_of_unsatisfiable
Proof state before:
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
inst✝¹ : ∀ (𝓜 : M), Semantics.Meaningful 𝓜
𝓢 : S
T : Set F
inst✝ : Complete 𝓢 (Semantics.models M T)
⊢ ¬Semantics.Satisfiable M T → System.Inconsistent 𝓢
Tactic:
contrapose
Proof state after:
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
inst✝¹ : ∀ (𝓜 : M), Semantics.Meaningful 𝓜
𝓢 : S
T : Set F
inst✝ : Complete 𝓢 (Semantics.models M T)
⊢ ¬System.Inconsistent 𝓢 → ¬¬Semantics.Satisfiable M T
Theorem: LO.Complete.inconsistent_of_unsatisfiable
Proof state before:
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
inst✝¹ : ∀ (𝓜 : M), Semantics.Meaningful 𝓜
𝓢 : S
T : Set F
inst✝ : Complete 𝓢 (Semantics.models M T)
⊢ ¬System.Inconsistent 𝓢 → ¬¬Semantics.Satisfiable M T
Tactic:
simpa [←System.not_consistent_iff_inconsistent] using satisfiable_of_consistent
Proof state after:
no goals
Theorem: LO.System.FiniteContext.not_mem_empty
Proof state before:
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
p : F
⊢ p ∉ ∅
Tactic:
simp [EmptyCollection.emptyCollection]
Proof state after:
no goals
Theorem: LO.System.FiniteContext.by_axm!
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : DecidableEq F
S : Type u_2
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
Γ Δ E : List F
p : F
h : autoParam (p ∈ Γ) _auto✝
⊢ p ∈ Collection.set { ctx := Γ }
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.System.FiniteContext.weakening!
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : DecidableEq F
S : Type u_2
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
Γ Δ E : List F
h✝ : Γ ⊆ Δ
p : F
h : Γ ⊢[𝓢]! p
⊢ { ctx := Γ } ⊆ { ctx := Δ }
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.System.FiniteContext.of'!
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : DecidableEq F
S : Type u_2
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
Γ Δ E : List F
p : F
h : 𝓢 ⊢! p
⊢ [] ⊆ Γ
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.Context.not_mem_empty
Proof state before:
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
p : F
⊢ p ∉ ∅
Tactic:
simp [EmptyCollection.emptyCollection, Set.mem_def]
Proof state after:
no goals
Theorem: LO.System.Context.provable_iff
Proof state before:
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
⊢ Γ *⊢[𝓢]! p → ∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p
Tactic:
rintro ⟨⟨Δ, h, b⟩⟩
Proof state after:
case intro.mk
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ { ctx := Γ }
b : Δ ⊢[𝓢] p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p
Theorem: LO.System.Context.provable_iff
Proof state before:
case intro.mk
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ { ctx := Γ }
b : Δ ⊢[𝓢] p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p
Tactic:
exact ⟨Δ, h, ⟨b⟩⟩
Proof state after:
no goals
Theorem: LO.System.Context.provable_iff
Proof state before:
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
⊢ (∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p) → Γ *⊢[𝓢]! p
Tactic:
rintro ⟨Δ, h, ⟨d⟩⟩
Proof state after:
case intro.intro.intro
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ Γ
d : { ctx := Δ } ⊢ p
⊢ Γ *⊢[𝓢]! p
Theorem: LO.System.Context.provable_iff
Proof state before:
case intro.intro.intro
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ Γ
d : { ctx := Δ } ⊢ p
⊢ Γ *⊢[𝓢]! p
Tactic:
exact ⟨⟨Δ, h, d⟩⟩
Proof state after:
no goals