Introduction to Logic: Key Concepts and Decision Problems

Author

Your Name

Published

February 5, 2025

Introduction

This lecture offers a comprehensive overview of fundamental concepts in logic, beginning with the foundational elements of vocabulary, syntax, and semantics. We delve into the concept of reduction as a powerful tool for comparing the complexity and inherent difficulty of decision problems. Furthermore, we examine the notions of expressiveness and succinctness in the context of logical formalisms, highlighting their trade-offs. Finally, we introduce and define four pivotal decision problems: model checking, validity, satisfiability, and logical equivalence. In addition to these, we also touch upon the definability problem, which explores the translation of properties between different logical formalisms. The relationships and, in particular, the interreducibility of validity, satisfiability, and logical equivalence will be demonstrated through rigorous reductions.

Recap of Basic Concepts in Logic

Vocabulary, Syntax, and Semantics

In the realm of logic, we establish the following key components:

Vocabulary: The set of symbols employed within the logical system. This includes variables, constants, function symbols, and relation symbols.
Syntax: The set of rules that govern the formation of well-formed formulas. These rules dictate how symbols from the vocabulary can be combined to create syntactically correct expressions.
Semantics: A mapping that assigns meaning to the symbols and formulas of the logic. This is achieved by relating them to mathematical objects within a specific structure or interpretation. For instance, a relational symbol $R$ might be mapped to a binary relation in a mathematical structure, while a function symbol $f$ might be interpreted as a function over a domain.

Decision Problems and Complexity

We briefly touched upon decision problems and their associated complexity classes. Let’s elaborate:

Reduction: A powerful technique for comparing the relative difficulty of problems. A reduction from problem $P$ to problem $Q$ demonstrates that $P$ is at least as easy as $Q$. More formally, a many-to-one reduction is a function $f$ that transforms instances $x$ of problem $P$ into instances $f(x)$ of problem $Q$ such that the answer to $x$ in $P$ is "yes" if and only if the answer to $f(x)$ in $Q$ is "yes". If this reduction can be performed in polynomial time, it implies that if $Q$ has a polynomial-time solution, then so does $P$.
Complexity Classes:
- P (Polynomial Time): The class of problems that can be solved in polynomial time by a deterministic Turing machine. These problems are considered "efficiently solvable."
- NP (Non-deterministic Polynomial Time): The class of problems for which a solution can be verified in polynomial time by a deterministic Turing machine. Equivalently, these problems can be solved in polynomial time by a non-deterministic Turing machine.

Expressiveness and Succinctness

Expressiveness: This refers to the ability of a logical formalism to express a wide range of properties about objects within its domain. A more expressive logic can capture more complex relationships and constraints.
Succinctness: This relates to the ability to express properties using concise formulas. More succinct formalisms can be easier to use and understand, as they allow for shorter and more manageable formulas. However, increased succinctness often comes at the cost of higher computational complexity for decision problems, as the same information is encoded in a smaller input size.

Consider two logical formalisms, $L_1$ and $L_2$, with the same expressiveness. $L_1$ might require exponentially longer formulas than $L_2$ to express the same property. While $L_2$ is more succinct, decision problems for $L_2$ might be harder due to the smaller input size representing the same information.

Key Decision Problems in Logic

Model Checking

Given a formula $\phi$ and a structure $S$, the model checking problem asks whether $\phi$ is true in $S$. We denote this as $S \models \phi$, meaning that the structure $S$ satisfies the formula $\phi$, or that $S$ is a model of $\phi$.

Input: A formula $\phi$ and a structure $S$.
Question: Does $S \models \phi$ hold? (Is $\phi$ true in $S$?)

Finite vs. Infinite Structures: The structure $S$ can be either finite or infinite.
Representation of Infinite Structures: If $S$ is infinite, a finite representation is necessary for computational purposes. For example, a finite graph can be used to represent the infinite set of all possible paths (traces) within it. Each infinite path can be considered as an infinite structure.
Fixed Structure: In some variations of the model checking problem, the structure $S$ can be fixed a priori. This simplifies the problem to determining the truth of different formulas $\phi$ on a specific, unchanging structure.

Consider a finite graph $G$ representing a system’s state transitions. Each node represents a state, and each edge represents a transition between states. A formula $\phi$ might describe a property like "the system eventually reaches a state where a certain condition holds." Model checking, in this case, involves verifying whether this property holds for all possible paths (traces) in the graph.

