Video
Unit video
The narrated video for Unit 18, about 24 minutes, is published with the first release.
Learning purpose: The closing unit. Where the observer stands when it checks something, why that question is older than AI, and how to sort claims by the evidence actually behind them.
Accessible text alternative: the transcript linked below, and this page, which covers the same material.
Transcript of the Unit 18 video
The narration is spoken by synthetic voices made for this course, each shown on screen as a drawn robot. No person is speaking.
The course's closing unit, the last on the complete route. No new practical work: it names the question the earlier units kept running into, says where that question comes from, and closes off the three overclaims easiest to reach from it. Units 0 to 8 make complete sense without it.
Reading time: about 26 minutes. Activity: about 12 minutes.
Checkpoint: cp18-sort-the-claims.
Before this unit: Unit 17 (disclosure, defence, and the evidence pack).
No prior study of logic or cybernetics is assumed. Every specialist term needed for the activity is defined below; the optional further reading carries the advanced detail.
What this unit does, and what it does not do
This unit covers established, published material: a distinction from cybernetics, where it came from, and classical theorems about self-reference. What is the course's own is labelled where it appears: section 3's working account of understanding, which is not a published result, and its readings, which are said to be readings. Its job is to raise the issue and say what "second order" means. It proves nothing about language models and teaches no unpublished research as settled. That restriction is deliberate: the earlier units have repeatedly trained you to ask what supports a claim, and a closing unit that quietly imported an unsettled framework would fail its own test in front of you.
Bracket labels — [C1], [C4], and so on — resolve to References and source policy, and Second-Order Reasoning: The Lens Behind The Course carries what this page leaves out — the structural account of understanding, and the constraints the unit is written under.
The title, and the movement behind it
The unit is called Alles Lüge! — "all lies!". That is the first step of a movement, not its conclusion, and the page walks all three steps.
- Everything sounds like a lie. If every record was made by some observer, from inside the system, nothing arrives already certified, and the short way to read that is: trust none of it. Lacrimosa's line, quoted in section 5, is that position at full volume [Q1].
- The standpoint above is gone. Harder, and more accurate. The trouble is not that everyone is lying; it is that there is no outside position from which a claim could be settled once and for all. "Gott hat sich erschossen / ein Dachgeschoss wird ausgebaut" — God has shot himself; a loft is being converted (Einstürzende Neubauten, "Haus der Lüge") [Q3]. Both halves of that matter: no architect, and the building work carrying on regardless. In this reading, the god stands for an observer outside, who could see the whole house and settle every claim made in it: that standpoint is gone. The loft stands for the work that goes on anyway, from inside, floor by floor, with no plan handed down from outside. A religious account disagrees about the god. Pope Leo XIV's encyclical Magnifica Humanitas (2026) warns against the idea that a "language — even a digital one — can translate everything, including the mystery of the person, into data and performance", says "A person's future is not calculable", and places what exceeds us in God [T25, pars. 10, 127-128]. The encyclical does not speak of standpoints. On this course's reading, it keeps an outside, as a mystery; but that is still not a place anyone inside can stand to settle a claim. The course takes no side between the two. Either way, the shape of the rest of the unit is the same: no guarantee from outside, and building regardless. Sections 2 and 4 are a related step in published form — the observer is inside the system it describes, and, for a formal language such as arithmetic, truth cannot be defined from inside that language. Related, not the same: section 4 says why the theorem does not carry over by itself.
- What is left is a method, and you have used it since Unit 8. Warrant, the grounds for trusting a claim, does not come down from above; it is built locally. Section 5 is that step.
Despair, then the missing god's-eye view, then acceptance — practical rather than consoling. If you take one step of the three from the title, take the third.
1. What you have already done
Five things, all done with your hands before you met any of the language here.
- B4 derived from the recurrence on paper, before you saw any generated code.
- The checker reporting
b1-signrather than "wrong". - Two valid Bernoulli conventions disagreeing at B1 and nowhere else, because neither program had said which one it used.
- Ada's B7 and the modern B7: one label, two different terms.
- A disclosure and a defence, written separately.
Section 3 says how each of those reads in this unit's vocabulary. Underneath all five is one question: where is the observer standing? When you check something, are you outside the system you are checking, or part of it? That question did not begin with artificial intelligence, and it has a substantial published literature going back to the 1940s ([C1] to [C5]). The rest of this page is what that literature calls it.
In the plain language used here:
- the observer is the person or system making a claim or carrying out a check;
- the context is the convention, specification, setting, and limits under which the claim is made; and
- the record is the retained evidence of what was observed or checked.
These three details make a claim easier to evaluate. They say who did what, under which conditions, and where the evidence can be inspected.
2. First order and second order
Cybernetics is the study of control and communication in the animal and the machine, as the title of a 1948 book put it [C9]. The Macy Conferences (below), whose title later became "Cybernetics", met on "circular causal and feedback mechanisms" [C4, "7th Conference"]: how a system steers itself by feedback, comparing what it does with what it aims at and correcting, as a thermostat does with a room's temperature. They deliberately mixed mathematicians, engineers, neurophysiologists, anthropologists and psychiatrists [C4].
The distinction this unit uses comes from cybernetics and is usually put like this.
- First-order cybernetics — the cybernetics of observed systems, systems watched from outside. The observer stands outside, describing a system without being part of it.
- Second-order cybernetics — the cybernetics of observing systems, systems that include the one watching. The observer is included in the system being described.
Heinz von Foerster formulated the distinction in those terms [C1, p. 303]. Margaret Mead's address "Cybernetics of Cybernetics", published in 1968, is commonly cited as the point where the reflexive turn was named [C2].
The consequence is small to state and large in effect. An observer inside the system is not taking a free look from nowhere: observing takes time, costs something, and can change what is observed. On this view a claim carries an index, a label saying who observed, in what context, with what record. Maturana's compact version: anything said is said by an observer [C3, p. 8].
The diagram indexes the claim by observer, context, record, and effects. These details make it possible for someone else to decide what can be checked.
A note on precision, since this unit is about exactly that. This line is very often quoted as everything said is said by an observer. It is not: page 8 of [C3] reads anything. The everything form is the title of a later Maturana essay (the 1987 piece in Thompson's Gaia: A Way of Knowing; see the note under [C3] in References and source policy), and it has propagated by repetition into places that cite the 1980 book for the wording it does not contain.
Two notes on the vocabulary, because both catch people out.
- This is not the first-order/second-order distinction in logic. The same words name different contrasts in different fields; this page means the cybernetic one.
- Including the observer makes a claim more checkable, not less: an indexed claim says what would have to be compared with what. Naming the Bernoulli convention turned an unresolvable disagreement into a resolved one.
Where it comes from
The Macy Conferences on Cybernetics were ten meetings held between 1946 and 1953, organised by the Josiah Macy Jr. Foundation, which published their transactions, and chaired by Warren McCulloch [C4, "Part 1"]. Their mixed disciplines and the later development of the reflexive question are described in the optional further-context section.
Second-order cybernetics is a recognised research tradition with a literature, not a fringe or recent position. It is also a tradition rather than a theorem — a category, not a criticism. A research programme can be decades old, published and influential while remaining a way of framing problems rather than something anyone proved. Telling those apart is the exercise at the end of this unit.
Keep two kinds of claim separate. Second-order cybernetics supplies an interpretive lens: a published way to frame observer-dependent problems. The logic results in section 4 are proved theorems within stated formal conditions. The lens does not follow from the theorems, and the theorems do not prove the course's interpretation.
3. The mapping, and what it is not
Adapted from Second-Order Reasoning: The Lens Behind The Course §3. The left column is what you did; the right is a reading of it.
A reading, not a proof. None of it is a deduction from the theorems in section 4. Reject the whole second-order framing and you still have a working oracle, a checker, and a correct routine.
| What the course does concretely | The second-order reading |
|---|---|
| An AI's statement that its Bernoulli routine is right is not independent evidence; the oracle is. | The check has to come from somewhere the system being checked does not control. An observing system observing itself is the hard case. |
B1 = -1/2 and B1 = +1/2 are both correct and they disagree. |
The claim was incomplete without its context. Supply the index — which convention — and the disagreement dissolves. |
| Ada's B7 and the modern B7 are different numbers under the same symbol. | Two observers, two contexts, one symbol. Not an arithmetic error by either. |
| The oracle is trustworthy because it is exact, external, and independently checked against published values. | Agreement between independent records, rather than access to a view from nowhere. |
The checker names b1-sign or ada-indexing instead of reporting "wrong". |
Which kind of disagreement this is determines what to do about it. |
| Note G's operation-4 inversion is established; its attribution is contested; and "what the faulty table computes" has as many answers as there are readings of it. | Saying which part is which — and which object a claim is about — is itself part of the claim. |
| Disclosure says how it was made; defence says why it is right. | Provenance and warrant are different things, and neither substitutes for the other. |
One working account of understanding, not a settled definition. This account is the course's own, stated for use here; it is not a published result. On it, your internal model supports understanding when its parts, relationships, and predictions continue to correspond reliably with the target under relevant checks. The lab gathers evidence for that correspondence when you predict, before a check runs, what it will show about the routine: agreement at a value, a property holding, or the first place two records diverge. A pass you did not predict is evidence about the code, not about your model of it.
Understanding in this sense is separate from the target's correctness, whether the target is actually right. You can model a wrong table accurately: you then understand what the table says without making the table right. And you still have to say which table you mean, as this course's makers failed to do with one faulty reading of Note G's table. A defence therefore needs evidence both that your model corresponds to its target and that the target is appropriate and correct for the claim you are making.
Other accounts emphasise causes and counterfactuals: understanding includes being
able to say what would happen after an intervention, or what would change under a
different condition. These are alternatives and useful additions, not positions
this short course settles. Second-Order Reasoning: The Lens Behind The Course gives the optional formal
structural statement (f : M1 → M2) and its limits. The practical rule remains:
pause when you can no longer understand and defend what is being produced. In
operational terms, pause if you cannot predict relevant behaviour, explain the
transformation, name an independent check, or interpret a failed check.
Confidence does not count as a fifth test.
Where the system ends. Unit 17 sets out Searle's Chinese Room and the systems reply to it. Part of that dispute is about where "the system" ends: the man alone, the man with his program and his paper, or the program running in his head. Searle holds that once the man memorises the program there is no system beyond him; critics hold that what runs in his head may be a second system [T21, sec. 4.1]. Read with this unit's lens, that is a disagreement about the boundary of the thing a claim is about; the lens does not decide it. The same question arises for claims about language models. "The model" may mean a set of trained weights, the weights with the text they were prompted with, or a deployed product with its tools, filters and the people who review its output. A claim about what "the model" understands, knows or can do can be checked, where it can be at all, only once it says which of these it is about, which is the indexing this unit asks for: a claim stated with its observer and its context. It does not settle Searle's question; it makes clear which question is being asked.
4. The classical results on self-reference
Three plain definitions come first:
- A formal system uses explicit symbols, starting assumptions, and rules for deriving one statement from others.
- A theorem is a statement established by proof under stated rules and assumptions.
- A truth predicate is an expression inside a language that would classify sentences of that language as true or not true.
Two established theorems are the rigorous core of "a system cannot fully account for itself from inside", and their limits matter as much as their content.
- Gödel's first incompleteness theorem (1931). Take a formal system with three properties. It is consistent: it never proves both a statement and its negation. It is effectively axiomatised: its axioms, its starting assumptions, can be listed by a procedure. And it can prove a basic stock of elementary arithmetic. Then it contains a sentence it can neither prove nor refute. This is the form usually stated today. Gödel's own proof [C6, pp. 187-189] of the "nor refute" half assumed a stronger condition, omega-consistency. Roughly, that means the system never proves that some number has a property while also proving, of each number in turn, that it lacks it. Rosser removed that condition in 1936 [C8, p. 87] [T24, secs. 2.1, 2.5].
- Tarski's undefinability theorem (Polish 1933; German text 1935 or 1936, the year disputed): truth for the language of arithmetic — which of its sentences are true of the natural numbers — cannot be defined by any formula of that same language [C7].
The same 1931 paper also states Gödel's second incompleteness theorem: a consistent, effectively axiomatised system that can carry out a little more arithmetic cannot prove its own consistency [C6, p. 196] [T24, sec. 1.1]. It is a result about what the system can derive from its own axioms. It does not say that the system's consistency cannot be shown by other means, and for many such systems it can [T24, sec. 1.1].
Those qualifications are not decoration, and this unit would be doing the thing it warns against if it dropped them. The theorem depends on "consistent" and "effectively axiomatised". Remove the second and the theorem is false. Take the set of all true sentences of arithmetic. It is consistent. It is also complete: for every sentence, it contains either that sentence or its negation, so nothing is left undecided. But no procedure can list it [T24]. The popular one-line versions omit exactly these conditions, which is what makes them so easy to carry somewhere they do not go.
The usual gloss adds that the unprovable sentence is true. That is a further step: it holds under the intended reading of the symbols, and saying so means saying which interpretation you mean. Provability is a property of the system. Truth depends on an interpretation: a way of reading the symbols under which the axioms are true. Logicians call such an interpretation a model, a different sense of the word from "language model".
What they do not say
This subsection matters more than the two lines above it, so read it slowly.
Both are mathematical results about formal systems of a specific kind: abstract entities with explicit symbols and deductive rules. A language model, however, is not a formal theory; it is a physical system — software running on hardware — studied empirically.
Applying a theorem about a formal, mathematical system directly to a physical, empirical one, with no argument that its conditions hold there, proves nothing: the conclusion has not been shown, whether or not it is true. They do not straightforwardly transfer to language models, to institutions, or to people, and this unit does not claim they do. Their role here is to establish that limits on self-reference are real and provable somewhere in logic — much weaker, and much safer, than asserting a mathematical limit on a particular piece of physical AI software.
A claim that Gödel settles something about machine intelligence is missing its middle. Not because software and formal systems are unrelated — a computer can implement a formal system, and results about formal systems can bear on computation, which is how computability theory works at all. The gap is specific: to carry the theorem across you have to say which component you are treating as a formal theory, show that the theorem's conditions actually hold of it, and argue that what follows for the formal object also follows for the running system. Each of those is a real step and each can fail.
So the fault is not the analogy. It is asserting the conclusion without the argument, and the conclusion may well be true for other reasons. Noticing that missing middle — in a paragraph that is fluent, confident, and cites a real theorem correctly — is the skill this course teaches.
One proved limit does concern programs. Turing proved an undecidability result about his machines in 1936-7 [T10, sec. 8], and the halting problem as now stated is a close variant of it, undecidable too [T12, sec. 2.4.3]: no program can decide, for every program and input, whether that program halts. To decide means always to give the correct yes or no; to halt means to stop, rather than run for ever. Rice's theorem (1953) [T11, pp. 364-365] generalises the point: every non-trivial property of what a program computes is undecidable [T13, sec. 3.2]. Non-trivial means that some programs have the property and some do not. Both rule out a general procedure that settles such a question for all programs at once. Neither rules out checking one program against one specification over a stated range, which is what the checker did in Unit 8. And neither settles what a particular AI system can or cannot verify: that still needs the missing middle.
The middle, for a guarantee. The missing middle is needed for guarantees as much as for limits. A proof assistant can show that a theorem holds for a formal model: definitions of a system, of an attacker, of success. Whether it holds for the system itself needs the model to be faithful and its assumptions to hold there -- the middle's second step, the conditions shown to hold. One 2026 preprint reports a security theorem, checked in Lean, for a model that assumes, as the paper states, an authenticated channel between the parties [L18, sec. IV.A]. Whether any system meets that assumption is outside the proof, and the result is only as strong as that assumption is where it is used. The same preprint describes gaps of the same kind between results: security proofs in its field can contain gaps between individually valid theorems combined under assumptions that do not match [L18, abstract]. Formalising also made explicit conditions that two cited results relied on without stating; the formal statements assume or add them [L18, sec. VI]. A chain of correct steps is only as good as the agreement of the conditions where they meet.
What is known about the middle for a language model
Some of the middle can be filled in, and some cannot yet.
- A trained model runs as a program, or inside one. Its weights, the numbers fixed during training, are applied by ordinary code with finite-precision arithmetic. Turing's and Rice's results limit any procedure meant to work for all programs [T12, sec. 2.4.3] [T13, sec. 3.2]. Whether they limit a procedure meant only for trained models depends on the class those models form: their precision, how much text they take in at once, the loop that produces an answer step by step, and any tools attached. The last point in this list shows how much that matters. None of it says anything about checking one model on one task.
- It is not a formal theory. It has no proof rules and no requirement of consistency: it can produce a claim and, on another run, its negation. Gödel's result needs a consistent, effectively axiomatised formal theory that proves enough arithmetic [C6, pp. 190-191]; Tarski's concerns defining truth inside a formal language that can express arithmetic [C7]. Nobody has shown that a given model formalises either, so the conditions are not shown to hold for the model as such.
- What it can compute depends on the assumptions. Take the transformer architecture in an idealised form, with hard attention: each step looks only at the best-matching positions of the input, rather than a weighted mix of all of them. In that form it has been proved Turing complete: able, given unlimited time and memory, to compute anything a general-purpose computer can [L15, Theorem 6]. Now take logarithmic numerical precision: numbers kept to a precision that grows only very slowly with the length of the input. In that form it has been shown to be far weaker, unable even to solve linear equalities accurately, if L is not P [L16, p. 531]. "L is not P" is a standard, unproved conjecture in complexity theory. Roughly, it says that some problems a computer can solve in reasonable time need more than a tiny amount of working memory. Which of these, if either, describes a deployed system is itself a question about its implementation.
So the honest position is a few proved limits whose reach depends on the class a model is placed in, a long list of what is not shown about any one system, and experiments for the rest.
First order, mostly
"Ohne nur ein Sehnen werd' ich warten" (Lacrimosa, "Alles Lüge") [Q1]: without a single longing I will wait. One way to read that line here: a language model produces nothing until it receives a prompt. In this unit's terms it works mostly at first order. That is a reading, not a result, and it rests on what is documented:
- Its output describes things from outside. Do not assume the answer records the standpoint it was produced from (its training, its cut-off, the prompt that framed it); ask for that account, and check what you can.
- In ordinary use a trained model's weights stay fixed while you use it; it does not learn by observing you, though one provider documents, as of November 2026, a memory that carries text into later conversations [D2, "How Claude stores memory"].
- When it describes itself, that description is more output: a 2023 study found that a displayed explanation need not reflect what drove the answer [L9, sec. 3.2].
- Without feedback from outside, asking a model to correct its answers on reasoning tasks was found in a 2024 study to help little, and sometimes to make them worse [L17, sec. 3.2].
So the second-order work, stating where a claim comes from and comparing it with something independent, is done by the person, or by a system someone designs with the check outside the model (Unit 11). The model can be part of such a loop; including the observer is part of the design, not part of the model.
5. What this does not license
Three overclaims are easy to reach from here. This unit closes each one off.
"Nothing can be known" — overclaim
The move is from a guarantee to a method: state your context, keep records, compare independent ones. The course is its own counterexample. You finished Unit 8 with evidence that your routine agreed with the oracle over the tested indices and satisfied the checked properties under a stated convention. That scoped conclusion is stronger than felt certainty because it states its limits. The course itself was made by that method rather than exempted from it: AI-assisted, narrated by synthetic voices, and held to checks you can rerun: the oracle against published values, the accessibility script, the reference list with its locators. Its AI-use disclosure, recorded once at course level, tells you how it was made, and you cannot confirm it from the course itself; the checks are what let you trust the course without taking it on faith.
The diagram refuses the absolute claim and replaces it with a method: state the context, keep records, compare independently, and report the limits.
"Und doch ich hör' nur Lügen" — and yet I hear only lies — (Lacrimosa, "Alles Lüge") [Q1]. That is step one of the movement above, and it is the position this section refuses. Total distrust is not scepticism but a way of stopping checking: someone who doubts everything cannot decide where to spend the effort.
"Therefore AI cannot be trusted at all" — overclaim
The observer question applies with equal force to human reasoners, to the oracle, to peer review, and to the published Note G table, which contained an error made by people. On this course's reading, human work always had this problem, and what AI adds is speed and volume. Nothing here establishes how often a language model is right or wrong. The response lies in how checking is designed, not in an attitude: put the check outside the thing being checked, index the claim, say what kind of support you have. The record goes to the author, who signs the claim and answers for its limits.
"Gödel and Tarski prove that AI cannot verify itself" — overclaim
They do not; see section 4. This is the most interesting of the three, because both halves are true and the link between them is not shown: real theorems, real systems, and an unstated argument between them. That shape reads extremely well, and it is exactly what Unit 7 trained you to catch.
The overclaim leans hardest on Gödel's second theorem: a consistent, effectively axiomatised system strong enough for arithmetic cannot prove its own consistency [C6, p. 196] [T24, sec. 1.1]. That is a limit on a formal system deriving one statement about itself from its own axioms. Checking a language model's output against an independent reference, such as the oracle, is a different act: the model has no axioms, and the check comes from outside it. The theorem says nothing about it.
What is left once the god's-eye view goes
Step three, and where the movement the title opens actually ends. Look under the system for the bedrock and there is none: "It is as black as Malevich's Square" (Einstürzende Neubauten, "Sabrina") [Q2] — a square you can stare into, holding nothing. The work goes on anyway, in the same house, on the same floor.

Kazimir Malevich, Black Square, 1915, Tretyakov Gallery, Moscow (public domain; image from Wikimedia Commons, which credits the Tretyakov Gallery).
Warrant is built from below, out of the three details section 1 named — observer, context, record — plus the agreement of records produced independently of each other. That is what the oracle gave you in Unit 8, and what naming the Bernoulli convention did to an unresolvable disagreement. Less than certainty, and checkable: the trade this course has been making throughout.
"It's not the red of which we bleed" (Einstürzende Neubauten, "Sabrina") [Q2]. This page borrows the line for a convention of the course's own: the red accent in these materials marks what is wrong (a divergence, an error, a failed check), never authority, and never travels without a word beside it. On this unit's slides it marks the first place where two independent records disagree, as in Unit 8's comparison with the oracle: where to look, not who is right. That is why it is not the red of which we bleed. A divergence is information to act on, not an injury and not an alarm. Warrant is assembled the same way: locally, from records you can point at, by someone who can be named.
6. Further context (optional)
Nothing in this section is required for the activity or checkpoint.
People and disciplines around the Macy Conferences
Participants came from mathematics, engineering, neurophysiology, anthropology, and psychiatry. They included Norbert Wiener, John von Neumann, Claude Shannon, Gregory Bateson, Margaret Mead, and Heinz von Foerster [C4, "Part 1"]. The reflexive question was developed afterwards by von Foerster and the Biological Computer Laboratory [C1], Bateson [C5], and Maturana and Varela [C3].
For the complete bibliography, use References and source policy: [C1] to [C5] and [C9] cover second-order cybernetics and its history; [C6], [C7] and [C8] cover Gödel, Tarski and Rosser, and [T24] is a survey of both incompleteness theorems; [T10] to [T13] cover Turing's result, Rice's theorem and the halting problem. Second-Order Reasoning: The Lens Behind The Course holds the structural account and the design constraints.
The register, and the rule that governs it
This is the only unit that uses the course's gothic register at full strength, including three short song quotations. It is a deliberate choice with a justification, not decoration: Ada Lovelace was Byron's daughter [G1, p. 553], and the 1816 Villa Diodati gathering is where the ghost-story challenge associated with Frankenstein [G3] and Polidori's The Vampyre [G4] is conventionally dated [G2, pp. 125-126]. The connection is thematic; no claim is made that this literature influenced Lovelace's work.
Notice what those citations carry. [G2] is honest that the nearest thing to a primary account is Mary Shelley's own introduction to the 1831 edition, and still records the date of the ghost-story challenge as contested — a range, not a night. So: connection supported, dating conventional rather than documented to the day, influence claim not made.
The three songs mark the three steps at the top of this page: [Q1] the despair, [Q3] the missing standpoint, [Q2] what is left. Take all three out and the argument is unchanged, which is the test they had to pass. Each quotation is short, attributed, and used for commentary; entries and rights position are in References and source policy.
The one rule. The register may carry the argument and may never substitute for it. Every claim on an atmospheric slide still carries its citation or its uncertainty label. If a sentence in this unit sounds good and cites nothing, it is a defect, and you are entitled to say so.
7. What you can now do
- Say what the first-order/second-order distinction is, and where it came from.
- Name three things you did in this course that the second-order reading illuminates, while saying plainly that illumination is not proof.
- State Gödel's and Tarski's results within their actual scope, and say why neither settles anything about a language model on its own.
- Tell a proved theorem from an established research programme from an overclaim, when all three appear on the same well-written page.
- Look back at the sentence you wrote in Unit 0, the one thing you would verify rather than trust: say which part of it your defence now supports, and what you would change in it. The activity's last step asks for exactly that.
Checkpoint
Work through the activity first: the checkpoint asks you to sort claims made by this unit, and it is a different exercise once you have sorted some yourself. It is the last thing the course asks of you.
From The verification lab and self-check:
python3 selfcheck.py run cp18-sort-the-claims # or in the browser
Both routes ask the same question and give the same diagnostics.
Where to look next
- Second-Order Reasoning: The Lens Behind The Course — the fuller treatment this unit summarises.
- References and source policy — full entries for [C1] to [C9] and [T10] to [T13], the gothic-context entries, the three song quotations, and the source policy.
Timings: video 24 min, reading 26 min, activity 12 min.
Check yourself
This unit has one checkpoint, answered here. A wrong answer says which misunderstanding it matches. Nothing is uploaded.
Local progress is available in a supported browser.
Prefer a terminal?
The same questions, from The verification lab and self-check:
python3 selfcheck.py run --unit 18