Eigenvariable

1 Eigenvariable in Logic

1.1 Definition and purpose

An eigenvariable is a variable that is introduced in a formal derivation to denote an unknown but fixed object or witness during the remainder of a local proof segment. Unlike a variable that is meant to be later instantiated, an eigenvariable is constrained to behave as though it were a new symbol chosen specifically for the proof: it may be referenced in subsequent steps, but it must not be replaced by arbitrary terms at will in a way that changes the intended meaning of the derivation.

In practice, eigenvariables are used to manage reasoning involving quantifiers while preserving correctness. They provide a disciplined way to move between quantified statements without accidentally assuming more than the proof rules allow.

1.2 Relationship to quantifiers

Eigenvariables typically appear in rules for manipulating universal and existential quantifiers:

• For a universal quantifier, one often reasons by selecting an arbitrary instance. The chosen term is conceptually arbitrary, and the logical correctness depends on not restricting it using information that should only be available after the quantifier step.
• For an existential quantifier, one often introduces a witness. The witness may be represented by a fresh name (e.g., a constant) or, in related proof systems, by an eigenvariable constrained appropriately to the derivation context.

Thus, eigenvariables function as controlled placeholders enabling sound transitions between statements quantified over potentially infinite domains.

1.3 Freshness and constraints

The defining requirement for an eigenvariable is freshness: it must not clash with existing variables or be improperly bound by surrounding quantifiers. Freshness is enforced so that the eigenvariable does not capture, identify, or coincide with symbols whose meaning is already determined in the proof context.

Beyond mere non-collision, many proof systems impose additional constraints, such as limiting where the eigenvariable may appear, requiring that it not occur in certain assumptions, or ensuring it does not become constrained by later instantiations. Collectively, these conditions guarantee that the eigenvariable behaves like a genuinely new, fixed symbol used only for that reasoning step.

2 Formal Proof Rules Using Eigenvariables

2.1 Universal quantifier instantiation

2.1.1 Eigenvariable conditions for instantiation

In systems where universals are handled by a rule resembling universal instantiation, an eigenvariable is often used to represent an arbitrary element in a way that respects the rule’s side conditions. The typical pattern is: to prove a statement from a universally quantified premise, one may introduce a fresh eigenvariable representing an arbitrary element and derive the target from that premise using the eigenvariable as if it were completely general.

Whether the rule is stated using an eigenvariable or an arbitrary term, the key is that the chosen object must not depend on assumptions that are not yet justified at that point in the derivation. Side conditions formalize this “not dependent” constraint.

2.1.2 Why freshness preserves soundness

Soundness can fail if the proof system allows an instantiation that effectively smuggles in extra information. If the “arbitrary” element chosen for a universal reasoning step shares a name or constraints with variables introduced elsewhere, the derivation may inadvertently treat it as special rather than general.

Freshness prevents accidental identification with existing symbols and blocks unintended capture. As a result, the universally quantified information is used uniformly: the derivation does not become valid only because the instantiation accidentally matches a particular case built into the proof context.

2.2 Existential quantifier reasoning

2.2.1 Skolemization vs eigenvariables

Existential reasoning is closely related to Skolemization, which replaces an existential quantifier with a Skolem function or constant depending on the surrounding universally quantified variables. Eigenvariables appear in similar roles in some rule presentations, where the system introduces a witness name under side conditions to represent a specific but otherwise unconstrained element satisfying the existential property.

The conceptual relation is:

• A Skolem term is a syntactic replacement used to eliminate an existential quantifier while keeping the proof correct via the structure of dependencies.
• An eigenvariable can serve as a witness placeholder constrained by the proof context, often ensuring that the witness is not incorrectly tied to assumptions that should not determine it.

Different proof systems phrase these ideas differently, but both are mechanisms for managing witnesses without invalid inference.

2.2.2 Typical proof-patterns

A common proof pattern for existential elimination uses the idea that, from a claim that “there exists an element with property P,” one may reason by assuming an arbitrary witness with property P and deriving a conclusion C. To keep the reasoning sound, the witness is introduced using a fresh name (or eigenvariable) and the conclusion is required to be independent of the specific identity of that witness.

In many presentations, the rule ensures that the witness name does not escape into contexts where it would become improperly generalized or where it would conflict with existing variables.

2.3 Natural deduction treatments

2.3.1 Rules for universal introduction

In natural deduction systems, universal introduction often requires that the variable used to derive the universal statement is not dependent on any undischarged assumptions. A typical constraint is: if one derives a formula containing a variable that is introduced as an eigenvariable, then one may generalize it to a universal quantification provided that variable does not occur in any open assumptions relevant to the derivation.

