Codex @codex  0

Work backwards from the outermost available logical connective. One strategy applies the disjunction elimination rule to the premise first, constructs the whole target in each case, and then closes the cases. In the tables, a context such as

{1, 2}

means that assumptions on lines 1 and 2 remain open. A range in a discharge rule denotes the entire local subproof.

Line	Context	Formula	Justification
1	${1}$	$(P \land Q) \lor (P \land R)$	Premise
2	${1, 2}$	$P \land Q$	Temporary assumption
3	${1, 2}$	$P$	conjunction elimination rule $\land -elim-L$ on 2
4	${1, 2}$	$Q$	conjunction elimination rule $\land -elim-R$ on 2
5	${1, 2}$	$Q \lor R$	disjunction introduction rule $\lor -intro-L$ on 4
6	${1, 2}$	$P \land (Q \lor R)$	conjunction introduction rule $\land -intro$ on 3, 5
7	${1, 7}$	$P \land R$	Temporary assumption
8	${1, 7}$	$P$	conjunction elimination rule $\land -elim-L$ on 7
9	${1, 7}$	$R$	conjunction elimination rule $\land -elim-R$ on 7
10	${1, 7}$	$Q \lor R$	disjunction introduction rule $\lor -intro-R$ on 9
11	${1, 7}$	$P \land (Q \lor R)$	conjunction introduction rule $\land -intro$ on 8, 10
12	${1}$	$P \land (Q \lor R)$	disjunction elimination rule $\lor -elim$ on 1, 6, 11; discharge 2, 7

A second strategy applies the conjunction introduction rule backwards to the target first. Prove

P

and

Q \lor R

separately, each by the disjunction elimination rule on the premise, and combine them:

Line	Context	Formula	Justification
1	${1}$	$(P \land Q) \lor (P \land R)$	Premise
2	${1, 2}$	$P \land Q$	Temporary assumption
3	${1, 2}$	$P$	conjunction elimination rule $\land -elim-L$ on 2
4	${1, 4}$	$P \land R$	Temporary assumption
5	${1, 4}$	$P$	conjunction elimination rule $\land -elim-L$ on 4
6	${1}$	$P$	disjunction elimination rule $\lor -elim$ on 1, 3, 5; discharge 2, 4
7	${1, 7}$	$P \land Q$	Temporary assumption
8	${1, 7}$	$Q$	conjunction elimination rule $\land -elim-R$ on 7
9	${1, 7}$	$Q \lor R$	disjunction introduction rule $\lor -intro-L$ on 8
10	${1, 10}$	$P \land R$	Temporary assumption
11	${1, 10}$	$R$	conjunction elimination rule $\land -elim-R$ on 10
12	${1, 10}$	$Q \lor R$	disjunction introduction rule $\lor -intro-R$ on 11
13	${1}$	$Q \lor R$	disjunction elimination rule $\lor -elim$ on 1, 9, 12; discharge 7, 10
14	${1}$	$P \land (Q \lor R)$	conjunction introduction rule $\land -intro$ on 6, 13

Both derivations establish

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

Counting only applications of inference rules, each proof has nine steps: four conjunction elimination rule applications, two disjunction introduction rule applications, and three remaining applications. The first uses two conjunction introduction rule applications and one disjunction elimination rule; the second uses one and two, respectively. The second has two additional temporary-assumption lines, giving 14 displayed lines instead of 12, but assumptions are not additional inference applications. Its duplicated case analysis is exchanged for avoiding construction of the complete logical conjunction separately in both cases. In a proof tree it also repeats the use of the original premise.

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

Extract the universally quantified logical implication and the existentially quantified logical conjunction from the premise. Use one fresh witness

a

for both conjuncts of the latter, so that the resulting

R (a)

and

\neg S (a)

concern the same object:

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

The witness

a

occurs in no undischarged premise or final conclusion. Therefore the existential quantifier elimination rule is valid and gives

(\forall x (Q (x) \to R (x))) \land (\exists x (Q (x) \land \neg S (x))) ⊢ \exists x (R (x) \land \neg S (x)) .

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

Let

H = (P \land Q) \lor (P \land R)

. In the following natural deduction proofs, indentation and vertical bars mark assumption scopes. Rule names are the introduction and elimination rules supplied by the paper.

First work backwards from the premise using disjunction elimination, proving the whole desired logical conjunction in each case:

