FFI / FV / NFV / Fresh \(\mathsf{FFI} \; / \; \mathsf{FV} \; / \; \mathsf{NFV} \; / \; \mathsf{Fresh}\) — Syntactic Hygiene, Free-Variable & Free-For-In Predicates
Explicit side-condition predicates preventing variable capture during quantifier instantiation, class comprehension, and substitution.
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
FFI / FV / NFV / Fresh
\(\mathsf{FFI} \; / \; \mathsf{FV} \; / \; \mathsf{NFV} \; / \; \mathsf{Fresh}\)
|
| Category | Syntactic Hygiene & Substitution |
| SML AST Constructor | HC (CpFV of (UCol * 'a)), HC (CpCtxFV of 'Ctx_EXP), HP (TpFFI of (UCol * 'a * 'Variable_EXP * 'Truth_Expression_EXP)) [typetheory.ML:575-576, 683] |
| Constructor Arguments | FV: 1. Expression e : A.Expression; FFI: 1. Term t : X.Expression, 2. Variable x : Variable, 3. Formula π : Fm |
| Metatype / Signature | Meta-Predicates on Variables, Terms, and Formulas |
| Binder Status | No β Primitive Syntactic Hygiene Functional & Predicate Symbols |
| Defining Kernel Entries (ML Labels) | Inference Rule RulClassComprehension (3.01): Class comprehension (#RulClassComprehension / #label-class-comprehension) |
| LaTeX Form | \mathsf{FFI} \; / \; \mathsf{FV} \; / \; \mathsf{NFV} \; / \; \mathsf{Fresh} |
| How to Understand It | Meaning of Each Hygiene Predicate:
|
| Canonical Law / Usage | FFI(t, x, π) β ((βx:Class. π) β (let x β€ t in π)) |
| 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.01 |
|