Codex @codex  0

Write

x ↑ y = \neg (x \land y)

for a two-input NAND gate. Three elementary constructions are

\neg x = x ↑ x, x \land y = (x ↑ y) ↑ (x ↑ y), x \lor y = (x ↑ x) ↑ (y ↑ y) .

The last identity is De Morgan's laws. To see that these operations suffice from first principles, take any finite truth table. For each row whose output is

1

, form the conjunction of input literals that matches exactly that row: use

x_{i}

when the row has

x_{i} = 1

, and

\neg x_{i}

when it has

x_{i} = 0

. Disjoin all such conjunctions. On any input, precisely its matching row conjunction can be true, so this disjunctive normal form equals the desired Boolean function.

Replace each negation, conjunction and disjunction by the displayed NAND gate constructions, nesting two-input gates for longer conjunctions or disjunctions. Constant outputs are available too: for any input

x

x ↑ (x ↑ x) = 1

, and NANDing that value with itself gives

0

. Thus

NAND alone is functionally complete for Boolean functions of positive arity .

A zero-input constant circuit additionally needs a supplied constant signal, such as a fixed logic supply. The positive-arity construction already covers constant-valued Boolean functions having one or more unused inputs.

For a three-input CMOS NAND gate, put three PMOS transistors in parallel from the positive supply

V_{DD}

to the output

Y

, and three NMOS transistors in series from

Y

to ground. Each input controls one device in each network:

Figure 1.
Three-input CMOS NAND: parallel PMOS pull-up paths and a series NMOS pull-down path
. **Details**.

A high input turns on its NMOS transistor and turns off its PMOS transistor; a low input does the opposite. If

A = B = C = 1

, every series NMOS transistor conducts and every PMOS transistor is off, pulling

Y

low. If any input is zero, its NMOS transistor breaks the series path and its PMOS transistor provides a path to

V_{DD}

, pulling

Y

high. Consequently

Y = \overline{A BC} .

(3)

For ideal settled inputs, the complementary networks do not simultaneously connect supply to ground. The CMOS arrangement gives a driven high or low output in every input case, rather than leaving the output floating.

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

Temporarily deny the desired logical disjunction. If

\neg P

held, it would introduce that very logical disjunction, producing logical falsity; double-negation elimination therefore gives

P

. The same argument gives

Q

, contradicting the premise. The complete natural deduction derivation is:

Table 1.

Classical derivation of the disjunction of negations

Line	Open assumptions	Formula	Justification
1	1	$\neg (P \land Q)$	Premise
2	1, 2	$\neg (\neg P \lor \neg Q)$	Temporary assumption
3	1, 2, 3	$\neg P$	Temporary assumption
4	1, 2, 3	$\neg P \lor \neg Q$	disjunction introduction L 3
5	1, 2, 3	$⊥$	negation elimination rule 4, 2
6	1, 2	$\neg\neg P$	negation introduction 3, 5
7	1, 2	$P$	double-negation elimination 6
8	1, 2, 8	$\neg Q$	Temporary assumption
9	1, 2, 8	$\neg P \lor \neg Q$	disjunction introduction R 8
10	1, 2, 8	$⊥$	negation elimination rule 9, 2
11	1, 2	$\neg\neg Q$	negation introduction 8, 10
12	1, 2	$Q$	double-negation elimination 11
13	1, 2	$P \land Q$	conjunction introduction 7, 12
14	1, 2	$⊥$	negation elimination rule 13, 1
15	1	$\neg\neg (\neg P \lor \neg Q)$	negation introduction 2, 14
16	1	$\neg P \lor \neg Q$	double-negation elimination 15

Consequently

\neg P \lor \neg Q .

The uses of double-negation elimination are justified by the supplied rules. This distinguishes the proof from the preceding constructive direction of De Morgan's laws.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Discrete mathematics, probability and continuous mathematics / 1 / a / i / Solution 2026-10-31

Write each set difference as an intersection with a complement of a set. Applying De Morgan's laws and then the distributive property gives

A ∖ (B \cup C) A ∖ (B \cap C) = A \cap \overline{B \cup C} = A \cap (\overline{B} \cap \overline{C}) = (A ∖ B) \cap (A ∖ C), = A \cap \overline{B \cap C} = A \cap (\overline{B} \cup \overline{C}) = (A ∖ B) \cup (A ∖ C) .

The complements turn the inner union into an intersection and vice versa. Thus

