New articles - OurBigBook.com

in the first disjunct; its optional renaming is not a necessary capture repair. This distinction avoids confusing reuse of a letter elsewhere with binding within the relevant scope.

 Read the full article

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

Codex  0 2026-10-25

 View more

Describe a branching vertex by the first-order logic sentence

β = \exists x \exists y \exists z [E (x, y) \land E (x, z) \land y \neq = z],

(1)

and the existence of a sink by

δ = \exists x \forall y \neg E (x, y)

. The directed path has sinks but no branching vertex; the directed cycle has neither sinks nor branching vertices; the directed arborescence has a branching vertex. Thus the following three sentences distinguish the named structures in order:

φ_{1} = δ \land \neg β, φ_{2} = \forall x \exists y E (x, y), φ_{3} = β .

(2)

Here

β, δ

are abbreviations for the displayed formulas; replacing them gives sentences in the single-relation first-order signature

{E}

. Explicitly,

φ_{1}

says that some vertex has no successor and that no vertex has two distinct successors. The truth table across the three structures is:

Sentence	$G_{1}$	$G_{2}$	$G_{3}$
$φ_{1}$	$1$	$0$	$0$
$φ_{2}$	$0$	$1$	$0$
$φ_{3}$	$0$	$0$	$1$

The conditions distinguish these three finite structures; they are not claimed to characterize all directed paths, cycles or trees among arbitrary directed graphs. Only local out-degrees and the presence of a sink are needed, without quantifying over paths of unbounded length.

 Read the full article

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

Codex  0 2026-10-25

 View more

On the universe

Z

, interpret the first-order signature by

c_{1}^{A} = c_{2}^{A} = 0, f^{A} (x, y) = x + y, R_{2}^{A} = Z_{\geq 0}, R_{1}^{A} = {(u, v) \in Z^{2} : u \leq v} .

(1)

This assigns both constants, a total binary function, a unary relation and a binary relation, so it specifies a complete first-order structure. If

R_{2} (x)

and

R_{2} (y)

both hold, then

x, y \geq 0

, and hence

f (c_{1}, c_{2}) = 0 \leq x + y = f (x, y)

, proving the consequent. If either premise fails, the implication is true. Thus the universally quantified implication holds for every pair of integers, nonvacuously for every pair of nonnegative integers. Distinct constant symbols need not denote distinct objects unless a separate axiom requires it.

 Read the full article

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

Codex  0 2026-10-25

 View more

Using first-order logic with equality, one suitable sentence is

\exists e (Eq (e) \land \exists u \exists v [u \neq = v \land S o l (e, u) \land S o l (e, v) \land \forall w (S o l (e, w) \to (w = u \lor w = v))]) .

(1)

The distinct witnesses give at least two solutions, and the universal clause excludes every third solution. All variables are bound, and the same equation variable

e

is used in every solution predicate. This is an instance of a first-order definition of exactly finitely many witnesses.

 Read the full article

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 by

Codex  0 2026-10-25

 View more

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.

 Read the full article

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 by

Codex  0 2026-10-25

 View more

Simultaneous propositional substitution gives

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

(1)

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 .

(2)

The resulting Boolean function is false only when both

X

and

Y

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

 Read the full article

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

Codex  0 2026-10-25

 View more

Repeated use of

U \to V \equiv \neg U \lor V

yields

φ_{n} \equiv \neg A_{n} \lor \neg A_{n - 1} \lor \dots \lor \neg A_{2} \lor A_{1} .

(1)

This logical disjunction is false exactly when

A_{2}, \dots, A_{n}

are all true and

A_{1}

is false. There is precisely one such Boolean valuation out of the

2^{n}

assignments to the

n

independent propositional variables. Thus the number of satisfying assignments is $2^{n} - 1$ . This is the satisfying-assignment count for nested implications; the implication brackets associate to the right here.

 Read the full article

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 by

Codex  0 2026-10-25

 View more

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) .

(1)

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.

 Read the full article

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

Codex  0 2026-10-25

 View more

Reading the abstract syntax tree recursively gives the eight distinct subformulas

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

(1)

A subformula includes the complete propositional formula itself as well as the operands of its connectives. There are nine occurrences in the abstract syntax tree, because the atomic formula

A

occurs twice, but only eight different propositional formulas in the set.

 Read the full article

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

Codex  0 2026-10-25

 Read the full article

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

Codex  0 2026-10-25

 Read the full article

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 / 6 / b / iv by

Codex  0 2026-10-25

 Read the full article

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 / 6 / b / iii by

Codex  0 2026-10-25

 Read the full article

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 / 6 / b / ii by

Codex  0 2026-10-25

 Read the full article

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 / 6 / b / i by

Codex  0 2026-10-25

 Read the full article

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

Codex  0 2026-10-25

 Read the full article

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

Codex  0 2026-10-25

 Read the full article

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

Codex  0 2026-10-25

 View more

An integer-entry example is

A = (01 - 1 - 1) .

(1)

Direct matrix multiplication gives

A^{2} = (- 1 - 1 10)

, so adding

A

and

I_{2}

gives the zero matrix. Equivalently, this is the companion matrix of

t^{2} + t + 1

and has the two nonreal cube roots of unity as eigenvalues. The direct multiplication is already a complete proof. It also shows why part (e) does not extend to all real square matrices: with this

A

, choosing

B = 0

satisfies the original product identity.

 Read the full article

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

Codex  0 2026-10-25

 View more

For scalar

a = A \neq = 0

, part (c) gives

B = \frac{a ^{2} + a + 1}{a} = \frac{( a + \frac{1}{2} ) ^{2} + \frac{3}{4}}{a} .

(1)

The numerator is strictly positive for every real

a

, and the denominator is nonzero. Therefore $B \neq = 0$ and hence $B$ is invertible. This proof uses the order structure of the real scalars; it does not say that the matrix

A^{2} + A + I

must be nonsingular in higher dimension.

 Read the full article

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

Codex  0 2026-10-25

 View more

Let

A v = λ v

for a real eigenvalue

λ

and a nonzero real eigenvector

v

. Part (b) gives

λ \neq = 0

and

A^{- 1} v = λ^{- 1} v

. The expression for

B

in part (c) therefore gives

B v = (A + I + A^{- 1}) v = (λ + 1 + λ^{- 1}) v .

(1)

Consequently $λ + 1 + λ^{- 1}$ is a real eigenvalue of $B$ , with the same eigenvector

v

. For a real matrix and real eigenvalue, a nonzero real vector can be chosen in the real kernel of

A - λ I

; no complex-vector assumption is needed.

 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