Symbol Reference: 𝛂 𝛃 𝛄 𝛅 𝛋 𝛒 𝛗 𝛙 — Greek Formula & Schema Metavariables

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

Formula Display:
Proof Trees:

𝛂 𝛃 𝛄 𝛅 𝛋 𝛒 𝛗 𝛙 \(\alpha, \beta, \gamma, \delta, \kappa, \rho, \varphi, \chi\) — Greek Formula & Schema Metavariables

Mathematical bold Greek metavariables ranging over arbitrary object formulas in logical axiom schemas and inference rules (Sections 1–5).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
𝛂 𝛃 𝛄 𝛅 𝛋 𝛒 𝛗 𝛙
\(\alpha, \beta, \gamma, \delta, \kappa, \rho, \varphi, \chi\)
Category Variables & Metavariables
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 Fm (or Prop in Variant 2)
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \alpha, \beta, \gamma, \delta, \kappa, \rho, \varphi, \chi
How to Understand It

In Variant 1 (MKTD1), bold mathematical Greek letters 𝛂, 𝛃, 𝛄, 𝛅, 𝛗, 𝛙 represent schematic formula variables of sort Fm:

  • In propositional logic (Entries AxmPropWeakening (1.01)–AxmPropVerum (1.13)), they stand for any well-formed formula instantiated into an axiom schema (such as Frege's Axiom AxmPropFrege (1.02) (𝛂 ⇒ (𝛃 ⇒ 𝛄)) ⇒ ((𝛂 ⇒ 𝛃) ⇒ (𝛂 ⇒ 𝛄))).
  • In Variant 2 (MKTD2), these correspond to explicitly quantified propositional type variables ∀(A:Prop). ∀(B:Prop). ....
Canonical Law / Usage (𝛂 ⇒ (𝛃 ⇒ 𝛂))
Related Symbols & Kernel Entries