Chapter 6 - Logic

6.1 Introduction

TLDR: This brief introduction emphasizes the core purpose of logic: to provide a rigorous and formal framework for reasoning and proving mathematical statements.

This section establishes the purpose of the entire chapter, setting the stage for a more detailed exploration of the principles and techniques of logic.

Key Takeaways:

• Foundation for Reasoning: Logic provides a structured system for constructing and evaluating arguments.
• Mathematical Rigor: It allows for the precise formalization of mathematical concepts and proofs.
• Guaranteed Validity: By adhering to logical rules, we can ensure that our conclusions are valid and justified by the premises.

6.2 Proof Systems

TLDR: This section introduces the concept of a proof system, a fundamental framework for formally verifying the truth of mathematical statements. It defines the components of a proof system (axioms, rules, and proofs), discusses the properties of soundness and completeness, and briefly highlights the role of proof systems in theoretical computer science.

6.2.1 Definition

A proof system is a formal framework for establishing the validity (truth) of mathematical statements through a sequence of logical deductions. In essence, it’s a system for rigorously checking the correctness of arguments.

Components of a Proof System:

• Alphabet ($\Sigma$): A set of symbols used to construct expressions within the system.

• Statements ($S\subseteq {\Sigma }^{\ast }$): Syntactically correct expressions constructed using the symbols of the alphabet. In other words, it’s a set of allowed formulas.

• Proofs ($P\subseteq {\Sigma }^{\ast }$): Sequences of statements constructed from axioms and inference rules, intended to provide evidence for the truth of a statement.

• Truth Function ($\tau :S\to \{0,1\}$): A function that defines the meaning of a statement. I.e., what makes it correct to call the statement “true” or “false”.

• Verification Function ($\varphi :S\times P\to \{0,1\}$): Takes a statement from the syntax and it’s associated proof string, and outputs true (1) if the proof string is correct to demonstrate the truth of the statement.

• Axioms: Basic statements that are assumed to be true without requiring any proof. They serve as the starting point for all derivations. Usually there are no axioms (so that the definition of the truth function is easier to define and there is a single method to generate the syntax of each statement), but the set of syntax rules define the axioms by allowing some expressions within the language to be built with no prerequisites. This can be understood as taking no assumptions in the theory, and only defining logical truth.

• Rules: Inference rules define how to derive new statements (conclusions) from existing ones (premises). This is usually presented in terms of syntactic objects, with the intended semantic interpretation.

• Proof: A proof is a step-by-step derivation of a statement from the axioms, where each step is justified by an application of one of the inference rules.

6.2.2 Examples

The examples are the main portion of what we’re formalizing, and hence require more definitions.

• Given some graph, that graph has a Hamiltonian Cycle.
• A variable $V$ exists such that the set of sentences that are “true” for $V$ can all be derived

6.2.3 Discussion

Proof systems are crucial for ensuring the reliability and consistency of mathematical knowledge. The system must adhere to two key principles:

• Soundness: A proof system is sound if every statement that can be derived using the system is actually true (i.e., the system only proves correct things). That is, if we prove (and hence get a 1 from the verification function, after parsing the syntax of the statement and its syntax) then the truth function gives the statement to be true. This can be shown mathematically by demonstrating $\forall s\in S\forall p\in P(\varphi (s,p)\to \tau (s))$.

• Completeness: A proof system is complete if every true statement can be derived within the system. This means that all “provable” things are true. That is, the range of provable sentences is “complete” to represent all the possible true things. This can be shown mathematically by demonstrating $\forall s\in S(\tau (s)\to \exists p\in P\varphi (s,p))$.

Tradeoff’s exist, as well, for efficiency.

• Is it easy to find the proof for each statement?
• Is it short (a small number of steps) for finding the proof of each statement?

6.2.4 Proof Systems in Theoretical Computer Science *

Proof systems are fundamental in theoretical computer science (TCS), playing a significant role in areas such as:

• Algorithm Verification: Proving the correctness of algorithms.
• Complexity Theory: Analyzing the computational resources required to find proofs.
• Cryptography: Designing secure systems based on the hardness of finding proofs for certain statements.

