Symbol Reference: Fm — Syntactic Formula AST Sort (Variant 1 Kernel)

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

Formula Display:
Proof Trees:

Fm \(\mathsf{Fm}\) — Syntactic Formula AST Sort (Variant 1 Kernel)

The ML and metatheoretic sort of first-order object formulas (𝛂, 𝛃, 𝛄 : Fm) manipulated by the Variant 1 kernel (newchecker.ML).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
Fm
\(\mathsf{Fm}\)
Category Metatheoretic AST Sorts
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 (Variant 1 AST)
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathsf{Fm}
How to Understand It

In Variant 1 (MKTD1), object-level formulas belong to the explicit syntactic sort Fm:

  • Constructed from atomic predicates (x ∈ y, x = y, Set(x)), propositional connectives (∧, ∨, ⇒, ⇔, ¬, ⊤, ⊥), and quantifiers (∀, ∃, ∃!).
  • Encoded into the class universe via Enc : Fm → Class and quoted via ‹𝛂›.
Canonical Law / Usage ∀(𝛂:Fm). ∀(𝛃:Fm). Fm
Related Symbols & Kernel Entries