Chapter 1

Logic and AI

Johannes Korbmacher about 45 min read updated 11/09/2026

Logic and AI are intimately connected. In this chapter you’ll learn how.

By the way, meet ∀I (read: “AI” — The symbol ∀ is the so-called universal quantifier, which reads “for all”. You’ll learn about it soon enough 😃)!

It is our course mascot, and will feature in many of the examples and exercises.

What is AI?

The term “artificial intelligence” (AI) is used in different ways. Sometimes we mean by it intelligence which is artificial. That is, we think of AI as an ability that computational systems (≈computers) can have or not. This is, for example, how Wikipedia defines AI in the first place (read the first sentence of the article). In this sense of the term we can ask, for example, whether “true” AI is possible.

Sometimes, by AI we mean a specific technology or set of technologies. In recent societal discourse especially, “artificial intelligence” has become virtually synonymous with generative AI (GenAI) and its various applications. This is the sense of AI in which ChatGPT , Copilot , Gemini , Claude , Grok , Llama and DeepSeek are AIs. In this sense of the term, AI is not only possible but real: these technologies exist (obviously)!

There is also a sense of AI as AI-engineering , which is concerned with the practical details of designing, optimizing, and realizing AI technologies. This is the sense of AI when somebody says that they “work in AI”.

In yet another sense of the word, AI is a scientific discipline. It is not easy to define this discipline in simple terms—when you think about it, most scientific disciplines are actually quite hard to define—but as a first shot we can say the following:

AI in this sense is a rather multifaceted discipline. Clearly, computer science plays an important role in AI as it studies computation and automation and the main (and perhaps only?) method for artificially replicating intelligent behavior is by automated, computational models—i.e. computer programs.

But AI is not only computer science. Understanding intelligent behavior is also a core objective of psychology . Thinking about what it means to have (artificial) intelligence (in the capability sense of the word), whether it’s possible to have true artificial intelligence, and so on are important questions in philosophy , especially the philosophy of mind .

The special role of language for thought—illustrated, for example, by Fodor’s language of thought hypothesis —shows that also linguistics plays a role in AI.—In short, AI is a highly interdisciplinary field of study.

All of these senses of AI will play a role in this course. For example, we’ll look at the role that logic plays in intelligent behavior, the role of logic in AI technologies, and the relationship between logic as a discipline and AI.

What is logic?

So, what is logic, then? Here is the standard definition:

Let’s talk about what that means.

The basic concept of logic is that of an inference (sometimes: “argument”), which is a simple piece of reasoning like the following:

  • All humans are mortal and Socrates is human. So, Socrates is mortal.

  • All swans we’ve observed so far were white. Therefore, all swans are white.

You’ve almost certainly come across these examples if you had any contact with philosophy or argumentation theory or the like.

To talk about logic and validity, it’s helpful to introduce some technical terminology. In an inference:

So, in the first inference, all humans being mortal and Socrates being human are the premises, and Socrates being mortal is the conclusion. In the second inference, all swans observed so far being white is the premise, and all swans being white is the conclusion.

Typically, there are some linguistic hints that allow you to identify premises and conclusions. Phrases like “so” and “therefore” are inference indicators . The conclusion typically follows them, though it can be the other way around. Take the inference indicator “since”, for example, and look at how we use it in the following inference:

  • The ground is wet since it’s raining and if it’s raining, the ground is wet.

Similarly, the premises typically precede any inference indicators, but as in our example can also come after. There are also premise indicators , like the “given that” in the following mathematical inference:

  • Given that this figure is a triangle and the sum of all angles in a triangle is 180°, we can conclude that the sum of all angles in this figure is 180°.

By the way, here “we can conclude that” is the conclusion indicator .

Once we’ve identified the logical structure of an inference, we often represent it in a visually clear way. For example, ∀I uses the so-called inference line to indicate the inferential structure here:

There are many different notations. For example, in mathematics, we often use three dots ∴ (read: “therefore”) to indicate that an inference takes place, and we use commas to separate the premises, like so:

All humans are mortal, Socrates is human ∴ Socrates is mortal

With an inference comes the expectation that the premises support the conclusion, that the conclusion follows from the premises. An inference where this is the case is a valid inference.

