Formal Theory¶

A set of sentences in a formal language, commonly closed under a specified consequence relation, that serves as the asserted or derivable content interpreted within models.

Version: v2 · 2026-09-06 · History
Domain-specific #: 1865
Origin domain: mathematical logic
Subdomain: formal theories and model theory
Aliases: Theory in mathematical logic, Deductively closed theory

Core Idea¶

Formal Theory is a set of sentences in a formal language, commonly closed under a specified consequence relation, that serves as the asserted or derivable content interpreted within models. ^[1]

Fix a formal language L. A theory T is a set of L-sentences; many texts reserve or emphasize deductive closure, so if T entails phi then phi belongs to T, while others call any axiom set a theory and write its closure separately. The convention must be stated. Models of T are L-structures satisfying every sentence in T, and syntactic properties such as consistency, completeness, decidability, and finite axiomatizability attach to the declared T and consequence relation.

The operative boundary is exact: The content-bearing sentence set distinguished from the formal machinery that generates or tests it remains uncovered. The abstraction is therefore not the topic named by its field, but the reusable role structure specified below.

Structural Signature¶

Sig role-phrases:

the formal language L — the vocabulary and formation rules for terms and sentences
the sentence set T — the asserted content constituting the theory
the consequence relation — semantic entailment or a proof relation under which closure may be taken
the axiomatization — a possibly smaller generating set whose closure is T
the model class Mod(T) — structures satisfying every sentence in the set
the consistency condition — absence of contradiction under the chosen logic
the completeness question — whether each sentence or its negation is decided
the effectiveness profile — decidability, recursive enumerability, and finite axiomatizability properties

Recognition test. A case qualifies only when its roles can be mapped to the declared the formal language L, the sentence set T, the consequence relation, the axiomatization, and when the characteristic boundary conditions are preserved. Surface vocabulary or a loose analogy is insufficient.

What It Is Not¶

Not the whole formal system. A theory is its sentence-level content, not the entire package of alphabet, grammar, proof machinery, and metalanguage.
Not necessarily a finite axiom list. The sentence set or its axiomatization can be infinite.
Not necessarily deductively complete. Consistency does not imply that every sentence is decided.
Not one intended model. A theory generally has a class of models.
Not an empirical scientific theory. The mathematical-logic term concerns formal sentences and consequence.
Not the same object under every convention. Authors differ on whether 'theory' already means consequence-closed.

Scope of Application¶

The abstraction has a bounded but recurring habitat. These are literal applications of the same domain machinery, not cross-domain metaphors. ^[1]

Model theory. theories are classified through models, elementary equivalence, categoricity, and definability.
Proof theory. axiomatizations and derivability expose strength, consistency, and conservativity.
Foundations. arithmetic, set theory, and type theories formalize mathematical commitments.
Computability. decision procedures and enumerability are studied for consequence sets.
Algebra and geometry. first-order theories describe fields, groups, orders, and other structure classes.
Theory comparison. extensions, reducts, interpretations, and conservative additions relate formal contents.

Clarity¶

Axioms and theory are not always coextensive. A finite axiom set A can generate an infinite consequence-closed T. Conversely, under the looser convention A itself may be called a theory. A reference-grade entry therefore records both the sentence set and the closure convention before comparing size or decidability.

A useful audit proceeds in order: identify the candidate roles, verify their types and quantifiers, apply the recognition test, and then test every stated exclusion. If a case supplies only the broad parent pattern while dropping the domain accent, it is not Formal Theory.

Manages Complexity¶

The abstraction separates content from machinery and from models. A vast class of structures can be represented by one sentence set; a vast consequence set can be represented by a small axiomatization; and metatheorems can compare theories without re-proving every sentence individually.

The compression remains accountable because every simplification has a named validity condition. A user can ask which role is missing, which assumption fails, and which neighboring abstraction should replace the candidate instead of treating the label as an unanalyzed bundle.

Abstract Reasoning¶

R1. Fix language, logic, and consequence relation first.

R2. State whether T is an axiom set or already deductively closed.

R3. Separate syntactic derivability from semantic entailment before invoking completeness theorems.

R4. Keep consistency, completeness, categoricity, and decidability as distinct properties.

R5. Compare theories through inclusion only when their languages and closure conventions align.

The reasoning pattern is deliberately typed: definitions establish identity, calculations or constructions establish consequences, and empirical or institutional evidence establishes whether a real case instantiates the roles. One kind of support cannot silently substitute for another.

Knowledge Transfer¶

The theory concept transfers literally across formal disciplines that supply languages and consequence relations. Generic bodies of belief or explanatory frameworks share only a loose analogy. The portable parent is Formal System; the residual domain identity is the sentence set as an object of mathematical logic.

The transfer boundary follows from the classification test: The sentence-set role recurs across logic and formal mathematics, but language, consequence relation, axiomatization, closure, consistency, completeness, and model class remain constitutive logical semantics. The safe portable move is to name the broader parent when the home-domain machinery is absent and to retain the domain name only when literal recognition succeeds.

Examples¶

Canonical: group theory in first-order logic¶

Use a language with multiplication, inverse, and identity symbols. Let A contain the group axioms. Its first-order consequence closure T consists of every sentence true in all groups by logical consequence. Mod(T) is the class of groups. T is not one group and is much larger than the short axiom list that generates it. ^[1]

