Symbol Reference: Ord — Ordinal Class Predicate (Ord, AST Constructor: TpOrd)

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

Formula Display:
Proof Trees:

Ord \(\mathrm{Ord}\) — Ordinal Class Predicate (Ord, AST Constructor: TpOrd)

Unary predicate Ord(X) asserting that X is transitive and all its elements are transitive (Entry DefOrdinalClass (3.16)).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
Ord
\(\mathrm{Ord}\)
Category Predicate Symbol (Unary Class Predicate)
SML AST Constructor HP (TpOrd of 'Class_EXP) [in datatype Truth_p, typetheory.ML:670]
Constructor Arguments 1. Class term X : Class
Metatype / Signature Class → Bool
Binder Status No — Defined Unary Predicate Symbol (Ordinal Class)
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathrm{Ord}
How to Understand It

SML AST Constructor: HP (TpOrd of 'Class_EXP) in Truth_p (typetheory.ML:670). Takes one class argument X : Class.
Canonical Law / Usage ∀(X:Class)(Ord(X) ⟷ (Tr(X) ∧ (∀(y:Class)((y ∈ X) → Tr(y)))))
Related Symbols & Kernel Entries