Symbol Reference: ≺ — Strict Cardinality Order Predicate (≺, AST Constructor: TpLess)

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

Formula Display:
Proof Trees:

≺ \(\prec\) — Strict Cardinality Order Predicate (≺, AST Constructor: TpLess)

Binary strict cardinality relation (A ≺ B) ⟷ ¬(B ⪯ A) (Entry DefCardLess (3.42)).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
≺
\(\prec\)
Category Predicate Symbol (Binary Class Relation)
SML AST Constructor HP (TpLess of ('Class_EXP * 'Class_EXP)) [in datatype Truth_p, typetheory.ML:680]
Constructor Arguments 1. Smaller class A : Class; 2. Larger class B : Class
Metatype / Signature Class × Class → Bool
Binder Status No — Binary Predicate Symbol (Strict Cardinality Order)
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \prec
How to Understand It

SML AST Constructor: HP (TpLess of ('Class_EXP * 'Class_EXP)) in Truth_p (typetheory.ML:680). Takes two class arguments (A : Class, B : Class).
Canonical Law / Usage (A ≺ B) ⟷ ¬(B ⪯ A)
Related Symbols & Kernel Entries