For example, proving the correctness of the encryption or validation scheme for bitcoin’s is only an interactive version of a proof system. These are known as probabilistically checkable proofs.

6.3 Elementary General Concepts in Logic

TLDR: This section explores the basic concepts underlying logic, independent of any specific logical system. Key themes are syntax, semantics, interpretations, models, satisfiability, tautology, logical consequence, and equivalence. The concepts of theorems and theories are also introduced.

6.3.1 The General Goal of Logic

The overriding goal of logic is to furnish a precise and consistent framework for reasoning about mathematical statements and for rigorously proving their truth. This involves creating a language with clear rules for construction and a system for deriving new truths from existing ones.

6.3.2 Syntax

The syntax of a logic defines the permissible symbols, and rules for combining those symbols to create well-formed expressions known as formulas (or statements). Syntax is all about the form and structure of expressions.

Analogy: Think of it as the grammar rules of a language. Just like a grammatically incorrect sentence is meaningless, a syntactically incorrect formula is not a valid statement in the logic.

Example: In propositional logic, an alphabet might consist of propositional symbols (like $A$, $B$, $C$) and logical operators ($\wedge$, $\vee$, $\neg$, $\Rightarrow$). The formation rules would specify how these symbols can be combined (e.g., “If $A$ and $B$ are formulas, then $(A\wedge B)$ is a formula.”).

6.3.3 Semantics

The semantics of a logic provides a meaning to the formulas defined by the syntax. Crucially, it tells us what the truth value of a statement is under certain “conditions,” formalized through interpretations. The semantics are all about meaning, correctness, and the “state of affairs” that make statements true or false.

• Interpretation: An interpretation provides concrete meaning to the symbols used in the formulas. It assigns values from a domain to the variables, functions, and predicates in the logic. This value assignment may also be called structure.

Example: In propositional logic, an interpretation (often called a truth assignment) is a function that assigns each propositional symbol to either True (1) or False (0).

Key Idea: The same formula might be true under one interpretation but false under another.

6.3.4 Connection to Proof Systems *

A proof system is a procedure that allows us to derive new statements (conclusions) from existing statements (premises) following logically correct steps. To be useful, the syntax and semantics must work well together: This is called Soundness and Completeness

In other words, a proof should only derive true statements and should be able to prove all statements.

6.3.5 Satisfiability, Tautology, Consequence, Equivalence

These are central concepts in determining the relationships between formulas:

• Satisfiable: A formula is satisfiable if there exists at least one interpretation that makes the formula true.

• Tautology (Valid): A formula is a tautology (or is valid) if it is true under all possible interpretations. Tautologies are statements that are “always true.”

• Logical Consequence: A formula $Q$ is a logical consequence of a formula (or a set of formulas) $P$, denoted $P\models Q$, if every interpretation that makes $P$ true also makes $Q$ true. Think of it as a guarantee: If $P$ is true, you can conclude that $Q$ is also true.

• Logical Equivalence: Two formulas, $F$ and $G$, are logically equivalent, denoted $F\iff G$, if they have the same truth value under every interpretation (i.e., they have identical truth tables). It’s also known as F and G are logical consequences of each other.

6.3.6 The Logical Operators $\wedge$, $\vee$, and $\neg$

These logical operators have already been introduced in previous sections, but are fundamental to define the structure of most logics. This is a reminder:

• Conjunction (AND): $P\wedge Q$ is true only if both $P$ and $Q$ are true.
• Disjunction (OR): $P\vee Q$ is true if at least one of $P$ or $Q$ is true.
• Negation (NOT): $\neg P$ is true if and only if $P$ is false.

6.3.7 Logical Consequence vs. Unsatisfiability

A crucial connection exists between logical consequence and unsatisfiability: $P\models Q$ (Q is a logical consequence of P) is equivalent to saying that the formula $P\wedge \neg Q$ is unsatisfiable. This is often useful for proving relationships in logic, as it enables the search for truth to be translated into a proof of contradiction.

6.3.8 Theorems and Theories

• Theory: A theory consists of a set of axioms—fundamental statements assumed to be true. These axioms form the basis for reasoning within that particular theory.
• Theorem: A theorem is a mathematical statement that can be proven to be true using only the axioms of a specific theory and the rules of logical inference. It’s a statement that is logically derived from the theory’s foundations.