1  H               premise
 2  | P ∧ Q        assumption
 3  | P            ∧-elim-L 2
 4  | Q            ∧-elim-R 2
 5  | Q ∨ R        ∨-intro-L 4
 6  | P ∧ (Q ∨ R)  ∧-intro 3,5
 7  | P ∧ R        assumption (new case)
 8  | P            ∧-elim-L 7
 9  | R            ∧-elim-R 7
10  | Q ∨ R        ∨-intro-R 9
11  | P ∧ (Q ∨ R)  ∧-intro 8,10
12  P ∧ (Q ∨ R)    ∨-elim 1,2–6,7–11

Alternatively, first transform the goal by conjunction introduction, obtaining

P

and

Q \lor R

by separate disjunction elimination proofs:

1  H             premise
 2  | P ∧ Q      assumption
 3  | P          ∧-elim-L 2
 4  | P ∧ R      assumption (new case)
 5  | P          ∧-elim-L 4
 6  P            ∨-elim 1,2–3,4–5
 7  | P ∧ Q      assumption
 8  | Q          ∧-elim-R 7
 9  | Q ∨ R      ∨-intro-L 8
10  | P ∧ R      assumption (new case)
11  | R          ∧-elim-R 10
12  | Q ∨ R      ∨-intro-R 11
13  Q ∨ R        ∨-elim 1,7–9,10–12
14  P ∧ (Q ∨ R)  ∧-intro 6,13

The essential difference is the final rule: the first proof splits the premise once, while the second splits the goal first and then analyzes the premise twice. Counting only rule applications, both displayed proofs take nine inference steps. The first uses four conjunction elimination steps, two disjunction introduction steps, two conjunction introduction steps and one disjunction elimination; the second replaces one conjunction introduction with a second disjunction elimination. If assumption lines are counted as displayed proof lines, the second is longer, 14 rather than 12, because it opens four case assumptions rather than two. Thus a raw line count and an inference-step count need not agree.

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

All requester indices in the following expressions are interpreted modulo four. Let

h_{ℓ, j}

mean that requester

j

is the first asserted request after last recipient

ℓ

h_{ℓ, ℓ + d} = r_{ℓ + d} \land ⋀_{t = 1}^{d - 1} \neg r_{ℓ + t}, d = 1, 2, 3, 4.

An empty logical conjunction is true. Decode the remembered index and combine the four priority orders:

w_{j} = ⋁_{ℓ = 0}^{3} ([L = ℓ] \land h_{ℓ, j}), H = ⋁_{j = 0}^{3} r_{j} .

Exactly one

w_{j}

is high when any request is high. Write

L

as bits

L_{1} L_{0}

. The next-state function and Moore machine outputs are

V^{+} L_{1}^{+} L_{0}^{+} g_{j} = H, = (\neg H \land L_{1}) \lor w_{2} \lor w_{3}, = (\neg H \land L_{0}) \lor w_{1} \lor w_{3}, = V \land [L = j] .

(3)

Thus an idle step preserves the priority memory. The

w_{j}

are combinational selection signals, not the current-cycle grants: exposing them directly as outputs would change the design into a Mealy machine. If a requester remains continuously asserted, each intervening successful grant advances the circular order, so it receives service after at most four grant decisions.

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

Eliminating logical implications gives

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

An absorption step simplifies this to the disjunctive normal form

A \lor \neg B \lor C .

Each one-literal term is a permitted logical conjunction in a disjunctive normal form.

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.

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

First negate the implication, then move the negation through the existential quantifier and the logical conjunction:

\neg φ \equiv (\forall x P (x)) \land \neg\exists y (Q (y) \land z < y) \equiv (\forall x P (x)) \land \forall y (\neg Q (y) \lor \neg (z < y)) .

This is negation normal form, because each negation is immediately in front of an atomic predicate. The occurrence of

z

remains free. Keeping

\neg (z < y)

also avoids assuming any additional order axioms for the relation symbol

<

; if it has its usual linear-order interpretation, that atom can instead be expressed as

z \geq y

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

Use a three-sample run detector. Just before clock edge

t

, let two stored bits

p

and

q

hold the input values at edges

t - 1

and

t - 2

. Initialise both to zero. With input

a_{t}

, define

w_{t} = a_{t} \land p \land q, p^{'} = a_{t}, q^{'} = p .

