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 of formulae — no matter how big is! — by checking the truth of every one of its finite subsets,

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 of formulae we are testing might be arbitrarily sized — it could be countably infinite, equinumerous with 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 .

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


We fix an arbitrary proposition of Agda, our meta-logic, and an atom 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, and 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' → ∥-∥-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 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 which actually consists only of the boolean value assigned to the atom something we can do case analysis on. If our compactness oracle thinks that must be true, then it can not have been the case that holds, since then we would have In other words, we have decided  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 was assigned false, then must not have failed: but the triple negative 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 : Dec (¬ ∣ P ∣) ¬P∨¬¬P = ∥-∥-out! 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