Symbol Reference: ! — At-Most-One Uniqueness Binder (!, AST Constructor: TpUniq)

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

Formula Display:
Proof Trees:

! \(!\) — At-Most-One Uniqueness Binder (!, AST Constructor: TpUniq)

Defined uniqueness binder !(v:A), 𝛗 asserting that at most one element of type A satisfies 𝛗.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
!
\(!\)
Category Binder (Uniqueness Quantifier)
SML AST Constructor HP (TpUniq of (UCol * 'Truth_AFUNEX)) [in datatype Truth_p, typetheory.ML:657]
Constructor Arguments 1. Domain conglomerate A : UCol; 2. Bound variable v : Variable; 3. Body 𝛗 : Fm
Metatype / Signature (Variable : Type) × Fm → Fm
Binder Status YES — At-Most-One Uniqueness Binder
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form !
How to Understand It

SML AST Constructor: HP (TpUniq of (UCol * 'Truth_AFUNEX)) in Truth_p (typetheory.ML:657). Classification: Binder. Defined by Entry DefAtMostOneBinder (4.04).
Canonical Law / Usage (!(v:A)⟦𝛗⟧) ⟷ ∀(v₁:A)∀(v₂:A)((𝛗[v₁/v] ∧ 𝛗[v₂/v]) → (v₁ = v₂))
Related Symbols & Kernel Entries