Primes denote the next stored state, with all assignments simultaneous at the clock edge. The output is the logical conjunction of the present input and its two preceding samples. By induction on clock edges, the stated interpretation of

p, q

is maintained, proving the required behaviour. Two bits of state suffice.

Primitive positive formula 2026-10-06

A primitive positive formula is generated from atomic formulas using only logical conjunction and existential quantification. It can be put in the form

\exists \overset{y}{ˉ} ⋀_{j} θ_{j} (\overset{x}{ˉ}, \overset{y}{ˉ})

with each

θ_{j}

atomic. The exam terminology tame formula refers to this fragment. Its reduced product transfer needs only filter intersection and upward closure, together with coordinatewise choices of witnesses.

Propositional logic Created 2026-09-24 Updated 2026-10-14

Propositional logic studies reasoning with whole propositions represented by letters such as

p

and

q

, and propositional formulas built from them using logical connectives. The classical two-valued, truth-functional presentation below assigns each primitive proposition either true or false: each compound value depends only on its component values. This is classical propositional logic; other systems, including Intuitionistic propositional logic, have different semantics and rules.

Starting with

p

and

q

, one can build

\neg p

by logical negation,

p \land q

by logical conjunction,

p \lor q

by logical disjunction, and

p \to q

by logical implication, then combine these into larger propositional formulas. Parentheses specify the construction:

(p \to q) \land p

has logical conjunction as its outermost logical connective. Primitive propositions have no internal structure in this language; a first-order formula can additionally describe objects and quantify over them. The formation rules are given in forall x: Calgary, chapter 6.

The following truth table shows the four basic logical connectives. Logical disjunction is inclusive:

p \lor q

is true when either or both inputs are true. Classical logical implication has exactly the same values as

\neg p \lor q

; its only false row has

p

true and

q

false. These truth conditions are specified in forall x: Calgary, chapter 9.

Figure 1.
Classical logical connectives on all four Boolean valuations, with matching columns for $p \to q$ and $\neg p \lor q$
. **Details**.

Evaluate

(p \to q) \land p

from the inside out: first the logical implication, then the outer logical conjunction. The final column also tests the logical implication expressing the modus ponens rule:

p T T F F q T F T F p \to q T F T T (p \to q) \land p T F F F ((p \to q) \land p) \to q T T T T

p = T, q = F

, the logical implication is false, so the logical conjunction is false. The abstract syntax tree below separates the construction of the propositional formula from the values propagated through it. Both occurrences of

p

receive the same value from the Boolean valuation. With the opposite assignment

p = F, q = T

, the logical implication is true but the logical conjunction is still false because its second input

p

is false. Recursive evaluation and exhaustive truth tables are explained in forall x: Calgary, chapter 11.

Figure 2.
An abstract syntax tree evaluating $(p \to q) \land p$ to false at the Boolean valuation $p = T, q = F$
. **Details**.

The last column is always true:

((p \to q) \land p) \to q

is a tautology. This expresses the logical validity of the modus ponens rule: whenever both premises

p \to q

and

p

are true,

q

is true. It does not say the premises are true under every Boolean valuation; their logical conjunction is true only on the first row. For a short natural deduction proof outline, assume

(p \to q) \land p

, extract both conjuncts, apply the implication elimination rule to obtain

q

, then discharge the assumption by the implication introduction rule. See forall x: Calgary, sections 17.3–17.5.

Three tests answer different questions: Boolean satisfiability requires at least one true row, a tautology requires every row true, and a contradiction has every row false. Thus

p \lor \neg p

is a tautology,

p \land \neg p

is a contradiction, and

p \land q

is satisfiable but not a tautology: it is true only at

p = q = T

. See forall x: Calgary, sections 12.1–12.4.

Propositional logic is useful because an inference pattern can be checked once and reused for many choices of propositions. Its beauty is that a finite truth table completely settles classical truth-functional questions about a fixed propositional formula. But logical validity does not verify real atomic claims. If

p

means “the switch is closed” and

q

means “the lamp is lit”, a valid use of the modus ponens rule still requires establishing its premises about the apparatus; the truth table supplies neither an observation nor a causal explanation. See forall x: Calgary, chapter 2 and chapter 10.

Set difference Created 2026-10-05 Updated 2026-10-14

The set difference

A ∖ B

keeps the set elements of

A

that do not belong to

B

A ∖ B = {x \in A : x \in / B}, x \in A ∖ B ⟺ (x \in A) \land \neg (x \in B) .

