Logic: The Architecture of Thought

Logic is the study of information encoded in the form of logical sentences, providing the foundational framework for reasoning, computation, and the analysis of systems from social relations to complex games.

Source: https://www.youtube.com/watch?v=5IIZ9hK1FM4

At its core, logic is the study of the structure of reasoning itself. It asks a fundamental question: how do we encode information in a form that allows us to derive new, guaranteed conclusions? The answer lies not in the content of what we say, but in the form of our sentences. This introductory course from Stanford’s Michael Genesereth provides a complete mental map of this landscape, charting the progression from the simple relationships of propositional logic to the expressive power of first-order logic, and demonstrating its application in the unexpected arena of general game playing. It begins with a definition that serves as our starting point: logic is the study of information encoded in the form of logical sentences.

The Language of Logic and Its Purpose

We use logic pervasively in both personal and professional life. The language of logic allows us to state observations, write definitions, and encode physical laws. We then use logical reasoning to derive conclusions from this information and convince others of their validity. Its use is not limited to human affairs; it increasingly operates at the interface between humans and machines. Email filtering rules, e-commerce pricing engines, and logic programming languages like Prolog are all practical implementations of logical systems. The study of logic is organized around three core elements: syntax (the rules for forming acceptable sentences), semantics (what those sentences mean), and logical entailment (which conclusions must be true given a set of known truths).

To make this concrete, consider the “sorority world” of four members: Abby, Bess, Cody, and Dana. Imagine we receive fragments of information about who likes whom from various informants. Each informant can express exactly what they know using logical sentences—perhaps “Dana likes Cody,” “Abby likes everyone that Bess likes,” or “Bess likes Cody or Dana but not both.” Our task is to combine these sentences into a theory and use logic to draw conclusions, such as inferring that Bess must like Cody, even if no single informant knew this fact. Each sentence constrains the possible states of the world. Believing a sentence means believing the world is in one of the possible states where that sentence is true. Logical entailment is the critical concept: a set of premises logically entails a conclusion if and only if every possible world that satisfies the premises also satisfies the conclusion.

Propositional Logic: The Foundation

The first and simplest logic examined is propositional logic. Here, the world is described using proposition constants—symbols like p or raining that represent conditions that are either true or false. Compound sentences are built from these constants using logical operators: negation (¬), conjunction (∧), disjunction (∨), implication (→), reduction (←), and equivalence (↔). The semantics of these operators are defined by truth tables, which systematically evaluate the truth value of compound sentences for every possible assignment of truth values to the constituent constants.

For example, the sentence p → q is false only when p is true and q is false; otherwise, it is true. This leads to the sometimes-counterintuitive notion that a false antecedent makes an implication vacuously true. From these basic building blocks, we can classify sentences: a sentence is valid if it is true under every truth assignment, unsatisfiable if false under every truth assignment, and contingent otherwise. Logical entailment in propositional logic can be checked exhaustively using truth tables, though this becomes impractical for languages with many constants.

An alternative to truth tables is proof. A proof is a sequence of sentences derived from premises using rules of inference. The power of proof lies in rules of inference like modus ponens (implication elimination): from p → q and p, we can derive q. The critical insight, attributed to Aristotle, is that these rules are correct due to their form, not their content. The pattern All X are Y; All Y are Z; therefore, All X are Z holds regardless of what X, Y, and Z represent. The Fitch system provides a structured method for building proofs, incorporating subproofs for making assumptions and deriving implications.

However, natural language is fraught with ambiguity and complexity that logic seeks to avoid. A formal language eliminates unintentional ambiguities (like the double meaning of “nothing is better than good sex”) and provides a basis for automated reasoning. Just as algebra uses symbolic manipulation to solve equations, logic uses rules like propositional resolution on sentences converted into clausal form (a set of clauses, where each clause is a disjunction of literals). The resolution principle allows us to derive new clauses from existing ones, and if we can derive the empty clause (a contradiction), we have proven that a set of sentences is unsatisfiable.

Herbrand Logic: Beyond Atomic Propositions

Propositional logic, while powerful, cannot express relationships between individual objects or make general statements about classes of objects. Herbrand logic extends propositional logic by introducing variables, function constants, and quantifiers. Instead of monolithic proposition constants, we have object constants (like joe), function constants (like mother), and relation constants (like knows), each with an arity specifying how many arguments they take.

Sentences are built from terms (which represent objects, e.g., mother(joe)) and relational sentences (which state that a relation holds of certain terms, e.g., knows(joe, jill)). The logical operators from propositional logic apply, and we gain two powerful quantifiers: the universal quantifier (∀, “for all”) and the existential quantifier (∃, “there exists”). A sentence like ∀x (hates(jane, x)) asserts that Jane hates everyone. Herbrand logic’s semantics are grounded in the Herbrand base, the set of all ground atomic sentences that can be formed from the vocabulary.

A truth assignment for Herbrand logic maps each sentence in the Herbrand base to true or false, and the semantics of operators and quantifiers extend this to all sentences. For a universally quantified sentence, it is true if every instance (replacing the variable with any ground term) is true. For an existentially quantified sentence, it is true if some instance is true. This allows us to encode complex domains. In a blocks world, we can define relations like on and above not by listing all facts, but by giving logical rules (e.g., a block is clear if there is no block on it). In arithmetic, we can use a single constant 0 and a successor function s to represent all natural numbers and define addition with a few axioms, like ∀x (plus(0, x, x)) and the successor axiom.