The first inference—the one about Socrates’ mortality—looks pretty solid. If all humans are mortal and Socrates is human, then he must be mortal. In logic, we call an inference like that, where the premises necessitate the conclusion, deductively valid . Deductive inferences are the traditional topic of most logical theory. They are often associated with mathematical reasoning.

But what about the second inference—the one about the swans? Even if all the swans we’ve observed were white, it’s certainly possible that there’s a non-white (robot?) swan—just that we haven’t seen it yet. So, the inference from all previously observed swans being white to all swans being white is not deductively valid—it is deductively invalid.

But isn’t there a sense in which the fact that all the swans we’ve observed were white does support the claim that all swans are white? We know that there are black swans, so let’s take a slightly modified inference. Suppose that there are a hundred marbles in some bowl. We can’t see inside the bowl and we can only take the marbles out one by one. We keep taking out marbles and they are all white. We’ve sampled the marbles randomly, we’ve taken them from the bottom of the bowl, from the top, and so on. They’re always white.

After some time of sampling—but before we’ve sampled them all—it would seem reasonable to conclude that all marbles are white. Not with certainty—a black marble might still be in there somewhere—but with reasonable confidence.

Of course, whether this is reasonable depends on what else we know. If someone told us that they’d hidden a black marble in the bowl, we shouldn’t draw that conclusion, however many white marbles we found. But under suitable circumstances, observing enough white marbles can give us sufficiently strong reasons to accept that they’re all white.

Unlike deductive validity, inductive support comes in degrees. An inference can be stronger or weaker, depending on how much support the premises give the conclusion. In our example, finding 90 white marbles would generally give us stronger reasons to conclude that they’re all white than finding just 10, assuming we’ve sampled in the same way and our background information stays the same.

The inference is still deductively invalid: the premises could be true while the conclusion is false. But it can be inductively valid : the premises support the conclusion strongly enough to justify accepting it, even though they don’t make it certain.

This is, in essence, what logicians study: different notions of “good” inference, ways in which the premises can support a conclusion. We’ve already seen a kind of classification emerging, which we’ll study in more detail:

Note that logicians (qua logicians) don’t study how people actually reason (psychology of reasoning), or how to use arguments to convince others (rhetoric), or things of that sort. These are all good to know, of course, but they are not the main interest of logicians.

Logical systems

Just like with the term “artificial intelligence”, the term “logic” is used with different meanings. What we’ve looked at so far is the academic discipline of logic. In this context, we might say that an inference is “logical” and mean that it’s valid (or inductively strong). This is in contrast to saying something like “it’s logical that I was scared”, which means something like “it’s understandable that I was scared”.

But there’s also a common way of speaking of “someone’s logic”, as in “according to your logic, we should go home”. This points to an important aspect of logical theory, which we’ll need to talk about before we can move to the relationship between logic and AI: the existence of different logical systems.

What we mean when we say that “according to your logic we should do the thing” is something like “according to the system of premises and inferences you accept, we should do the thing”. It turns out that this sense of logic, we also find in logical theory.

Logicians approach the study of valid inference the way most scientists approach their subject matter: using mathematical models . We call the models that logicians use to study valid inference logical systems .

A logical system typically has three components:

Together, these three components provide a mathematical model of valid inference. Throughout the course, you’ll learn more about syntax, semantics, and proof theory by studying how they are used in different AI applications. By the end, you’ll have a good idea of what the different components of logical systems do, and how they work together to provide a comprehensive model of valid inference.

In essence, logical systems are not all that different from the mathematical models used by physicists, for example. To illustrate, think about how a physicist would approach the question of how far ∀I can throw its ball:

The physicist might use Newtonian mechanics to predict how far the ball will fly, but they wouldn’t apply the laws of mechanics directly to the real world. First, they’d build a mathematical model of the situation, which looks something like this:

In this model, the physicist would assign a mass to the ball, represent the ball as a point in 2-dimensional Euclidean space , and treat the forces acting on the ball as vectors . Assuming that there’s no air resistance, it’s a high-school level exercise to calculate where the ball will land using the laws of classical mechanics (can you still do it?).

