1 General concept

Embedding is a way of placing one mathematical or logical structure inside another while retaining the features that matter for the intended analysis. The source object is mapped into a target object in a controlled manner, so that the source can be studied as if it were part of the larger setting. This idea appears throughout mathematics, logic, and computer science because it provides a bridge between systems that may differ in size, language, or level of abstraction.

1.1 Definition and basic idea

At its core, an embedding is a structure-preserving map from one system into another. The map is usually required to be faithful enough that distinct elements remain distinct and the relevant relations, operations, or truths are not distorted. In many settings, an embedded object behaves like a copy of the original object inside the target.

1.2 Faithful representation

A faithful representation preserves the information needed to recover the original structure from its image. This does not always mean that every aspect is preserved in every possible sense, but rather that the chosen properties are carried over accurately. In logic, this often means that formulas, derivations, or semantic consequences remain valid under translation.

1.3 Relationship to substructures

An embedded structure is often identified with its image, which then functions as a substructure of the larger one. This viewpoint is especially useful when the target contains additional elements or operations not present in the source. The source retains its identity through the embedding, even though it is now situated within a broader context.

1.4 Examples from logic and mathematics

Common examples include the inclusion of the natural numbers into the integers, the embedding of a graph into another graph that preserves adjacency, and the translation of one formal system into another. In each case, the original object is not merely transformed but represented in a way that keeps its essential pattern intact. Such examples illustrate why embeddings are central tools for comparing structures.

2 Embedding in model theory

In model theory, embeddings are maps between structures that preserve the interpretation of symbols from a language. They are used to compare models, transfer properties, and analyze how theories behave across different domains. The strongest forms preserve all first-order truths, while weaker forms preserve only selected relations or functions.

2.1 Elementary embeddings

An elementary embedding preserves the truth of every formula in the language under consideration. If a statement holds in the source structure for certain elements, then its translated version holds in the target for the images of those elements. This makes elementary embeddings especially powerful, since they carry across not only atomic facts but also complex logical consequences.

2.2 Elementary submodels

When the image of an elementary embedding is a substructure of the target, it is called an elementary submodel. Such submodels satisfy exactly the same first-order sentences as the larger model, relative to parameters from the smaller one. They provide a precise way to isolate a portion of a model that remains logically indistinguishable from the whole, at least within the chosen language.

2.3 Preserving formulas and truth

Model-theoretic embeddings are judged by how well they preserve formulas, satisfaction, and definable relations. A good embedding ensures that the logical behavior of elements is maintained after translation. This property is crucial when transferring theorems between models or studying whether a structure can be realized inside another without changing its logical profile.

2.4 Initial and end extensions

Some embeddings arise from extending a structure at one end or in an initial segment. An initial extension adds new elements without altering the earlier part of the order, while an end extension places new elements beyond all existing ones. These constructions are useful in ordered structures and set-theoretic contexts, where the placement of new elements affects what can be expressed or proved.

3 Embedding in proof theory

In proof theory, embedding often refers to the interpretation of one formal theory within another. The goal is to translate proofs, derivations, or inference rules in a way that preserves provability. This allows one to compare proof systems and to establish metatheoretic results about their relative strength.

3.1 Theory interpretations

A theory interpretation maps the symbols and axioms of one theory into another theory so that the translated axioms are derivable in the target. If the interpretation is successful, the source theory can be studied through the proof resources of the target. Such interpretations are frequently used to show that one formal system can simulate another.

3.2 Relative consistency

One major use of embeddings in proof theory is to establish relative consistency. If a theory can be embedded into a second theory that is already known to be consistent, then the first theory is shown to be consistent relative to the second. This does not give absolute consistency, but it demonstrates that the source theory does not introduce contradictions beyond those already present in the target framework.

3.3 Conservativity results

Embeddings can also support conservativity results, which show that a stronger theory does not prove new theorems of a certain restricted form about the weaker theory. Such results help explain which additions to a formal system increase expressive or deductive power and which merely restate existing content in a richer language. They are important in measuring the effect of axioms and extensions.

3.4 Proof translations

A proof translation converts derivations from one calculus into another while maintaining their validity. The translated proof may be longer or more complex, but it must still establish the corresponding conclusion in the target system. Proof translations are central in comparing deductive systems such as natural deduction, sequent calculus, and Hilbert-style formulations.

4 Embedding in formal languages

Formal languages can be embedded into one another by translating symbols, formulas, and rules in a way that respects meaning. This is common when one language is less expressive, more specialized, or more convenient for a particular purpose. The aim is to represent the source language faithfully inside the target language.

4.1 Language translations

Language translation replaces the vocabulary of one formal system with expressions in another. The mapping must preserve how terms and sentences are built, so that grammatical structure is retained. When done well, translation makes it possible to compare theories that originally appear unrelated.

4.2 Encoding syntax

Syntax can be encoded within a target language by representing expressions as structured objects such as numbers, trees, or sequences. This method allows statements about formulas, proofs, and derivations to be discussed inside a formal framework. Encoding syntax is a standard technique in logic and metamathematics because it turns abstract linguistic behavior into manipulable objects.

4.3 Semantic preservation

An embedding of languages is semantically successful when truth, satisfiability, or entailment is preserved under translation. This ensures that what counts as valid in the source remains valid in the target, within the limits of the chosen interpretation. Semantic preservation is essential when a translation is meant to support reasoning rather than merely to rephrase symbols.

4.4 Definitional extensions

