The words spoken in the Unit 18 video, scene by scene, as its captions show them, with what the animations show marked [On screen: ...] where they play. Each speaker is named where the speaker changes. The Unit 18 reading covers the same material.
The narration is spoken by synthetic voices made for this course, each shown on screen as a drawn robot. No person is speaking.
Unit 18 — Alles Lüge! First- and second-order reasoning
Narrator: This is the last unit. It adds no new practical work. It names a question the rest of the course kept running into. No prior logic or cybernetics is assumed. The title, all lies, is the first of three steps, not the conclusion. First, everything sounds like a lie. Then it turns out there is no standpoint above it all, from which anyone could settle a claim. Then we build the grounds for trusting claims from below anyway. This unit calls those grounds warrant.
You already did this
Start with what you actually did. You worked out B-four from the recurrence, on paper, before you looked at any generated code. You watched the checker report b1-sign rather than "wrong". You saw two valid conventions disagree at B-one, because neither program had said which convention it used. You met Ada's B-seven and the modern B-seven: one label for two different terms. And you wrote two separate statements: how it was made, and why it is right. Five things. One question underneath them.
Three details that make a claim checkable
Three plain details will matter. The observer is who made the claim or ran the check. The context is the convention, specification, setting, and limits. The record is retained evidence another person can inspect.
One question underneath
Where is the observer standing? When you check something, are you outside the system you are checking, or part of it? That question is not new, it did not begin with artificial intelligence, and it has a substantial published literature going back to the 1940s.
First order and second order
First, what cybernetics is. It is the study of control and communication in the animal and the machine, as the title of a book of nineteen forty-eight put it. The Macy Conferences, whose title later became Cybernetics, met on circular causal and feedback mechanisms: how a system steers itself by comparing what it does with what it aims at and correcting, as a thermostat does with a room. Within cybernetics, two positions have names. First-order cybernetics is the cybernetics of observed systems: systems watched from outside. The observer stands outside and describes a system without being part of it. Second-order cybernetics is 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. Margaret Mead's address "Cybernetics of Cybernetics", published in 1968, is commonly cited as the point where the reflexive turn, cybernetics applied to cybernetics itself, was named. This is not the first-order and second-order distinction in logic; the same words name a different contrast there.
What follows from including the observer
[On screen: Headed 'An observation is an event in the system', four questions, each with its answer: at what cost or change, time, resources, intervention; who observed, observer or instrument; in what context, state conditions and convention; with what record, keep inputs, outputs and checks. Lines from all four lead into a green panel headed 'Scoped claim': Routine R agreed with oracle O for tested indices 0-30, using convention C, as recorded in evidence file E. Below it: the index makes the claim more checkable.]
The consequence is small to state and large in effect. If the observer is inside, observation is an event in the system rather than a free look from nowhere: it takes time, it costs something, and it can change what is observed. On this view a claim carries an index, a label saying who observed, in what context, with what record. Humberto Maturana's formulation is the compact one: anything said is said by an observer. Anything, not everything. The line is often quoted as "everything said". That wording is the title of a later Maturana essay, and it has spread by repetition into citations of a book that does not contain it. An indexed claim is more checkable, not less: it says what would have to be compared with what.
No view from nowhere
The trouble is not that everyone is lying. It is that the standpoint outside the system, the one a claim could be settled from once and for all, is not available to anyone inside it. "Gott hat sich erschossen; ein Dachgeschoss wird ausgebaut". God has shot himself, and a loft is being converted. The line is from Einstürzende Neubauten, "Haus der Lüge". 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. That is the shape of the rest of this unit. A religious account disagrees about the god, and is worth setting beside the song. In the encyclical Magnifica Humanitas, of twenty twenty-six, Pope Leo the Fourteenth warns against the idea that any language, even a digital one, can translate everything, including the mystery of the person, into data and performance. He writes that a person's future is not calculable, and he places what exceeds us in God. On this course's reading, that keeps an outside, as a mystery. But it is still not a place anyone inside can stand to settle a claim. The course takes no side between the two.
Where it comes from — the Macy Conferences
Where did this vocabulary come from? The Macy Conferences on Cybernetics, met earlier, were a series of ten meetings held between 1946 and 1953, organised by the Josiah Macy Jr. Foundation and chaired by Warren McCulloch.
A tradition, not a theorem
The reflexive turn was named later, and developed afterwards: by von Foerster, by Bateson, and by Maturana and Varela. This is a recognised research tradition with a literature, not a fringe position and not a recent one. It is also a tradition rather than a theorem. A research programme can be decades old, published and influential while remaining a way of framing problems rather than something anyone proved. That is a category, not a criticism.
What you did → how it reads (1 of 2)
Everything on the left is something you did. Everything on the right is a reading in this vocabulary. The oracle gave independent evidence about your routine; the routine's own claim could not. The check came from somewhere the routine did not control. The convention was a missing index, and supplying it dissolved the disagreement.
What you did → how it reads (2 of 2)
Ada's B-seven and the modern B-seven are two observers, two contexts, one symbol. It is not an arithmetic error by either. And when the checker reports b1-sign rather than "wrong", which kind of disagreement this is determines what to do about it. None of that is a proof and this unit does not offer it as one. The concrete lessons stand on their own. Reject the whole framing and you still have a working oracle, a checker, and a correct routine.
Understanding, and where the system ends
One working account of understanding runs through the course. Your model of something supports understanding when it keeps corresponding to its target under relevant checks. It is a working account, not a settled definition: other accounts stress causes and counterfactuals, what would happen after an intervention or under a different condition, and the course does not choose between them. As in Unit 17, the checks are evidence of your understanding only where you predicted their outcome before they ran. And understanding is separate from correctness: you can map a wrong table well, and you still have to say which table you mean. And a claim has to say where the system it is about ends. In Searle's Chinese Room: the man alone, the man with his program, or the program running in his head. Searle holds that once the man memorises the program there is nothing beyond him; his critics hold that what runs in his head may be a second system. For a language model: the trained weights, the weights with a prompt, or a deployed product with its tools, filters and the people who review its output. A claim about what "the model" can do is checkable, where it is at all, only once it says which; that is the indexing this unit asks for. It does not settle Searle's question, but it makes clear which question a claim asks.
Three formal terms
Before the two logic results, three definitions. A formal system uses explicit symbols, assumptions, and derivation rules. A theorem is a statement established by proof under stated rules. A truth predicate is an expression inside a language that classifies sentences of that language as true or not true.
Two classical results
Two established theorems are worth naming. Gödel's first incompleteness theorem dates from nineteen thirty-one. Here it is in the form Rosser strengthened in nineteen thirty-six, so that plain consistency is enough. 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 the system contains a sentence it can neither prove nor refute.
Questioner: Do the conditions really matter that much?
Narrator: Yes. This unit would be doing the thing it warns against if it dropped them. Take away "effectively axiomatised" and the theorem is simply false. Here is why. Take the set of all true sentences of arithmetic. It is consistent. It is also complete: for every sentence, it holds either that sentence or its negation, so nothing is left undecided. But no procedure can list it. Tarski's undefinability theorem was first published in Polish in nineteen thirty-three. The year of the German text, nineteen thirty-five or thirty-six, is disputed. The theorem says that truth for the language of arithmetic cannot be defined by any formula of that same language. Truth here means which of its sentences are true of the natural numbers. Back to Gödel. The same nineteen thirty-one paper has a second theorem. Such a system, if it can carry out a little more arithmetic, cannot prove its own consistency. That limits what the system can derive from its own axioms. It does not say its consistency cannot be shown by other means.
What they do not say
Questioner: So do these theorems apply to language models?
Narrator: Now the part that matters more. Both are mathematical results about formal systems of a specific kind: abstract entities with explicit symbols and deductive rules. A language model is not a formal theory. It is a physical system, software running on hardware, studied by physics, engineering and experiment. Applying a theorem about a formal system directly to a physical system, with no argument that its conditions hold there, proves nothing. The conclusion has not been shown, whether or not it is true. These theorems do not straightforwardly transfer to language models. Their job here is to establish that limits on self-reference, on what a system can establish about itself, are real and provable somewhere in logic. That is a much weaker and much safer claim than asserting a mathematical limit on a particular piece of physical AI software.
The missing middle
[On screen: Headed 'A theorem does not transfer itself'. On the left, a panel headed Formal results: Gödel, consistent, effectively axiomatised, enough arithmetic; Tarski, truth for the language not definable in that language; explicit symbols and rules. On the right, a panel headed Running language-model system: software on hardware, statistical outputs, observed experimentally. A dashed arc leaps straight from the left panel to the right one; it is crossed out in orange and labelled premises skipped. A line then appears in the right panel: may implement formal components. Between the panels three required premises appear in turn: 1, identify the formal component; 2, establish every hypothesis; 3, argue the conclusion transfers. The closing line reads: without the middle, the claim is not established.]
A claim that Gödel settles something about machine intelligence is missing its middle. That is not because software and formal systems are unrelated. A computer can implement a formal system, and that connection is how computability theory, the study of what can be computed, works at all. The gap is specific. To carry the theorem across you have to do three things. Say which component you are treating as a formal theory. Show 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 steps can fail. So the fault is not the analogy. It is asserting the conclusion without the argument. Noticing that missing middle, in a paragraph that is fluent and cites a real theorem correctly, is precisely the skill this course teaches.
A proved limit on programs
One proved limit does concern programs. Turing, in nineteen thirty-six and seven, proved an undecidability result about his machines. The halting problem as now stated is a close variant, and undecidable too: 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, in nineteen fifty-three, generalised the point. Every non-trivial property of what a program computes is undecidable. 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: its 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. A preprint from twenty twenty-six reports a security theorem, checked in Lean, for a model that assumes, as the paper states, an authenticated channel between the parties. Whether any system meets that assumption is outside the proof, and the result is only as strong as the assumption is where it is used. The same preprint notes that security proofs in its field can contain gaps of the same kind: individually valid theorems, combined under assumptions that do not match. 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
How much of the middle can be filled in for a language model? A trained model runs as a program, or inside one. Its weights, the numbers fixed in training, are applied by ordinary code with finite arithmetic. The limits Turing and Rice proved are about any procedure meant to work for all programs. Do they also limit a procedure meant only for trained models? That 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 the tools attached. 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. Tarski's is about defining truth inside a formal language that can express arithmetic. Nobody has shown that a given model formalises either. What it can compute depends on the assumptions. Take the transformer design in an idealised form, with hard attention: at each step it looks only at the best-matching parts of the input. In that form it has been proved Turing complete. That means able, given unlimited time and memory, to compute anything a general-purpose computer can. Now take logarithmic precision: numbers kept to a precision that grows only very slowly with the input. In that form it has been shown to be far weaker, if a standard, unproved conjecture holds. That conjecture is written L is not P. Roughly, it says that some problems a computer can solve in reasonable time need more than a tiny working memory. So: 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
Lacrimosa's "Alles Lüge", the song behind this unit's title, has the line: "Ohne nur ein Sehnen werd' ich warten", without a single longing, I will wait. One way to read it 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. It is unchanged by observing: 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 twenty twenty-six, a memory that carries text into later conversations. Its self-description is more output. A study from twenty twenty-three found that a displayed explanation need not reflect what drove the answer. And self-correction on reasoning tasks, without outside feedback, was found in a study from twenty twenty-four to help little, and sometimes to make the answers worse. So the second-order work, stating where a claim comes from and comparing it with something independent, is done by you, or by a system someone designs with the check outside the model, as in Unit 11.
Overclaim 1 — "nothing can be known"
[On screen: The claim 'Nothing can be known', absolute and naming no test, is struck through and marked refused: doubting everything checks nothing. It leads through four steps: state context, keep records, compare independently, and report limits. The result is scoped knowledge supported within stated limits.]
"Nothing can be known." No. What we lose is the guarantee, not knowledge. The move is from a guarantee to a method: state your context, keep records, compare independent ones.
Checker: Unit 8 is the counterexample: you established that your routine agreed with the oracle over the tested indices and satisfied the checked properties under a stated convention. Scoped knowledge, from a record rather than a feeling.
Narrator: "Und doch ich hör' nur Lügen", and yet I hear only lies, from Lacrimosa, "Alles Lüge". That is the unit's title, and it is step one of three, not where this ends.
The course as its own counterexample
The course itself is a counterexample too. It was made by that method, not exempted from it. AI systems helped make it, and synthetic voices narrate it. And it is held to checks you can rerun: the oracle against published values, the accessibility script, and the reference list with its locators. Its 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.
Overclaim 2 — "AI cannot be trusted at all"
That answers the first overclaim. The second takes the same worry and points it at AI alone. "Therefore AI cannot be trusted at all." No. The observer question applies with equal force to human reasoners, to the oracle, to peer review, and to a published table with an error in it. 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.
[On screen: Left of a dashed boundary, inside the system: the system's output is re-checked by the same system and comes back as a revised output that is still self-certified, because nothing outside looked. Right of the boundary, outside what is checked: an independent reference the system did not make and the system's output meet in an independent comparison, which produces an indexed evidence record of the result, context, convention and limits. The record is handed to a box labelled author accountability: the author signs the claim and answers for its limits. The closing line reads: put the check outside, index the claim, say what support you have.]
A model that only re-reads its own output is still self-certifying, vouching for itself: nothing outside it looked. The response is in how the system is designed: put the check outside, index the claim, say what support you have. And the record goes to the author, who signs the claim and answers for its limits.
Overclaim 3 — "Gödel and Tarski prove AI cannot verify itself"
"Gödel and Tarski prove that AI cannot verify itself." No. They do not, and the missing middle says why. Both halves are true: the theorems are real, and so is the system. What is missing is the link between them, the three steps nobody took. Which component is the formal theory? Do the theorem's conditions hold of it? And does the conclusion carry over to the running system? The claim leans hardest on Gödel's second theorem: a consistent system of that kind cannot prove its own consistency. That limits a formal system deriving a statement about itself from its own axioms. Checking a 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.
Where warrant comes from
Look underneath for the bedrock and there is none. One song puts it this way: Einstürzende Neubauten, "Sabrina". "It is as black as Malevich's Square": a square you can stare into, holding nothing. The work goes on anyway, and warrant is built from below: records you can point at, scope someone can defend, a name attached to both. The same song has another line: "It's not the red of which we bleed". This course borrows the line for its own convention: here red marks what is wrong, a divergence, an error, a failed check, never authority. In this unit's slides red marks one thing: the first place where two independent records disagree, as in the comparison with the oracle in Unit 8. It says where to look, not who is right. A divergence is information to act on, not a wound and not an alarm.
[On screen: Three panels in sequence. Step 1, despair: Alles L\u00fcge by Lacrimosa, Q1, everything sounds like a lie. Step 2, missing standpoint: Haus der L\u00fcge by Einst\u00fcrzende Neubauten, Q3, no standpoint outside the system to appeal to. Step 3, practical acceptance: Sabrina by Einst\u00fcrzende Neubauten, Q2, warrant is built from below anyway; this is marked as where the unit ends.]
Three songs, three steps. Everything sounds like a lie. There is no standpoint outside the system to appeal to. And warrant is built from below anyway, which is where this unit ends.
The stopping boundary
The practical boundary is the same one you met earlier. Pause when you can no longer understand and defend the result: when you cannot predict relevant behaviour, explain the transformation, name an independent check, or interpret a failed check. Confidence is not another form of evidence.
Your turn
So the activity does the honest thing. You sort three claims by what supports them, a proved theorem, an established research programme or an overclaim, including claims made in this unit, then one claim of your own from Unit 17. Then reread the sentence you wrote in Unit 0, the one thing you would verify rather than trust, and how. Say which part of it your defence now supports, and what you would change. Then run checkpoint cp18-sort-the-claims. That is the last thing the course asks of you.
Closing, 20 seconds, no speech. A candidate record on the left, a check against an independent reference in the middle, and a bracketed claim on the right fade in side by side. Below them: Continue with the course material, ai.qyber.dev/edu-ai-literacy-ada-verification/, Course playlist: youtube.com/playlist?list=PLPsBWTfgvakM, All links are also in the description, and Keep your record. Check the next claim.