What’s characteristic of mathematical models is that they abstract away from irrelevant features of reality (ignoring the trees, for example), they idealize the situation (by treating the ball as a point-mass, for example), and they introduce simplifying assumptions (such as no air resistance, for example). Ultimately, this is what makes it possible to apply exact mathematical calculations to a real-world scenario like ours.

Throughout the books, we’ll be dealing with different kinds of models, which always involve abstractions, idealizations, and other modeling assumptions. We’ll try to be as explicit as possible about these assumptions, since a lot depends on them in terms of the conclusions we can draw from results obtained with those models.

Logical systems work in just the same way as our physicist’s model: they involve abstractions, idealizations, and simplifying assumptions in order to allow us to make exact mathematical calculations about valid inference:

Developing and studying logical systems is the core business of logical theory and has led to a rich body of logical knowledge.

One last thing to note about logical systems is that there are many of them. In this course, you’ll learn about a wide range of logical systems and how they are used in AI. So, there’s what we might call logical diversity!

There are different ways of classifying logical systems, but let’s just look at two to get the point of logical diversity across.

One natural way of classifying logical systems is by the kind of inferences they deal with. For example, there are systems that deal with:

Another way of classifying logical systems is by their background assumptions/philosophies. For example, there’s:

As you’ll see different systems are useful in different contexts.

Logic and AI

Logic has played a special role in AI since its inception as an academic discipline in the second half of the 20th century. One event that is often mentioned as a “beginning” of AI is the 1956 Dartmouth Summer Research Project on Artificial Intelligence , which was organized by Claude Shannon , John McCarthy , Nathaniel Rochester , and Marvin Minsky who are therefore considered by some the “founding fathers”. The research proposal for the event contains one of the first documented uses of the term “artificial intelligence” to refer to an academic discipline.

The naming of the discipline is typically attributed to McCarthy, who thought that logic is the path to achieving human-level artificial intelligence (in the ability sense of the term). But we don’t need to think about human-level intelligence to understand the relevance of logic to AI research. An insight typically attributed to Claude Shannon in his master’s thesis is that we can think of the behavior of electrical circuits (specifically relays ) in logical terms.

To illustrate the idea, take this simple circuit with two switches, A and B:

If—and only if—both A and B are flipped, the light turns on. Shannon realized that this is effectively the operation of logical conjunction from Boolean logic : Think of a switch being flipped “on” as 1 and it being switched “off” as 0. Similarly, take the light turning “on” to be 1 and it being “off” as 0. Then the behavior of the circuit is to return 1 just in case both A and B are 1 and 0 otherwise—which is just the operation of logical conjunction from Boolean logic. We’ll study Boolean logic in detail later, but the idea is that a logical conjunction is true—value 1—just in case both conjuncts are true, and false otherwise. Under the interpretation sketched here, this is precisely the behavior of our circuit!

This relates logic to circuits, but what does this have to do with AI? One way of making the connection is to widen our understanding of “intelligent behavior” from human intelligence to something that allows us to think of a circuit like the one above as a reasoning, intelligent agent. The idea is that we can reconstruct the behavior of the circuit as an inference from two statements—A and B, which we take to mean that the respective switches are “on”—to an action being carried out—turning on the light, which we can think of as yet another statement, L. So the circuit in a sense performs an inference: it infers L from both A and B.

Widening our understanding of intelligence like this allows us to study the behavior of sliding doors, AC systems, self-driving cars, and much more as AI systems using logic. This is a very powerful idea.

The thought that logic is the path to achieving human-level artificial intelligence is the paradigm of logic-based AI, which was the dominant paradigm for AI research from the 1950s until at least the late 1980s. Around that time, probability theory and statistics slowly started to take over as the main approach to the problems of AI, putting the focus on ideas like machine learning and big data .

The success of this approach is not in small part due to artificial neural networks (ANNs) , which are, effectively, statistical models of data, obtained through machine learning on an architecture that is inspired by the structure of the human brain. Today, statistics-based AI is, by far, the dominant paradigm in AI research. This is the approach that led to the recent developments in GenAI.

To understand this shift, it’s helpful to look at the various ways in which logic and AI are related. On a very general level, we can distinguish three ways in which logic is relevant for AI research: there is a foundational, methodological, and auxiliary entanglement between logic and AI research. As we’ll see, even though logic-based AI is no longer an important paradigm in AI research, there are still many different ways in which logic is an important framework for many fundamental tasks in AI research—and that’s not likely to change.

