New articles - OurBigBook.com

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 / 8 / d / i / Solution by

Codex  0 2026-10-25

 View more

Expand three cases as two applications of disjunction elimination rule. For the association

(ϕ \lor ψ) \lor ρ

, the first outer branch assumes

ϕ \lor ψ

and applies the given

ϕ

and

ψ

subproofs to obtain

κ

. The other outer branch is the given

ρ

subproof. In schematic natural deduction form:

1  (φ ∨ ψ) ∨ ρ                         given
2  | φ ∨ ψ                             first outer case
3  | | φ                               first inner case
4  | | κ                               given φ-subproof
5  | | ψ                               second inner case
6  | | κ                               given ψ-subproof
7  | κ                                 ∨-elim, 2, cases 3–4 and 5–6
8  | ρ                                 second outer case
9  | κ                                 given ρ-subproof
10 κ                                   ∨-elim, 1, cases 2–7 and 8–9

All three case assumptions are discharged and common surrounding assumptions remain. If the original three-way logical disjunction is parsed as

ϕ \lor (ψ \lor ρ)

, use the

ϕ

subproof as the first outer branch and eliminate

ψ \lor ρ

inside the second. Thus either binary association has the asserted three-case disjunction elimination, without presupposing an unproved associativity.

 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 / 7 / c / ii / Solution by

Codex  0 2026-10-25

 View more

The logical implication associates to the right. Assume its two antecedents, then use nested applications of the disjunction elimination rule.

1  | P ∨ Q                              assume
2  | | P ∨ ¬Q                           assume
3  | | | P                              first case of 1
4  | | | P                              available from 3
5  | | | Q                              second case of 1
6  | | | | P                            first case of 2
7  | | | | P                            available from 6
8  | | | | ¬Q                           second case of 2
9  | | | | ⊥                            ¬-elim, 5 and 8
10 | | | | P                            ⊥-elim, 9
11 | | | P                              ∨-elim, 2, cases 6–7 and 8–10
12 | | P                                ∨-elim, 1, cases 3–4 and 5–11
13 | (P ∨ ¬Q) → P                       →-intro, discharge 2–12
14 (P ∨ Q) → ((P ∨ ¬Q) → P)             →-intro, discharge 1–13

This proof uses logical falsity elimination rule, but does not need law of excluded middle or double-negation elimination.

 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 / 7 / c / i / Solution by

Codex  0 2026-10-25

 View more

Retain the two given logical implications and temporarily assume their common starting proposition.

1  P → Q                    premise
2  Q → R                    premise
3  | P                      assume
4  | Q                      →-elim, 3 and 1
5  | R                      →-elim, 4 and 2
6  P → R                    →-intro, discharge 3–5

Only the original premises remain undischarged, giving the required composition of logical implications.

 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 / 6 / a / v / Solution by

Codex  0 2026-10-25

 View more

The iteration matrix has eigenvalues $0, - 1/2, 1/2$ : expanding its characteristic polynomial down the first column leaves the triangular two-by-two block with diagonal entries

- 1/2, 1/2

. The distinct eigenvalues ensure diagonalizability. Thus its spectral radius is

1/2 < 1

The previous bound gives

∥ f_{n} ∥ \leq 2^{- n} ∥ f_{0} ∥ \to 0

, so the Gauss-Seidel iteration converges for every initial guess under the stated diagonalization. Its limit is the exact solution

(1, 1, - 1)^{T}

. Since

e_{n} = S f_{n}

, a fixed matrix also sends this transformed error to zero; its operator norm can account for any amplification in the original coordinates.

 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 / 6 / a / iv / Solution by

Codex  0 2026-10-25

 View more

Write

D = diag (λ_{1}, \dots, λ_{m})

and let

∣Λ∣ = max_{i} ∣ λ_{i} ∣

. The stated Euclidean norm gives

∥ f_{n} ∥^{2} = \sum_{i} ∣ λ_{i} ∣^{2 n} ∣ (f_{0})_{i} ∣^{2} \leq ∣Λ ∣^{2 n} \sum_{i} ∣ (f_{0})_{i} ∣^{2} = ∣Λ ∣^{2 n} ∥ f_{0} ∥^{2} .

(1)

Taking nonnegative square roots proves $∥ f_{n} ∥ \leq ∣Λ ∣^{n} ∥ f_{0} ∥$ . At