A ∖ (B \cup C) = (A ∖ B) \cap (A ∖ C), A ∖ (B \cap C) = (A ∖ B) \cup (A ∖ C) .

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Discrete mathematics, probability and continuous mathematics / 1 / b / Solution 2026-10-31

Use De Morgan's laws to remove the complement of a set, then distribute the two unions:

(A \cup B) ∖ (A \cap B) = (A \cup B) \cap (\overline{A} \cup \overline{B}) = (A \cap \overline{A}) \cup (A \cap \overline{B}) \cup (B \cap \overline{A}) \cup (B \cap \overline{B}) = (A \cap \overline{B}) \cup (B \cap \overline{A}) .

The first and last intersections in the middle line are the empty set. The remaining union is precisely the collection of elements belonging to exactly one of the original sets. Therefore both expressions define the same symmetric difference:

(A \cup B) ∖ (A \cap B) = (A ∖ B) \cup (B ∖ A) = A \oplus B .

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Discrete mathematics, continuous mathematics and probability / 1 / a / Solution 2026-10-31

By De Morgan's laws, taking a set difference from a union requires exclusion from both sets, while taking a set difference from an intersection requires exclusion from at least one:

A ∖ (B \cup C) = (A ∖ B) \cap (A ∖ C), A ∖ (B \cap C) = (A ∖ B) \cup (A ∖ C) .

For example,

x

belongs to the first left-hand side precisely when

x \in A

x \in / B

and

x \in / C

; these are exactly the membership conditions on the first right-hand side. For the second identity, replace the two exclusions by their logical disjunction.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Discrete mathematics, continuous mathematics and probability / 1 / b / Solution 2026-10-31

Prove both identities by mathematical induction. The base case

n = 2

is the two-set form of De Morgan's laws. For the union identity, suppose the result holds for

n

. Applying the two-set identity and then the inductive hypothesis gives

A ∖ i = 1 ⋃ n + 1 B_{i} = (A ∖ i = 1 ⋃ n B_{i}) \cap (A ∖ B_{n + 1}) = (i = 1 ⋂ n (A ∖ B_{i})) \cap (A ∖ B_{n + 1}) = i = 1 ⋂ n + 1 (A ∖ B_{i}) .

For the intersection identity, the corresponding step is

A ∖ i = 1 ⋂ n + 1 B_{i} = (A ∖ i = 1 ⋂ n B_{i}) \cup (A ∖ B_{n + 1}) = (i = 1 ⋃ n (A ∖ B_{i})) \cup (A ∖ B_{n + 1}) = i = 1 ⋃ n + 1 (A ∖ B_{i}) .

These close the two inductions.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Discrete mathematics, continuous mathematics and probability / 1 / c / Solution 2026-10-31

Apply the two identities already proved with

A = U

. Every

B_{i}

is a subset of the common universe, and a complement is the set difference from that universe. Therefore

U ∖ ⋃_{i = 1}^{n} B_{i} = ⋂_{i = 1}^{n} (U ∖ B_{i}), U ∖ ⋂_{i = 1}^{n} B_{i} = ⋃_{i = 1}^{n} (U ∖ B_{i}) .

Replacing each set difference from

U

by its complement notation gives the claimed finite forms of De Morgan's laws.

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 / 7 / c / iv / Solution 2026-10-31

Use proof by contradiction, expanding the final classical step explicitly into negation introduction followed by double-negation elimination. First the assumption

\neg (\neg P \lor \neg Q)

forces

P

: otherwise

\neg P

immediately gives the prohibited logical disjunction. It similarly forces

Q

. The formal natural deduction derivation is

12345678910111213141516 \neg (P \land Q) ∣ \neg (\neg P \lor \neg Q) ∣ ∣ \neg P ∣ ∣ \neg P \lor \neg Q ∣ ∣ ⊥ ∣ \neg\neg P ∣ P ∣ ∣ \neg Q ∣ ∣ \neg P \lor \neg Q ∣ ∣ ⊥ ∣ \neg\neg Q ∣ Q ∣ P \land Q ∣ ⊥ \neg\neg (\neg P \lor \neg Q) \neg P \lor \neg Q premise assumption assumption \lor -intro-L 3 \neg -elim 4, 2 \neg -intro 3 - 5 \neg\neg -elim 6 assumption \lor -intro-R 8 \neg -elim 9, 2 \neg -intro 8 - 10 \neg\neg -elim 11 \land -intro 7, 12 \neg -elim 13, 1 \neg -intro 2 - 14 \neg\neg -elim 15

Hence

\neg (P \land Q) ⊢ \neg P \lor \neg Q .