Foundational

Valid inference simply is paradigmatic intelligent behavior. So, logical systems directly target what we’re trying to model in AI—logical systems are models of intelligent behavior. So, by our definition, logical systems are part of AI. This makes logic part of AI and the results of logical research qua logical research relevant to AI research.

The relevance of logic in this sense is mainly foundational, meaning that logic contributes to the understanding of (one of) the basic concepts of AI. A part of logical theory that’s particularly relevant here is metalogic , which deals with the limits and possibilities of logical systems in principle. What’s particularly interesting about this is that metalogical research is, more or less, research in pure mathematics, which turns out to be highly relevant to practical questions in AI research.

Here are two famous metalogical results that (some) people think are highly relevant to AI research:

  • Gödel’s (first) incompleteness theorem , in its Gödel–Rosser form, which implies that for every consistent , effectively axiomatized theory strong enough to represent elementary arithmetic, there is a mathematical statement that is undecidable in the system, meaning that the statement can neither be proven nor refuted in that system.

    Many researchers, including Gödel himself, have thought that this has deep implications for AI. The arguments here are rather subtle and without going into the very technical details of Gödel’s result it is very easy to make mistakes, but a very rough version of the argument runs as follows:

    Since the human mind is consistent and capable of mathematical reasoning, but there is no in principle undecidable mathematical fact for the human mind, Gödel’s result shows that the human mind cannot be modeled or replicated by a logical system.

    If this is correct, it dooms a wide range of approaches to AI, including the logic-based approaches we mentioned before.

  • Church and Turing’s undecidability theorem , which entails that validity in the standard system of predicate logic is (algorithmically) undecidable , meaning that there is no algorithm and there can never be an algorithm that correctly determines in finitely many steps whether any given inference in the system of predicate logic is valid.

    This result seems to show directly that we cannot “fully automate” validity checking using AI and maintain absolute reliability at the same time.

The relevance of logic to AI in this sense is hard to deny. At the same time, a young engineer setting out to change the world with AI, might think of logic in this sense as just theory with little practical relevance. But it’s important to keep in mind that it is essential to understand the foundations of your field before embarking on ground breaking research. Otherwise, one runs the risk of fundamental mistakes, misunderstandings, or simply hitting the limits of what’s in principle possible—which would be a huge waste of effort.

Methodological

Historically, perhaps the most lasting influence that logic has had on the development of AI is via the logic-based AI paradigm, which is also known as symbolic AI due to its use of transparent, human-readable methods.

The idea that logic is the path to achieving human-level artificial intelligence has led to the development of many important technologies, both as abstract designs and as concrete technologies, such as the LISP programming language.

The technologies which have had arguably the most influence within AI to come from the logic-based paradigm are the so-called expert systems , which are computer systems designed to behave like human experts at certain reasoning or decision making tasks. Historical examples include Mycin , a research system for medical diagnosis, and XCon , which configured DEC VAX computer systems. Today, this task roughly corresponds to picking the right components for your new gaming PC build.

An expert system (typically) has two components:

Typically, the information in the KB takes the form of if-then rules . For a toy example, suppose we put the following diagnostic rule into our expert system. We stipulate the rule for the example; it is not a medical claim:

If the patient has a runny nose, a sore throat, and a mild fever,
  then the patient likely has a common cold.

If we present the system with the known fact that our patient does have a runny nose, a sore throat, and a mild fever, the inference engine could easily derive that the patient likely has a common cold. If some symptom is missing, say the patient doesn’t have a fever, this rule no longer supplies that prediction. That doesn’t establish that the patient has no cold; it just means we can’t use this rule to reach the conclusion.

One major advantage of expert systems—especially in hindsight, compared to modern statistics-based systems—is that their decisions, predictions, recommendations, … are explainable. In our case of the common cold, for example, we can explain why the system predicts that has the common cold: because the robot presents the symptoms and there is a corresponding rule for the symptoms. With a large neural network, by contrast, it may be difficult to say which features of the input led to a prediction. This is often called the black-box problem. The field of explainable AI (XAI) studies how to make the behavior of AI systems understandable. XAI is not another name for neural or statistical AI: it is a research aim that can concern different kinds of systems.

