module Logic.Propositional.Classical.Compactness where

# Compactness of classical propositional logic is a constructive taboo🔗

The **compactness** property, for a logical system, says
that we can determine the satisfiability
of a set
$Φ$
of formulae — no matter how big
$Φ$
is! — by checking the truth of every one of its *finite* subsets,
$Ψ⊆Φ.$

subset-is-sat : ∀ {Γ} → (Proposition Γ → Ω) → Type _ subset-is-sat {Γ} ϕs = ∃[ ρ ∈ (Fin Γ → Bool) ] ((ϕ : Proposition Γ) → ϕ ∈ ϕs → ⟦ ϕ ⟧ ρ ≡ true) has-compactness : Type has-compactness = ∀ {Γ} → (ϕs : Proposition Γ → Ω) → (∀ (ϕs' : Proposition Γ → Ω) → ϕs' ⊆ ϕs → Finite (∫ₚ ϕs') → subset-is-sat ϕs') → subset-is-sat ϕs

Keep in mind that compactness is *not* immediate, even
classically, since the set
$Φ$
of formulae we are testing might be arbitrarily sized — it could be
countably infinite, equinumerous with
$R,$
or worse — and so it does not necessarily satisfy any boundedness
principles that would allow us to “patch together” pieces of truth — or
even carve out those pieces in the first place.

In fact, while compactness may sound like a natural statement, we
will show that this property is *too strong* to ask of classical
propositional logic, in our neutral meta-theory: if compactness holds,
then so does weak
excluded middle. Here, we formalise an argument due to (Saving
2023).

compactness→wlem : has-compactness → WLEM compactness→wlem compact P = ¬P∨¬¬P where

We fix an arbitrary proposition
$P:Ω$
*of Agda*, our meta-logic, and an atom
$x$
of our object logic. We will apply compactness to the set

of formulae.

x : Proposition 1 x = atom 0 [x∣P] : Proposition 1 → Ω [x∣P] ϕ = elΩ ((x ≡ ϕ) × ∣ P ∣) [¬x∣¬P] : Proposition 1 → Ω [¬x∣¬P] ϕ = elΩ ((“¬” x ≡ ϕ) × (¬ ∣ P ∣))

Despite the previous examples of bad subset being extremely large,
this is actually quite tame! It only has three possible *finite*
subsets, namely the empty set,
${x},$
and
${¬x},$
all of which are easily seen to be satisfiable. However, showing this to
a proof assistant requires quite a bit of work in combinatorics, so the
actual formalisation is a slightly nightmarish case bash.

finitely-consistent : (ϕs' : Proposition 1 → Ω) → ϕs' ⊆ ([x∣P] ∪ [¬x∣¬P]) → Finite (∫ₚ ϕs') → subset-is-sat ϕs'

##
We will set the `<details>`

aside for the curious reader.

finitely-consistent ϕs' sub (fin {zero} ∥enum∥) = pure $ (λ _ → true) , λ ϕ ϕ∈ϕs' → absurd (card-zero→empty ∥enum∥ (ϕ , ϕ∈ϕs')) finitely-consistent ϕs' sub (fin {suc zero} ∥enum∥) = do enum ← ∥enum∥ let module enum = Equiv enum let (ϕ , ϕ∈ϕs') = enum.from 0 sub ϕ ϕ∈ϕs' <&> λ where (inl xp) → (λ _ → true) , λ ϕ' ϕ'∈ϕs' → ∥-∥-proj! do sub ϕ' ϕ'∈ϕs' >>= λ where (inl xp') → □-tr do (x=ϕ' , _) ← xp' pure (subst (λ e → ⟦ e ⟧ (λ _ → true) ≡ true) x=ϕ' refl) (inr ¬xp') → □-tr do (_ , p) ← xp (_ , ¬p) ← ¬xp' absurd (¬p p) (inr ¬xp) → (λ _ → false) , λ ϕ' ϕ'∈ϕs' → ∥-∥-proj! do sub ϕ' ϕ'∈ϕs' >>= λ where (inl xp') → □-tr do (_ , ¬p) ← ¬xp (_ , p) ← xp' absurd (¬p p) (inr ¬xp') → □-tr do (¬x=ϕ' , _) ← ¬xp' pure (subst (λ e → ⟦ e ⟧ (λ _ → false) ≡ true) ¬x=ϕ' refl) finitely-consistent ϕs' sub (fin {suc (suc n)} ∥enum∥) = do enum ← ∥enum∥ let module enum = Equiv enum let (ϕ , ϕ∈ϕs') = enum.from 0 let (ϕ' , ϕ'∈ϕs') = enum.from 1 sub ϕ ϕ∈ϕs' >>= λ where (inl xp) → sub ϕ' ϕ'∈ϕs' >>= λ where (inl xp') → □-tr do (x=ϕ , _) ← xp (x=ϕ' , _) ← xp' absurd (fzero≠fsuc $ sym (enum.ε 0) ∙ ap enum.to (Σ-prop-path! (sym x=ϕ ∙ x=ϕ')) ∙ enum.ε 1) (inr ¬xp') → □-tr do (_ , p) ← xp (_ , ¬p) ← ¬xp' absurd (¬p p) (inr ¬xp) → sub ϕ' ϕ'∈ϕs' >>= λ where (inl xp') → □-tr do (_ , ¬p) ← ¬xp (_ , p) ← xp' absurd (¬p p) (inr ¬xp') → □-tr do (x=ϕ , _) ← ¬xp (x=ϕ' , _) ← ¬xp' absurd (fzero≠fsuc $ sym (enum.ε 0) ∙ ap enum.to (Σ-prop-path! (sym x=ϕ ∙ x=ϕ')) ∙ enum.ε 1)

By compactness, we must have a satisfying assignment for the set of formulae

${x∣P}∪{¬x∣¬P},$which actually consists only of the boolean value assigned to the
atom
$x:$
something we can do case analysis on. If our compactness oracle thinks
that
$x$
must be true, then it *can not have been the case that
$¬P$
holds*, since then we would have
$x=false.$
In other words, we have decided
$¬¬P.$

x-true→¬¬P : (ρ : Fin 1 → Bool) → (∀ ϕ → ϕ ∈ [x∣P] ∪ [¬x∣¬P] → sem-prop ϕ ρ ≡ true) → ⟦ x ⟧ ρ ≡ true → ¬ ¬ ∣ P ∣ x-true→¬¬P ρ sat x-true ¬p = not-no-fixed $ ⟦ x ⟧ ρ ≡⟨ x-true ⟩≡ true ≡˘⟨ sat (“¬” x) (inc (inr (inc (refl , ¬p)))) ⟩≡˘ not (⟦ x ⟧ ρ) ∎

Conversely, if $x$ was assigned false, then $¬P$ must not have failed: but the triple negative $¬¬¬P$ can be reduced to a single negative, even constructively.

x-false→¬P : (ρ : Fin 1 → Bool) → (∀ ϕ → ϕ ∈ [x∣P] ∪ [¬x∣¬P] → sem-prop ϕ ρ ≡ true) → ⟦ x ⟧ ρ ≡ false → ¬ ∣ P ∣ x-false→¬P ρ sat x-false p = not-no-fixed $ ⟦ x ⟧ ρ ≡⟨ sat x (inc (inl (inc (refl , p)))) ⟩≡ true ≡˘⟨ ap not x-false ⟩≡˘ not (⟦ x ⟧ ρ) ∎

If we put this all together, then we can decide $¬P!$

¬P∨¬¬P : Dec (¬ ∣ P ∣) ¬P∨¬¬P = ∥-∥-proj! do (ρ , ρ-sat) ← compact ([x∣P] ∪ [¬x∣¬P]) finitely-consistent pure $ Bool-elim (λ b → ρ 0 ≡ b → Dec (¬ ∣ P ∣)) (λ x-true → no (x-true→¬¬P ρ ρ-sat x-true)) (λ x-false → yes (x-false→¬P ρ ρ-sat x-false)) (ρ 0) refl

## References

- Saving, Mark. 2023. “Answer to ‘Constructive Proof of
Compactness Theorem for Countable Propositional
Languages’.”
*Mathematics Stack Exchange*. https://math.stackexchange.com/a/4669653.