Symbol Reference: set / Set — Sethood Predicate (set, AST Constructor: TpSet)

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

Formula Display:
Proof Trees:

set / Set \(\mathrm{set}\) — Sethood Predicate (set, AST Constructor: TpSet)

Unary sethood predicate X set asserting that class X is an element of some class Y (Entry DefIsSet (3.02)). Variables always keep default type Class; sethood is always a predicate on Class.

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

SML AST Constructor: HP (TpSet of 'Class_EXP) in Truth_p (typetheory.ML:661). Takes one class argument X : Class.
Canonical Law / Usage ∀(X:Class)((X set) ⟷ (∃(Y:Class)(X ∈ Y)))
Related Symbols & Kernel Entries