An explicit chain of rules helps, but it doesn’t settle every explanatory question either. We may still ask why those rules belong in the knowledge base, whether the premises are reliable, or whether a long derivation is useful to the person asking for an explanation. We’ll return to the difference between explaining a result and verifying it below.

So, why did the paradigm shift from logic-based AI to statistics-based AI?—The full (hi)story of this shift is nuanced and complicated, but looking at aspects of it in a slightly simplified fashion may still help us understand the rather complex entanglement between logic and AI research.

We can identify at least two factors that contributed to the shift. One is the failure of logic-based systems to deliver on their promises. And the second one is the success of statistics-based systems with problems that logic-based systems failed to solve.

The “failures” of logic-based systems are themselves a complex topic, but we can illustrate at least some of the issues with an anecdote reported by Laërtius . According to the anecdote, Plato once defined a human as a featherless biped, much to the approval of everybody in the agora at the time (which is where the cool kids hung out). Along came history’s first punk, Diogenes , and presented Plato with a plucked chicken, remarking “Behold, Plato’s human.”

This seemingly unrelated anecdote from the history of philosophy illustrates a very relevant problem for logic-based AI systems: identifying the precise conditions under which concepts apply can be incredibly hard—even in seemingly simple cases (being a human) and even for clear experts (Plato was at the forefront of scientific research in his time, and he certainly could identify humans).

Plato’s definition seems to give us the following if-then rule:

If something’s a featherless biped, then it is human.

Diogenes presents us with an object that satisfies the two conditions in the if-part of the rule, but not the condition in the then-part. He found a counterexample to Plato’s definition. We can easily imagine this kind of situation happening with expert systems, where the expert knowledge is expressed in similar if-then rules and the AI-system makes corresponding classification errors by rigidly applying these rules. Fixing systems in light of such errors is a tedious process, which cannot easily be automated and requires further expert input: finding correct if-then rules often requires a lot of effort, trial-and-error, fine-tuning, etc. and then maintenance, bug-fixing, and so on.

Moreover, each problem (medical diagnostics, computer assembly, identifying humans, …) requires its own, separate expert knowledge and expert system. Correspondingly, in general, we can’t expect the solutions to problems for one expert system to transfer to the problems of another.

These difficulties contributed to a change in focus of AI research, more and more away from logic-based AI and towards more statistics-based approaches. Importantly, however, they did not bring an end to all work on symbolic systems. Search, knowledge representation, and automated reasoning continued to develop alongside statistical learning.

A helpful example in the history of AI comes from dealing with games. It turns out that games are a natural testing ground for AI technologies. They give us clear rules and a way of checking how well a system performs: Does it follow the rules? Does it win? How does it perform compared to humans? With games, we can compare different approaches on the same task. The game developer and AI researcher John Carmack makes the point concisely about commercial video games specifically in his 2025 Upper Bound talk notes : “Commercial games are great because they are unbiased by researchers.” The point is that games provide natural, complex tasks that researchers didn’t design to suit their own approach to AI.

Logic-based AI has had some spectacular successes. In 1997, IBM’s Deep Blue defeated the reigning world chess champion, Garry Kasparov. Deep Blue worked through possible moves, the opponent’s replies, its own responses, and so on. To judge which moves were promising, it used explicitly programmed criteria developed with the help of chess experts. If you’re interested, you can read about the details in the technical report . This was a major achievement of the symbolic approach: human expertise expressed in a form that a computer could apply at enormous speed.

But this approach proved much harder to make work for the other board games, for example the game Go . Like chess, Go is a traditional strategy board game, originating in China some thousands of years ago. In Go, however, there are typically far more possible moves at each turn than in chess. Each move allows further replies, each reply further responses, and so on—the possibilities quickly become overwhelming. To get anywhere, we need good ways of deciding which moves are worth exploring. We also need to judge whether a position is promising without working through the rest of the game. For Go, both proved particularly difficult to capture in explicitly programmed rules.

DeepMind’s AlphaGo achieved a breakthrough using artificial neural networks (ANNs). Through training on human games and games played against itself, it learned to identify promising moves and assess its chances of winning from a position. It used these learned judgments to guide its exploration of possible moves. Here, much of the expertise that programmers had painstakingly encoded in Deep Blue was acquired through learning. The original AlphaGo paper explains how the networks and search work together.