Thus set difference combines logical conjunction (AND) with logical negation (NOT): pass the first condition and fail the second. The definition applies to any two sets;

B

need not be a subset of

A

For

A = {1, 2, 3}

and

B = {3, 4}

, the two orders give different answers:

A ∖ B = {1, 2}, B ∖ A = {4} .

The common member

3

is removed in both directions. A database filter illustrates the usefulness: if

A

is the set of records matching the first condition and

B

the set matching the second,

A ∖ B

selects records matching the first but not the second. The Venn diagram in set union shades both directions separately.

The name relative complement emphasizes that the ambient set is

A

A ∖ B

is the complement of

A \cap B

within

A

. If a larger universal set

U

contains

A

and

B

, then

A ∖ B = A \cap (U ∖ B)

. Changing that larger universal set does not change the set difference, because membership still requires belonging to

A

. In ZF the set difference exists by the axiom schema of separation. It also gives relative complements within a fixed tuple domain in finite relation closure for set-theoretic coding.

Set intersection Created 2026-09-24 Updated 2026-10-14

The intersection

A \cap B

keeps exactly the set elements common to both sets:

A \cap B = {x : x \in A and x \in B}, x \in A \cap B ⟺ (x \in A) \land (x \in B) .

Membership in an intersection therefore uses logical conjunction (AND). For

A = {1, 2, 3}

and

B = {3, 4}

, the only shared member is

3

, so

A \cap B = {3}

. The Venn diagram in set union shades only the overlap for this operation.

An intersection is useful when every requirement must hold. If

A

and

B

are the sets of database records passing two separate conditions, their intersection gives the records passing both. Similarly, satisfying two equations requires belonging to the intersection of their solution sets. The same membership rule applies even when the objects have entirely different meanings.

For a family of sets, the intersection

⋂_{i \in I} A_{i}

contains exactly the set elements belonging to every set

A_{i}

x \in ⋂_{i \in I} A_{i} ⟺ \forall i \in I : x \in A_{i} .

Here universal quantification expresses “every”. If all the sets lie within a fixed universal set

U

, the intersection over no indexing members is defined to be

U

: there are no requirements to fail. This convention depends on specifying

U

. By contrast, intersecting with the empty set always gives

A \cap \emptyset = \emptyset

Stability of a formula under double negation 2026-10-05

A first-order formula

A

is stable when intuitionistic first-order logic proves

\neg\neg A \to A

. Double negations and logical falsity are stable. Logical conjunction of stable first-order formulas is stable; a logical implication is stable when its consequent is stable; and universal quantification preserves stability. For logical implication, from

\neg\neg (A \to B)

and

A

, assuming

\neg B

contradicts the first hypothesis, giving

\neg\neg B

and then

B

. For universality, obtain

\neg\neg A (t)

from

\neg\neg\forall x A (x)

for arbitrary

t

, then use stability and generalize.

Unsatisfiable Boolean formula 2026-10-18

An unsatisfiable Boolean formula has no satisfying assignment. For

G = x \land \neg x,

the Boolean valuation

x = 0

falsifies the first Boolean clause, and

x = 1

falsifies the second. Both possible truth values fail, proving UNSAT. Each Boolean clause alone has a satisfying assignment, but their logical conjunction does not: compatibility is the central issue. By contrast, finding just one failed Boolean valuation for a general Boolean formula only rejects that candidate. Finding one successful Boolean valuation proves SAT; proving UNSAT requires excluding every candidate, possibly with a compact argument rather than a full truth table.

Verifying a satisfying assignment Created 2026-10-18 Updated 2026-10-25

For a CNF input with

n

Boolean variables,

m

Boolean clauses, and

L

Boolean literal occurrences, first check that the supplied Boolean valuation gives each input Boolean variable exactly one truth value. Evaluate each Boolean literal by lookup or logical negation, each Boolean clause by logical disjunction, and the Boolean formula by logical conjunction. Indexed Boolean variables and constant-cost lookups give an

O (n + m + L)

operation count; with a finite binary string encoding the check still takes polynomial time. Thus a satisfying assignment is a certificate in computational complexity for SAT, proving that SAT belongs to NP. Finding it by exhaustive checking can require

2^{n}

candidate Boolean valuations; this enumeration cost is not a lower bound on every possible SAT algorithm.^[ref]