Symbol Reference: Theory / 𝒯 / ℰ / MKTD1 / MKTD2 — Formal Axiomatic Theory Sort & The 12+6 Canonical Theory Variants (Default: MKTD1 & MKTD2)

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

Theory / 𝒯 / ℰ / MKTD1 / MKTD2 \(\mathsf{Theory} \; / \; \mathcal{T} \; / \; \mathcal{E} \; / \; \mathsf{MKTD1} \; / \; \mathsf{MKTD2}\) — Formal Axiomatic Theory Sort & The 12+6 Canonical Theory Variants (Default: MKTD1 & MKTD2)

Represents an axiomatic theory 𝒯 : Theory (including unspecified theories ℰ extending IΣ₁ such as PA, NBG, or MK, and the canonical default theories MKTD1 and MKTD2).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
Theory / 𝒯 / ℰ / MKTD1 / MKTD2
\(\mathsf{Theory} \; / \; \mathcal{T} \; / \; \mathcal{E} \; / \; \mathsf{MKTD1} \; / \; \mathsf{MKTD2}\)
Category Metatheoretic AST Sorts & Theory Variants
SML AST Constructor Kernel AST Symbol / Sort Constructor in typetheory.ML (Class_p / Truth_p / EXP / UCol)
Constructor Arguments Typed arguments as specified by the Signature / Sort field above
Metatype / Signature Syntactic Sort of Formal Theories
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathsf{Theory} \; / \; \mathcal{T} \; / \; \mathcal{E} \; / \; \mathsf{MKTD1} \; / \; \mathsf{MKTD2}
How to Understand It

The 12+6 Canonical Theory & Proof Assistant Variants (Directive 12):

Every .nbg file and formal development specifies its target theory and proof assistant variant at the top of the file. The default theory is MKTD = Morse-Kelley + Tarski + Dunaev (Morse-Kelley impredicative class theory + Tarski's Axiom of Universes + Dunaev's refined axioms and explicit quotation/antiquotation, encoding/decoding, embedding, and conglomerate types):

  • Variant 1 (1st-Order Syntactical Proof Assistant, suffix 1): NBG1, NBGT1, NBGTD1, MK1, MKT1, MKTD1 (Default Variant 1).
  • Variant 2 (Higher-Order Formulas-as-Types Proof Assistant, suffix 2): NBG2, NBGT2, NBGTD2, MK2, MKT2, MKTD2 (Default Variant 2).
  • Shared / Dual-Variant Reserved Identifiers (suffix *): NBG*, NBGT*, NBGTD*, MK*, MKT*, MKTD*.
  • Metatheoretic Theory Variables (𝒯, ℱ, ℰ, 𝒲): In Section 5 (Entries ThmLoeb (5.01)–ThmSecondIncompleteness (5.02)), ℰ ranges over any sufficiently strong formal theory extending IΣ₁ (such as PA, NBG, MK, or MKTD).
Canonical Law / Usage (IΣ₁ ⊆ ℰ) ⇒ (Consistent(ℰ) ⇒ ¬(ℰ ⊢ ‹Consistent(ℰ)›))
Related Symbols & Kernel Entries