Admissible Framework

This module formalizes:

• se100.def.AdmissibleFramework — Admissible Framework

A framework is admissible when it satisfies three conditions:

1. internal consistency;
2. evidentiary grounding; and
3. documented interpretive function.

The documented interpretive-function condition requires presentation as an interpretive function together with a named source, documented scope, and citable basis.

def SE.Framework.DocumentedInterpretiveFunction {L : Logic.Language.PropositionalLanguage} (M : FrameworkSystem L.carrier) (F : M.Carrier) : Prop

A framework has a documented interpretive function when it is presented as an interpretive function with a named source, documented scope, and citable basis.

This groups the four requirements that constitute the third admissibility condition in the paper.

Equations

• SE.Framework.DocumentedInterpretiveFunction M F = (M.presentedAsInterpretiveFunction F ∧ M.hasNamedSource F ∧ M.hasDocumentedScope F ∧ M.hasCitableBasis F)

@[simp]

theorem SE.Framework.documentedInterpretiveFunction_iff {L : Logic.Language.PropositionalLanguage} {M : FrameworkSystem L.carrier} {F : M.Carrier} : DocumentedInterpretiveFunction M F ↔ M.presentedAsInterpretiveFunction F ∧ M.hasNamedSource F ∧ M.hasDocumentedScope F ∧ M.hasCitableBasis F

A framework has a documented interpretive function exactly when it is presented as an interpretive function with a named source, documented scope, and citable basis.

def SE.Framework.AdmissibleFramework {L : Logic.Language.PropositionalLanguage} (C : Logic.ConsequenceSystem L) (M : FrameworkSystem L.carrier) (F : M.Carrier) : Prop

A candidate framework is admissible when it is internally consistent, evidentially grounded, and has a documented interpretive function.

Equations

• SE.Framework.AdmissibleFramework C M F = (SE.Logic.Consistent C (M.commitments F) ∧ M.evidentiallyGrounded F ∧ SE.Framework.DocumentedInterpretiveFunction M F)

@[simp]

theorem SE.Framework.admissibleFramework_iff {L : Logic.Language.PropositionalLanguage} {C : Logic.ConsequenceSystem L} {M : FrameworkSystem L.carrier} {F : M.Carrier} : AdmissibleFramework C M F ↔ Logic.Consistent C (M.commitments F) ∧ M.evidentiallyGrounded F ∧ DocumentedInterpretiveFunction M F

A framework is admissible exactly when it is internally consistent, evidentially grounded, and has a documented interpretive function.