These developments are part of what Richard Sutton in his landmark 2019 paper with the same name calls “The Bitter Lesson” . His argument is that, in the long run, general methods that make use of more computing power tend to outperform methods built around human expertise. The two methods he singles out are search and learning. This also puts Deep Blue in an interesting position: it relied on human expertise, but its ability to search through enormous numbers of possible moves is itself one of Sutton’s examples. The question is how much expertise we need to build into a system, and how much it can acquire through search and learning.

The success of statistics-based systems like AlphaGo at solving problems that logic-based systems have struggled with for a long time is another factor in the paradigm shift from logic-based to statistics-based systems. The comparison between Deep Blue and AlphaGo is instructive, but the success of statistics-based AI really is “across the board”: image recognition, translation, text-generation, …. In fact, statistics-based methods are at the heart of the recent developments of GenAI.

The statistics-based approach uses machine learning to train its systems. In contrast to expert systems, we no longer need to hard-code the relations between different facts, but the system learns these relations from the data. Rather than if-then rules, statistics-based systems typically use conditional probabilities to make predictions. For example, when a chatbot like ChatGPT or Claude answers a prompt, its underlying model estimates how likely different pieces of text are to come next, given the prompt and what’s been written so far. These probabilities are used to select the next piece of text. The process then repeats, building up the answer piece by piece.

It’s important to note, however, that it can be very hard to extract the learned rules from a statistics-based model: the models are, generally speaking opaque. This is in part because of the size of the models—the language models that underpin chatbot-technologies have literally billions of parameters—and in part because of the way the machine learning algorithms work.

Auxiliary

While statistics-based methods are, at the moment, the state of the art, logic still plays an important role in AI research. Logic-based research in AI has sparked the development of extremely sharp and powerful tools for different tasks in AI development, which are still in use today.

One big area where this is the case is what’s known as Knowledge Representation and Reasoning (KRR) . While subsymbolic systems, especially GenAI-systems like ChatGPT, can store factual information, they are—at least in the current state of the art—fairly unreliable with hallucinations being one of the main issues. A useful comparison is with our own imperfect memory. We might remember the general idea of something we’ve read, but get the details wrong when we try to recall it. And feeling confident that we’ve remembered correctly doesn’t make it so!

For exact retrieval of stored records (think: an account balance or an order number), we normally use databases . Roughly, the difference is between trying to remember the information and writing it down so we can look it up later. A GenAI system can also use a database for this purpose. Keeping the record there gives it something to consult when its own answer would amount to relying on memory.

The connection between databases and logic is very deep: Codd’s theorem shows that querying a database is, in many cases, essentially just a special way of evaluating the formulas of the logical system of predicate logic.

KRR is just one example of where a logical tool is useful outside the scope of expert systems, and symbolic AI in the narrow sense of using logic as the sole foundation for AI. During the course, you’ll see logic is (almost) everywhere in AI, ranging from low-level transistors via high-level programming languages to the abstract study of AI’s abilities—all of this has to do with logic. Logic is, to this day, one of the main auxiliary disciplines of AI research.

The way forward

This concludes our overview of the different ways in which logic is related to AI research. We’ve seen that logic is a foundational discipline for AI since it studies paradigmatic intelligent behavior, that there are logic-based paradigms for AI research and development, and that logic provides useful tools for AI research, especially for knowledge representation.

When AI researchers are skeptical of “logic”, we need to ask which of these roles they have in mind. For example, Geoffrey Hinton questions whether intelligence requires an internal language of symbols. In a 2022 interview with Stephen Hanson , he puts his alternative like this: “what we need is vectors inside the head.” The idea is that neural networks can represent information through lists of numbers, without translating it into logical formulas. This challenges the logic-based approach to building AI. It leaves open the other roles of logic we’ve discussed. And, as we’ll see, even logic-based technologies are alive and kicking. In the rest of this chapter, we’ll have a look at some ways in which logical methods feature in cutting-edge AI research, specifically in the area of GenAI.

System 1 and System 2

One influential way of framing the direction of this research is in terms of a distinction that’s been popularized by Daniel Kahneman in his famous popular science book Thinking, Fast and Slow .

