open import 1Lab.Classical
open import 1Lab.Prelude

open import Data.Fin.Indexed
open import Data.Power
open import Data.Bool
open import Data.Dec
open import Data.Fin
open import Data.Nat
open import Data.Sum

open import Logic.Propositional.Classical

open import Meta.Brackets

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 $\Phi$ of formulae — no matter how big $\Phi$ is! — by checking the truth of every one of its finite subsets, $\Psi \subseteq \Phi \text{.}$

private variable
  ℓ : Level
  Γ Δ Θ : Nat
  ψ θ ζ : Ctx Γ
  P Q R : Proposition Γ

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 $\Phi$ of formulae we are testing might be arbitrarily sized — it could be countably infinite, equinumerous with $\mathbb{R}\text{,}$ 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:\Omega$ of Agda, our meta-logic, and an atom $x$ of our object logic. We will apply compactness to the set

of formulae.

  x : Proposition 
  x = atom 

  [x∣P] : Proposition  → Ω
  [x∣P] ϕ = elΩ ((x ≡ ϕ) × ∣ P ∣)

  [¬x∣¬P] : Proposition  → Ω
  [¬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\}\text{,}$ and $\{\neg x\}\text{,}$ 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  → Ω)
    → ϕs' ⊆ ([x∣P] ∪ [¬x∣¬P])
    → Finite (∫ₚ ϕs')
    → subset-is-sat ϕs'

  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 
    sub ϕ ϕ∈ϕs' <&> λ where
      (inl xp) →
        (λ _ → true) , λ ϕ' ϕ'∈ϕs' → ∥-∥-out! 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' → ∥-∥-out! 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 
    let (ϕ' , ϕ'∈ϕs') = enum.from 
    sub ϕ ϕ∈ϕs' >>= λ where
      (inl xp) → sub ϕ' ϕ'∈ϕs' >>= λ where
        (inl xp') → □-tr do
          (x=ϕ , _) ← xp
          (x=ϕ' , _) ← xp'
          absurd
            (fzero≠fsuc $
              sym (enum.ε )
              ∙ ap enum.to (Σ-prop-path! (sym x=ϕ ∙ x=ϕ'))
              ∙ enum.ε )
        (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.ε )
              ∙ ap enum.to (Σ-prop-path! (sym x=ϕ ∙ x=ϕ'))
              ∙ enum.ε )

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

which actually consists only of the boolean value assigned to the atom $x\text{:}$ 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 $\neg P$ holds, since then we would have $x=\mathrm{false}\text{.}$ In other words, we have decided $\neg \neg P\text{.}$

  x-true→¬¬P
    : (ρ : Fin  → 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 $\neg P$ must not have failed: but the triple negative $\neg \neg \neg P$ can be reduced to a single negative, even constructively.

  x-false→¬P
    : (ρ : Fin  → 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 $\neg P\text{!}$

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