Framework Class

This module formalizes:

• se100.note.FrameworkClass — The Framework Class

The framework class is the class of all intrinsically admissible interpretive frameworks.

It is represented intensionally as a set defined by the admissibility predicate. It is not represented as a finite collection, enumeration, registry, or design-time list of known frameworks.

A framework becoming known does not change the intrinsic framework class.

def SE.Framework.FrameworkClass {L : Logic.Language.PropositionalLanguage} (C : Logic.ConsequenceSystem L) (M : FrameworkSystem L.carrier) : MathlibMini.Set M.Carrier

The class of all admissible interpretive frameworks.

Membership is determined only by intrinsic admissibility. The class does not depend on designer knowledge and is not assumed to be finite, enumerable, or decidable.

Equations

• SE.Framework.FrameworkClass C M = MathlibMini.Set.ofPredicate fun (F : M.Carrier) => SE.Framework.AdmissibleFramework C M F

@[simp]

theorem SE.Framework.mem_frameworkClass_iff {L : Logic.Language.PropositionalLanguage} {C : Logic.ConsequenceSystem L} {M : FrameworkSystem L.carrier} {F : M.Carrier} : F ∈ FrameworkClass C M ↔ AdmissibleFramework C M F

A candidate framework belongs to the framework class exactly when it is admissible.