Skip to content

Many-sorted logic

A formal logic whose language and structures partition objects into multiple sorts, restricting constants, variables, functions, predicates, substitution, and quantification to declared sort signatures.

Version
v1 · 2026-09-28 · History
Domain-specific #
10552
Domain group
Formal Sciences
Origin domain
Mathematics
Subdomain
Mathematical Logic → Mathematics

Core Idea

Many-sorted logic builds several kinds of object directly into a formal language. A set of sorts is paired with a signature whose constants, function symbols, and predicate symbols declare the sorts of their arguments and, for functions, their outputs. Variables and quantifiers are sort-indexed.

Structures supply a carrier for each sort and interpret symbols with compatible maps and relations. Substitution and inference must preserve those declarations, so a term can be syntactically ill formed before truth is considered—for example, applying an animal-valued mother function to a plant. Many-sorted theories can often be translated into single-sorted logic with predicates, but primitive sorting can make models and proofs clearer and restrict unwanted expressions.

Structural Signature

Sig role-phrases:

  • set of sorts. Names distinct object kinds in the language. Constitutive type universe. If altered: One undifferentiated sort gives ordinary single-sorted logic.
  • sorted signature. Assigns input and output sorts to functions and argument sorts to predicates. Identity-bearing syntax. If altered: An untyped symbol can create ill-formed terms.
  • sort-indexed variables and terms. Ensures expressions inhabit declared sorts. Constitutive formation rule. If altered: Cross-sort substitution is disallowed unless mediated by a symbol.
  • many-carrier structure. Interprets each sort with a domain and symbols with compatible operations or relations. Constitutive semantics. If altered: Whether carriers must be disjoint depends on formalization.
  • sort-respecting inference. Preserves well-formedness through substitution, quantification, and proof. Necessary logical closure. If altered: A semantically intuitive but ill-sorted formula is invalid.

What It Is Not

  • Typed programming language. Is a proof semantics rather than program execution central?
  • Order-sorted logic. Are subtype relations between sorts included?
  • Unary predicate encoding. Are sorts primitive or encoded?
  • Ontology. Are formal term and inference rules specified?

Scope of Application

Use many-sorted logic with sorts, signature, carrier assumptions, equality policy, quantification, and translation conventions stated.

  • Formal specification. Types system components.
  • Algebra. Defines many-sorted structures.
  • Knowledge representation. Separates entity kinds.
  • Program semantics. Models typed terms.
  • Model theory. Studies equivalence with one-sorted encodings.

Clarity

Sort distinction is syntactic and semantic structure, not merely a human-readable label on one unrestricted language.

Manages Complexity

Translations to unary predicates must preserve nonemptiness, symbol typing, equality, and quantifier domains. Empty sorts or overlapping carriers vary by convention and can change equivalence claims.

Abstract Reasoning

  1. Declare the set of sorts.
  2. Assign a sorted signature to every symbol.
  3. Generate only sort-correct terms and formulas.
  4. Interpret each sort and symbol in a structure.
  5. Verify substitutions and translations preserve sorting.

Knowledge Transfer

Typed partitioning transfers to programming and databases, but formal signatures, carriers, and proof rules delimit many-sorted logic. The nearest stopping boundary is explicit: Single-sorted first-order logic with unary sort predicates is closest: it can encode many-sorted theories, but sorting is represented inside one domain rather than enforced primitively by syntax. The inclusion test remains: A logical system is many-sorted when multiple sorts are built into its signature, term formation, structures, quantifiers, and substitutions. The structure no longer applies when the case exits when all variables range over one undifferentiated domain and symbols carry no sort constraints.

Examples

Canonical

A theory has plant and animal sorts and a function mother: animal→animal; mother(lassie) is well formed while mother(oak) is rejected syntactically.

Mapped back: set of sorts → plant and animal; sorted signature → mother animal to animal; sort-indexed variables and terms → lassie versus oak; many-carrier structure → two carriers; sort-respecting inference → ill-sorted term rejected.

Applied / In Practice

A single-sorted theory lets every variable range over all organisms and adds predicates Plant and Animal. It may encode similar content, but sorting is not primitive in its syntax.