In the book, Kahneman describes the distinction between two kinds of reasoning activities regularly performed by human agents:

Here are some examples:

System 1System 2
Recognizing a faceCounting the A’s in a text
Telling if one object is taller than anotherSolving a logic puzzle
Performing a familiar calculation, like 5+7Working out 432×441
Recalling an answer from memoryChecking the answer against a written record
⋮⋮

Think back to the comparison with imperfect memory. An answer can come to mind immediately, without us working through how we know it. That’s useful, but we can misremember. When the answer matters, we might stop and check: did I really read that? Does the calculation work? Does this conclusion follow from what I know? These are system 2 activities.

One approach to AI takes this distinction as a guide to the division between statistics-based and logic-based systems. On this view, GenAI is good at the system 1 side: recognizing patterns and coming up with plausible answers. Logic-based systems supply the system 2 side: working through explicit rules and their consequences.

On a strong version of this view, GenAI on its own cannot provide reliable system 2 thinking. The way forward is then to combine symbolic and subsymbolic components in hybrid systems . Think of teaching ChatGPT to use a calculator rather than letting it try to solve a calculation “in its head”. The same idea applies to memory: give the system a database to consult, and to reasoning: give it logical tools for working out what follows.

But this is one approach. Another is to think that system 2 abilities can emerge within GenAI systems themselves. The system can learn to break a problem into steps, try different approaches, and revise its answer. For example, research on reasoning models has found improvements from training models to reason and giving them more time to work on a problem. On this approach, we try to develop the system’s own ability to reason deliberately. For a recent overview of how researchers try to develop these abilities, see Zhang and colleagues’ From System 1 to System 2: A Survey of Reasoning Large Language Models , published in 2026.

The comparison with human thinking gives us a way to frame these approaches; it doesn’t settle which abilities an AI architecture can have. Nor do we have to choose once and for all: a system that learns to reason can also use tools. But even if GenAI develops excellent system 2 abilities, we still need a way to check its reasoning. This gives logical methods a role in either approach.

Logic-checking

You’ve probably seen a disclaimer like this underneath a chatbot’s answers (here taken from OpenAI’s ChatGPT):

ChatGPT can make mistakes. Check important info.

But how should we do the checking? If the answer gives us a date or an account balance, we can look it up in a reliable source. If it gives us an argument, there’s a further question: do the premises actually support the conclusion? Checking the facts alone won’t settle that. We also need to check the reasoning.

This is where logic comes into play. We can use logical methods for verification : checking whether a proposed result meets the requirements we’ve set for it. Here, we want to check whether an inference is valid. Asking another GenAI system to review the answer might help us spot a mistake, but its reasoning needs checking too, of course. And we’re off to the races.

Remember that we introduced logical systems as mathematical models of valid inference. Consequently, they are the right framework for answering the questions where asking here: is the AI-generated reasoning logically sound. The important point is that we can use these methods to check an AI’s reasoning, in a theoretically well-founded way—regardless of how the AI came up with the argument.

Take the inference “If it rains, the ground is wet; the ground is wet; so it rains.” The ground could be wet because a sprinkler was running, even though it hasn’t rained. We’ve found a counterexample : the premises are true, but the conclusion is false. This shows that the inference is deductively invalid. The semantics of a logical system lets us make this kind of check mathematically precise, so that a computer can help us find such cases.

Now consider “If it rains, the ground is wet; it rains; so the ground is wet.” Here, the conclusion does follow. The proof theory of a logical system gives us rules for making such steps explicit. By following these rules, we can build a proof of a conclusion from its premises. A computer can then check whether each step follows the rules. This is what makes logical tools so useful here: an AI can suggest an argument, and we can check whether its steps establish the conclusion. If a step fails the check, we need to repair the argument before accepting it as a proof.

Of course, we still need to choose a suitable logical system and represent the argument correctly in its formal language . As with our physicist’s model of the ball, the assumptions we make matter here. Checking the reasoning in our model doesn’t by itself tell us whether we’ve made the right modeling assumptions, or whether the premises are true. But it lets us check what follows from them. That’s what we need logical expertise and tools for.

Checking AI-generated math