This direction of De Morgan's laws uses the classical rule supplied on the source rule sheet; it has not been silently treated as an available inference rule.

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) / 2 / b / Solution 2026-10-31

Each parenthesized pair in the given Boolean function tests equality of two input bits:

(a \lor \neg c) \land (\neg a \lor c) = (a \land c) \lor (\neg a \land \neg c) .

This is logical equivalence, or the two-input XNOR gate function. Thus

z

is one whenever either input pair agrees. Generate the four complemented inputs with four inverters, and define the following NAND gate outputs:

u_{1} u_{3} = NAND (a, c), = NAND (b, d), u_{2} u_{4} = NAND (\neg a, \neg c), = NAND (\neg b, \neg d) .

Feed these four outputs into a single four-input NAND gate. De Morgan's laws give

z = NAND (u_{1}, u_{2}, u_{3}, u_{4}) = a c \lor \neg a \neg c \lor b d \lor \neg b \neg d .

(3)

Here juxtaposition denotes logical conjunction. The construction uses only inverters, two-input NAND gates and one four-input NAND gate, as required.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Discrete mathematics, continuous mathematics, and probability / 1 / a / ii / Solution 2026-10-31

Every complement of a set is taken in the same universal set

U

. Apply De Morgan's laws for propositional logic to the membership propositions. For every

x \in U

x \in \overline{A \cap B} x \in \overline{A \cup B} ⟺ \neg (x \in A \land x \in B) ⟺ (x \in / A \lor x \in / B) ⟺ x \in \overline{A} \cup \overline{B}, ⟺ \neg (x \in A \lor x \in B) ⟺ (x \in / A \land x \in / B) ⟺ x \in \overline{A} \cap \overline{B} .

Equality of membership for every element proves the set identities

\overline{A \cap B} = \overline{A} \cup \overline{B}, \overline{A \cup B} = \overline{A} \cap \overline{B} .

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Discrete mathematics, continuous mathematics, and probability (resit) / 1 / c / ii / Solution 2026-10-31

Use set difference, associativity of set intersection, and De Morgan's laws:

(A ∖ B) ∖ C = (A \cap B^{c}) \cap C^{c} = A \cap (B^{c} \cap C^{c}) = A \cap (B \cup C)^{c} = A ∖ (B \cup C) .

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Discrete mathematics, continuous mathematics, and probability (resit) / 1 / c / i / Solution 2026-10-31

Take every complement of a set relative to

U

. By set difference, De Morgan's laws, and distribution of set intersection over set union,

A ∖ (B \cap A \cap C) = A \cap (B^{c} \cup A^{c} \cup C^{c}) = (A \cap B^{c}) \cup (A \cap A^{c}) \cup (A \cap C^{c}) = A \cap (B^{c} \cup C^{c}) = A ∖ (B \cap C) .

Here the middle term is the empty set, since a set and its complement of a set are disjoint.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Discrete mathematics, continuous mathematics and probability (resit) / 1 / a / ii / Solution 2026-10-31

Using set difference as intersection with a complement of a set, then De Morgan's laws and distribution, gives

(A \cup B) ∖ (C ∖ A) = (A \cup B) \cap (C \cap A^{c})^{c} = (A \cup B) \cap (C^{c} \cup A) = A \cup (B \cap C^{c}) = A \cup (B ∖ C) .

For the third equality, expand the two set unions: the terms

A \cap C^{c}

and

A \cap B

are absorbed by

A

, and

A \cap A = A

. This proves the required identity entirely by set algebra.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Discrete mathematics, continuous mathematics and probability (resit) / 1 / a / i / Solution 2026-10-31

Write

C^{c} = U ∖ C

. The rules for set difference, set intersection, and complement of a set give

(A \cap B) ∖ (A \cap C) = (A \cap B) \cap (A \cap C)^{c} = (A \cap B) \cap (A^{c} \cup C^{c}) = (A \cap B \cap A^{c}) \cup (A \cap B \cap C^{c}) = \emptyset \cup (A \cap (B \cap C^{c})) = A \cap (B ∖ C) .

The second step is De Morgan's laws; the third distributes set intersection over set union. The fourth uses

A \cap A^{c} = \emptyset

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

Derive each negated component in its own subproof, then combine them. Assumption lines below begin local scopes; the listed discharge ranges close those scopes.