Mapped back: the formal language L; the sentence set T; the axiomatization; the consequence relation; the model class Mod(T).

Applied / In Practice: extending arithmetic¶

Start with a formal arithmetic theory T and add a sentence sigma. The extension T+sigma may decide questions that T leaves open, but it must be checked for relative consistency and whether the added sentence changes consequences in a target sublanguage. Calling the extension 'stronger' requires specifying the ordering—sentence inclusion, interpretability, or proof-theoretic strength. ^[1]

Mapped back: the sentence set T; the consistency condition; the completeness question; the effectiveness profile.

Structural Tensions¶

T1: Axiom set versus closure. A finite presentation aids use, while the full theory captures invariant consequence content. Diagnostic: Which convention does T denote?

T2: Syntax versus semantics. Derivability and truth in all models can coincide under a completeness theorem, but they are defined differently. Diagnostic: Is the current claim proof-theoretic or model-theoretic?

T3: Consistency versus completeness. Avoiding contradiction does not guarantee a decision for every sentence. Diagnostic: Which property has actually been established?

T4: Expressive language versus tractability. Richer languages state more directly but often worsen decidability and model behavior. Diagnostic: What effectiveness is lost by the added expressive resources?

T5: Intended model versus noncategoricity. Axioms may aim at one structure while admitting many nonisomorphic models. Diagnostic: Has categoricity been proved in the relevant cardinality and logic?

T6: Domain autonomy vs prime reduction. Formal System supplies rules and proof machinery, but it does not identify the asserted or closed sentence set whose models and metaproperties are studied. Diagnostic: Can the content vary while the formal system stays fixed? If yes, retain the distinct domain node.

Structural–Framed Character¶

The five-criterion aggregate is 0.10 (structural). The classification is reasoned rather than cosmetic:

Vocabulary travels — structural (0.25). The operative vocabulary retains the home-domain types named in the Structural Signature even when a thinner parent pattern travels.
Evaluative weight — structural (0.00). The score records whether applying the abstraction requires a normative or interpretive judgment in addition to structural recognition.
Institutional origin — structural (0.00). The score records whether the abstraction is constituted by a scholarly, legal, technical, or administrative convention rather than merely discovered in nature.
Human-practice bound — structural (0.00). The score records how far the named roles depend on a human practice, measurement regime, language, or institution.
Import versus recognize — structural (0.25). Beyond its home habitat, use of the name increasingly becomes import by analogy rather than recognition of the same mechanism.

The portable skeleton is: select assertions in a rule-governed language and close or evaluate them under a consequence relation. That skeleton belongs to the related parent abstractions; it does not make the fully accented node a prime. Its character: structural, with a real structural core whose recognition remains bounded by domain-specific types and validity conditions.

Structural Core vs. Domain Accent¶

This section decides why Formal Theory is a domain-specific abstraction rather than a prime.

Structural core: Select assertions in a rule-governed language and close or evaluate them under a consequence relation. This relational skeleton can recur outside the home domain and is the part legitimately carried by broader primes.

Domain accent: Formal sentences, axiomatization, semantic models, proof relations, consistency, completeness, and decidability. Remove those types and constraints and the result may still resemble the skeleton, but it is no longer recognized as this named abstraction.

Why it does not clear the prime bar: Formal systems are portable machinery; formal theories are content-bearing sentence sets inside that machinery and have their own model-theoretic identity. Cross-domain transfer is therefore routed through the parents, while the named entry remains available for precise in-domain diagnosis.

Formal System. is the strict parent furnishing language and inference.
Consistency. is a major property of a theory rather than the theory itself.
Axiom. is a generator or member, not the consequence-closed object.

These are prose relations only. They do not create structured DAG edges, and placement must still pass the live endpoint, redundancy, and cycle checks recorded in the bundle's placement memo.

Relationships to Other Abstractions¶

Current abstraction Formal Theory Domain-specific

Parents (1) — more general patterns this builds on

Formal Theory presupposes Formal System Prime

Formal System. is the strict parent furnishing language and inference.

Children (1) — more specific cases that build on this

Internal Set Theory Domain-specific is a kind of Formal Theory

domain_specific:formal_theory is the proposed minimal parent by strict specialization.

Hierarchy paths (2) — routes to 2 parentless roots

Formal Theory → Formal System → Formalization → Representation → Abstraction

Show alternative path (1)

Neighborhood in Abstraction Space¶

Formal Theory sits in a moderately populated region (60^th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.

Family — Formal Languages, Types & Programs (41 abstractions)

Nearest neighbors

Relational Model — 0.88
Negation as Failure — 0.88
Abstract Syntax Tree — 0.87
Sequent — 0.87
Rice's Theorem — 0.86

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

Not to Be Confused With¶

Formal system. the full syntax-and-inference package. Tell: Can the same machinery carry a different sentence set?
Axiomatization. a generating set for a theory. Tell: Is the object the generators or all consequences?
Model. a structure satisfying the sentences. Tell: Is the object linguistic content or an interpretation?
Metatheory. reasoning about theories and proof systems. Tell: Are statements inside T or about T?
Scientific theory. an empirical explanatory framework. Tell: Are the components formal sentences under a declared consequence relation?

References¶

[1] Herbert B. Enderton, A Mathematical Introduction to Logic, 2^nd ed., Academic Press, 2001. registry ↩a ↩b ↩c ↩d