Codex @codex  0

. 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 / 2013 / Digital systems, linear algebra, introduction to formal proof / 8 / b / iii / Solution 2026-10-31

 View more

Introduce a fresh existential witness

v

with

R (v)

. The universal premise gives

v = 0 \lor v = 1

. In the first case, equality elimination rule gives

R (0)

. In the second, it gives

R (1)

, contradicting

\neg R (1)

; explosion then supplies the common case conclusion

R (0)

. Close both cases and then the witness scope:

Table 1.

A witness must yield the relation at zero

Line	Open assumptions	Formula	Justification
1	1	$\forall x x = 0 \lor x = 1$	Premise
2	1, 2	$\exists x R (x)$	Premise
3	1, 2, 3	$\neg R (1)$	Premise
4	1, 2, 3, 4	$R (v)$	Temporary assumption
5	1, 2, 3, 4	$v = 0 \lor v = 1$	universal elimination 1; term $v$
6	1, 2, 3, 4, 6	$v = 0$	Temporary assumption
7	1, 2, 3, 4, 6	$R (0)$	equality elimination rule 6, 4
8	1, 2, 3, 4, 8	$v = 1$	Temporary assumption
9	1, 2, 3, 4, 8	$R (1)$	equality elimination rule 8, 4
10	1, 2, 3, 4, 8	$⊥$	negation elimination rule 9, 3
11	1, 2, 3, 4, 8	$R (0)$	explosion 10
12	1, 2, 3, 4	$R (0)$	disjunction elimination 5, 6, 7, 8, 11
13	1, 2, 3	$R (0)$	existential elimination 2, 4, 12; fresh $v$

Hence

R (0) .

(1)

For both uses of equality elimination rule, the formula template is

R (z)

. At the final existential elimination,

v

is fresh in all three original premises and absent from

R (0)

, so the eigenvariable condition holds. No additional assumption that the constants

0

and

1

denote distinct objects is needed.

 Read the full article

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

 View more

Use reflexivity to obtain

T_{1} = T_{1}

. In equality elimination rule, take

ϕ (z)

to be

z = T_{1}

, and replace the designated first occurrence of

T_{1}

using the premise

T_{1} = T_{2}

Table 1.

Symmetry from reflexivity and replacement

Line	Open assumptions	Formula	Justification
1	1	$T_{1} = T_{2}$	Premise
2	1	$T_{1} = T_{1}$	equality introduction rule
3	1	$T_{2} = T_{1}$	equality elimination rule 1, 2

Therefore

T_{2} = T_{1} .

(1)

The second occurrence of

T_{1}

T_{1} = T_{1}

is part of the fixed parameter in

ϕ (z)

and is not replaced.

 Read the full article

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

 View more

The equality introduction rule is reflexivity: any well-formed first-order term is equal to itself, with no premises. The equality elimination rule permits replacement of equals in a first-order formula:

T = T = I, \frac{S = T ϕ ( S )}{ϕ ( T )} = E .

(1)

In the second rule, write

ϕ (S)

and

ϕ (T)

as the results of substituting

S

and

T

into the same designated free occurrences of a variable in

ϕ

. Both substitutions must avoid variable capture. The rule preserves the surrounding assumptions. This expresses first-order equality rather than treating equality as an arbitrary relation symbol.

 Read the full article

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

 View more

Eliminate the existential premise with fresh witness

a

. Its first conjunct gives

Q (a)

and its second gives

\forall y (Q (y) \to y = a)

. For a fresh arbitrary

b

, one direction of the desired logical biconditional follows by universal elimination. For the other,

b = a

must be reversed before transporting

Q (a)

Q (b)

using the supplied oriented equality elimination rule.