This mirrors the freshness intuition: the generalized statement must not accidentally rely on information that is specific to the chosen variable instance.

2.3.2 Rules for existential elimination

For existential elimination, natural deduction uses a witness name introduced under a temporary assumption. The rule allows one to use that witness to prove the desired conclusion, but it must then discharge the witness assumption and produce a result that does not depend on the witness’s particular identity.

Freshness and non-dependence conditions are again central. They prevent the proof from using hidden information about the witness that is not justified by the existential claim alone.

3 Eigenvariables in Sequent Calculus

3.1 Sequent-style quantifier rules

Sequent calculus expresses derivations in terms of sequents, typically of the form “from assumptions Γ derive conclusion Δ.” Quantifier rules in sequent calculi often include explicit side conditions to ensure that eigenvariables are used correctly when introducing or eliminating quantifiers.

For example, a rule for a universal quantifier on the right may require introducing a fresh variable representing an arbitrary element, and a corresponding rule for an existential quantifier may require freshness to serve as a witness without invalid dependencies.

3.2 Eigenvariables on the left vs right

In sequent calculus, quantifier polarity matters:

• On the left (under assumptions), eigenvariables are usually constrained so that the assumed quantified statement is used in a way compatible with the rest of the sequent.
• On the right (as a goal), eigenvariables often represent an arbitrary element or a witness whose existence or arbitrariness must be guaranteed by the proof structure rather than by accidental coincidences.

This left/right distinction affects the exact side conditions required to maintain soundness, because assumptions and goals are treated asymmetrically in sequent calculi.

3.3 Capture avoidance and renaming

A central technical aspect is variable capture avoidance. If an eigenvariable were allowed to collide with a variable bound by a quantifier, then substituting or rearranging formulas could change meanings. To avoid this, rules typically assume that eigenvariables are fresh and employ alpha-conversion, renaming bound variables where necessary.

In effect, eigenvariables rely on disciplined renaming so that the syntactic manipulation performed by proof rules corresponds to the intended semantic reasoning.

3.4 Variable hygiene across proof steps

Eigenvariables introduce a hygiene discipline: once an eigenvariable is introduced, it should be treated consistently in later steps within its scope, and it should not be replaced by arbitrary terms or merged with unrelated symbols.

Good “variable hygiene” ensures that when proof steps are composed, the eigenvariables from different rule applications do not interfere, and quantifier structure remains faithful. Proof systems often implement this discipline using freshness checks and systematic renaming.

4 Correctness and Soundness Considerations

4.1 Common failure modes without freshness

If eigenvariable freshness is ignored, typical failures include:

• Accidental specialization: treating an “arbitrary” element as if it were constrained by existing assumptions through name collisions.
• Variable capture: allowing a variable to become bound unexpectedly after substitution or rearrangement, changing the meaning of formulas.
• Improper dependencies: letting an eigenvariable depend on assumptions that should not determine it at that stage of the proof.

Each failure breaks the guarantee that the proof rules reflect valid reasoning about quantifiers.

4.2 Alpha-conversion and equivalence

Correctness arguments frequently use the fact that proofs are invariant under alpha-conversion, meaning that renaming bound variables does not change logical meaning. With eigenvariables, alpha-conversion supports the ability to rename bound variables to restore freshness without affecting validity.

As a result, many soundness proofs treat eigenvariable conditions modulo such renamings, focusing on the semantic role rather than the literal spelling of variable names.

4.3 Interaction with substitutions

Substitutions are the main mechanism by which proofs transform expressions. Eigenvariables constrain substitutions by making it invalid to substitute freely for the eigenvariable in ways that would change the intended “fixed but unknown” role. When a proof rule introduces an eigenvariable, subsequent substitutions must respect its restricted status and must not reintroduce unsound dependencies.

In proof-theoretic terms, eigenvariables often represent a choice that cannot be later revised, so substitution operations must be constrained or carefully sequenced.

4.4 Completeness intuitions

Completeness relates to whether the proof system can derive all valid statements. Eigenvariable conditions are designed to be strong enough to preserve soundness but not so restrictive that they prevent deriving valid formulas.

Intuitively, completeness is maintained because any valid proof can be translated into a form where necessary witnesses or arbitrary elements are represented by fresh names and where alpha-renaming and disciplined substitution reconstruct the intended reasoning.

Although formal completeness proofs can be technical, the core intuition is that eigenvariable conditions are bookkeeping constraints that mirror the semantics of quantifiers rather than adding unjustified limitations.

5 Examples and Proof Sketches

5.1 Simple universal reasoning with eigenvariables

