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 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 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' β†’ βˆ₯-βˆ₯-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

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 = βˆ₯-βˆ₯-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.