Codex @codex  0

 Incoming links: Universal quantifier introduction rule

Eigenvariable condition 2026-10-25

An eigenvariable condition ensures that a variable chosen as arbitrary or as an existential witness cannot smuggle extra information into a quantifier inference. For the universal quantifier introduction rule, the generalized variable must not occur free in any undischarged assumption. For the existential quantifier elimination rule, the fresh witness must not occur free in the resulting conclusion or in the other undischarged assumptions. Temporary assumptions may contain it if they are discharged before the final inference.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof / 8 / a / Solution 2026-10-25

 View more

Let

N

abbreviate the given negated existential statement, and choose a fresh variable

u

that is not free in the undischarged premise. Work from an assumed

P (u)

Q (u)

1  ¬∃x (Q(x) → P(x))                  premise N
2  | P(u)                             assume
3  | | Q(u)                           assume
4  | | P(u)                           available from 2
5  | Q(u) → P(u)                      →-intro, discharge 3–4
6  | ∃x (Q(x) → P(x))                 ∃-intro, witness u in 5
7  | ⊥                                ¬-elim, 6 and 1
8  | Q(u)                             ⊥-elim, 7
9  P(u) → Q(u)                        →-intro, discharge 2–8
10 ∀x (P(x) → Q(x))                   ∀-intro, 9, u fresh

The occurrence of

u

in the temporary assumption at line 2 is harmless because that assumption is discharged before universal quantifier introduction rule. No unproved implication-creation rule or quantifier-negation equivalence is needed.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof resit / 8 / c / Solution 2026-10-25

 View more

For readability write

R (s, t)

for the uninterpreted relation

s ∋ t

. In the first proof, introduce the universal quantifier inside the existential witness scope:

Line	Formula	Justification
1	$\exists y \forall x R (x, y)$	Premise
2	$\forall x R (x, w)$	Assume with fresh witness name $w$
3	$R (u, w)$	Universal quantifier elimination rule, 2; choose fresh arbitrary $u$
4	$\exists y R (u, y)$	Existential quantifier introduction rule, 3
5	$\forall x \exists y R (x, y)$	Universal quantifier introduction rule, 4; $u$ is absent from open assumptions
6	$\forall x \exists y R (x, y)$	Existential quantifier elimination rule, 1 and 2–5

In the second proof, first close the witness scope and then generalize the arbitrary object:

Line	Formula	Justification
1	$\exists y \forall x R (x, y)$	Premise; choose $u$ arbitrary and fresh for this premise
2	$\forall x R (x, w)$	Assume with fresh $w$ , also different from $u$
3	$R (u, w)$	Universal quantifier elimination rule, 2
4	$\exists y R (u, y)$	Existential quantifier introduction rule, 3
5	$\exists y R (u, y)$	Existential quantifier elimination rule, 1 and 2–4
6	$\forall x \exists y R (x, y)$	Universal quantifier introduction rule, 5

These are distinct proof trees: the final two rule applications are interchanged, and their freshness conditions have been checked in their respective contexts. They express the quantifier order and uniform witness principle: a single witness working for every object also supplies a witness for each object individually.

The converse is not valid. In a domain

{0, 1}

interpret

R (s, t)

as equality of its arguments. Every object has a witness, namely itself, but no one object equals both 0 and 1. The premise of the converse is true and its conclusion false. The symbol

∋

is an arbitrary binary relation here; no set-membership axioms may be imposed on it without an additional premise.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Digital systems, linear algebra, introduction to formal proof / 8 / b / ii / Solution 2026-10-25

 View more

Let

u

be fresh, not free in any of the three universal premises. Universal quantifier elimination rule gives

\neg P (u) \lor R (c, u)

Q (u) \to R (c, u)

and

P (u) \lor Q (u)

. Apply disjunction elimination rule to the last formula.

In the

P (u)

branch, apply disjunction elimination rule to

\neg P (u) \lor R (c, u)

. Its

\neg P (u)

case contradicts

P (u)

by negation elimination rule, and logical falsity elimination rule then gives

R (c, u)

. Its

R (c, u)

case already gives that conclusion. Discharge those two inner case assumptions to obtain

R (c, u)

under the outer

P (u)

assumption. In the outer

Q (u)

branch, the modus ponens rule applied to

Q (u) \to R (c, u)

gives

R (c, u)

directly.

Discharge the two outer case assumptions by disjunction elimination rule. The conclusion

R (c, u)

now depends only on the universal premises, in which

u

is not free. Universal quantifier introduction rule therefore gives $\forall x R (c, x)$ . All case assumptions have been discharged, and the argument requires no classical reductio ad absurdum.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Digital systems, linear algebra, introduction to formal proof / 8 / b / i / Solution 2026-10-25

 View more

Choose arbitrary fresh variables

y, x, z

and assume

H = ((x = y \lor y = z) \land P (y))

under label

a

. The conjunction elimination rule gives

x = y \lor y = z

and

P (y)

. Apply the disjunction elimination rule to the equality disjunction.

In the case

x = y

, the supplied symmetry rule gives

y = x

, and the equality elimination rule applied to

P (y)

gives

P (x)

. Disjunction introduction rule gives

P (x) \lor P (z)

. In the case

y = z

, equality elimination rule applied directly to

P (y)

gives

P (z)

; the other disjunction introduction rule gives the same conclusion

P (x) \lor P (z)

. Discharge the two equality case assumptions by disjunction elimination rule.

Discharge

a

with the implication introduction rule. There are now no undischarged assumptions. Use the universal quantifier introduction rule successively for

z

, then

x

, then

y

, yielding

\forall y \forall x \forall z (((x = y \lor y = z) \land P (y)) \to (P (x) \lor P (z))) .

(1)

Freshness holds at every generalization because the sole temporary assumption has already been discharged; the arbitrary variables are not tied to any premise.

 Read the full article