In essence, a theory sets the rules of the game, and theorems are the winning strategies that can be proven within those rules.

6.4 Logical Calculi

TLDR: This section formalizes the idea of a proof by introducing logical calculi. It discusses Hilbert-style calculi, soundness, and completeness, explains derivation rules with examples, and clarifies how to build derivations from assumptions. The connection to proof systems is briefly mentioned.

6.4.1 Introduction

A logical calculus is a formal system designed to define precisely what constitutes a valid proof. It provides a set of rules that can be applied in a purely syntactic way to derive new statements from existing ones. These rules are designed to mimic the logical reasoning process. It gives a concrete way to perform syntactic derivations.

Key aspects of a logical calculus:

• Syntactic: The manipulation of symbols is based purely on their form, without needing to understand their meaning (semantics).
• Rule-Based: Derivations proceed by applying specific inference rules.

6.4.2 Hilbert-Style Calculi

Hilbert-style calculi are a type of logical calculi that rely on a relatively small set of axioms (statements assumed to be true) and inference rules to manipulate statements. The derivation rules are applied one after another, starting with the axioms until one reaches the goal formula, therefore the logic is built solely from manipulating formulas. This makes them relatively easy to describe, but proofs can often be quite long and unintuitive. Another type of calculi exists, often called sequent calculi, where the objects are more complicated than just formulas.

6.4.3 Soundness and Completeness of a Calculus

These two properties define the relationship between the syntax of a logic (how statements are formed) and its semantics (what the statements mean).

• Soundness (or Correctness): A calculus is sound if every statement that can be derived within the calculus is actually true. This guarantees that the calculus only produces valid conclusions. More precisely, for every set $M$ of formulas and every formula $F$, if $M⊢F$, then $M\models F$, where $⊢$ indicates derivability in the calculus and $\models$ indicates logical consequence (defined in chapter 2).

• Completeness: A calculus is complete if every true statement can be derived within the calculus. It guarantees that all valid conclusions can be reached. More precisely, for every set $M$ of formulas and every formula $F$, if $M\models F$, then $M⊢F$.

A calculus is hence sound and complete if there is an if and only if connection between logical consequences and derivability, which means derivability and logical consequence are identical.

6.4.4 Some Derivation Rules

Derivation rules are the heart of a logical calculus. They describe how to transform one or more existing formulas (premises) into a new formula (the conclusion). Here are some examples, with the notation showing the premises above a line and the conclusion below:

• Modus Ponens:

  $\frac{P\Rightarrow QP}{Q}$

  This rule states that if we have derived both $P\Rightarrow Q$ and $P$, we can derive $Q$.

• Double Negation:

  $\frac{\neg \neg P}{P}$

  This rule allows us to remove a double negation.

• De Morgan’s Laws:

  $\frac{\neg (P\wedge Q)}{\neg P\vee \neg Q}$ $\frac{\neg (P\vee Q)}{\neg P\wedge \neg Q}$

  These rules allow us to transform negations of conjunctions and disjunctions.

6.4.5 Derivations from Assumptions

Often, we want to prove a statement under certain assumptions. A derivation from assumptions shows that a statement is true given a specific set of premises. It’s crucial for conditional reasoning.

Notation: $P⊢Q$ means that $Q$ can be derived from the assumption $P$. This means there exists a derivation where $Q$ is at the end and $P$ is used as an axiom.

6.4.6 Connection to Proof Systems *

Logical calculi are formal systems that can be implemented by an algorithm. Proofs can hence be automatically verified by a computer. In a proof system, the set of statements can be the set of pairs $(M,G)$ with $M$ a set of axioms and $G$ the goal. A proof could then be an algorithm that decides whether a statement is a theorem in theory $T$ or not.

6.5 Propositional Logic

TLDR: This section formalizes propositional logic by defining its syntax (how to write formulas) and semantics (how to interpret their truth values). It introduces normal forms for simplifying formulas and then describes the resolution calculus, a method for proving unsatisfiability in propositional logic.

6.5.1 Syntax

The syntax of propositional logic specifies how to construct valid formulas. It consists of:

