Meta-Logical Substrate

The meta-logical substrate: the collection of CIC structural rules, type-formation principles, and axioms provided by the proof assistant that are not derived from K0-K6. Classifies contraction, weakening, and exchange by their object-level status under K5.

Meta-Logical Substrate

Summary

The meta-logical substrate: the collection of CIC structural rules, type-formation principles, and axioms provided by the proof assistant that are not derived from K0-K6. Classifies contraction, weakening, and exchange by their object-level status under K5.

Statement

%
\label{def:meta-logical-substrate}
The \textbf{meta-logical substrate} of a formal development
is the collection of
\begin{enumerate}
    \item logical rules
          (introduction and elimination rules
          for connectives and quantifiers),
    \item type-formation principles
          (dependent products, inductive definitions,
          universe stratification),
    \item structural rules
          (contraction, weakening, exchange), and
    \item ambient axioms
          (\texttt{propext}, \texttt{funext},
          \texttt{Quot.sound},
          and optionally \texttt{Classical.choice})
\end{enumerate}
provided by the proof assistant
that are \textbf{not} derived
from the object theory's own axioms.
For TauLib, the object theory
is the coherence kernel $\KAxiom{0}$--$\KAxiom{6}$;
the meta-logical substrate
is everything that CIC contributes
on top of that kernel.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 167
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part18/ch68-meta-logical-toolkit.tex lines 316-343

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.MetaLogic.Substrate
• Name: Tau.MetaLogic.MetaLogicalSubstrate

Dependencies

• Canonical: I.D03, I.D14

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.