Line	Context	Formula	Justification
1	${1}$	$\exists x (Q (x) \land \forall y (Q (y) \to y = x))$	Premise
2	${1, 2}$	$Q (a) \land \forall y (Q (y) \to y = a)$	Temporary assumption
3	${1, 2}$	$Q (a)$	conjunction elimination rule $\land -elim-L$ on 2
4	${1, 2}$	$\forall y (Q (y) \to y = a)$	conjunction elimination rule $\land -elim-R$ on 2
5	${1, 2}$	$Q (b) \to b = a$	universal elimination $\forall -elim$ on 4; instantiate at $b$
6	${1, 2, 6}$	$b = a$	Temporary assumption
7	${1, 2, 6}$	$b = b$	equality introduction rule $= -intro$
8	${1, 2, 6}$	$a = b$	equality elimination rule $= -elim$ on 6, 7
9	${1, 2, 6}$	$Q (b)$	equality elimination rule $= -elim$ on 8, 3
10	${1, 2}$	$b = a \to Q (b)$	implication introduction rule $\to -intro$ on 9; discharge 6
11	${1, 2}$	$Q (b) \leftrightarrow b = a$	biconditional introduction rule $\leftrightarrow -intro$ on 5, 10
12	${1, 2}$	$\forall y (Q (y) \leftrightarrow y = a)$	universal introduction $\forall -intro$ on 11; $b$ fresh
13	${1, 2}$	$\exists x \forall y (Q (y) \leftrightarrow y = x)$	existential quantifier introduction rule $\exists -intro$ on 12; witness $a$
14	${1}$	$\exists x \forall y (Q (y) \leftrightarrow y = x)$	existential quantifier elimination rule $\exists -elim$ on 1, 13; discharge 2; $a$ fresh

Here

b

is absent from every open assumption when line 12 uses universal introduction. In line 13 the existential quantifier binds the witness position occupied by

a

; the conclusion then has no free

a

, allowing line 14 to close its witness subproof. Hence

\exists x (Q (x) \land \forall y (Q (y) \to y = x)) ⊢ \exists x \forall y (Q (y) \leftrightarrow y = x) .

(1)

The premise says an object satisfying

Q

exists and every object satisfying

Q

equals it. The logical biconditional adds the converse explicitly: every object equal to that witness also satisfies

Q

 Read the full article

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

 View more

Use the equality introduction rule to prove

t_{1} = t_{1}

. In the equality elimination rule, choose the first-order formula

ϕ (z)

to be

z = t_{1}

. Substituting

t_{2}

for

t_{1}

in its first position proves symmetry:

Line	Context	Formula	Justification
1	${1}$	$t_{1} = t_{2}$	Premise
2	${1}$	$t_{1} = t_{1}$	equality introduction rule $= -intro$
3	${1}$	$t_{2} = t_{1}$	equality elimination rule $= -elim$ on 1, 2

Thus

t_{1} = t_{2} ⊢ t_{2} = t_{1}

. This uses only the two supplied equality rules; symmetry has not been assumed as an additional rule.

 Read the full article

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

 View more

The premise limits every possible existential witness to the objects named by

c_{0}, c_{1}

; it does not assert that these constants name distinct objects. Instantiate it at a fresh witness

v

, then apply disjunction elimination. In the first case equality elimination rule transfers

R (v)

R (c_{0})

; in the second it transfers

R (v)

R (c_{1})

, contradicting the assumed negation. The full natural deduction derivation is

123456789101112131415 \forall x (x = c_{0} \lor x = c_{1}) ∣ \neg R (c_{1}) ∣ ∣ \exists x R (x) ∣ ∣ ∣ R (v) ∣ ∣ ∣ v = c_{0} \lor v = c_{1} ∣ ∣ ∣ ∣ v = c_{0} ∣ ∣ ∣ ∣ R (c_{0}) ∣ ∣ ∣ ∣ v = c_{1} ∣ ∣ ∣ ∣ R (c_{1}) ∣ ∣ ∣ ∣ ⊥ ∣ ∣ ∣ ∣ R (c_{0}) ∣ ∣ ∣ R (c_{0}) ∣ ∣ R (c_{0}) ∣ (\exists x R (x)) \to R (c_{0}) \neg R (c_{1}) \to ((\exists x R (x)) \to R (c_{0})) premise assumption assumption witness assumption; v fresh \forall -elim 1 first case assumption = -elim 6, 4 second case assumption = -elim 8, 4 \neg -elim 9, 2 ⊥ -elim 10 \lor -elim 5, 6 - 7, 8 - 11 \exists -elim 3, 4 - 12 \to -intro 3 - 13 \to -intro 2 - 14

(1)

The sibling case subproofs end before the witness subproof closes. At line 13,

v

is absent from

R (c_{0})

and from all surrounding assumptions, so no witness escape occurs. The final two applications of implication introduction give

\forall x (x = c_{0} \lor x = c_{1}) ⊢ \neg R (c_{1}) \to (\exists x R (x)) \to R (c_{0}) .

(2)

The logical falsity elimination rule is needed to complete the contradictory second case with the same conclusion as the first case.

 Read the full article

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

 View more

Choose fresh arbitrary eigenvariables

u, v

. Under

u = v

, use the equality elimination rule to transport

P (u)

P (v)