n = 0

this is equality. This is a contraction bound in the transformed coordinates; an arbitrary nonorthogonal

S

does not give the same unit-constant bound for the original error norm.

 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 / 6 / a / iii / Solution by

Codex  0 2026-10-25

 View more

For the spectral error bound for a diagonalizable fixed-point iteration, the exact solution

x

is a fixed point:

x = G x + c

. Subtracting it from the iteration gives the error recurrence

e_{n} = G e_{n - 1}

, with

e_{n} = x_{n} - x

. Multiplying by

S^{- 1}

and using

G = S D S^{- 1}

gives

f_{n} = S^{- 1} GS f_{n - 1} = D f_{n - 1} .

(1)

Iterating proves $f_{n} = D^{n} f_{0}$ , including

n = 0

because

D^{0} = I

. This argument does not assume

S

is orthogonal; it simply expresses the error in an eigenbasis.

 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 / 6 / a / ii / Solution by

Codex  0 2026-10-25

 View more

From zero, the first update is $x_{1} = (- 1, 3/2, 1/4)^{T}$ . For the next update, the first component is

- 1 + 3/2 - 1/4 = 1/4

, the second is

3/2 - (1/2) (3/2) = 3/4

, and the third is

1/4 - (3/4) (3/2) + (1/2) (1/4) = - 3/4

. Therefore $x_{2} = (1/4, 3/4, - 3/4)^{T}$ .

 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 / 6 / a / i / Solution by

Codex  0 2026-10-25

 View more

Update the unknowns in row order, immediately using newly computed components. The component equations are

x_{1}^{(n)} x_{2}^{(n)} x_{3}^{(n)} = - 1 + x_{2}^{(n - 1)} - x_{3}^{(n - 1)}, = \frac{1}{2} (2 - x_{1}^{(n)} - x_{3}^{(n - 1)}) = \frac{3}{2} - \frac{1}{2} x_{2}^{(n - 1)}, = \frac{1}{2} (- 2 - x_{1}^{(n)} + x_{2}^{(n)}) = \frac{1}{4} - \frac{3}{4} x_{2}^{(n - 1)} + \frac{1}{2} x_{3}^{(n - 1)} .

(1)

Thus $G = 000 1 - 1/2 - 3/4 - 1 0 1/2$ and $c = (- 1, 3/2, 1/4)^{T}$ . Using only old values in all three row equations would instead describe the Jacobi method, not the Gauss-Seidel method.

 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 / 5 / f / ii / Solution by

Codex  0 2026-10-25

 View more

The image of a linear map of

P_{1}

is exactly the one-dimensional span of

q_{1}

: its formula always returns a multiple of

q_{1}

, and

P_{1} q_{1} = q_{1} \neq = 0

. Hence $rank (P_{1}) = 1$ .

The rank-nullity theorem gives

dim N (P_{1}) = n - 1

. Since

C (I_{n} - P_{1}) = N (P_{1})

by (e)(i), $rank (I_{n} - P_{1}) = n - 1$ . This includes the case

n = 1

, where the complementary projector is zero.

 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 / 5 / f / i / Solution by

Codex  0 2026-10-25

 View more

For a sum of mutually orthogonal projectors, orthonormality gives

q_{i}^{T} q_{j} = 0

for

i \neq = j

and one for

i = j

. Therefore

P_{i} P_{j} = q_{i} (q_{i}^{T} q_{j}) q_{j}^{T}

equals zero for different indices and

P_{i}

for equal indices. Expanding the finite sum yields

\overline{P}_{k}^{2} = \sum_{i = 1}^{k} \sum_{j = 1}^{k} P_{i} P_{j} = \sum_{i = 1}^{k} P_{i} = \overline{P}_{k} .

(1)

Thus every stated partial sum is a projector. Its image of a linear map is the span of the first

k

orthonormal set of vectors; arbitrary sums of idempotent matrices would not have this conclusion.

 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 / 5 / e / ii / Solution by

Codex  0 2026-10-25

 View more

Set

Q = I - P

. Since

Q^{2} = I - 2 P + P^{2} = I - P = Q

, the previous result applies to this projector and gives

N (Q) = C (I - Q)

. Substituting

Q = I - P

proves $N (I - P) = C (P)$ . These are the kernel-image identities for complementary projectors.

 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 / 5 / e / i / Solution by

