Types, sorts, labels

Explain the difference between type theory, many-sorted logic, and labelled logic.

Here’s a crisp way to tell them apart.

Type theory

• What it is: A foundational framework where every term has a type, and proofs are programs (Curry–Howard). Judgments look like Γ ⊢ t : A.
• Goal/use: Control formation of expressions, avoid paradoxes, and give computational meaning to proofs. Basis for proof assistants (Coq, Agda) and typed PLs.
• Key features: Functions and data are typed; often supports dependent types (types can mention terms), inductive types, and definitional/propositional equality.
• Semantics: Usually given by constructive/computational models (e.g., type-theoretic or categorical semantics).
• Example: If bornOn : Person → Date, then from p : Person you derive bornOn p : Date. A proposition like “every person has a birth date” is a function type: (p : Person) → Date.

Many-sorted (multi-sorted) logic

• What it is: Ordinary first-order logic but with multiple domains (“sorts”). Symbols come with sort signatures, and quantifiers range over a chosen sort.
• Goal/use: Make FOL more structured and readable by separating domains (Persons, Dates, Books, …).
• Key features: Still classical/intuitionistic FOL proof theory and semantics; no programs-as-proofs. Technically reducible to single-sorted FOL via unary predicates.
• Semantics: A model gives a disjoint nonempty domain for each sort and interprets symbols accordingly.
• Example: ∀p:Person ∃d:Date . BornOn(p,d) with BornOn : Person × Date → Bool.

Labelled logic (labelled deductive systems / labelled sequent/natural deduction)

• What it is: A proof-theoretic style where formulas are annotated with labels that stand for worlds, states, resources, times, etc., and you reason both with formulas and relational atoms between labels.
• Goal/use: Internalize semantics (like Kripke frames) into the calculus to handle modal, temporal, substructural, and non-classical logics cleanly.
• Key features: Judgments look like x : A alongside relational facts like x R y; rules manipulate labels and relations (e.g., for □/◇ in modal logic).
• Semantics: Labels mirror semantic structures (accessibility, orderings, resource composition). It’s a technique that can be combined with many base logics (including many-sorted or typed settings).
• Example (modal): From x R y and y : A infer x : ◇A. Or x : □A means “A holds at all y with x R y”.

---

Quick comparison

Axis	Type theory	Many-sorted logic	Labelled logic
Main idea	Classify terms by types; proofs-as-programs	Partition the domain into sorts within FOL	Annotate formulas with labels for worlds/resources
Typical judgment	Γ ⊢ t : A	⊢ φ with sort-correct terms	Γ; Σ ⊢ x : A with relational atoms in Σ
Expressiveness	Very high (e.g., dependent types, inductives)	FOL-level (more organized syntax)	Varies; extends a base logic’s proof system
Computation	Built-in (normalization, type checking)	None inherent	None inherent; proof-structural device
Reducibility	Not just “sugar” over FOL	Reducible to single-sorted FOL	Not a separate logic; a proof calculus style
Typical use	Proof assistants, PL theory, foundations	Clean specs/models with multiple domains	Modal/temporal/substructural proof theory

Common confusion to avoid

• Types vs sorts: both “classify,” but sorts are a semantic partition inside (otherwise standard) FOL and are eliminable; types govern term formation and computation, often with propositions-as-types and dependencies.
• Labelled vs typed/sorted: labels annotate where/under which conditions a formula holds (e.g., world x), not what kind of thing a term is. You can have labelled calculi with many sorts or types—these concerns are orthogonal.

If you want, I can show the same example (say, a tiny modal spec about knowledge or time) in all three styles side-by-side.