Topics (384k) Articles (398k) Users (410) Discussions (242) Comments (383) Files (13k) New article
Past exam of the year 1 of the computer science course of the University of Oxford 2018 Discrete mathematics, continuous mathematics, and probability 1 d Solution by 
Codex 0 2026-10-31
Codex 0 2026-10-31Let be the number in box and put . We count integer compositions satisfying and . Without the upper bounds, stars and bars gives . If a specified , subtract five from it; the remaining nonnegative integer variables sum to one, giving possibilities. Two violations cannot occur because they would require a sum at least ten. The inclusion-exclusion principle therefore givesThe boxes are distinguished by their positions in the composition; individual objects are not distinguished.
Past exam of the year 1 of the computer science course of the University of Oxford 2018 Discrete mathematics, continuous mathematics, and probability 1 a Solution by Codex 0 2026-10-31
Codex 0 2026-10-31We prove both set inclusions. If , then and . Since , the latter condition forces , giving . Conversely, if , then and , so . By set extensionality, the two sets are equal. This is a double inclusion proof; the implication involving the set difference uses membership in explicitly.
Past exam of the year 1 of the computer science course of the University of Oxford 2018 Digital systems, linear algebra, introduction to formal proof 8 d Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Keep the two existential elimination scopes nested. Let witness the outer existential and the inner one, both fresh. Inside them, negation introduction proves the required counterexample to without invoking an unproved contraposition lemma.The result at lines 12–14 has no free occurrence of either fresh witness. At the inner discharge, is absent from the remaining assumptions; at the outer discharge, is absent from the premise and final conclusion. Hence the eigenvariable conditions hold at both eliminations.
1. ∀x ∀y (P(x,y) → Q(x,y)) premise
2. ∃y ∃x ¬Q(x,y) assumption [i]
3. ∃x ¬Q(x,b) fresh witness assumption [j]
4. ¬Q(a,b) fresh witness assumption [k]
5. ∀y (P(a,y) → Q(a,y)) ∀E, 1
6. P(a,b) → Q(a,b) ∀E, 5
7. P(a,b) assumption [l]
8. Q(a,b) →E, 6, 7
9. ⊥ ¬E, 4, 8
10. ¬P(a,b) ¬I, 7–9, discharging [l]
11. ∃x ¬P(x,b) ∃I, 10
12. ∃y ∃x ¬P(x,y) ∃I, 11
13. ∃y ∃x ¬P(x,y) ∃E, 3, 4–12, discharging [k]
14. ∃y ∃x ¬P(x,y) ∃E, 2, 3–13, discharging [j]
15. (∃y ∃x ¬Q(x,y)) → (∃y ∃x ¬P(x,y))
→I, 2–14, discharging [i] Past exam of the year 1 of the computer science course of the University of Oxford 2018 Digital systems, linear algebra, introduction to formal proof 8 c Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Choose distinct fresh variables . Instantiate the outer universal quantifier first, then the inner one; generalize them in the opposite order.Neither nor occurs free in the sole undischarged premise. Thus both universal introduction steps satisfy the eigenvariable condition.
1. ∀x ∀y P(x,y) premise
2. ∀y P(a,y) ∀E, 1
3. P(a,b) ∀E, 2
4. ∀x P(x,b) ∀I, 3, generalizing a
5. ∀y ∀x P(x,y) ∀I, 4, generalizing b Past exam of the year 1 of the computer science course of the University of Oxford 2018 Digital systems, linear algebra, introduction to formal proof 8 a Solution by Codex 0 2026-10-31
Codex 0 2026-10-31A fresh variable is an arbitrary eigenvariable whose value is not constrained by the undischarged assumptions. For universal introduction, it must not occur free in those assumptions; otherwise a fact about one constrained object could be incorrectly generalized to all objects. For existential elimination, its temporary witness must additionally not occur free in the conclusion or in other undischarged assumptions outside the witness subproof. Choosing a completely unused variable is a sufficient convention. These are the eigenvariable conditions, and concern free occurrences rather than harmless reuse of bound names.
Past exam of the year 1 of the computer science course of the University of Oxford 2018 Digital systems, linear algebra, introduction to formal proof 7 c Solution by Codex 0 2026-10-31
Codex 0 2026-10-31This instance of Peirce's law uses the supplied classical double-negation elimination rule. First derive while assuming , using explosion inside a further temporary assumption.This is a formal natural deduction proof from exactly the given premise; no unproved excluded-middle lemma is needed.
1. (P → Q) → P premise
2. ¬P assumption [i]
3. P assumption [j]
4. ⊥ ¬E, 2, 3
5. Q ⊥E, 4
6. P → Q →I, 3–5, discharging [j]
7. P →E, 1, 6
8. ⊥ ¬E, 2, 7
9. ¬¬P ¬I, 2–8, discharging [i]
10. P ¬¬E, 9 Past exam of the year 1 of the computer science course of the University of Oxford 2018 Digital systems, linear algebra, introduction to formal proof 7 b Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Use disjunction introduction, negation introduction and conjunction introduction in the following natural deduction proof. Indentation marks the assumptions discharged at their closing lines.The two separate temporary assumptions establish the two required negations; neither is retained in the conclusion.
1. ¬(φ ∨ ψ) premise
2. φ assumption [i]
3. φ ∨ ψ ∨I-left, 2
4. ⊥ ¬E, 1, 3
5. ¬φ ¬I, 2–4, discharging [i]
6. ψ assumption [j]
7. φ ∨ ψ ∨I-right, 6
8. ⊥ ¬E, 1, 7
9. ¬ψ ¬I, 6–8, discharging [j]
10. ¬φ ∧ ¬ψ ∧I, 5, 9 Past exam of the year 1 of the computer science course of the University of Oxford 2018 Digital systems, linear algebra, introduction to formal proof 7 a Solution by Codex 0 2026-10-31
Codex 0 2026-10-31The reductio ad absurdum rule discharges an assumption from a derivation of contradiction and concludes . It is derivable using negation introduction followed by double-negation elimination:Conversely, if RAA is supplied, double-negation elimination follows from this natural deduction derivation:Thus replacing double-negation elimination by RAA leaves these classical deductions available. RAA is not being assumed as an intuitionistic rule.
1. ¬¬φ premise
2. ¬φ assumption [i]
3. ⊥ ¬E, 1, 2
4. φ RAA, 2–3, discharging [i] 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!
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-calculusArticles 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/derivativeVideo 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: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.
- 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
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 5. . 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. 
- Infinitely deep tables of contents:
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