Herbrand logic enables us to formalize syntax itself. We can use Herbrand sentences to define a grammar for “pseudo-English,” specifying what constitutes a legal sentence, a noun phrase, or a verb phrase. This demonstrates logic’s power to describe its own structures, a theme that recurs in meta-logic.

Proof and Resolution in Herbrand Logic

The proof system for Herbrand logic, extending Fitch, incorporates rules for the new quantifiers. Universal Introduction allows us to generalize from an arbitrary sentence to a universally quantified one, provided the variable is not free in any active assumption. Universal Elimination lets us conclude a specific instance from a universal statement. Existential Introduction allows us to assert an existential if we have a specific example, and Existential Elimination allows us to use an existential sentence in a subproof to derive a conclusion independent of the specific witness.

For automated reasoning, Herbrand resolution is paramount. Sentences are first converted to clausal form, a process involving steps to move negations inward, standardize variables, and eliminate existentials using Skolem functions (e.g., replacing ∃x P(x) with P(sk), where sk is a new constant). The resolution principle is generalized: two clauses can resolve if their complementary literals are unifiable. Unification is the process of finding a substitution for variables that makes two expressions identical. The most general unifier (MGU) is the most general substitution that achieves this.

Resolution derivations and proofs allow us to check for unsatisfiability and, via the Unsatisfiability Theorem, logical entailment (to prove Δ ⊨ Φ, we check if Δ ∪ {¬Φ} is unsatisfiable). We can also use resolution to answer queries with free variables by adding a goal literal and deriving clauses containing that goal.

Induction: Reasoning About Infinite Domains

To reason about infinite domains, like all natural numbers, we use induction. Complete induction requires proving a statement for all instances. For a finite Herbrand base, this is simple domain closure. For infinite bases structured like a linear sequence (one base constant, one successor function), we use linear induction: prove for the base case, and prove that if it holds for an arbitrary element, it holds for its successor. For tree-structured terms, we use tree induction, proving for the base and each function constructor. Structural induction is the most general, applying to any algebraic structure.

For example, in arithmetic, we can prove that plus(x, 0, x) for all x by showing it for 0 (base case) and proving that if it holds for x, it holds for s(x) (successor case). Induction is a powerful but careful tool; it requires proving the statement for all instances, not just observing a pattern.

First-Order Logic: The Power of Interpretation

While Herbrand logic is powerful, it assumes a fixed universe of discourse (the Herbrand universe). First-order logic lifts this restriction, decoupling the language from a specific domain. The syntax is similar to Herbrand logic but adds equations (=). The critical difference is semantic: an interpretation consists of an arbitrary universe of discourse and a mapping of the language’s constants to objects, functions, and relations within that universe.

Truth is defined relative to an interpretation and a variable assignment. A universally quantified sentence ∀x φ is true if the scope φ is true for every possible value of x in the universe. An existentially quantified sentence ∃x φ is true if the scope is true for at least one value. This abstract semantics means a set of first-order sentences can be true in many different interpretations. For instance, the blocks world sentences describing a stack of three blocks could be true in a universe of blocks, people, or numbers, as long as the on relation has the right structure.

First-order logic is strictly less expressive than Herbrand logic in terms of logical entailment, because Herbrand logic’s fixed universe can convey more information. However, first-order logic’s flexibility is its strength. Its proof system, extending Fitch, includes rules for equality (reflexivity and substitution of equals) but drops domain-specific rules like induction, which are not sound in a general first-order context. Crucially, the Fitch system for first-order logic is both sound and complete: a conclusion is logically entailed if and only if it is provable.

General Game Playing: Logic in Action

The final segment of the course presents a fascinating application: general game playing (GGP). Unlike specialized chess programs, a general game player knows nothing about the game in advance. It receives a formal description of the game—its rules, legal moves, state transitions, and goals—at runtime, and must use this description to play.

The game description language (GDL) is based on Herbrand logic, treating game states as databases of facts. Rules define what is legal, how the state updates, and what constitutes a goal. For example, tic-tac-toe is defined with sentences specifying roles, initial state, legal moves (like marking a blank cell), update rules, and winning conditions. The game manager handles the environment, communicating with players and enforcing the rules.

Playing a game involves using the logical description to reason about moves. At each state, a player uses the rules to compute its legal moves and the opponent’s, then simulates future states to evaluate outcomes. This leads to game tree search, which is computationally infeasible for complex games. Heuristics like goal proximity, mobility (preferring states with more legal moves), and especially Monte Carlo simulation (playing random games to evaluate a state) are used. However, heuristics can fail spectacularly, as in a cylinder checkers match where a player repeatedly gave up pieces to minimize the opponent’s mobility, leading to its own defeat.

A deeper approach is meta-gaming: analyzing the game description before playing to find structural insights, such as identifying independent sub-games or symmetries, which can dramatically reduce the search space. GGP thus serves as a powerful test bed for artificial intelligence, emphasizing the use of declarative knowledge and reasoning in dynamic, resource-bounded environments. It connects to a long-standing vision in AI, from John McCarthy’s “advice taker” to Edward Feigenbaum’s “what to how” spectrum, aiming for systems that act based on described goals rather than hard-coded programs.

Logic, as presented in this course, is far more than a set of formal rules. It is a lens for analyzing structure, whether in social dynamics, arithmetic, or strategic competition. By abstracting away content and focusing on form, it provides universal tools for representation, reasoning, and computation. From the simple implications of propositional logic to the rich universes of first-order logic and their application in making machines that can learn to play arbitrary games, logic remains one of our most powerful intellectual tools for navigating the complexity of the world.

This article is adapted from an introductory course on logic by Michael Genesereth of Stanford University.