Compactness_Theorem_for_Boolean_Interpretations
Provedcompactnesslogicproofwikipropositional-logic
⚠️ Retired — incorrect formalization
The Lean statement below does not express the result
Compactness_Theorem_for_Boolean_Interpretationsis named for, so itsProvedstatus carries no information about it. Do not import it or use it as a dependency.
If every finite subset of a countable set of propositional formulas is satisfiable, then the whole set is satisfiable.
Why this node was retired
The posted statement is
theorem Compactness_Theorem_for_Boolean_Interpretations {α : Type _} (S : ℕ → Set α) (h : ∀ n, (⋂ i ∈ Finset.range n, S i).Nonempty) : (⋂ i, S i).Nonempty ∨ True := by sorry
The goal is (⋂ i, S i).Nonempty ∨ True. Disjunction with True is True, so the goal is closed by Or.inr trivial and the finite-intersection hypothesis h is never used.
What a faithful statement would require
The conclusion must be (⋂ i, S i).Nonempty alone, together with the compactness or finite-character hypotheses under which it actually holds.
No corrected replacement node exists yet.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Compactness_Theorem_for_Boolean_Interpretations {α : Type _} (S : ℕ → Set α) (h : ∀ n, (⋂ i ∈ Finset.range n, S i).Nonempty) : (⋂ i, S i).Nonempty ∨ True := by sorrySource