Suppose one has a premise asserting that every element satisfies a property P. To show that some conclusion follows, one can introduce a fresh eigenvariable a to represent an arbitrary element. From the universal premise, infer P(a), then proceed using P(a) to derive the desired result, ensuring that any final universal statement does not improperly depend on a.

The eigenvariable acts as a stand-in for an arbitrary element without being tied to special information from elsewhere in the context.

5.2 Deriving consequences while keeping variables fixed

Consider a derivation where a quantified premise is used to establish an intermediate claim. The eigenvariable is kept fixed through the relevant steps so that the derivation corresponds to reasoning about a single arbitrary instance, not a changing one.

This fixedness is crucial: if the proof allowed the “instance” represented by the eigenvariable to vary implicitly, then rules for quantifier introduction or elimination would no longer match their intended interpretation.

5.3 Worked proof skeletons

A typical skeleton for universal introduction in a natural deduction style is:

1. Introduce a fresh eigenvariable x.
2. Derive a statement φ(x) under assumptions that do not mention x as a free dependency (aside from the step introducing x).
3. Discharge any temporary assumptions and conclude ∀x φ(x), justified by the fact that x is fresh relative to undischarged assumptions.

For existential elimination:

1. Assume ∃x φ(x).
2. Temporarily assume φ(c) for a fresh eigenvariable c.
3. Derive the goal ψ without using c in a way that makes ψ depend on the specific choice of c.
4. Conclude ψ by eliminating the existential assumption.

These skeletons illustrate how freshness ensures that the rules correspond to uniform quantifier reasoning.

6 Related Concepts

6.1 Free vs bound variables

Variables in logical formulas may be bound by quantifiers or free relative to the formula. Eigenvariables function as specific symbols introduced during proof construction; they behave like controlled placeholders whose occurrences are intended to be free within a particular sub-derivation, while still respecting the quantifier structure that binds other variables.

Freshness constraints are closely tied to the distinction between free and bound occurrences, since capture occurs when substitutions convert free occurrences into bound ones.

6.2 Skolem constants and Skolem functions

Skolemization replaces existential quantifiers by Skolem terms, which may be constants (no dependency) or functions (dependent on surrounding variables). These terms embody witness choices that preserve satisfiability or validity in the transformed formulas under the standard logical metatheory.

Eigenvariables and Skolem terms are conceptually linked: both represent witness-like objects introduced to handle quantifiers, though they arise in different proof-theoretic ways.

6.3 Unification variables (contrast)

Unification variables (often used in automated theorem proving and logic programming) represent placeholders whose values are determined by unification during proof search. By contrast, eigenvariables are introduced to represent unknown but fixed elements with strict restrictions on how they may be instantiated.

The main contrast is that unification variables are typically solved for, whereas eigenvariables are kept as fresh names to preserve rule soundness.

6.4 Name generation and variable management

Modern proof environments treat eigenvariables as part of a broader name management discipline. Name generation must ensure freshness, record scope, and enforce hygiene rules automatically to prevent capture and invalid substitutions.

This discipline often underlies tactic frameworks and proof elaborators, where quantifier rules are implemented using systematic renaming and constraint checking.

7 Implementation Notes (Proof Assistants)

7.1 Fresh-name generation strategies

Proof assistants typically implement freshness using generators that create new identifiers not used elsewhere in the current context. Strategies include:

• using internal unique identifiers,
• tracking used names and selecting a new one,
• or using de Bruijn indices internally to avoid name clashes altogether.

Even when names are user-facing, the system often relies on an internal representation that simplifies capture avoidance.

7.2 Checking eigenvariable conditions

When applying a quantifier rule that requires an eigenvariable, the assistant must verify side conditions such as:

• the variable is fresh with respect to specified contexts,
• the eigenvariable does not occur in forbidden sets of assumptions,
• dependencies are respected, especially when generalizing or discharging assumptions.

These checks are typically integrated into the kernel’s rule application mechanism to ensure that only sound derivations are accepted.

7.3 Automation and tactic constraints

Automation tools must handle eigenvariables carefully. Tactics that perform substitution, rearrangement, or proof search can inadvertently introduce variable conflicts if they do not preserve freshness.

As a result, tactic frameworks often restrict certain operations, require renaming before unification-like steps, or provide specialized combinators that encapsulate correct eigenvariable handling.

7.4 Error messages and debugging variable issues

When variable hygiene fails, the assistant should ideally explain what went wrong: for instance, pointing out a capture-avoidance problem, a violation of a freshness constraint, or an illegal dependency introduced by a substitution.

Good diagnostics help users distinguish between mistakes in their high-level reasoning and low-level issues related to variable scope, renaming, or rule side conditions.