A hot topic in current AI research is using GenAI to solve mathematical problems, including problems that have been open for decades. Like games, mathematics gives AI researchers a way of testing and showcasing the abilities of their systems. Can a system find a solution that requires many steps of reasoning? Can it discover an argument that nobody has thought of before? There is also a practical ambition here: to develop tools that help mathematicians with their research. These aims feature in both DeepMind’s work on AlphaProof and OpenAI’s work on open mathematical problems .

But computer-generated proofs present us with a fundamental problem. GenAI is very good at producing text that looks and sounds plausible. But mathematical arguments need to be a rigorous, gap-free, and logically valid piece of argumentation. And when an argument runs through pages of complicated mathematics, checking this can take a great deal of expertise and work. This is where an important logic-based technology comes into play: proof assistants . A proof assistant lets us express mathematical statements in a formal language, construct proofs, and check computationally that each step follows the rules.

A proof assistant that’s seeing adoption in the mathematics community is Lean . Mathematicians are increasingly using Lean to write out their definitions and proofs in a form that a computer can check. They also build on one another’s work: Lean’s mathematical library, Mathlib , collects definitions and checked proofs that can be reused in further arguments. This makes Lean useful for organizing mathematical knowledge and collaborating on proofs, as well as for checking individual results. Interestingly, its applications also extend to verifying computer software , too.

These features make Lean useful for AI research as well. A system can propose a proof, formalize it in Lean, and use the feedback to try again if a step fails. DeepMind’s AlphaProof, for example, learns to find proofs through repeated attempts in Lean’s formal environment. Lean provides the checks that tell the system when it has succeeded. So logical tools can help with both learning to prove and checking the resulting proofs.

This kind of work has produced intriguing results. In August 2026, OpenAI reported ten advances in mathematics and theoretical computer science , releasing mathematical writeups alongside Lean proofs . On September 8, it announced a proposed solution to the Navier–Stokes problem , a long-standing problem about equations describing the motion of fluids, again accompanied by a Lean formalization .2 In these projects, Lean gives mathematicians a way to check the formal proofs independently of the AI systems that produced them. The recent announcements still require mathematical scrutiny, including whether the formal statements capture the problems they claim to solve.

A complete proof checked by a proof assistant like Lean gives us a very high standard of verification . But mathematical practice involves more than checking proofs. As Terence Tao explains in “There’s more to mathematics than rigour and proofs” , rigorous reasoning and mathematical intuition need to work together. We also want to understand why a result holds, how it connects to other results, and what we can learn from its proof. Lean helps secure the steps on which that understanding rests. We’ll learn how to use it ourselves later in the course.

Further readings

This textbook is what might be called a didactic textbook. The aim is to familiarize the reader with the basic concepts of logical theory and their role in AI research. The focus lies on teaching with examples and illustrating bigger ideas. In contrast, an encyclopedic textbook focuses more on providing an exhaustive discussion of the most important concepts in the field.

The distinction between didactic and encyclopedic textbooks is not strict and not exhaustive, but the present textbook clearly falls into the former category. This is why it’s a good idea to supplement it with more encyclopedic textbooks.

The Open Logic Project develops open textbooks collaboratively. Different books select and arrange material from its Open Logic Text for different courses. Sets, Logic, Computation, for example, is Richard Zach’s remix of that shared material. Russell and Norvig’s Artificial Intelligence: A Modern Approach is a standard introduction to AI as a field of academic research. I’ll recommend specific chapters from these books as we go.

For this chapter:

The Open Logic links lead to freely downloadable PDFs. For AIMA, the link leads to the publisher; the chapter numbers refer to the fourth edition.

Notes:

  1. Why is this a simplifying assumption? ↩︎

  2. The announcement also sparked a dispute about research credit and how AI companies should work with mathematicians. Tristan Buckmaster’s account raises concerns about OpenAI’s response to his work with Levent Alpöge on related fluid equations, including pressure over publication and authorship. OpenAI’s account acknowledges that news of their progress prompted its effort, but says its researchers and AI agents did not see their work before its public release. The accounts differ, and questions about credit and research conduct remain contested. This illustrates another limit of proof checking: Lean can check a formal proof, but it cannot settle who deserves credit for the ideas or whether the researchers were treated fairly. ↩︎