RAISE AI Safety prerequisites map entirely in one post
post by RAISE · 2019-07-17T08:57:18.226Z · LW · GW · 5 commentsContents
How to use this Credits Main path Level 1. Basic logic Level 2. Basic set theory Level 3. Set Theoretic Relations and Enumerability Level 4. Formal Semantics Level 5. Formal Proof Level 6. Turing Machines and the Halting Problem Level 7. Equivalence Relations and Orderings Level 8. Abacus Computability and Mathematical Proof by Induction Level 9. The Natural Numbers in Set Theory and More Induction Level 10. Recursive Functions Level 11. Set Theoretic Recursion Level 12. The Equivalence of Different Notions of Computability Level 13. Isomorphisms Level 14. Logic Review and The Relationship Between Computation and Logic Level 15. Finite and Countable Sets Level 16 (elective). Linear Orders and Completing the Real Numbers Level 17. Basic Model Theory Level 18 (elective). A quick look at cardinal and ordinal numbers Level 19. Arithmetization and Representation of Recursive Functions Level 20. Godel’s Incompleteness Theorems and Axiomatic ZFC Logic and proof path Level 1. Basic logic Level 2. Quantified logic. Introduction to mathematical arguments Level 3. Formal semantics basics Level 4. Formal proofs Level 5. Proof by induction Set theory path Level 1. Basic set theory Level 2. Set theoretic relations Level 3. Equivalence relations and orderings Level 4. Natural numbers and induction Level 5. Set theoretic recursion Level 6. Operations, structures, isomorphism Level 7. Cardinality. Finite and countable sets Elective: Level 8. Linear orderings. Completeness. Uncountable sets Elective: Level 9. Cardinal numbers Elective: Level 10. Ordinal numbers. Axiom of replacement. Transfinite induction and recursion Elective: Level 11. Axiom of choice Level 12. ZF(C) set theory Computability theory path Level 1. Enumerability and diagonalization Level 2. Turing machines and the halting problem Level 3. Abacus computability Level 4. Recursive functions Level 5. The equivalence of different notions of computability Level 6. First order logic Level 7. Undecidability of first order logic Level 8. Models, their existence. Proofs and completeness. Level 9. Arithmetization. Representability of recursive functions Level 10. Indefinability, undecidability, incompleteness. The unprovability of consistency. None 5 comments
After reflecting on recent criticism [LW · GW], all RAISE projects have been discontinued, and a postmortem is in our plans. (Update: the postmortem is here [LW · GW]) One of those projects was the AI Safety prerequisites online course originally announced here [LW · GW]. We're sharing the curriculum here in almost plaintext format so that people can easily find and access it. There is also a GDoc here. (Note: two other products of RAISE are series of lessons on IRL and IDA. They don't have such neatly formed curriculums, and they are still accessible as online lessons.)
It was supposed to be a guide for helping people who want to get into AI safety research. It contains only foundations of math topics (Logic and proof, ZF(C) Set theory, Computability theory to be precise), which are more useful for agent foundations stuff and not useful for machine learning stuff. It was planned to be extended to cover more topics, but that never happened.
How to use this
The main path contains 20 levels. It is the recommended path through the curriculum. Its levels are actually short sequences of levels from the three other paths.
To see what textbooks are required to study a path, see its beginning. Computability theory and set theory paths require two paid textbooks.
13 out of 20 levels of the main path are covered by our online course, which is free (but still requires paid textbooks). To use the online course, register here. You might prefer to use it instead of the text below because it provides more sense of progress, contains solutions to the exercises, has some writing mistakes fixed, maybe feels like a less tedious thing, and provides some additional exercises which we don't think are important.
Credits
The curriculum was made by Erik Istre [LW · GW] and Trent Fowler [LW · GW]. People who created the online course are: Philip Blagoveschensky [LW · GW], Davide Zagami, Toon Alfrink [LW · GW], Hoagy Cunningham, Danilo Naiff, Lewis Hammond. Also these people contributed: Jacob Spence, Roland Pihlakas. Also, thanks to Grasple for providing their services for free.
Main path
Level 1. Basic logic
The big ideas:
- Sentential Logic
- Truth Tables
- Predicate Logic
- Methods of Mathematical Proof
To move to the next level you need to be able to:
- Translate informal arguments into formal logic.
- Evaluate an argument as either valid or invalid.
- Explain how to prove an implication/conditional, a conjunction, a disjunction, and a negation and know what this looks like informally (i.e. in words and not symbols).
Why this is important:
- This builds the basic knowledge you need to be able to produce and understand mathematical proof. A firm foundation in how logical machinery operates is the best way to be assured that a proof you produce or read is correct. This also teaches the basic methods by which a proof is produced.
Skill Guides for this Level:
- Logic and proof path. Level 1. Basic logic
- Logic and proof path. Level 2. Quantified logic. Introduction to mathematical arguments
Level 2. Basic set theory
The big ideas:
- Axioms of Set Theory
- Set Operations
To move to the next level you need to be able to:
- Explain what a set is.
- Calculate the intersection, union and difference of sets.
- Prove two sets are equal.
- Apply basic axioms of Zermelo-Fraenkel set theory.
Why this is important:
- Set theory has become entrenched as the basic language with which all mathematics can be discussed. While there are more estranged parts of set theory that will likely be irrelevant to you, a fluency in the basic materials of set theory is necessary to understand more advanced mathematics.
Skill Guides for this level:
Level 3. Set Theoretic Relations and Enumerability
The big ideas:
- Ordered Pairs
- Relations
- Functions
- Enumerability
- Diagonalization
To move to the next level you need to be able to:
- Define functions in terms of relations, relations in terms of ordered pairs, and ordered pairs in terms of sets.
- Define what a one-to-one (or injective) and onto (or surjective) function is. A function that is both is called a one-to-one correspondence (or bijective).
- Prove a function is one-to-one and/or onto.
- Explain the difference between an enumerable and a non-enumerable set.
Why this is important:
- Establishing that a function is one-to-one and/or onto will be important in a myriad of circumstances, including proofs that two sets are of the same size, and is needed in establishing (most) isomorphisms.
- Equivalence relations and partial orderings are essential mathematical concepts which are powerful tools that can be used to analyze other mathematical objects or build new ones.
- Enumerability and non-enumerability introduces the difference between something being computable and non-computable.
Skill Guides for this level:
- Computability theory path. Level 1. Enumerability and diagonalization
- Set theory path. Level 2. Set theoretic relations
Level 4. Formal Semantics
The big ideas:
- Formal Semantics
- Model
To move to the next level you need to be able to:
- Evaluate the truth value of logical sentences in a given model.
- Build models for a set of logical sentences and then use those models to deduce information about the sentences.
Why this is important:
- An AI built on a formal system will reason based on some sort of proof and model theory. The former gives its methods of proof (which you’ll learn in the next chapter), and the latter its semantics.
- This level will give you your first sense of what models of logical sentences look like.
Skill guides for this level:
Level 5. Formal Proof
The big ideas:
- Natural Deduction Proof System
To move to the next level you need to be able to:
- Explain the difference between a formal system of proof and our informal notion of proof.
- Derive proofs of logical formula in the system of natural deduction.
Why this is important:
- Learning mathematical proof is hard, as you may have experienced in levels 2 and 3. By learning a formal system of proof you will make your own thoughts more rigorous, understand the smallest details that need to be covered to perform a proof, and build your intuition for informal proof.
Skill guides for this level:
Milestone - You’re now a !
- You now understand the basics of logic and how they apply to proof.
- You can take an argument and peel away the content to look purely at its structural details.
- You understand the basics of building a model of formal sentences of logic.
- You know the basic building blocks of set theory.
- You now know there exist uncomputable functions, and you know how to rigorously define the concept of a function.
Take a moment to reflect on what you’ve learned so far. Remind yourself of the important concepts that you’ve come across, and mark down any concepts which are still giving you trouble. Determine whether you need to seek out further resources to clear up any confusions.
Level 6. Turing Machines and the Halting Problem
The big ideas:
- Turing Machine
- The Halting Problem
To move to the next level you need to be able to:
- Describe a turing machine and write basic turing algorithms.
- Give the basic idea of the halting problem.
- Give the basic idea of the proof that the halting function isn’t computable.
Why this is important:
- This is the beginning of learning formal computability. This allows us to think about computation without the limits of a physical domain. The first step to reasoning about Artificial General Intelligence will be understanding how it can be done before we worry about its practical feasibility.
- The halting problem is a pervasive and annoying problem. It’ll come up again and again, in many disguises. If we could solve the halting problem, things would be easy. Since we can’t, things are hard. Understanding the limitations it imposes is important.
Skill guides for this level:
Level 7. Equivalence Relations and Orderings
The big ideas:
- Equivalence Relations
- Partitions
- Orderings
To move to the next level you need to be able to:
- Explain the relationship between equivalence relations and partitions.
- Name two different kinds of orderings and the conditions on the ordering relations required for these kinds.
Why this is important:
- This level is about further building up your mathematical toolbox. While equivalence relations and orderings currently seem like random abstract notions, they are both very important. The former is gives you a way to instantiate different notions of equality, which is important in modeling. The latter appears in constructing models for another turing machine equivalent notion of computability, the lambda calculus.
Skill guides for this level:
Level 8. Abacus Computability and Mathematical Proof by Induction
The big ideas:
- Proof by Induction
- Abacus Computability
To move to the next level you need to be able to:
- Explain mathematical proof by induction.
- Explain the abacus machine and the differences between a turing machine and an abacus machine.
- Build basic algorithms for an abacus machine.
Why this is important:
- Mathematical proof by induction is a very powerful technique. While you’ll first learn to use it in the context of natural numbers, you’ll soon see it has applications beyond this domain.
- An abacus machine gives you a higher level means of expressing algorithms, allowing you to abstract away from the minute details of strokes on a tape.
Skill guides for this level:
- Logic and proof path. Level 5. Proof by induction
- Computability theory path. Level 3. Abacus computability
Level 9. The Natural Numbers in Set Theory and More Induction
The big ideas:
- Representing Natural Numbers with Sets
To move to the next level you need to be able to:
- Explain the relationship between inductive sets and the set theoretic construction of the natural numbers.
- Use the method of mathematical induction to prove claims about the natural numbers.
Why this is important:
- This builds an understanding of how set theory is used to provide rigorous constructions of mathematical objects we usually take for granted, like the natural numbers. Learning how to provide these constructions is an important part of building models in model theory.
Skill guides for this level:
Level 10. Recursive Functions
The big ideas:
- Primitive Recursive Functions
- Recursive Functions
- Primitive Recursive Sets
- Recursive Sets
To move to the next level you need to be able to:
- Translate the formal syntax of the recursive functions into an informal representation of a function and vice versa.
- Explain the difference between primitive recursion and recursion.
- Explain the difference between semi-recursive and recursive.
Why this is important:
- By this point in your FAI career, you may have developed some sort of fascination of the power of this idea of “recursion”. Well, now you’re learning that notion. It is powerful, but it can also get a bit complicated so take your time and on this concept.
Skill guides for this level:
Level 11. Set Theoretic Recursion
The big ideas:
- The Recursion Theorem
- Peano Axioms
To move to the next level you need to be able to:
- State the recursion theorem and explain how this theorem coincides with our informal notion of recursion.
- Use the recursion theorem to create new functions.
- Explain what the axioms of Peano arithmetic are.
Why this is important:
- This is recursion...again! (In true recursive spirit.) However, it’s a bit different this time. This time we’re showing a way to look at recursion from a set theory perspective. We can take the recursive functions of computability as given and do some things with them, or we can use our set theoretic foundations to build the theory of recursion itself. Think of this as further justification and an assurance of what we’re doing.
- You’ll also get a look at what are known as “Peano’s axioms”. If we assume these axioms, or alternatively provide a set theoretic structure in which they hold, the claim is that these axioms can give us all our theorems of informal arithmetic in a formal system. Formalization of arithmetic will be important later for deriving limitative results about formal systems.
Skill guides for this level:
Level 12. The Equivalence of Different Notions of Computability
The big ideas:
- Equivalence of Turing Machines and Recursive Computability
To move to the next level you need to be able to:
- Describe the general process of coding turing machines.
- Explain what a universal turing machine is.
Why this is important:
- Establishing the equivalence of independently developed methods of computation is a strong argument in favor of the Church-Turing thesis.
- The existence of a universal turing machine is a good thing. It made the general purpose computer that we’re so used to today a feasible invention. We don’t need 1000 specialized machines, but only one that can imitate those 1000.
Skill guides for this level:
Milestone - You’re now a !
- You now understand the basic abstract representations of computation.
- You know some of what we can expect from computers and also what we can’t expect from them.
- You know a lot more set theoretic tools like equivalence relations and orderings.
- You’ve seen the construction of the natural numbers from the perspective of set theory.
- You know about mathematical induction and you’ve used it!
- You know about recursion and you’ve used it!
- More abstractly, your mathematical maturity has greatly increased from when you began.
As last time, take a moment to reflect on what you’ve learned so far. Remind yourself of the important concepts that you’ve come across, and mark down any concepts which are still giving you trouble. Determine whether you need to seek out further resources to clear up any confusions.
Level 13. Isomorphisms
The big ideas:
- Isomorphism
To move to the next level you need to be able to:
- Define isomorphism between structures.
- Prove that two structures are isomorphic.
Why this is important:
- Isomorphism is one of the most fundamental mathematical concepts. Finding isomorphisms allows you to move insights from one problem domain into another, which can be incredibly useful.
- However, it should be noted that “isomorphism” only rigorously applies when talking about algebraic structures, i.e. structures with relations and operations and a domain.
Skill guides for this level:
Level 14. Logic Review and The Relationship Between Computation and Logic
The big ideas:
- First Order Logic Syntax
- First Order Logic Semantics
- The Relationship Between Logic and Computability
To move to the next level you need to be able to:
- Read and translate the syntax for formal logic, and translate informal sentences to logic.
- Build models to evaluate logical claims.
- Explain how logic and turing machines/primitive recursion are related and how this leads to showing the undecidability of first-order logic.
Why this is important:
- This chapter reviews concepts from Levels 4 and 5 so it’s important for the same reasons covered there.
- The undecidability of logic has important implications for how an Artificial General Intelligence is limited (in much the same way we are!) in deriving proofs.
Skill guides for this level:
- Computability theory path. Level 6. First order logic
- Computability theory path. Level 7. Undecidability of first order logic
Level 15. Finite and Countable Sets
The big ideas:
- Finite Set
- Countable Set
To move to the next level you need to be able to:
- State the Cantor-Bernstein Theorem.
- Understand basic properties of finite and countable sets.
- Define what a countable set is.
- Prove that a set is of countable size.
Why this is important:
- The Cantor-Bernstein theorem may not have strict relevance for you. You can consider it part of your general mathematical well-being. It’s some set theory you really should know.
- Finite and countable sizes are what we as finite beings have “constructive” access to. We reason about other cardinalities, but it all becomes a little less graspable and tangible. These sizes of sets are important and probably give us everything we need in the real world. (For more on this: Computable Real Numbers)
Skill guides for this level:
Level 16 (elective). Linear Orders and Completing the Real Numbers
The big ideas:
- Constructing the Real Numbers
To move to the next level you need to be able to:
- Define when two linear orders are similar.
- Explain how the concept of completeness motivates the real numbers.
- Explain how Dedekind cuts generate completeness for the rational numbers.
Why this is important:
- If we look at the rationals from the perspective of completeness, we motivate the development and construction of the real numbers. This provides another useful example of a mathematical construction.
- In the current context, the real numbers are a prime example of an uncountable set.
Skill guides for this level:
Level 17. Basic Model Theory
The big ideas:
- Models
- Soundness
- Completeness
- Sequent Calculus
To move to the next level you need to be able to:
- Define a model.
- Explain the Lowenheim-Skolem theorem and the compactness theorem.
- Use a Gentzen style system or sequent calculus to derive proofs.
- Explain the concepts of soundness and completeness.
Why this is important:
- Model theory allows us to map a formal proof theoretic system into a defined domain where it hopefully applies. Whether or not it applies appropriately depends on the soundness and completeness results. This is all about asking “Do my formal deductions match up with something out there and do all of the somethings out there match up with my formal deductions?” As you may already know or will see in a few levels, the latter question is impossible to prove in formalized situations, but still worth pondering.
Skill guides for this level:
Milestone - You’re now a !
- You know the rigorous definition of an isomorphism.
- You now can explain the relationship between computability and logic.
- You understand way more about the size of things and way more sophisticated ways to count than you ever thought necessary.
- You can give a general outline of how to build the real numbers from the rationals.
- You can use a Gentzen style system to develop proofs.
- You can use soundness and completeness to demonstrate those Gentzen style proofs are “nice”.
- You know how to think about models more in-depth and about some of the more important theorems that apply to them.
As last time, take a moment to reflect on what you’ve learned so far. Remind yourself of the important concepts that you’ve come across, and mark down any concepts which are still giving you trouble. Determine whether you need to seek out further resources to clear up any confusions.
Level 18 (elective). A quick look at cardinal and ordinal numbers
To move to the next level you need to be able to:
- Explain what a cardinal number is.
- Demonstrate the general idea behind the proof of Cantor’s Theorem.
- Explain what an ordinal number is.
- Use the generalized notions of transfinite induction and transfinite recursion to prove statements about large sets.
Why this is important:
- This level is mainly for expanding what set theoretic tools you’re familiar with. While it is unlikely that cardinal theory or ordinal theory will directly play into AGI research, it still may crop up in unexpected places like model theory.
- Ordinal theory also sets you up to later learn what is known as “proof theoretic strength” of a formal system which is expressed in ordinal numbers and relies on transfinite induction.
Skill guides for this level:
- Set theory path. Elective: Level 9. Cardinal numbers
- Set theory path. Elective: Level 10. Ordinal numbers. Axiom of replacement. Transfinite induction and recursion
Level 19. Arithmetization and Representation of Recursive Functions
The big ideas:
- The Axiom of Choice
- Arithmetization of Syntax
- Mathematical Induction
- Representability of Functions
To move to the next level you need to be able to:
- Elective: State the axiom of choice and at least loosely explain it to someone with basic set theory.
- Describe the process of generating Godel numbers for logical statements.
- Define what it means for a recursive function to be representable in a system of arithmetic.
Why this is important:
- Being aware of the axiom of choice makes it easier to be aware when you are invoking it. This generally points out how the apparently simplest of assumptions can turn out to be just that: assumptions. We must be prepared to discover all of our assumptions working into our informal proofs before we think about applying them to a potentially hazardous problem like an AGI.
- The rest of this level is setting up the material for the oft-quoted Godel incompleteness theorems which place hard limits on what formal systems are capable of.
Skill guides for this level:
- Set theory path. Elective: Level 11. Axiom of choice
- Computability theory path. Level 9. Arithmetization. Representability of recursive functions
Level 20. Godel’s Incompleteness Theorems and Axiomatic ZFC
The big ideas:
- Godel’s Incompleteness Theorems
- Independence Result
- Zermelo-Fraenkel Set Theory
To move to the next level you need to be able to:
- Explain the diagonal lemma and why it leads to the limitative results of formal systems. Further, explain under what precise conditions we must be for these results to accurately apply.
- Explain Godel’s first and second incompleteness theorems and the general procedure of their proofs.
- Define what an independence result is and a particular example of such a result for ZFC.
- Explain why Godel’s Incompleteness theorems also apply to a formal set theory like ZFC.
Why this is important:
- This level is all about formal systems and what they can’t do. These are the problems that will need to be circumvented, or at least shown to be irrelevant to a development of a formal AGI.
Skill guides for this level:
- Set theory path. Level 12. ZF(C) set theory
- Computability theory path. Level 10. Indefinability, undecidability, incompleteness. The unprovability of consistency.
Milestone - You’re now a !
- You’re now a well-rounded set theorist.
- You can explain how to code up logical statements and give them Godel Numbers.
- You can explain why this leads to limitative results in formal systems and what these results mean.
As last time, take a moment to reflect on what you’ve learned so far. Remind yourself of the important concepts that you’ve come across, and mark down any concepts which are still giving you trouble. Determine whether you need to seek out further resources to clear up any confusions.
Logic and proof path
The main textbook used in this path is a free textbook "Forall x" version 1.4. download v1.4 another link for v1.4 latext version Note that numbering of exercises sometimes changes between versions.
Another resource used in this path is Introduction to Mathematical Arguments by Michael Hutchings.
Level 1. Basic logic
-
Read Chapter 1 of forall x, “What is Logic?”.
- Work the following exercises:
- Part A
- Part B
- Part C
- Part D
- Work the following exercises:
-
Read Chapter 2 of forall x, “Sentential Logic”
- Work the following exercises:
- Part C
- Part D
- Part G
- Part H
- Work the following exercises:
-
Read Chapter 3 of forall x, “Truth Tables”
- Work the following exercises:
- From Part A:
- 1
- 4
- 5
- 11
- From Part B:
- 1
- 2
- 6
- 8
- 9
- 10
- From Part C:
- 2
- 4
- From Part D:
- 3
- 6
- 7
- 8
- 10
- Part E
- Extra Credit: Part F
- From Part A:
- Work the following exercises:
Level 2. Quantified logic. Introduction to mathematical arguments
- Read Chapter 4 of forall x, “Quantified Logic”
- Less Important Sections: “Definite Descriptions”
- Part A
- From Part B:
- Work at least 5, one with the word “all”, one with the word “some”, and one with the word “no”.
- From Part D:
- 1
- 5
- 6
- Part H
- Part I
- Part K
- All odd numbers.
- Read Introduction to Mathematical Arguments until the end of section 3
- Print/save/copy the table on page 9 and always have it handy
- Section 3.3 talks about groups, which you may have never heard of. Pay attention to the structure of the proof, since that is what we’re interested in here, and ignore the content if it seems confusing. Proof by uniqueness proceeds by saying “if I want to prove there is only one something, I assume I have two somethings and show that they turn out to be the same thing”.
- Work exercises:
- 1
- 2
- 3
- Extra Credit: 4
Level 3. Formal semantics basics
- Read Chapter 5 of forall x, “Formal Semantics”
- Work Exercises:
- Part B
- Part D
- Part F: 1, 2, 3, 5, 8
- Part G: 3, 6, 10
- Part H: 1, 4, 5, 9
- Part I: 1, 2, 3
- Extra Credit: Part J
- Work Exercises:
Level 4. Formal proofs
- Read Chapter 6 of forall x, “Proofs”
- Part A
- Part B
- Part E: 1, 2, 5
- Part G: 1, 3, 4
- Part I
- Part J
- Part Q
- Part T: 1, 2, 4
- Part U: 1, 2, 3, 7, 8, 10
- Extra Credit: Part M
Level 5. Proof by induction
- Read Section 4 of Introduction to Mathematical Arguments , “Proof by Induction”
- This is a very powerful and important proof technique to get comfortable with. Make sure you understand the structure of this argument.
- Work the following exercises:
- 1
- 2
- 4
- Extra Credit:
- 4
- Optional Read Appendix “Sets”
- This will provide a review of the basic concepts of sets if you want a refresher/reinforcement.
- All of the exercises for the appendix are good checks on your knowledge of set theory.
- For 8, draw pictures to guess at new relationships and then prove them or disprove them by finding a counterexample.
Set theory path
This path uses the Introduction to set theory. Third edition. Revised and expanded by Hrbacek, Jech.
Level 1. Basic set theory
- In Introduction to Set Theory by Hrbacek and Jech
- Read Chapter 1 Section 1 “Introduction to Sets”
- Read Chapter 1 Section 2 “Properties”
- Read Chapter 1 Section 3 “The Axioms”
-
Work the following exercises:
- 3.1
- 3.2
- This question is equivalent to asking you to prove:
- “If the Weak Axiom of Existence and the Comprehension Schema hold, then the empty set exists.”
- This is a general note to always try to translate a mathematical assertion into a straightforward logical statement. Once you have it in that logical statement, then you can rely on your logical knowledge to know general steps you need to do to prove that statement.
- This question is equivalent to asking you to prove:
-
3.4
- Proving this requires a few steps that are not immediately obvious.
- First, prove there is a set that contains A and B. (What axioms implies this?)
- Second, prove there is a set that contains the elements of A and B. (Again, what axiom?)
- Finally, use the Comprehension Schema on this set to get the desired set.
- Proving this requires a few steps that are not immediately obvious.
-
3.5a
- This one also requires a few steps as with 3.4. To find these steps, work backwards.
- What instance of the comprehension schema do you need to make this set exist?
- What other set’s existence does that instance of the comprehension schema rely on?
- How do you make that one exist?
- Does this new set rely on another one for existence?
- Continue to move backwards until you can be sure that you have a set that exists. You will have to rely on the fact that the existence of A, B, and C is assumed.
- This one also requires a few steps as with 3.4. To find these steps, work backwards.
-
Extra Credit: 3.3
-
- Read Chapter 1 Section 4
- Work the following exercises:
- 4.1
- Do all formulas involving union, intersection, and difference.
- If you’re proving set equality between two arbitrary sets A and B, you are always starting with the assumption that you have an arbitrary element x in A and trying to show that it gets into B.
- Reread the axiom of extensionality and explain why you are trying to prove that “if x is in A then x is in B” and “if x is in B then x is in A”.
- Extra credit: The symmetric difference formulas.
- 4.2a
- How do you prove a chain of “if and only if”? Investigate what it means to prove for arbitrary sentences A, B, and C: A iff B iff C.
- 4.2b
- 4.3
- Extra Credit: 4.4
- 4.1
- Work the following exercises:
Level 2. Set theoretic relations
This level uses Introduction to Set Theory by Hrbacek and Jech.
- The level of abstraction will start getting a bit higher as we progress. We’ll be defining objects to define other objects to define other objects. Check yourself and make sure you know what each term refers to and what each terms means as the abstraction progresses.
- Read Chapter 2 Section 1 “Ordered Pairs”
- Work the following exercises:
- 1.1
- Part of 1.2
- It’s enough to work out the proof of existence for (a, b). This is to review your axioms.
- 1.3
- Extra Credit: 1.6
- This is mainly interesting to state the equivalent theorem. This illustrates that set theory can represent the same concept in multiple ways. The proof of this equivalent theorem is tedious and unenlightening after going through Theorem 1.2.
- Work the following exercises:
- Read Chapter 2 Section 2 “Relations”
- Work the following exercises:
- 2.3 Parts: a, b, c, d
- 2.4 Parts: a, d
- 2.6
- Extra Credit: 2.1
- Further axiom review.
- Work the following exercises:
- Read Chapter 2 Section 3 “Functions”
- Pay special attention to:
- Definition 3.1
- Definition 3.3
- Definition 3.7
- A function that is one-to-one is also called injective, and a function that is onto is also called surjective. A function that is both is called a one-to-one correspondence or a bijection.
- Pay special attention to:
- Work the following exercises:
- 3.1
- 3.2
- 3.3
- 3.4a
- 3.5
- 3.6
- Extra credit:
- 3.10
- 3.11
Level 3. Equivalence relations and orderings
Resources: Introduction to Set Theory by Hrbacek and Jech
- Read Chapter 2 Section 4 “Equivalences and Partitions”
- Pay special attention to:
- Definition 4.1
- Definition 4.3
- Definition 4.6
- Theorem 4.10
- Work the following exercises:
- Prove Theorem 4.10.
- 4.1
- Not necessary to produce proofs for this one, play with the relations and see what you come up with.
- 4.2
- Pay special attention to:
- Read Chapter 2 Section 5 “Orderings”
- Pay special attention to:
- Definition 5.2
- Definition 5.5
- Work the following exercises:
- 5.1
- 5.3
- 5.5
- 5.7
- 5.12
- Extra Credit:
- 5.13
- 5.14
- Pay special attention to:
Level 4. Natural numbers and induction
Resources: Introduction to Set Theory by Hrbacek and Jech
-
Read Chapter 3 “Natural Numbers” Section 1 “Introduction to Natural Numbers”
- Work the following exercises:
- 1.1
- For the second half of 1.1, assume there is such a z and reason from there. Refer to Introduction to Mathematical Arguments Proof by Contradiction and/or Uniqueness proofs.
- 1.1
- Work the following exercises:
-
Read Chapter 3 Section 2 “Properties of Natural Numbers”
- Pay special attention to:
- The Induction Principle
- Work the following exercises:
- 2.1
- 2.2
- 2.3
- 2.4
- 2.6
- 2.7
- Extra Credit:
- 2.11
- 2.12
- 2.13
- Pay special attention to:
-
Read Chapter 3 Section 3 “The Recursion Theorem”
- Pay special attention to:
- The Recursion Theorem
- Work the following exercises:
- 3.1
- 3.2
- Extra Credit:
- 3.5
- 3.6
- Pay special attention to:
-
Read Chapter 3 Section 4 “Arithmetic of Natural Numbers”
- Pay special attention to:
- The Peano Axioms
- Work the following exercises:
- 4.1
- 4.2
- 4.3
- 4.4
- 4.5
- Extra Credit:
- 4.7
- 4.8
- Pay special attention to:
Level 5. Set theoretic recursion
Resources: Introduction to Set Theory by Hrbacek and Jech
- Read Chapter 3 Section 3 “The Recursion Theorem”
- Pay special attention to:
- The Recursion Theorem
- Work the following exercises:
- 3.1
- 3.2
- Extra Credit:
- 3.5
- 3.6
- Pay special attention to:
- Read Chapter 3 Section 4 “Arithmetic of Natural Numbers”
- Pay special attention to:
- The Peano Axioms
- Work the following exercises:
- 4.1
- 4.2
- 4.3
- 4.4
- 4.5
- Extra Credit:
- 4.7
- 4.8
- Pay special attention to:
Level 6. Operations, structures, isomorphism
Resources: Introduction to Set Theory by Hrbacek and Jech
- Read Chapter 3 Section 5 “Operations and Structures”
- Pay special attention to:
- Definition 5.6
- This is a more abstract notion of isomorphism. It is dependent not only on a bijection, but making sure that structural features are preserved (like relations or functions).
- Work the following exercises:
- 5.1
- 5.4
- 5.6
- 5.12
- Pay special attention to:
Level 7. Cardinality. Finite and countable sets
Resources: Introduction to Set Theory by Hrbacek and Jech
- Read Chapter 4 “Finite, Countable, and Uncountable Sets” Section 1 “Cardinality of Sets”
- Pay special attention to:
- Theorem 1.6 (Cantor-Bernstein)
- Work the following exercises:
- 1.1
- 1.2
- 1.5
- Extra Credit:
- 1.10
- 1.11
- 1.12
- Pay special attention to:
- Read Chapter 4 Section 2 “Finite Sets”
- Pay special attention to:
- Lemma 2.2
- This lemma is also known as the pigeonhole principle in combinatorics. In fact, most of this chapter is teaching you the basic counting methods of finite combinatorics, which is important in probabilities of events with finitely many outcomes.
- Lemma 2.2
- Work the following exercises:
- 2.1
- 2.2
- 2.3
- 2.5
- Pay special attention to:
- Read Chapter 4 Section 3 “Countable Sets”
- Pay special attention to:
- Corollary 3.6
- This gives you a vague idea of how “small” countable sets are compared to uncountable.
- Corollary 3.6
- Work the following exercises:
- 3.1
- 3.2
- 3.3
- Extra Credit:
- 3.5
- 3.6
- Pay special attention to:
Elective: Level 8. Linear orderings. Completeness. Uncountable sets
Resources: Introduction to Set Theory by Hrbacek and Jech
- Read Chapter 4 Section 4 “Linear Orderings”
- Work the following exercises:
- 4.1
- 4.3
- Work the following exercises:
- Read Chapter 4 Section 5 “Complete Linear Orderings”
- Pay special attention to:
- Theorem 1.3
- Definition 5.5
- Definition 5.6
- Work the following exercises:
- 5.1
- For a little review of proof by contradiction.
- 5.2
- Extra credit:
- 5.5
- 5.8
- 5.1
- Pay special attention to:
- Read Chapter 4 Section 6 “Uncountable Sets”
- Pay special attention to:
- Cantor’s Proof of Theorem 6.1
- Work the following exercises:
- 6.1
- Pay special attention to:
Elective: Level 9. Cardinal numbers
Resources: Introduction to Set Theory by Hrbacek and Jech
- Don’t get stuck in this level. Become familiar with these ideas and then move on. If you’re working in computation, countable sets are mostly what you worry about. It’s nice to be aware of these properties of cardinality to be more set theoretically well-rounded.
- Read Chapter 5 “Cardinal Numbers” Section 1 “Cardinal Arithmetic”
- Pay special attention to:
- Theorem 1.8 (Cantor’s Theorem)
- Theorem 1.9
- Don’t spend too much time on:
- The operations of cardinal arithmetic. Unlikely to be very important to you.
- Work the following exercises:
- 1.5
- 1.7
- Pay special attention to:
- Read Chapter 5 “Cardinal Numbers” Section 2 “The Cardinality of the Continuum”
Elective: Level 10. Ordinal numbers. Axiom of replacement. Transfinite induction and recursion
Resources: Introduction to Set Theory by Hrbacek and Jech
- Same as the previous level. Ordinal numbers won’t be terribly important except in some model theoretic cases. Don’t get bogged down, this is probably way more ordinal theory than you’ll need. Become familiar with the ideas, and then move on.
- Read Chapter 6 “Ordinal Numbers” Section 1 “Well-Ordered Sets”
- Work the following exercises:
- 1.4
- Work the following exercises:
- Read Chapter 6 Section 2 “Ordinal Numbers”
- Pay special attention to:
- Definition 2.2
- Work the following exercises:
- 2.1
- 2.2
- 2.3
- Pay special attention to:
- Read Chapter 6 Section 3 “The Axiom of Replacement”
- Work the following exercises:
- 3.1
- Work the following exercises:
- Read Chapter 6 Section 4 “Transfinite Induction and Recursion”
- Pay special attention to:
- 4.1 Transfinite Induction
- 4.5 Transfinite Recursion
- Pay special attention to:
- Neither section 5 or section 6 is likely to be useful to you. Read if you’re interested but don’t feel compelled to.
Elective: Level 11. Axiom of choice
Resources: Introduction to Set Theory by Hrbacek and Jech
- This level is for further mathematical enrichment. Anyone claiming to be skilled in set theory should be aware of the axiom of choice and it’s consequences. However, as with the last two levels, you only need familiarity. Don’t get stuck here. The next level will return to set theory that is more important to you.
- Read Chapter 8 “The Axiom of Choice” Section 1 “The Axiom of Choice and Its Equivalences”
- Optional Read Chapter 8 Section 2 “The Use of the Axiom of Choice in Mathematics”
Level 12. ZF(C) set theory
Resources: Introduction to Set Theory by Hrbacek and Jech
- We are again back to something that matters to AGI research: formal systems.
- Read Chapter 15 “The Axiomatic Set Theory” Section 1 “The Zermelo-Fraenkel Set Theory With Choice”
- Read Chapter 15 Section 2 “Consistency and Independence”
- The existence of independence results is part of the heart of the problem in building an AGI. How do we make a formal system capable of self-extension so as to cover as many problem domains as possible when we know our formal systems always have blind spots?
- Read Chapter 15 Section 3 “The Universe of Set Theory”
- This last section should give you an idea of what work is still being done in set theory, and that the field is far from closed. More generally, it shows that formal systems are in constant need of being tuned and pushed to their limits if we are to keep improving them.
Computability theory path
This path uses Computability and Logic (Fifth Edition) by Boolos, Burgess and Jeffrey. An instructor's manual is available, it has hints for many problems.
Level 1. Enumerability and diagonalization
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- Read Chapter 1 “Enumerability”
- Pay special attention to:
- Example 1.2
- Example 1.3
- Example 1.9
- Example 1.13
- Work the following exercises:
- Note that to demonstrate a set is enumerable is to describe a function (or list) that will eventually list any element of the set. This description must be precise enough that anyone who inspects your enumeration becomes convinced that every element will in fact be listed.
- 1.1
- 1.2
- 1.3
- 1.5
- Hint: Example 1.9
- Extra credit: 1.7
- Pay special attention to:
- Read Chapter 2 “Diagonalization”
- Diagonalization is a concept that will begin to pop up in a lot of places. In general, it sketches out the boundaries of what is logically possible. It’ll come up again, so start trying to wrap your head around it.
- Pay special attention to:
- Theorem 2.1 and how it is proved
- Work the following exercises:
- 2.1
- Hint: Refer to the proof of Theorem 2.1
- Another hint: Refer back to your solution of exercise 1.5
- Extra credit: 2.13
- 2.1
Level 2. Turing machines and the halting problem
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- Read Chapter 3 “Turing Machines”
- Work the following exercises:
- 3.1
- 3.2
- 3.3
- Extra Credit:
- 3.5
- Work the following exercises:
- Read Chapter 4 “Uncomputability” Section 1 “The Halting Problem”
- Optional Read Chapter 4 Section 2 “The Productivity Function”
- Work the following exercises:
- 4.1
- 4.2
- Extra Credit:
- 4.5
- Work the following exercises:
Level 3. Abacus computability
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- Read Chapter 5 “Abacus Computability”
- Work the following exercises:
- 5.1
- 5.2
- 5.4
- Extra Credit:
- 5.3
- 5.5
Level 4. Recursive functions
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- Read Chapter 6 “Recursive Functions”
- While reading this chapter and before the exercises:
- What is the difference between a primitive recursive function and a recursive function?
- Practice unpacking the formal recursion syntax with functions given in the text. Do the reverse; practice tracing the steps to write them in formal syntax.
- Work the following exercises:
- 6.1
- 6.3
- Extra Credit:
- 6.2
- 6.7
- While reading this chapter and before the exercises:
- Read Chapter 7 “Recursive Sets and Relations” Sections 1 and 2
- Optional Read Chapter 7 Section 3 “Further Examples”
- Work the following exercises:
- 7.1
- 7.3
- 7.5
- Extra Credit
- 7.9
- Work the following exercises:
Level 5. The equivalence of different notions of computability
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- Read Chapter 8 “Equivalent Definitions of Computability”
- This chapter’s main importance is in understanding the process of proving equivalence. Go through the proofs a couple time to ensure you are understanding. You don’t need to be able to reproduce them, but be able to follow.
- Extra Credit Exercise:
- 8.1
Level 6. First order logic
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- This level works out to be a review of first order logic and semantics. This also introduces you to a very important method of using proof by induction in logic.
- Read Chapter 9 “A Precis of First-Order Logic: Syntax”
- Work the following problems:
- 9.1
- 9.2
- 9.3
- 9.4
- Extra Credit:
- 9.6
- 9.7
- 9.8
- Work the following problems:
- Read Chapter 10 “A Precis of First-Order Logic: Semantics”
- Work the following problems:
- 10.1
- 10.2
- 10.3
- 10.4
- 10.7
- Extra Credit:
- 10.8
- 10.12
- 10.14
- Work the following problems:
Level 7. Undecidability of first order logic
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- Read Chapter 11 “The Undecidability of First-Order Logic”
- Work the following exercises:
- 11.1
- 11.2
- Extra Credit:
- 11.12
- 11.13
- Work the following exercises:
Level 8. Models, their existence. Proofs and completeness.
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- Read Chapter 12 “Models”
- Work the following exercises:
- 12.1
- 12.2
- 12.8
- 12.15
- Extra Credit:
- 12.6
- 12.9
- 12.19
- Work the following exercises:
- Read Chapter 13 “The Existence of Models”
- Familiarity with the ideas in this chapter is encouraged, but it is nonessential to spend a significant amount of time here.
- Read Chapter 14 “Proofs and Completeness”
- Work the following exercises:
- 14.1
- 14.2
- 14.3
- 14.5
- Extra Credit: 14.9
- Work the following exercises:
Level 9. Arithmetization. Representability of recursive functions
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- This level builds the machinery to construct the proofs to Godel’s Incompleteness Theorems.
- Read Chapter 15 “Arithmetization”
- Work the following exercises:
- 15.1
- 15.2
- 15.5
- Extra Credit:
- 15.9
- Work the following exercises:
- Read Chapter 16 “Representability of Recursive Functions”
- Section 16.4 is a must. It is worth knowing the comparison between the system presented in this book and what else you might see in the literature.
- Work the following exercises:
- 16.1
- 16.2
- 16.3
- 16.10
- 16.11
- Extra Credit:
- 16.8
- 16.9
- 16.21
Level 10. Indefinability, undecidability, incompleteness. The unprovability of consistency.
Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey
- The most important thing in the chapters of this level is to take the proofs slowly and understand them bit by bit.
- Read Chapter 17 “Indefinability, Undecidability, Incompleteness”
- Work the following exercises:
- 17.1
- Work the following exercises:
- Read Chapter 18 “The Unprovability of Consistency”
5 comments
Comments sorted by top scores.
comment by moridinamael · 2019-07-17T12:44:20.914Z · LW(p) · GW(p)
I'm going to burn some social capital on asking a stupid question, because it's something that's been bothering me for a long time. The question is, why do we think we know that it's necessary to understand a lot of mathematics to productively engage in FAI research?
My first line of skepticism can perhaps be communicated with a simplified analogy: It's 10,000 BC and two people are watching a handful of wild sheep grazing. The first person wonders out loud if it would be possible to somehow teach the sheep to be more docile.
The second person scoffs, and explains that they know everything there is to know about training animals, and it's not in the disposition of sheep to be docile. They go on to elaborate all the known strategies for training dogs, and how none of them can really change the underlying temperament of the animal.
The first person has observed that certain personality traits seem to pass on from parent to child and from dog to puppy. In a flash of insight they conceive of the idea of intentional breeding.
They cannot powerfully articulate this insight at the level of genetics or breeding rules. They don't even know for a fact that sheep can be bred to be more docile. But nonetheless, in a flash, in something like one second of cognitive experience they've gone from not-knowing to knowing this important secret.
End of analogy. The point being: it is obviously possible to have true insights without having the full descriptive apparatus needed to precisely articulate and/or prove the truth of the insight. In fact I have a suspicion that most true, important insight comes in the form of new understandings that are not well-expressed by existing paradigms, and eventually necessitate a new communication idiom to express the new insight. Einstein invented Einstein notation because not just because it's succinct, but because it visually rearranges the information to emphasize what's actually important in the new concept he was communicating and working with.
So maybe my steelman of "why learn all this math" is something like "because it gives you the language that will help you construct/adapt the new language which will be required to express the breakthrough insight." But that doesn't actually seem like it would be important in being able to come up with that insight in the first place.
I will admit I feel a note of anxiety at the thought that people are looking at this list of "prerequisites" and thinking, wow, I'm never going to be useful in thinking about FAI. Thinking that because they don't know what Cantor's Diagonalization is and don't have the resources in terms of time to learn, their brainpower can't be productively applied to the problem. Whereas, in contrast, I will be shocked if the key, breakthrough insight that makes FAI possible is something that requires understanding Cantor's Diagonalization to grasp. In fact, I will be shocked if the key, breakthrough insight can't be expressed almost completely in 2-5 sentences of jargon-free natural language.
I have spent a lot of words here trying to point at the reason for my uncertainty that "learn all of mathematics" is a prerequisite for FAI research, and my concerns with what I perceive to be the unproven assumption that the pathway to the solution necessarily lies in mastering all these existing techniques. It seems likely that there is an answer here that will make me feel dumb, but if there is, it's not one that I've seen articulated clearly despite being around for a while.
Replies from: gwern, rohinmshah↑ comment by gwern · 2019-07-18T00:36:05.160Z · LW(p) · GW(p)
As a historical fact, you certainly can invent selective breeding without knowing anything we would consider true: consider Robert Bakewell and the wildly wrong theories of heredity current when he invented line breeding and thus demonstrated that breeds could be created by artificial selection. (It's unclear what Bakewell and/or his father thought genetics was, but at least in practice, he seems to have acted similarly to modern breeding practices in selecting equally on mothers/fathers, taking careful measurements and taking into account offspring performance, preserving samples for long-term comparison, and improving the environment as much as possible to allow maximum potential to be reached.) More broadly, humans had no idea what they were doing when they were domesticated everything; if Richard Dawkins is to be trusted, it seems that the folk genetics belief was that traits are not inherited and everything regressed to an environmental mean, and so one might as well eat one's best plants/animals since it'll make no difference. And even more broadly, evolution has no idea what 'it' is doing for anything, of course.
The problem is, as Eliezer always pointed out, that selection is extremely slow and inefficient compared to design - the stupidest possible optimization process that'll still work within the lifetime of Earth - and comes with zero guarantees of any kind. Genetic drift might push harmful variants up, environmental fluctuations might extinguish lineages, reproductively fit changes which Goodhart the fitness function might spread, nothing stops a 'treacherous turn', evolved systems tend to have minimal modularity and are incomprehensible, evolution will tend to build in instrumental drives which are extremely dangerous if there is any alignment problem (which there will be), sexual selection can drive a species extinct, evolved replicators can be hijacked by replicators on higher levels like memetics, any effective AGI design process will need to learn inner optimizers/mesa-optimizers which will themselves be unpredictable and only weakly constrained by selection, and so on. If there's one thing that evolutionary computing teaches, it's that these are treacherous little buggers indeed (Lehman et al 2018). The optimization process gives you what you ask for, not what you wanted.
So, you probably can 'evolve' an AGI, given sufficient computing power. Indeed, considering how many things in DL or DRL right now take the form of 'we tried a whole bunch of things and X is what worked' (note that a lot of papers are misleading about how many things they tried, and tell little theoretical stories about why their final X worked, which are purely post hoc) and only much later do any theoreticians manage to explain why it (might) work, arguably that's how AI is proceeding right now. Things like doing population-based training for AlphaStar or NAS to invent EfficientNet are just conceding the obvious and replacing 'grad student descent' with gradient descent.
The problem is, we won't understand why they work, won't have any guarantees that they will be Friendly, and they almost certainly will have serious blindspots/flaws (like adversarial examples or AlphaGo's 'delusions' or how OA5/AlphaStar fell apart when they began losing despite playing apparently at pro level before). NNs don't know what they don't know, and neither do we.
Nor are these flaws easy to fix with just some more tinkering. Much like computer security, you can't simply patch your way around all the problems with software written in C (as several decades of endless CVEs has taught us); you need to throw it out and start with formal methods to make errors like buffer overflows impossible. Adversarial examples, for instance: I recall that one conference had something like 5 adversarial defenses, all defined heuristically without proof of efficacy, and all of them were broken between the time of submission and the actual conference. Or AlphaGo's delusions couldn't be fixed despite quite elaborate methods being used to produce Master (which at least had better ELO) until they switched to the rather different architecture of AlphaZero. Neither OA5 nor AlphaStar has been convincingly fixed that I know of, they simply got better to the point where human players couldn't exploit them without a lot of practice to find reproducible ways of triggering blindspots.
So, that's why you want all the math. So you can come up with provably Friendly architectures without hidden flaws which simply haven't been triggered yet.
Replies from: moridinamael, Pattern↑ comment by moridinamael · 2019-07-18T06:17:28.928Z · LW(p) · GW(p)
To be clear, I didn't mean to say that I think AGI should be evolved. The analogy to breeding was merely to point out that you can notice a basically correct trick for manipulating a complex system without being able to prove that the trick works a priori and without understanding the mechanism by which it works. You notice the regularity on the level of pure conceptual thought, something closer to philosophy than math. Then you prove it afterward. As far as I'm aware, this is indeed how most truly novel discoveries are made.
You've forced me to consider, though, that if you know all the math, you're probably going to be much better and faster at spotting those hidden flaws. It may not take great mathematical knowledge to come up with a new and useful insight, but it may indeed require math knowledge to prove that the insight is correct, or to prove that it only applies in some specific cases, or to show that, hey, it wasn't actually that great after all.
↑ comment by Pattern · 2019-07-18T05:44:21.528Z · LW(p) · GW(p)
The problem is, we won't understand why they work, won't have any guarantees that they will be Friendly, and they almost certainly will have serious blindspots/flaws (like adversarial examples or AlphaGo's 'delusions' or how OA5/AlphaStar fell apart when they began losing despite playing apparently at pro level before). NNs don't know what they don't know, and neither do we.
I hadn't heard about that. I suppose that's what happens when you don't watch all the videos of their play.
↑ comment by Rohin Shah (rohinmshah) · 2019-07-17T15:55:54.990Z · LW(p) · GW(p)
Fwiw I also think it is not necessary to know lots of areas of math for AI safety research. Note that I do in fact know a lot of areas of math relatively shallowly.
I do think it is important to be able to do mathematical reasoning, which I can roughly operationalize as getting to the postrigorous stage in at least one area of math.