• Alphabet: A set of symbols. In propositional logic, this alphabet includes:

  • Propositional variables (also called atomic formulas): Symbols like $A_1,A_2,A_3,...$ representing basic propositions.
  • Logical connectives: $\neg$ (negation), $\wedge$ (conjunction), $\vee$ (disjunction), etc.
  • Parentheses: Used for grouping.

• Formulas: Well-formed strings constructed using the alphabet according to specific formation rules:

  1. An atomic formula ($A_i$) is a formula.
  2. If $F$ is a formula, then $\neg F$ is a formula.
  3. If $F$ and $G$ are formulas, then $(F\wedge G)$ and $(F\vee G)$ are formulas.

6.5.2 Semantics

The semantics of propositional logic defines how to assign truth values (true or false, often represented as 1 or 0) to propositional formulas. This relies on the definition of suitable interpretations.

• A truth assignment (or interpretation) for a set $Z$ of atomic formulas is a function $A:Z\to \{0,1\}$. It maps each atomic formula in $Z$ to either true (1) or false (0). The truth assignment must be suitable for a given formula in that $Z$ is a set of atomic formulas.

• Given a truth assignment $A$, the truth value of a compound formula is determined recursively based on the truth values of its subformulas and the definitions of the logical connectives:

  • $A(A_i)=$ The truth value assigned to atomic formula $A_i$ by $A$.
  • $A(\neg F)=1$ if $A(F)=0$, and $A(\neg F)=0$ if $A(F)=1$.
  • $A(F\wedge G)=1$ if $A(F)=1$ and $A(G)=1$, and $A(F\wedge G)=0$ otherwise.
  • $A(F\vee G)=1$ if $A(F)=1$ or $A(G)=1$ (or both), and $A(F\vee G)=0$ otherwise.
  • $A(F\Rightarrow G)=1$ if $A(F)=0$ or $A(G)=1$, and $A(F\Rightarrow G)=0$ if $A(F)=1$ and $A(G)=0$.
  • $A(F\iff G)=1$ if $A(F)=A(G)$, and $A(F\iff G)=0$ otherwise.

6.5.3 Brief Discussion of General Logic Concepts

The general concepts of satisfiability, tautology, logical consequence, and logical equivalence, already presented, are now instantiated specifically for propositional logic. Because propositional logic has a fixed and finite definition of a model, many proofs can be greatly simplified.

6.5.4 Normal Forms

Normal forms provide structured ways to represent propositional formulas. Two key normal forms are:

• Conjunctive Normal Form (CNF): A formula is in CNF if it’s a conjunction of clauses, where each clause is a disjunction of literals: $F=(L_{11}\vee L_{12}\vee ...\vee L_{1m_1})\wedge (L_{21}\vee L_{22}\vee ...\vee L_{2m_2})\wedge ...\wedge (L_{n1}\vee L_{n2}\vee ...\vee L_{n{m}_n})$ where the $L_{ij}$ are literals.

• Disjunctive Normal Form (DNF): A formula is in DNF if it’s a disjunction of conjunctions of literals: $F=(L_{11}\wedge L_{12}\wedge ...\wedge L_{1m_1})\vee (L_{21}\wedge L_{22}\wedge ...\wedge L_{2m_2})\vee ...\vee (L_{n1}\wedge L_{n2}\wedge ...\wedge L_{n{m}_n})$ where the $L_{ij}$ are literals.

6.5.5 The Resolution Calculus for Propositional Logic

Clausal Form

Is is possible to convert propositional logic to its clausal form. Therefore, from now on it’s assumed that propositional logic will have conjunctive normal form.

The Resolution Calculus for Propositional Logic

The resolution calculus is a simple but powerful inference rule for reasoning about sets of propositional clauses. Its primary goal is to prove that a given set of propositional clauses is unsatisfiable. The main formula for resolution is

$\frac{\{P\vee Q,\neg P\vee R\}}{Q\vee R}$

