Symbol Reference: Prf — Formal Proof / Derivation Tree Sort

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

Formula Display:
Proof Trees:

Prf \(\mathsf{Prf}\) — Formal Proof / Derivation Tree Sort

Represents a formal derivation tree / proof certificate p : Prf witnessing that a theory 𝒯 derives a statement S : Stmt.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
Prf
\(\mathsf{Prf}\)
Category Metatheoretic AST Sorts
SML AST Constructor Kernel AST Symbol / Sort Constructor in typetheory.ML (Class_p / Truth_p / EXP / UCol)
Constructor Arguments Typed arguments as specified by the Signature / Sort field above
Metatype / Signature Syntactic Sort of Proof Certificates
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathsf{Prf}
How to Understand It

In Variant 1 (newchecker.ML), every theorem entry is accompanied by an explicit derivation tree checked by the kernel. In metatheoretic reflection (Entries AxmSoundnessOfBaseTheory (3.72)–ThmDunaevSecondProjection (3.78)), Prf is the sort of proof objects whose existence witnesses 𝒯 ⊢ S.
Canonical Law / Usage ∃(p:Prf). Proofs(p, Enc(𝛂))
Related Symbols & Kernel Entries