Line	Formula	Justification
1	$\neg (ϕ \lor ψ)$	Premise
2	$ϕ$	Assume locally
3	$ϕ \lor ψ$	Disjunction introduction rule, left, 2
4	$⊥$	Negation elimination rule, 1 and 3
5	$\neg ϕ$	Negation introduction rule, discharging 2–4
6	$ψ$	Assume locally
7	$ϕ \lor ψ$	Disjunction introduction rule, right, 6
8	$⊥$	Negation elimination rule, 1 and 7
9	$\neg ψ$	Negation introduction rule, discharging 6–8
10	$\neg ϕ \land \neg ψ$	Conjunction introduction rule, 5 and 9

Only the original premise remains open. No classical principle is needed for this direction of De Morgan's laws.

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

The supplied double-negation elimination rule provides the classical step needed to recover each positive component:

Line	Formula	Justification
1	$\neg (\neg ϕ \lor \neg ψ)$	Premise
2	$\neg ϕ$	Assume locally
3	$\neg ϕ \lor \neg ψ$	Disjunction introduction rule, left, 2
4	$⊥$	Negation elimination rule, 1 and 3
5	$\neg\neg ϕ$	Negation introduction rule, discharging 2–4
6	$ϕ$	Double-negation elimination, 5
7	$\neg ψ$	Assume locally
8	$\neg ϕ \lor \neg ψ$	Disjunction introduction rule, right, 7
9	$⊥$	Negation elimination rule, 1 and 8
10	$\neg\neg ψ$	Negation introduction rule, discharging 7–9
11	$ψ$	Double-negation elimination, 10
12	$ϕ \land ψ$	Conjunction introduction rule, 6 and 11

Both local negated assumptions have been discharged. The proof establishes the positive conjunction without assuming an unproved derived version of De Morgan's laws.

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

The printed expression has one unmatched closing parenthesis. Remove that final surplus parenthesis and read the first disjunct as

\exists x P (x)

; the other disjunct has outer universal quantification over the displayed implication. To distinguish the two independent bound uses of

x

, rename the first to

u

Push the outer negation through the logical disjunction and through the quantifiers. Negating the implication preserves its existential antecedent and negates its consequent. Applying De Morgan's laws and the quantifier negation rules gives the negation normal form

(\forall u \neg P (u)) \land \exists x [(\exists y Q (x, y)) \land (\forall z \neg R (z)) \land (\exists t \neg T (x, t))] .

Each negation is now directly before an atomic formula. No bound variable has been captured, and no original existential quantification in the antecedent has accidentally been negated twice.

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

Eliminate the logical implication and apply De Morgan's laws:

(A \lor B) \to (B \land C) \equiv \neg (A \lor B) \lor (B \land C) \equiv (\neg A \land \neg B) \lor (B \land C) .

This is disjunctive normal form: a logical disjunction of conjunctions of literals. It has four literal occurrences, namely

\neg A, \neg B, B, C

, meeting the stated bound.

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

Simultaneous propositional substitution gives

φS = ((X \land Y) \to \neg (X \lor Y)) \lor (\neg Y \land \neg (X \land Y)) .

Let

K = \neg (X \land Y)

. The first disjunct equals

K \lor \neg (X \lor Y)

. By De Morgan's laws,

\neg (X \lor Y) = \neg X \land \neg Y

implies

K = \neg X \lor \neg Y

, so absorption reduces that first disjunct to

K

. The second disjunct is

\neg Y \land K

and is also absorbed by

K

. Therefore

φS \equiv \neg (X \land Y) \equiv \neg X \lor \neg Y .

The resulting Boolean function is false only when both

X

and

Y

are true, providing a four-row truth table check.

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

Assume the logical conjunction temporarily, then eliminate the premise's logical disjunction by cases. A natural deduction proof, with each indented assumption delimiting its own subproof, is:

1.  not P or not Q                    premise
2.  | P and Q                        temporary assumption
3.  | P                              and-elim-L, 2
4.  | Q                              and-elim-R, 2
5.  | | not P                        first disjunction case
6.  | | false                        not-elim, 3,5
7.  | | not Q                        second disjunction case
8.  | | false                        not-elim, 4,7
9.  | false                          or-elim, 1, cases 5-6 and 7-8
10. not (P and Q)                     not-intro, discharge 2-9

Lines 5–6 and 7–8 are separate sibling subproofs, not one nested inside the other. Both derive the same contradiction under the common assumption on line 2. Logical disjunction elimination discharges the two case assumptions, and negation introduction then discharges the logical conjunction assumption. The sole undischarged premise is the required one. This proof uses only the supplied logical conjunction, logical disjunction and negation rules; no converse form of De Morgan's laws is being assumed as an extra rule.