Resolution Rule: For a given clause set, a clause can be added by 4. Resolvent: Given two clauses, $C_1$ and $C_2$, containing complementary literals $P$ and $\neg P$ respectively, create a new clause $C$ by taking all literals from $C_1$ and $C_2$, except for $P$ and $\neg P$: $C=(C_1\setminus \{P\})\cup (C_2\setminus \{\neg P\})$. Where $C_1,C_2\subseteq F$ for a given CNF formula $F$. 5. Addition: The new clause $C$ is added to F.

The set of these operations is called the resolution step, with its goal of iteratively adding the new clause (called the resolvent) in such a way that $S$ is unsatisfiable.

6.6 Predicate Logic (First-order Logic)

TLDR: This section extends propositional logic to predicate logic (also known as first-order logic), introducing predicates, variables, quantifiers, and functions. It explains free and bound variables, substitution, semantics (including interpretations and structures), and the addition of equality. Key equivalences involving quantifiers are covered, as well as normal forms and derivation rules. The section concludes with a powerful example of the versatility of predicate logic by demonstrating Russel’s paradox.

6.6.1 Syntax

The syntax of predicate logic builds upon propositional logic with new elements allowing to capture complex structures. It defines the grammar for constructing well-formed statements:

• Variable Symbols: Symbols representing objects within a specific domain, such as $x_i$ where $i\in \mathbb{N}$ is an index. These represent a generalized object with properties within the specified universe.

• Function Symbols: Symbols representing functions that map objects from the domain to other objects. A function symbol has the form $f_i^{(k)}$, where $i$ identifies the specific function, and $k\in \mathbb{N}$ indicates the function’s arity (the number of arguments it takes). When $k=0$, functions are called constants.

• Predicate Symbols: Symbols representing properties or relations that hold for objects in the domain. A predicate symbol takes the form $P_i^{(k)}$, where $i$ identifies the specific predicate and $k\in \mathbb{N}$ is the arity. Given two elements, $P_i^{(k)}$ describes whether they are part of a relation of the same name.

• Terms: Expressions representing objects in the domain.

  1. A variable is a term.
  2. If $t_1,...,t_k$ are terms and $f_i^{(k)}$ is a function symbol, then $f_i^{(k)}(t_1,...,t_k)$ is a term.

• Formulas: Well-formed expressions representing statements that can be either true or false, built up according to the following rules:

  1. If $t_1,...,t_k$ are terms and $P_i^{(k)}$ is a predicate symbol, then $P_i^{(k)}(t_1,...,t_k)$ is a formula (called an atomic formula).
  2. If $F$ and $G$ are formulas, then $\neg F$, $(F\wedge G)$, and $(F\vee G)$ are formulas.
  3. If $F$ is a formula and $x_i$ is a variable symbol, then $\forall x_{i}F$ and $\exists x_{i}F$ are formulas (using quantifiers).

6.6.2 Free Variables and Variable Substitution

In predicate logic, the concept of variables changes. There are now two kinds of variables:

• Free Variable: A variable occurrence in a formula that is not within the scope of any quantifier ($\forall$ or $\exists$). This requires an interpretation to give a fixed value to give meaning to the formula.
• Bound Variable: A variable occurrence that is within the scope of a quantifier. Its value is determined by the quantifier.

The process of substitution replaces all free occurrences of a variable within a formula with a specific term while respecting a logical correctness. For example, the term t is subbed in the formula A at the free variable x, denoted $A[x/t]$.

6.6.3 Semantics

The semantics of predicate logic defines the conditions for a formula to be true or false, which depends on choosing a suitable interpretation. An interpretation consists of a structure $A=(U,\varphi ,\psi ,\xi )$, where

• $U$ is the universe or domain of discourse.
• $\varphi$ is a function that maps each function symbol from the syntax to an interpretation that maps k-tuples of $U^k\to U$. This allows any function to receive its semantic meaning.
• $\psi$ is a function that maps each k-ary predicate symbol from the syntax to an interpretation $U^k\to \{0,1\}$, with a binary output. This means that each predicate has an interpretation as some relationship among objects of $U$.
• $\xi$ is a function that assigns values to variables to provide the framework for truth to be built on.

To evaluate, A also needs to be suitable for the formula F. Then the semantics can be defined by stating how formulas get interpreted:

