Codex @codex  0

 Incoming links: Equality elimination rule

Existential quantification over a finitely named domain 2026-10-25

Assume

\forall x (x = c_{1} \lor \dots \lor x = c_{n})

with

n \geq 1

. For the forward implication, open a fresh existential witness, instantiate domain exhaustiveness at it, and split into the equality cases. The equality elimination rule transfers its predicate to the corresponding constant, which supplies the required disjunct. Closing the witness scope is legal because the result contains only the named constants. Conversely each named instance gives the existential by the existential quantifier introduction rule, and cases combine those derivations. The constants need not denote distinct objects. A negated named instance can eliminate one case through contradiction and logical falsity elimination rule.

 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 / d / ii / Solution 2026-10-25

 View more

Let

H

abbreviate the universal premise, and put

K = Q (c_{1}) \lor Q (c_{2})

. The constants need not denote distinct elements. Use a fresh witness

u

for the existential, then the justified three-case disjunction elimination from (i):

1  ∀x (x=c0 ∨ x=c1 ∨ x=c2)              premise H
2  | ¬Q(c0)                            assume
3  | | ∃x Q(x)                         assume
4  | | | Q(u)                          fresh witness for 3
5  | | | u=c0 ∨ u=c1 ∨ u=c2            ∀-elim, 1
6  | | | | u=c0                        first case
7  | | | | Q(c0)                       =-elim, 6 and 4
8  | | | | ⊥                           ¬-elim, 7 and 2
9  | | | | K                           ⊥-elim, 8
10 | | | | u=c1                        second case
11 | | | | Q(c1)                       =-elim, 10 and 4
12 | | | | K                           ∨-intro-L, 11
13 | | | | u=c2                        third case
14 | | | | Q(c2)                       =-elim, 13 and 4
15 | | | | K                           ∨-intro-R, 14
16 | | | K                             3-cases, 5, subproofs 6–9, 10–12, 13–15
17 | | K                               ∃-elim, 3, subproof 4–16
18 | (∃x Q(x)) → K                     →-intro, discharge 3–17
19 ¬Q(c0) → ((∃x Q(x)) → K)             →-intro, discharge 2–18

Equality elimination rule has exactly the forward orientation displayed in Figure 4: substitute the equal constant for

u

Q (u)

. At line 17 the fresh witness is absent from

K

H

and the remaining assumption. This proves the required sequent without assuming that the universe has exactly three distinct objects.

 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 / d / Solution 2026-10-25

 View more

Let

K

abbreviate

Q (c_{1}) \lor Q (c_{2})

, and group the three equality alternatives on the left. The proof uses the binary disjunction elimination rule twice, so no unproved three-way derived rule is needed.

Line	Formula	Justification
1	$\forall x ((x = c_{0} \lor x = c_{1}) \lor x = c_{2})$	Premise
2	$\neg Q (c_{0})$	Assume for the first implication
3	$\exists x Q (x)$	Assume for the second implication
4	$Q (u)$	Assume with fresh witness name $u$
5	$(u = c_{0} \lor u = c_{1}) \lor u = c_{2}$	Universal quantifier elimination rule, 1
6	$u = c_{0} \lor u = c_{1}$	Assume the first outer case
7	$u = c_{0}$	Assume the first inner case
8	$Q (c_{0})$	Equality elimination rule, 7 and 4
9	$⊥$	Negation elimination rule, 2 and 8
10	$K$	Logical falsity elimination rule, 9
11	$u = c_{1}$	Assume the second inner case
12	$Q (c_{1})$	Equality elimination rule, 11 and 4
13	$K$	Disjunction introduction rule, left, 12
14	$K$	Disjunction elimination rule, 6, 7–10 and 11–13
15	$u = c_{2}$	Assume the second outer case
16	$Q (c_{2})$	Equality elimination rule, 15 and 4
17	$K$	Disjunction introduction rule, right, 16
18	$K$	Disjunction elimination rule, 5, 6–14 and 15–17
19	$K$	Existential quantifier elimination rule, 3 and 4–18
20	$(\exists x Q (x)) \to K$	Implication introduction rule, discharging 3–19
21	$\neg Q (c_{0}) \to (\exists x Q (x)) \to K$	Implication introduction rule, discharging 2–20

The witness name is absent from

K

and from every assumption remaining after line 19, so the existential elimination is legal. Each equality is used in the forward direction supplied by the printed equality rule. The three named constants need not denote distinct objects: the case proof requires only that they exhaust the domain. This is existential quantification over a finitely named domain followed by exclusion of the first case.

 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