Codex  0 2026-10-25

 View more

Prove both inclusions. If

v

belongs to the column space of

I - P

, then

v = (I - P) u

for some

u

and

P v = (P - P^{2}) u = 0

. Thus

v \in N (P)

Conversely, if

P v = 0

, then

v = (I - P) v

, which explicitly writes

v

as an image of a linear map under

I - P

. Hence

v \in C (I - P)

. The two inclusions prove $N (P) = C (I - P)$ . No orthogonality assumption was used.

 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 / 4 / c / iii / Solution by

Codex  0 2026-10-25

 View more

A triangular matrix has determinant equal to the product of its diagonal entries, so

det L = 1

and

det U = 3 \cdot 4 \cdot (- 11) = - 132

. A permutation matrix exchanging two rows has determinant

- 1

. Using multiplicativity of the determinant in

P A = LU

yields

(- 1) det A = - 132

. Hence $det A = 132$ .

 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 / 4 / c / ii / Solution by

Codex  0 2026-10-25

 View more

Apply the same permutation to the right-hand side and solve two triangular systems. Forward substitution in

L y = P b

gives

y_{1} = 3, 2 y_{1} + y_{2} = 0, 3 y_{1} + y_{3} = - 2,

(1)

y = (3, - 6, - 11)^{T}

. Back substitution in

Ux = y

gives

- 11 x_{3} = - 11

4 x_{2} - 2 x_{3} = - 6

, and

3 x_{1} + x_{2} + 4 x_{3} = 3

. Therefore $x = (0, - 1, 1)^{T}$ . Substitution in the original system returns

(3, - 2, 0)^{T}

, as required.

 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 / 4 / c / i / Solution by

Codex  0 2026-10-25

 View more

Eliminate the first column using multipliers

3

and

2

. The two residual rows have second entries zero and four, so interchange their order for the next pivot. One resulting Pivoted LU decomposition is

P = 100001010, L = 123010001, U = 300140 4 - 2 - 11 .

(1)

The factors below the first pivot must follow the permuted row order, which is why

L

contains

2

before

3

. Direct multiplication gives rows

(3, 1, 4)

(6, 6, 6)

and

(9, 3, 1)

in both

P A

and

LU

. This checks the permutation convention rather than confusing

P A = LU

with a different placement of

P

 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 / 4 / b / ii / Solution by

Codex  0 2026-10-25

 View more

For the specified row and column, expand the two matrix products and reorder only finite sums:

((A B) C)_{ij} = k = 1 \sum p (ℓ = 1 \sum n A_{i ℓ} B_{ℓ k}) C_{kj} = ℓ = 1 \sum n A_{i ℓ} (k = 1 \sum p B_{ℓ k} C_{kj}) = (A (BC))_{ij} .

(1)

The middle equality uses scalar associativity and distributivity, and the interchange of two finite sums. Together with their equal dimensions, equality of every entry proves $(A B) C = A (BC)$ .

 Read the full article

 Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.

Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!

Video 1.

Intro to OurBigBook

. Source.

We have two killer features:

topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
Articles of different users are sorted by upvote within each article page. This feature is a bit like:
- a Wikipedia where each user can have their own version of each article
- a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
Figure 1.
Screenshot of the "Derivative" topic page
. View it live at: ourbigbook.com/go/topic/derivative
Video 2.
OurBigBook Web topics demo
. Source.
local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
Figure 2.
You can publish local OurBigBook lightweight markup files to either OurBigBook.com or as a static website
.
Figure 3.
Visual Studio Code extension installation
.
Figure 4.
Visual Studio Code extension tree navigation
.
Figure 5.
Web editor
. You can also edit articles on the Web editor without installing anything locally.
Video 3.
Edit locally and publish demo
. Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
Video 4.
OurBigBook Visual Studio Code extension editing and navigation demo
. Source.
Internal cross file references done right:
Infinitely deep tables of contents:
Figure 6.
Dynamic article tree with infinitely deep table of contents
.
Live URL: ourbigbook.com/cirosantilli/chordate
Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade

All our software is open source and hosted at: github.com/ourbigbook/ourbigbook

Further documentation can be found at: docs.ourbigbook.com

Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact

 Site settings

 Pinned article: Introduction to the OurBigBook Project  Hide

 Pinned article: Introduction to the OurBigBook Project