Validity, Satisfiability, and Unsatisfiability

Given a formula $\phi$, the validity problem asks whether $\phi$ is true in every possible structure.

Input: A formula $\phi$.
Question: Is $\phi$ true in every structure $S$? (Is $\phi$ a tautology?)

Given a formula $\phi$, the satisfiability problem asks whether there exists a structure $S$ such that $\phi$ is true in $S$.

Input: A formula $\phi$.
Question: Does there exist a structure $S$ such that $S \models \phi$?

Given a formula $\phi$, the unsatisfiability problem asks whether $\phi$ is false in every structure $S$.

Input: A formula $\phi$.
Question: Is $\phi$ false in every structure $S$? (Is $\phi$ a contradiction?)

Interreducibility of Validity, Satisfiability, and Unsatisfiability

We can demonstrate that validity, satisfiability, and unsatisfiability are interreducible, meaning they share the same level of computational difficulty. This implies that an efficient algorithm for one problem can be used to construct an efficient algorithm for the others.

There exists a polynomial-time reduction from the validity problem to the unsatisfiability problem.

Proof. Proof. Given a formula $\phi$, we construct a new formula $\phi' = \neg \phi$. We claim that $\phi$ is valid if and only if $\phi'$ is unsatisfiable.

If $\phi$ is valid: Then, by definition, for all structures $S$, $S \models \phi$. This implies that for all structures $S$, $S \not\models \neg\phi$, meaning $\phi' = \neg\phi$ is unsatisfiable.
If $\phi'$ is unsatisfiable: Then, by definition, for all structures $S$, $S \not\models \phi'$. Since $\phi' = \neg\phi$, this means for all structures $S$, $S \not\models \neg\phi$, which implies for all structures $S$, $S \models \phi$. Thus, $\phi$ is valid.

The transformation from $\phi$ to $\phi'$ takes linear time (just adding a negation). Thus, we have a polynomial-time reduction. ◻

There exists a polynomial-time reduction from the unsatisfiability problem to the validity problem.

Proof. Proof. Given a formula $\phi'$, we construct a new formula $\phi = \neg \phi'$. We claim that $\phi'$ is unsatisfiable if and only if $\phi$ is valid.

If $\phi'$ is unsatisfiable: Then, by definition, for all structures $S$, $S \not\models \phi'$. This implies that for all structures $S$, $S \models \neg\phi'$, meaning $\phi = \neg\phi'$ is valid.
If $\phi$ is valid: Then, by definition, for all structures $S$, $S \models \phi$. Since $\phi = \neg\phi'$, this means for all structures $S$, $S \models \neg\phi'$, which implies for all structures $S$, $S \not\models \phi'$. Thus, $\phi'$ is unsatisfiable.

The transformation from $\phi'$ to $\phi$ takes linear time. Thus, we have a polynomial-time reduction. ◻

Satisfiability and unsatisfiability are complementary problems. An algorithm for one can be used to solve the other by simply inverting the answer (i.e., if an algorithm determines a formula is satisfiable, then it is not unsatisfiable, and vice versa).

Logical Equivalence

Given two formulas $\phi_1$ and $\phi_2$, the logical equivalence problem asks whether for every structure $S$, $S \models \phi_1$ if and only if $S \models \phi_2$. In other words, $\phi_1$ and $\phi_2$ have the same truth value in every possible structure.

Input: Two formulas $\phi_1$ and $\phi_2$.
Question: Is it the case that for all $S$, $S \models \phi_1 \iff S \models \phi_2$?

There exists a polynomial-time reduction from the logical equivalence problem to the validity problem.

Proof. Proof. Given formulas $\phi_1$ and $\phi_2$, we construct a new formula $\phi' = (\phi_1 \implies \phi_2) \land (\phi_2 \implies \phi_1)$. This formula can also be written as $\phi' = \phi_1 \iff \phi_2$ or $\phi' = (\phi_1 \land \phi_2) \lor (\neg\phi_1 \land \neg\phi_2)$. We claim that $\phi_1$ and $\phi_2$ are logically equivalent if and only if $\phi'$ is valid.

