A representation for the non-instances of linear terms

Abstract

Given a signature (S, Σ) and a Σ-term t ∈ TΣ (X)s of sort s ∈ S, X = (Xs)s∈ S G S being a family of countably infinite sets of variables, we call a set B ⊆ TΣ (X)s of Σ-terms a representation for the non-instances of t (w.r.t. (S, Σ) ) iff the Σ -groundinstances of the elements of B are precisely those Σ -groundterms of sort s that are not a Σ -instance of t. We recursively define a family (Bt)t∈T Σ (X)s, s∈S of sets of Σ-terms (w.r.t. an implicit well ordering of the sets XS of variables) in such a way, that for each linear Σ -term t, Bt is a representation for the non-instances of t (w.r.t. (S, Σ)) that satisfies both a minimality and an embedding property. In particular, Bt is computable and finite if, in addition, Σ contains but a finite number of operation symbols.