Framework

This module defines the abstract interface for candidate interpretive frameworks.

A framework has a commitment theory together with the properties needed to state evidentiary grounding and documented interpretive function.

This interface does not require a framework to be admissible. Admissibility is defined separately.

The framework carrier is not assumed to be finite, enumerable, decidable, or known at design time.

structure SE.Framework.FrameworkSystem (P : Logic.Language.PropositionCarrier) : Type (max u (v + 1))

An abstract interface for candidate interpretive frameworks over an object-language proposition carrier.

The interface exposes only the information required by the admissibility definition. Concrete framework representations may supply this information from richer evidence, provenance, documentation, or interpretation records.

• Carrier : Type v

  The carrier of candidate interpretive frameworks.

• commitments : self.Carrier → Logic.Theory.CommitmentTheory P

  The commitment theory associated with a framework.

• evidentiallyGrounded : self.Carrier → Prop

  Whether the framework satisfies the paper's evidentiary-grounding condition.

• presentedAsInterpretiveFunction : self.Carrier → Prop

  Whether the framework is presented as an interpretive function.

• hasNamedSource : self.Carrier → Prop

  Whether the framework has a named source.

• hasDocumentedScope : self.Carrier → Prop

  Whether the framework has documented scope.

• hasCitableBasis : self.Carrier → Prop

  Whether the framework has a citable basis.