Theorem 4.3: the family f_d is a filter on the deductive part

Proved

CogCons.deductiveFilter_isFilter

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

consequence-operatorlogictopology

Let $C_d \subsetneq C$ be a deductive system (the deductive part of $C$ ) and $f \in C_d$ . Let $f_d$ be the family of subsets $A \subseteq C_d$ with $f \in A$ that contain a deductive subset. Then:

$C_d \in f_d$ ;
if $A \in f_d$ and $A \subseteq B \subseteq C_d$ , then $B \in f_d$ ;
if $A, B \in f_d$ , then $A \cap B \in f_d$ .

So $f_d$ is a filter on $C_d$ .

Preamble

import Mathlib
import Definitions.Def_CogCons_consequence_space

open CogCons.CognitiveConsequenceSpace

Formal statement

namespace CogCons

theorem deductiveFilter_isFilter {C : Type*} (S : CognitiveConsequenceSpace C)
    (Cd : Set C) (hCd : S.IsDeductive Cd) (hCd_ne : Cd ≠ Set.univ) (f : C) (hf : f ∈ Cd) :
    Cd ∈ S.deductiveFilter Cd f ∧
    (∀ A B : Set C, A ∈ S.deductiveFilter Cd f → A ⊆ B → B ⊆ Cd →
      B ∈ S.deductiveFilter Cd f) ∧
    (∀ A B : Set C, A ∈ S.deductiveFilter Cd f → B ∈ S.deductiveFilter Cd f →
      A ∩ B ∈ S.deductiveFilter Cd f) := by sorry

end CogCons

Source

S. Acharjee and U. Gogoi, *The limit of human intelligence*, arXiv:2310.10792v2 [math.GM] (2023), https://arxiv.org/abs/2310.10792, Theorem 4.3 (p. 18)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted these Lean statements, not by an independent auditor working blind from the code alone. The author knew the intended meaning while writing it, so it may read that intent into the code. Do not treat it as independent verification; compare the Lean code against the source directly.

For every type $C$ , every cognitive-consequence space $S$ on $C$ , every $C_d \subseteq C$ with $\mathrm{Cn}(C_d) = C_d$ and $C_d \ne C$ , and every $f \in C_d$ , writing $\mathcal F = \{A : A \subseteq C_d,\ f \in A,\ \exists B \subseteq A \text{ with } \mathrm{Cn}(B) = B\}$ : (1) $C_d \in \mathcal F$ ; (2) for all $A, B \subseteq C$ , if $A \in \mathcal F$ , $A \subseteq B$ and $B \subseteq C_d$ then $B \in \mathcal F$ ; (3) for all $A, B$ , if $A, B \in \mathcal F$ then $A \cap B \in \mathcal F$ . The hypothesis $C_d \ne C$ is not needed for these conclusions.

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph