free variable

自由变元

Foundations & Logic · Undergraduate · Mathematics Resources editorial compilation (AI-assisted)

Translation evidence: Literature usage

Meaning in context

A variable is free in a formula if at least one occurrence is outside any quantifier binding that occurrence.

若变元在公式中至少有一次出现未被相应量词约束，则它是该公式的自由变元。

Example

yy is free in ∀x  (x+y=y+x)\forall x\;(x+y=y+x).

Usage and distinctions

Freedom is a property of occurrences first: one variable can have both free and bound occurrences.

Recommended reading in this subject · Preparation & skip guidance

Definition sources

  1. Avigad, Hua, Lewis and van Doorn — Logic and Proof§7.2 The Universal Quantifier; §7.3 The Existential Quantifier · Checked 2026-10-14

Translation sources

  1. 杨睿之（复旦大学）— 数理逻辑，第15讲PDF p.4 前情提要：「自由变元的语义」 · Checked 2026-10-14
Edit source / propose a PRReport a correction

Original encyclopedia and terminology content: CC BY-SA 4.0. Contribute or report a correction.