Table of contents
Term
What this is
A Term over a signature Σ and variable set X is an element of the free Σ-algebra T(Σ, X), defined inductively:
- Every variable x ∈ X is a term.
- Every constant c ∈ Σ (arity 0) is a term.
- If f ∈ Σ has arity n and t₁, …, tₙ are terms, then f(t₁, …, tₙ) is a term.
- Nothing else is a term.
This is the definition shared by universal algebra, first-order logic, lambda calculus, type theory, and term rewriting — every field that uses the word “term” uses it to mean an element of such a free algebra.
The defining property is compositionality under the unique homomorphism: any function ρ : X → A assigning variables to elements of any Σ-algebra A extends uniquely to a Σ-algebra homomorphism ⟦-⟧_ρ : T(Σ, X) → A. This is the universal property of the free algebra. It means: the denotation of a compound term is completely determined by the denotations of its immediate sub-expressions, with no additional information required.
The critical distinction: term vs. formula
In first-order logic, terms and formulas are categorically separate syntactic levels:
- A term denotes an individual — an object in the domain of discourse. It is substituable: you can replace a variable in a term with another term and get a term. Terms are not truth-bearers.
- A formula (wff) expresses a truth condition. It is built from terms and predicates. A formula can be true or false under an interpretation. Formulas are not substituable for individual-denoting variables.
Terms appear inside formulas as arguments to predicates. Formulas do not appear inside terms.
Ground terms and open terms
A term is ground (or closed) if it contains no variables — it is an element of T(Σ, ∅), the initial Σ-algebra. Ground terms are the syntactic individuals of the language: every ground term denotes a specific element in every algebra via the unique initial homomorphism.
A term is open if it contains at least one free variable. Open terms denote elements only relative to a variable assignment ρ.
Substitution — replacing variables with terms — is the core operation on terms. It is the mechanism behind function application (β-reduction), instantiation of schemas with concrete arguments, and evaluation under an assignment.
In this system
The relational hyperverse math defines NuclearLanguageTerm as: an element of T_Σ_nuclear(X), the free Σ_nuclear-algebra generated by a set X of atomic propositions. The signature Σ_nuclear includes the Heyting connectives (∧, ∨, ⇒, ⊤, ⊥) and the two nuclear operators (Saturate, Transfer). Terms are generated inductively by these formation rules; the denotation map under any variable assignment is the unique homomorphism into any Σ_nuclear-algebra.
At the fiber level, every term has type Prop — the single type of the RelationalHistoryFiberDoctrineLanguage. This means every term is simultaneously a term in the algebra-theoretic sense and a Formula in the logical sense: each term expresses a truth condition.
The denotation map ⟦-⟧_t : T_Σ(X) → H_t maps each term to an element of the fiber Heyting algebra H_t. The denotation is an Application of the interpretation function to the specific term and history.
Open questions
- Whether terms at the hyperversal level (type Univ rather than Prop) require a separate spec entry or extend this one.