If $\phi_1$ and $\phi_2$ are logically equivalent: Then, for all structures $S$, $S \models \phi_1$ if and only if $S \models \phi_2$. This means that in every structure, either both $\phi_1$ and $\phi_2$ are true, or both are false. Thus, $\phi' = (\phi_1 \implies \phi_2) \land (\phi_2 \implies \phi_1)$ is true in every structure, making it valid.
If $\phi'$ is valid: Then, for all structures $S$, $S \models \phi'$. This means that in every structure, $(\phi_1 \implies \phi_2) \land (\phi_2 \implies \phi_1)$ is true. This implies that $\phi_1$ and $\phi_2$ have the same truth value in every structure, making them logically equivalent.

The transformation from $\phi_1, \phi_2$ to $\phi'$ takes linear time. Thus, we have a polynomial-time reduction. ◻

There exists a polynomial-time reduction from the validity problem to the logical equivalence problem.

Proof. Proof. Given a formula $\phi'$, we construct two new formulas: $\phi_1 = \phi'$ and $\phi_2 = \top$, where $\top$ represents a tautology (a formula that is always true, such as $x=x$ or $P \lor \neg P$). We claim that $\phi'$ is valid if and only if $\phi_1$ and $\phi_2$ are logically equivalent.

If $\phi'$ is valid: Then, for all structures $S$, $S \models \phi'$. Since $\phi_2 = \top$ is also true in every structure, $\phi_1 = \phi'$ and $\phi_2 = \top$ have the same truth value in every structure, making them logically equivalent.
If $\phi_1$ and $\phi_2$ are logically equivalent: Then, for all structures $S$, $S \models \phi_1$ if and only if $S \models \phi_2$. Since $\phi_2 = \top$ is true in every structure, this implies that $\phi_1 = \phi'$ must also be true in every structure, making $\phi'$ valid.

The transformation from $\phi'$ to $\phi_1, \phi_2$ takes constant time. Thus, we have a polynomial-time reduction. ◻

Definability

Given two logical formalisms $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, and a formula $\phi_1 \in \mathcal{L}_{1}$, the definability problem asks whether there exists a formula $\phi_2 \in \mathcal{L}_{2}$ such that $\phi_2$ is logically equivalent to $\phi_1$. In essence, it asks if the property expressed by $\phi_1$ in $\mathcal{L}_{1}$ can also be expressed in $\mathcal{L}_{2}$.

Input: Two logical formalisms $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, and a formula $\phi_1 \in \mathcal{L}_{1}$.
Question: Does there exist a formula $\phi_2 \in \mathcal{L}_{2}$ such that $\phi_2$ is logically equivalent to $\phi_1$?

Compatibility of Formalisms: This problem presupposes that $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ are compatible in terms of the structures they can interpret. This means that the structures used to give meaning to formulas in $\mathcal{L}_{1}$ should also be valid for formulas in $\mathcal{L}_{2}$, and vice-versa.
High Complexity: The definability problem is generally undecidable and is not reducible to the other problems discussed (model checking, validity, satisfiability, or logical equivalence).
Example: A classic example is the question of whether a given formula in monadic second-order logic ($\mathcal{L}_{1}$) can be expressed by a formula in first-order logic ($\mathcal{L}_{2}$). These logics differ in their ability to quantify over sets of elements versus individual elements, respectively.

The definability problem is analogous to asking whether a program written in one programming language (e.g., Java) can be translated into another language (e.g., C) while preserving its functionality. The translated program must be equivalent in the sense that it produces the same output for the same input as the original program.

Conclusion

This lecture has provided a foundational understanding of key concepts in logic. We began by defining the essential components of any logical system: vocabulary, syntax, and semantics. We then transitioned to the realm of decision problems, focusing on model checking, validity, satisfiability, and logical equivalence. Through rigorous proofs, we established the interreducibility of the latter three, demonstrating that they are, in essence, computationally equivalent. Finally, we introduced the definability problem, which grapples with the challenging task of translating formulas between distinct logical formalisms while preserving their meaning.

Model checking stands as a central problem in logic, fundamentally asking whether a given formula is true within a specific structure. Its applications range from software and hardware verification to reasoning about complex systems.
Validity, satisfiability, and logical equivalence, despite their different formulations, are computationally equivalent. An efficient algorithm for one can be adapted to solve the others.
Definability addresses the intricate issue of translating formulas between different logical formalisms. This problem is generally undecidable and has significant implications for understanding the expressive power of different logics.

