Symbol Reference: {a, b} — Unordered Pair Functional Symbol ({a, b}, AST Constructor: CpUPair)

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

Formula Display:
Proof Trees:

{a, b} \(\{a, b\}\) — Unordered Pair Functional Symbol ({a, b}, AST Constructor: CpUPair)

Binary functional symbol {a, b} = {a} ∪ {b} (Entry DefUnorderedPair (3.49)). Clicking { or } in a 2-element pair expression {a, b} navigates to this page.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
{a, b}
\(\{a, b\}\)
Category Functional Symbol (Binary Class Operator)
SML AST Constructor HC (CpUPair of ('Class_EXP * 'Class_EXP)) [in datatype Class_p, typetheory.ML:564]
Constructor Arguments 1. First element a : Class; 2. Second element b : Class
Metatype / Signature Class × Class → Class
Binder Status No — Binary Mixfix Functional Symbol (Unordered Pair {a, b})
Defining Kernel Entries (ML Labels) Definition DefUnorderedPair (3.49): Unordered pair (#DefUnorderedPair / #label-unordered-pair)
LaTeX Form \{a, b\}
How to Understand It

SML AST Constructor: HC (CpUPair of ('Class_EXP * 'Class_EXP)) in Class_p (typetheory.ML:564). Takes two class arguments (a : Class, b : Class).
Canonical Law / Usage {a, b} = {a} ∪ {b}
Related Symbols & Kernel Entries

Defining Axioms, Rules & Formal Definitions (Rendered Directly from Kernel Entries)

Generated without code duplication by invoking render_entry_row_base "../manual.html" on the corresponding kernel Entry records.

# Formal Entity Specification
3.49
Title Unordered pair #DefUnorderedPair #label-unordered-pair
Classification Definition
Formula
0(∀(a:Class)∀(b:Class)({a,b}={x|(x=a)∨(x=b)}))
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{b} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/upair-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{b} \href{../symbols/upair-op.html}{\}} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{a} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/or-conn.html}{\lor} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{b} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST CpUPair
Scheme of Types 0(∀([a@Variable]:[Class@Type])∀([b@Variable]:[Class@Type])({[a@Class.Expression],[b@Class.Expression]}={[x@Class.Expression]|([x@Class.Expression]=[a@Class.Expression])∨([x@Class.Expression]=[b@Class.Expression])}))
Verification Definitional (Kernel AST) · Standalone Entry (DefUnorderedPair) → · (3.49) · #DefUnorderedPair