Mapped back: set of sorts → one formal sort; sorted signature → untyped mother; sort-indexed variables and terms → none; many-carrier structure → one domain; sort-respecting inference → predicate constraints only.

Structural Tensions

T1: native sorts vs. one-sorted encoding. Translations aid comparison while losing immediate syntactic discipline. Diagnostic: Which assumptions preserve equivalence?

T2: strict typing vs. cross-sort relations. Sorts prevent nonsense but require explicit bridges. Diagnostic: Which coercions or shared objects are legitimate?

Structural–Framed Character

Description turns on set of sorts, sorted signature, sort-indexed variables and terms, many-carrier structure, sort-respecting inference. Skeletal core. A language prevents category errors by assigning objects and operations to compatible kinds. Domain-bound accent. Sorts, signatures, variables, functions, predicates, quantifiers, and structures define the logic. Transfer remains bounded because Why not prime. Typed separation is portable; this is a formal-logical system. The negative boundary is concrete: Any typed programming language, ontology, class hierarchy, polymorphic type system, unary predicate encoding, order-sorted algebra, database schema, or informal category distinction is not automatically many-sorted logic. Many-sorted logic is structural-formal: sort declarations constrain both expression formation and model interpretation. Its character: logical universes partitioned into typed carriers.

Structural Core vs. Domain Accent

Skeletal core. A language prevents category errors by assigning objects and operations to compatible kinds.

Domain-bound accent. Sorts, signatures, variables, functions, predicates, quantifiers, and structures define the logic.

Why not prime. Typed separation is portable; this is a formal-logical system.

This entry is a kind of Formal System.

  • First-order logic. Many-sorted variants refine its domains and syntax.
  • Type system. Sorts play a related static role.
  • No strict parent is asserted.

Relationships to Other Abstractions

Local relationship map for Many-sorted logicParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.Many-sorted logicDOMAINPrime abstraction: Formal System — is a kind ofFormal SystemPRIME

Current abstraction Many-sorted logic Domain-specific

Parents (1) — more general patterns this builds on

  • Many-sorted logic is a kind of Formal System Prime

    Many-sorted logic is a formal system specialized by a typed sort signature; it is not a kind of Omega-logic.

Hierarchy paths (2) — routes to 2 parentless roots

Neighborhood in Abstraction Space

Many-sorted logic sits in a crowded region of the domain-specific corpus (38th percentile for distinctiveness): several abstractions share nearly its structure, so a description that fits it tends to fit its neighbors too.

Family — Formal Models & Logical Foundations (33 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With

  • Typed programming language. Tell: Is a proof semantics rather than program execution central?
  • Order-sorted logic. Tell: Are subtype relations between sorts included?
  • Unary predicate encoding. Tell: Are sorts primitive or encoded?
  • Ontology. Tell: Are formal term and inference rules specified?

References

  • Frozen Wikipedia discovery revision: https://en.wikipedia.org/wiki/Many-sorted_logic (revision 1331051693).
  • Preserved source candidate: http://sqig.math.ist.utl.pt/pub/CaleiroC/06-CG-manysorted.pdf
  • Preserved source candidate: http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf
  • Preserved source candidate: https://web.archive.org/web/20110708231225/http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf
  • Preserved source candidate: http://archive.numdam.org/article/CM_1956-1958__13__277_0.pdf
  • Preserved source candidate: http://gdz.sub.uni-goettingen.de/index.php?id=11&L=4&PPN=GDZPPN002289989&L=1
  • Preserved source candidate: https://web.archive.org/web/20150220005037/http://gdz.sub.uni-goettingen.de/index.php?id=11&L=4&PPN=GDZPPN002289989&L=1
  • Preserved source candidate: https://www.sfu.ca/~jeffpell/papers/SortalRestrQuant.pdf
  • Preserved source candidate: https://web.archive.org/web/20070608182648/http://react.cs.uni-sb.de/~zarba/notes.html

The frozen Wikipedia revision is discovery provenance. The retained source set was reviewed for identity, formal or operational relation, and scope. The encyclopedia's structural synthesis is bounded to those claims; a thin authority surface is recorded as a nonblocking source-strengthening repair rather than concealed.