Follow-up Questions:

How can we effectively represent infinite structures using finite means for the purpose of model checking? Consider techniques like abstraction and symbolic representation.
Provide examples of formulas that fall into the following categories:
- Valid: A formula that is true in every possible structure (e.g., $p \lor \neg p$).
- Satisfiable but not valid: A formula that is true in at least one structure but not in all (e.g., $p \land q$).
- Unsatisfiable: A formula that is false in every structure (e.g., $p \land \neg p$).
What are some practical applications of determining logical equivalence between formulas? Think about areas like program optimization, database query optimization, and automated reasoning.

Next Lecture Preview: In the upcoming lecture, we will embark on a journey into the realm of specific logical formalisms. Our exploration will commence with propositional logic, a fundamental system dealing with truth values and logical connectives. We will then progress to quantified Boolean formulas (QBF), an extension of propositional logic that introduces quantifiers over Boolean variables. Finally, we will reach the powerful and expressive domain of first-order logic, which allows quantification over objects and relations. This will conclude the introductory segment of the course, paving the way for a deeper exploration of the applications, extensions, and intricacies of first-order logic in subsequent lectures.

--- title: "Introduction to Logic: Key Concepts and Decision Problems" author: "Your Name" date: "2025-02-05" format: html: toc: true # Table of Contents toc-depth: 2 code-tools: true theme: cosmo # Or "journal" for Distill-like minimalism --- # Introduction This lecture offers a comprehensive overview of fundamental concepts in logic, beginning with the foundational elements of **vocabulary**, **syntax**, and **semantics**. We delve into the concept of **reduction** as a powerful tool for comparing the complexity and inherent difficulty of decision problems. Furthermore, we examine the notions of **expressiveness** and **succinctness** in the context of logical formalisms, highlighting their trade-offs. Finally, we introduce and define four pivotal decision problems: **model checking**, **validity**, **satisfiability**, and **logical equivalence**. In addition to these, we also touch upon the **definability** problem, which explores the translation of properties between different logical formalisms. The relationships and, in particular, the interreducibility of validity, satisfiability, and logical equivalence will be demonstrated through rigorous reductions. # Recap of Basic Concepts in Logic ## Vocabulary, Syntax, and Semantics In the realm of logic, we establish the following key components: - **Vocabulary**: The set of symbols employed within the logical system. This includes variables, constants, function symbols, and relation symbols. - **Syntax**: The set of rules that govern the formation of well-formed formulas. These rules dictate how symbols from the vocabulary can be combined to create syntactically correct expressions. - **Semantics**: A mapping that assigns meaning to the symbols and formulas of the logic. This is achieved by relating them to mathematical objects within a specific structure or interpretation. For instance, a relational symbol $R$ might be mapped to a binary relation in a mathematical structure, while a function symbol $f$ might be interpreted as a function over a domain. ## Decision Problems and Complexity We briefly touched upon decision problems and their associated complexity classes. Let's elaborate: - **Reduction**: A powerful technique for comparing the relative difficulty of problems. A reduction from problem $P$ to problem $Q$ demonstrates that $P$ is at least as easy as $Q$. More formally, a many-to-one reduction is a function $f$ that transforms instances $x$ of problem $P$ into instances $f(x)$ of problem $Q$ such that the answer to $x$ in $P$ is \"yes\" if and only if the answer to $f(x)$ in $Q$ is \"yes\". If this reduction can be performed in polynomial time, it implies that if $Q$ has a polynomial-time solution, then so does $P$. ::: center ::: - **Complexity Classes**: - **P** (Polynomial Time): The class of problems that can be solved in polynomial time by a deterministic Turing machine. These problems are considered \"efficiently solvable.\" - **NP** (Non-deterministic Polynomial Time): The class of problems for which a solution can be verified in polynomial time by a deterministic Turing machine. Equivalently, these problems can be solved in polynomial time by a non-deterministic Turing machine. ## Expressiveness and Succinctness - **Expressiveness**: This refers to the ability of a logical formalism to express a wide range of properties about objects within its domain. A more expressive logic can capture more complex relationships and constraints. - **Succinctness**: This relates to the ability to express properties using concise formulas. More succinct formalisms can be easier to use and understand, as they allow for shorter and more manageable formulas. However, increased succinctness often comes at the cost of higher computational complexity for decision problems, as the same information is encoded in a smaller input size. ::: tcolorbox Consider two logical formalisms, $L_1$ and $L_2$, with the same expressiveness. $L_1$ might require exponentially longer formulas than $L_2$ to express the same property. While $L_2$ is more succinct, decision problems for $L_2$ might be harder due to the smaller input size representing the same information. ::: # Key Decision Problems in Logic ## Model Checking ::: tcolorbox []{#def:model_checking label="def:model_checking"} Given a formula $\phi$ and a structure $S$, the model checking problem asks whether $\phi$ is true in $S$. We denote this as $S \models \phi$, meaning that the structure $S$ satisfies the formula $\phi$, or that $S$ is a model of $\phi$. ::: **Input**: A formula $\phi$ and a structure $S$.\ **Question**: Does $S \models \phi$ hold? (Is $\phi$ true in $S$?) - **Finite vs. Infinite Structures**: The structure $S$ can be either finite or infinite. - **Representation of Infinite Structures**: If $S$ is infinite, a finite representation is necessary for computational purposes. For example, a finite graph can be used to represent the infinite set of all possible paths (traces) within it. Each infinite path can be considered as an infinite structure. - **Fixed Structure**: In some variations of the model checking problem, the structure $S$ can be fixed a priori. This simplifies the problem to determining the truth of different formulas $\phi$ on a specific, unchanging structure. ::: tcolorbox Consider a finite graph $G$ representing a system's state transitions. Each node represents a state, and each edge represents a transition between states. A formula $\phi$ might describe a property like \"the system eventually reaches a state where a certain condition holds.\" Model checking, in this case, involves verifying whether this property holds for all possible paths (traces) in the graph. ::: ## Validity, Satisfiability, and Unsatisfiability ::: tcolorbox []{#def:validity label="def:validity"} Given a formula $\phi$, the validity problem asks whether $\phi$ is true in *every* possible structure. ::: **Input**: A formula $\phi$.\ **Question**: Is $\phi$ true in every structure $S$? (Is $\phi$ a tautology?) ::: tcolorbox []{#def:satisfiability label="def:satisfiability"} Given a formula $\phi$, the satisfiability problem asks whether there *exists* a structure $S$ such that $\phi$ is true in $S$. ::: **Input**: A formula $\phi$.\ **Question**: Does there exist a structure $S$ such that $S \models \phi$? ::: tcolorbox []{#def:unsatisfiability label="def:unsatisfiability"} Given a formula $\phi$, the unsatisfiability problem asks whether $\phi$ is false in *every* structure $S$. ::: **Input**: A formula $\phi$.\ **Question**: Is $\phi$ false in every structure $S$? (Is $\phi$ a contradiction?) ## Interreducibility of Validity, Satisfiability, and Unsatisfiability We can demonstrate that validity, satisfiability, and unsatisfiability are interreducible, meaning they share the same level of computational difficulty. This implies that an efficient algorithm for one problem can be used to construct an efficient algorithm for the others. ::: tcolorbox []{#lem:validity_to_unsat label="lem:validity_to_unsat"} There exists a polynomial-time reduction from the validity problem to the unsatisfiability problem. ::: ::: proof *Proof.* Given a formula $\phi$, we construct a new formula $\phi' = \neg \phi$. We claim that $\phi$ is valid if and only if $\phi'$ is unsatisfiable. - **If $\phi$ is valid**: Then, by definition, for all structures $S$, $S \models \phi$. This implies that for all structures $S$, $S \not\models \neg\phi$, meaning $\phi' = \neg\phi$ is unsatisfiable. - **If $\phi'$ is unsatisfiable**: Then, by definition, for all structures $S$, $S \not\models \phi'$. Since $\phi' = \neg\phi$, this means for all structures $S$, $S \not\models \neg\phi$, which implies for all structures $S$, $S \models \phi$. Thus, $\phi$ is valid. The transformation from $\phi$ to $\phi'$ takes linear time (just adding a negation). Thus, we have a polynomial-time reduction. ◻ ::: ::: tcolorbox []{#lem:unsat_to_validity label="lem:unsat_to_validity"} There exists a polynomial-time reduction from the unsatisfiability problem to the validity problem. ::: ::: proof *Proof.* Given a formula $\phi'$, we construct a new formula $\phi = \neg \phi'$. We claim that $\phi'$ is unsatisfiable if and only if $\phi$ is valid. - **If $\phi'$ is unsatisfiable**: Then, by definition, for all structures $S$, $S \not\models \phi'$. This implies that for all structures $S$, $S \models \neg\phi'$, meaning $\phi = \neg\phi'$ is valid. - **If $\phi$ is valid**: Then, by definition, for all structures $S$, $S \models \phi$. Since $\phi = \neg\phi'$, this means for all structures $S$, $S \models \neg\phi'$, which implies for all structures $S$, $S \not\models \phi'$. Thus, $\phi'$ is unsatisfiable. The transformation from $\phi'$ to $\phi$ takes linear time. Thus, we have a polynomial-time reduction. ◻ ::: ::: tcolorbox []{#rem:sat_unsat_complementary label="rem:sat_unsat_complementary"} Satisfiability and unsatisfiability are complementary problems. An algorithm for one can be used to solve the other by simply inverting the answer (i.e., if an algorithm determines a formula is satisfiable, then it is not unsatisfiable, and vice versa). ::: ## Logical Equivalence ::: tcolorbox []{#def:logical_equivalence label="def:logical_equivalence"} Given two formulas $\phi_1$ and $\phi_2$, the logical equivalence problem asks whether for every structure $S$, $S \models \phi_1$ if and only if $S \models \phi_2$. In other words, $\phi_1$ and $\phi_2$ have the same truth value in every possible structure. ::: **Input**: Two formulas $\phi_1$ and $\phi_2$.\ **Question**: Is it the case that for all $S$, $S \models \phi_1 \iff S \models \phi_2$? ::: tcolorbox []{#lem:equivalence_to_validity label="lem:equivalence_to_validity"} There exists a polynomial-time reduction from the logical equivalence problem to the validity problem. ::: ::: proof *Proof.* Given formulas $\phi_1$ and $\phi_2$, we construct a new formula $\phi' = (\phi_1 \implies \phi_2) \land (\phi_2 \implies \phi_1)$. This formula can also be written as $\phi' = \phi_1 \iff \phi_2$ or $\phi' = (\phi_1 \land \phi_2) \lor (\neg\phi_1 \land \neg\phi_2)$. We claim that $\phi_1$ and $\phi_2$ are logically equivalent if and only if $\phi'$ is valid. - **If $\phi_1$ and $\phi_2$ are logically equivalent**: Then, for all structures $S$, $S \models \phi_1$ if and only if $S \models \phi_2$. This means that in every structure, either both $\phi_1$ and $\phi_2$ are true, or both are false. Thus, $\phi' = (\phi_1 \implies \phi_2) \land (\phi_2 \implies \phi_1)$ is true in every structure, making it valid. - **If $\phi'$ is valid**: Then, for all structures $S$, $S \models \phi'$. This means that in every structure, $(\phi_1 \implies \phi_2) \land (\phi_2 \implies \phi_1)$ is true. This implies that $\phi_1$ and $\phi_2$ have the same truth value in every structure, making them logically equivalent. The transformation from $\phi_1, \phi_2$ to $\phi'$ takes linear time. Thus, we have a polynomial-time reduction. ◻ ::: ::: tcolorbox []{#lem:validity_to_equivalence label="lem:validity_to_equivalence"} There exists a polynomial-time reduction from the validity problem to the logical equivalence problem. ::: ::: proof *Proof.* Given a formula $\phi'$, we construct two new formulas: $\phi_1 = \phi'$ and $\phi_2 = \top$, where $\top$ represents a tautology (a formula that is always true, such as $x=x$ or $P \lor \neg P$). We claim that $\phi'$ is valid if and only if $\phi_1$ and $\phi_2$ are logically equivalent. - **If $\phi'$ is valid**: Then, for all structures $S$, $S \models \phi'$. Since $\phi_2 = \top$ is also true in every structure, $\phi_1 = \phi'$ and $\phi_2 = \top$ have the same truth value in every structure, making them logically equivalent. - **If $\phi_1$ and $\phi_2$ are logically equivalent**: Then, for all structures $S$, $S \models \phi_1$ if and only if $S \models \phi_2$. Since $\phi_2 = \top$ is true in every structure, this implies that $\phi_1 = \phi'$ must also be true in every structure, making $\phi'$ valid. The transformation from $\phi'$ to $\phi_1, \phi_2$ takes constant time. Thus, we have a polynomial-time reduction. ◻ ::: ## Definability ::: tcolorbox []{#def:definability label="def:definability"} Given two logical formalisms $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, and a formula $\phi_1 \in \mathcal{L}_{1}$, the definability problem asks whether there exists a formula $\phi_2 \in \mathcal{L}_{2}$ such that $\phi_2$ is logically equivalent to $\phi_1$. In essence, it asks if the property expressed by $\phi_1$ in $\mathcal{L}_{1}$ can also be expressed in $\mathcal{L}_{2}$. ::: **Input**: Two logical formalisms $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, and a formula $\phi_1 \in \mathcal{L}_{1}$.\ **Question**: Does there exist a formula $\phi_2 \in \mathcal{L}_{2}$ such that $\phi_2$ is logically equivalent to $\phi_1$? - **Compatibility of Formalisms**: This problem presupposes that $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ are compatible in terms of the structures they can interpret. This means that the structures used to give meaning to formulas in $\mathcal{L}_{1}$ should also be valid for formulas in $\mathcal{L}_{2}$, and vice-versa. - **High Complexity**: The definability problem is generally undecidable and is not reducible to the other problems discussed (model checking, validity, satisfiability, or logical equivalence). - **Example**: A classic example is the question of whether a given formula in monadic second-order logic ($\mathcal{L}_{1}$) can be expressed by a formula in first-order logic ($\mathcal{L}_{2}$). These logics differ in their ability to quantify over sets of elements versus individual elements, respectively. ::: tcolorbox The definability problem is analogous to asking whether a program written in one programming language (e.g., Java) can be translated into another language (e.g., C) while preserving its functionality. The translated program must be equivalent in the sense that it produces the same output for the same input as the original program. ::: # Conclusion This lecture has provided a foundational understanding of key concepts in logic. We began by defining the essential components of any logical system: **vocabulary**, **syntax**, and **semantics**. We then transitioned to the realm of decision problems, focusing on **model checking**, **validity**, **satisfiability**, and **logical equivalence**. Through rigorous proofs, we established the **interreducibility** of the latter three, demonstrating that they are, in essence, computationally equivalent. Finally, we introduced the **definability problem**, which grapples with the challenging task of translating formulas between distinct logical formalisms while preserving their meaning. ::: tcolorbox - **Model checking** stands as a central problem in logic, fundamentally asking whether a given formula is true within a specific structure. Its applications range from software and hardware verification to reasoning about complex systems. - **Validity**, **satisfiability**, and **logical equivalence**, despite their different formulations, are computationally equivalent. An efficient algorithm for one can be adapted to solve the others. - **Definability** addresses the intricate issue of translating formulas between different logical formalisms. This problem is generally undecidable and has significant implications for understanding the expressive power of different logics. ::: **Follow-up Questions:** - How can we effectively represent infinite structures using finite means for the purpose of model checking? Consider techniques like abstraction and symbolic representation. - Provide examples of formulas that fall into the following categories: - **Valid**: A formula that is true in every possible structure (e.g., $p \lor \neg p$). - **Satisfiable but not valid**: A formula that is true in at least one structure but not in all (e.g., $p \land q$). - **Unsatisfiable**: A formula that is false in every structure (e.g., $p \land \neg p$). - What are some practical applications of determining logical equivalence between formulas? Think about areas like program optimization, database query optimization, and automated reasoning. **Next Lecture Preview:** In the upcoming lecture, we will embark on a journey into the realm of specific logical formalisms. Our exploration will commence with **propositional logic**, a fundamental system dealing with truth values and logical connectives. We will then progress to **quantified Boolean formulas (QBF)**, an extension of propositional logic that introduces quantifiers over Boolean variables. Finally, we will reach the powerful and expressive domain of **first-order logic**, which allows quantification over objects and relations. This will conclude the introductory segment of the course, paving the way for a deeper exploration of the applications, extensions, and intricacies of first-order logic in subsequent lectures.