A definitional extension enlarges a language by adding new symbols that are explicitly introduced using existing ones. Such extensions are often viewed as conservative embeddings because they do not change the original theory’s content, only its expressive convenience. They simplify notation and can make proofs shorter without altering the underlying logical commitments.

5 Embedding in type theory and lambda calculus

In type theory and lambda calculus, embeddings relate one typed system or term language to another. They are used to model computations, compare expressive power, and transport properties between formal calculi. Since types and terms carry both syntax and meaning, embeddings in this area must preserve computational behavior as well as logical structure.

5.1 Type embeddings

A type embedding assigns types from one system to types in another so that values of the source type can be treated as values of the target type. The mapping often preserves type constructors such as products, sums, or function types. This makes it possible to represent one type discipline within a richer or differently organized one.

5.2 Term translations

Term translations carry expressions from one calculus into another while maintaining reduction behavior and typing relations. A translated term should evaluate or normalize in a way that reflects the original term’s computation. These translations are widely used when comparing programming languages and formal systems with different evaluation rules.

5.3 Soundness of embeddings

An embedding is sound when well-typed or valid source expressions remain well-typed or valid after translation. Soundness is especially important in type theory, where an incorrect embedding could introduce ill-formed terms or break normalization properties. A sound translation gives confidence that the target faithfully simulates the source.

5.4 Curry-Howard correspondences

The Curry-Howard correspondence links logical propositions with types and proofs with programs. Embeddings in this setting can be understood as moving between logical systems and typed calculi while preserving the proof-term relationship. This connection has made embeddings a useful device for transferring results between logic and computation.

6 Structural properties

Embeddings are studied not only by what they preserve, but also by their formal structural properties. Questions about injectivity, composition, and surjectivity help determine how rigid or flexible a given embedding is. These properties also clarify how embeddings differ from stronger or weaker kinds of maps.

6.1 Injectivity and preservation

Many embeddings are injective, meaning that different source elements map to different target elements. Injectivity prevents collapse of distinct objects and is a basic requirement for faithful representation. Along with injectivity, one usually demands preservation of relations, operations, or formulas appropriate to the setting.

6.2 Closure under composition

Embeddings are often stable under composition. If one structure embeds into a second and the second embeds into a third, then the first typically embeds into the third by composing the maps. This closure property makes embeddings a practical tool for building chains of comparisons between multiple systems.

6.3 Isomorphism versus embedding

An isomorphism is a bidirectional embedding that establishes a perfect match between two structures. By contrast, an embedding need not be onto the target, so the source may occupy only a proper part of a larger system. Every isomorphism is an embedding, but not every embedding is an isomorphism.

6.4 Non-surjective embeddings

A non-surjective embedding maps the source into only a portion of the target. This is common and often desirable, since the target may contain extra material that is irrelevant to the source’s structure. Non-surjective embeddings are useful when one wants to study a theory or model as a component of a richer environment.

7 Applications in logic

Embeddings have many applications in logic because they allow one to transport results between systems with different axioms, languages, or proof rules. They are used both to compare foundational frameworks and to construct models with particular properties. In many cases, embeddings provide the mechanism by which an abstract logical result becomes concrete.

7.1 Comparing logical systems

By embedding one logical system into another, logicians can assess similarities and differences in expressive power and deductive strength. If a translation preserves validity and provability, then results in the target may illuminate the source. Such comparisons are especially valuable when systems have distinct syntax but overlapping aims.

7.2 Expressiveness results

Embeddings are often used to show that one formalism can express everything another can, or that it cannot. A successful embedding may demonstrate that a weaker system can simulate a stronger one in some restricted sense. Conversely, the failure of an embedding can indicate genuine limitations in expressive power.

7.3 Completeness and soundness proofs

Embedding techniques sometimes appear in proofs of soundness and completeness. A soundness argument may show that derivability in a source calculus is preserved under translation into a semantics or another calculus. A completeness argument may use an embedding into a canonical or saturated model to show that every semantically valid statement is derivable.

7.4 Model construction techniques

Embeddings are also useful for constructing models with desired features. By placing a partial structure inside a larger one, it becomes possible to extend, refine, or analyze the original while preserving selected properties. This approach is common in set theory, algebraic logic, and the study of definable structures.

Embedding is closely related to several other notions that compare or transfer structure between systems. These concepts overlap, but each emphasizes a different aspect of the relationship. Distinguishing them helps clarify what exactly is preserved and what kind of correspondence is obtained.

8.1 Interpretation

An interpretation translates the symbols and axioms of one theory into another, often with an emphasis on meaning rather than literal structural inclusion. It may preserve provability or truth without requiring a direct substructure-like image. Interpretations are broader than embeddings in some settings and may allow more flexible encodings.

8.2 Representation

Representation refers to presenting one object through another, usually in a way that makes computation or analysis easier. A representation may encode information faithfully without preserving the full structure required by an embedding. In logic, representations are often chosen for convenience, clarity, or technical control.

8.3 Homomorphism

A homomorphism preserves designated operations or relations between algebraic or logical structures. It may collapse distinct elements and therefore need not be injective. Embeddings are typically stronger than homomorphisms because they aim to preserve structure without identifying different source elements.

8.4 Isomorphism

An isomorphism is a structure-preserving bijection with a structure-preserving inverse. It shows that two systems are, for all relevant purposes, the same. Embeddings resemble isomorphisms in their faithfulness, but they may fall short of full equivalence because they do not require surjectivity or a complete two-way match.