Theorem: LO.Complete.meaningful_of_consistent (Logic/Logic/System.lean)

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
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 𝓢

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
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 𝓢

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 ⊢
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 𝓢

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
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

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)
State after:
no goals