. For the reverse direction, first derive

v = u

by the symmetry derivation above. In full natural deduction form:

12345678910111213 [u = v]^{a} [P (u)]^{b} P (v) P (u) \to P (v) u = u v = u [P (v)]^{c} P (u) P (v) \to P (u) (P (u) \to P (v)) \land (P (v) \to P (u)) u = v \to ((P (u) \to P (v)) \land (P (v) \to P (u))) \forall y (u = y \to ((P (u) \to P (y)) \land (P (y) \to P (u)))) \forall x \forall y (x = y \to ((P (x) \to P (y)) \land (P (y) \to P (x)))) assumption assumption = E 1, 2 \to I (2 - 3) = I = E 1, 5 (ϕ (w) \equiv w = u) assumption = E 6, 7 \to I (7 - 8) \land I 4, 9 \to I (1 - 10) \forall I 11 \forall I 12.

(1)

All temporary assumptions are discharged before either universal quantifier introduction rule application, so both eigenvariable conditions hold. No premises remain:

⊢ \forall x \forall y (x = y \to ((P (x) \to P (y)) \land (P (y) \to P (x)))) .

(2)

 Read the full article

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

 View more

For transitivity of first-order equality, take

ϕ (v)

to be

T_{1} = v

. The equality elimination rule applied to

T_{2} = T_{3}

and

ϕ (T_{2})

gives

\frac{T _{2} = T _{3} T _{1} = T _{2}}{T _{1} = T _{3}} = E .

(1)

For symmetry of first-order equality, first obtain

T_{1} = T_{1}

by the equality introduction rule. Now take

ψ (v)

to be

v = T_{1}

and substitute using

T_{1} = T_{2}

\frac{T _{1} = T _{2} T _{1} = T _{1} = I}{T _{2} = T _{1}} = E .

(2)

These choices of formula show exactly which occurrence is replaced, so neither argument assumes the property it is establishing.

 Read the full article

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

 View more

The equality introduction rule is reflexivity, with no premise. The equality elimination rule is substitution of equal first-order terms into a first-order formula:

Γ ⊢ t = t = I, \frac{Γ ⊢ s = t Γ ⊢ ϕ ( s )}{Γ ⊢ ϕ ( t )} = E .

(1)

The indicated substitution must be capture-avoiding substitution in first-order logic: the first-order terms must be free for the replaced variable. One can designate a particular argument occurrence by choosing

ϕ (v)

appropriately; the rule does not demand replacing every occurrence of an identical-looking term in a formula.

 Read the full article

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

 View more

Choose distinct fresh parameters

a, b

. Within the assumption

a = b

, equality elimination rule gives the forward implication directly. Derive the reverse equality explicitly before using it for the reverse implication:

1  | a = b                                           assumption
 2  | | P(a)                                         assumption
 3  | | P(b)                                         =-elim 1,2
 4  | P(a) → P(b)                                    →-intro 2–3
 5  | a = a                                          =-intro
 6  | b = a                                          =-elim 1,5; φ(u) := (u = a)
 7  | | P(b)                                         assumption
 8  | | P(a)                                         =-elim 6,7
 9  | P(b) → P(a)                                    →-intro 7–8
10  | (P(a) → P(b)) ∧ (P(b) → P(a))                  ∧-intro 4,9
11  a = b → ((P(a) → P(b)) ∧ (P(b) → P(a)))          →-intro 1–10
12  ∀y. a = y → ((P(a) → P(y)) ∧ (P(y) → P(a)))      ∀-intro 11, b fresh
13  ∀x. ∀y. x = y → ((P(x) → P(y)) ∧ (P(y) → P(x)))  ∀-intro 12, a fresh

The equality assumption is discharged before either universal quantifier introduction rule. There are then no undischarged assumptions, so both eigenvariable condition requirements hold. The final universal theorem expresses that equal arguments are interchangeable in the predicate

P

in both directions.

 Read the full article

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

 View more

Equality introduction rule is reflexivity; equality elimination rule permits substitution of equals in a formula:

Γ ⊢ t = t (= I), \frac{Γ ⊢ s = t Γ ⊢ ϕ ( s )}{Γ ⊢ ϕ ( t )} (= E) .

(1)

Terms substituted into

ϕ

must be free for substitution, so no variable becomes captured. The notation

ϕ (s), ϕ (t)

means substitution into the same designated free variable positions of one formula; other occurrences may remain fixed. These rules express first-order equality without assuming symmetry or transitivity as additional axioms.

 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