1. Variables: If $t=x_i$ then $A(t)=\xi (x_i)$
2. Applying a function: If $t=f^{(k)}(t_1,...,t_k)$ then $A(t)=\varphi (f^{(k)})(A(t_1),...,A(t_k))$
3. Evaluating a predicate P: $A(P^{(k)}(t_1,...,t_k)=\psi (P^{(k)})(A(t_1),...,A(t_k))$
4. $\vee ,\wedge ,\neg$: These get interpreted the same as chapter 2.

*This also requires a definition of $A_{[x\to u]}$, which defines what happens when a variable gets overwritten.

6.6.4 Predicate Logic with Equality

Standard predicate logic can be augmented with a built-in equality symbol ”=”, signifying that two terms represent the same object in the domain. The key is adding axioms for what can happen between objects in the domain.

6.6.5 Some Basic Equivalences Involving Quantifiers

Many important logical equivalences hold that allow you to transform formulas with quantifiers:

• Negation of Universal Quantification: $\neg \forall xP(x)\equiv \exists x\neg P(x)$ (It’s not true for all x if and only if there exists an x for which it is not true).
• Negation of Existential Quantification: $\neg \exists xP(x)\equiv \forall x\neg P(x)$ (It’s not true that there exists an x if and only if it’s true that for all x it is not true).
• Distribution of $\forall$ over $\wedge$: $(\forall xP(x))\wedge (\forall xQ(x))\equiv \forall x(P(x)\wedge Q(x))$ (If everything satisfies P and everything satisfies Q, then everything satisfies both P and Q).
• Distribution of $\exists$ over $\vee$: $(\exists xP(x))\vee (\exists xQ(x))\equiv \exists x(P(x)\vee Q(x))$ (If something satisfies P or something satisfies Q, then there exists something that satisfies either P or Q).

6.6.6 Substitution of Bound Variables

The specific name of a bound variable does not affect the meaning of a formula, as long as we consistently rename all occurrences of the variable within the scope of its quantifier and avoid name collisions with free variables. This means: Given that $y$ does not appear anywhere in $G$, then $\forall xG\iff \forall yG[x/y]$

6.6.7 Normal Forms

Just like propositional logic, predicate logic also supports normal forms. The most fundamental form being:

• Prenex Normal Form: A statement where all quantifiers appear at the beginning of the statement and is then followed by a quantifier-free formula. (eg: $\forall w\forall x\exists y\exists zP(w,x,y,z)$).

6.6.8 Derivation Rules

Derivation rules enable us to formally derive new statements from existing ones in predicate logic. Examples of these are,

Universal Instantiation

If $G$ is such that there exists any formula $P$ such that $\forall xG$, where $x$ is a variable, then every term $t$ (a defined way to reach $G$) can be plugged in, such that:

$\forall xP⊢P[x/t]$

In such a case, we also say that the formula $P$ can be logically derived from the formula $\forall xP$.

6.6.9 An Example Theorem and its Interpretations

This section shows how to connect the theory to the practice of using it. It is done by giving an example, a theorem from Russel, and providing specific, non-abstract interpretations on it.

Consider the statement: $\neg \exists x\forall y(P(y,x)\iff \neg P(y,y))$

The interpretation that arises for this is with $y=set$ and $x=element$: there does not exist a set containing every set that isn’t an element of it’s self. This statement, in set notation is called the “Russel Paradox” (see chapter 3 for more info).

6.7 Beyond Predicate Logic *

TLDR: This short section acknowledges the limitations of predicate logic and points towards the existence of more expressive logical systems designed to overcome those limitations.

Predicate logic (first-order logic), while powerful, has inherent limitations in its expressiveness. This means there are certain kinds of statements that cannot be directly captured within the syntax and semantics of predicate logic. The meta-statement is a powerful example that these are a fundamental property of logic and can not be fixed with new constructions.

One key limitation is that predicate logic cannot readily express meta-theorems, which are statements about the logic itself. Other logical systems have been developed to address this, for instance:

• Second-order logic: Allows quantification over properties (predicates) and functions, not just over objects in the domain.
• Modal Logic: Deals with possibility and necessity.

These more expressive logics come with their own complexities and trade-offs, but they provide solutions for representing concepts beyond the capabilities of standard predicate logic.