Introduction to Logical Formalisms and Semantics

Author

Your Name

Published

February 5, 2025

Introduction

This lecture delves into the concept of a logical language, exploring its fundamental components: vocabulary, syntax, and semantics. We will investigate how logical formalisms serve as tools to represent and analyze statements, with a particular emphasis on the crucial role of semantics in bridging the gap between symbols, formulas, and their intended meanings. Throughout this lecture, we will examine various examples of logical formalisms, including classical first-order logic, and introduce essential concepts such as validity, satisfiability, and the significance of quantifiers and relations. The primary goal is to cultivate an intuitive understanding of the construction and interpretation of logical statements, laying the groundwork for more in-depth discussions in subsequent lectures.

Vocabulary: The set of symbols that constitute the language.
Syntax: The set of rules that govern the formation of well-formed formulas.
Semantics: The mechanism for assigning meaning to symbols and formulas, connecting them to the real world or a mathematical structure.

Components of a Logical Formalism

A logical formalism is built upon three essential components:

Vocabulary: This constitutes the set of symbols that are permissible in the language. These symbols can include variables, constants, function symbols, predicate symbols, logical connectives, and quantifiers.
- Example: In propositional logic, the vocabulary might consist of propositional variables like $p$, $q$, $r$, and logical connectives like $\land$ (and), $\lor$ (or), $\neg$ (not), $\rightarrow$ (implies).
Syntax: This defines the set of rules that dictate how well-formed formulas (wffs) are constructed from the vocabulary. It specifies the grammar of the logical language.
- Example: In propositional logic, a rule might state that if $\phi$ and $\psi$ are wffs, then $(\phi \land \psi)$ is also a wff.
Semantics: This provides the method for assigning meaning to the symbols and formulas of the language. It establishes how formulas are interpreted in a given context or model.
- Example: In propositional logic, the semantics might define that a formula $(\phi \land \psi)$ is true if and only if both $\phi$ and $\psi$ are true.

The components of a logical formalism can be likened to those of a programming language:

Vocabulary corresponds to the keywords, identifiers, and operators.
Syntax corresponds to the grammar rules that define valid programs.
Semantics corresponds to the meaning and execution behavior of the programs.

Example: Aristotle’s Syllogism

Let’s examine a classic example of a syllogism, a form of logical argument attributed to Aristotle:

If all humans are mortal and Socrates is human, then Socrates is mortal.

This statement, expressed in natural language, can be translated into a logical formula using the framework of first-order logic. The translation is as follows:

\[\label{eq:aristotle_syllogism}(\forall X (A(X) \rightarrow B(X)) \land A(Y_0)) \rightarrow B(Y_0)\]

where:

$X$ is a bound variable representing any entity within the universe of discourse.
$Y_0$ is a free variable representing a specific entity, in this case, Socrates.
$A(X)$ is a unary predicate that holds true if $X$ belongs to the set of humans.
$B(X)$ is a unary predicate that holds true if $X$ belongs to the set of mortals.
$\forall$ is the universal quantifier, meaning "for all".
$\rightarrow$ represents logical implication.
$\land$ represents logical conjunction.

Explanation

First Premise: "All humans are mortal" is translated as $\forall X (A(X) \rightarrow B(X))$. This can be read as: "For every entity $X$ in the universe, if $X$ possesses the property of being human (represented by $A(X)$), then $X$ also possesses the property of being mortal (represented by $B(X)$)."
Second Premise: "Socrates is human" is translated as $A(Y_0)$. This asserts that the specific entity represented by $Y_0$ (Socrates) belongs to the set of humans.
Conclusion: "Socrates is mortal" is translated as $B(Y_0)$. This concludes that the entity $Y_0$ (Socrates) belongs to the set of mortals.

In the formula [eq:aristotle_syllogism], $X$ is a bound variable because it falls under the scope of the universal quantifier $\forall$. In contrast, $Y_0$ is a free variable because it is not associated with any quantifier. To determine the truth value of a formula with free variables, we need to assign specific entities from the universe to these variables.

The diagram above visually represents the relationships described in the syllogism. Socrates ($Y_0$) is an element of the set of Humans, which is a subset of Mortals, all within the Universe of discourse.

Classical First-Order Logic

The preceding example of Aristotle’s syllogism is a classic illustration of classical first-order logic. This system of logic provides a formal framework for reasoning about objects, their properties, and the relationships between them.

Quantification over Entities: Variables in first-order logic represent individual entities within a defined domain or universe of discourse. Quantifiers, such as the universal quantifier ($\forall$) and the existential quantifier ($\exists$), allow us to make statements about all or some of these entities.
Predicates: Predicates represent properties of entities or relationships between them.
- Unary Predicates: These describe properties of single entities. For example, $A(X)$ might represent the property "X is human."
- Binary Predicates: These describe relationships between two entities. For example, $married(X, Y)$ might represent the relationship "X is married to Y."
- n-ary Predicates: In general, predicates can have any number of arguments, representing relationships between multiple entities.
Functions: Functions map entities to other entities. For example, $fatherOf(X)$ might represent a function that maps a person to their father.
Constants: Constants represent specific entities within the domain. For example, $socrates$ might be a constant representing the individual Socrates.
Logical Connectives: Standard logical connectives like $\land$ (and), $\lor$ (or), $\neg$ (not), $\rightarrow$ (implies), and $\leftrightarrow$ (if and only if) are used to build complex formulas.

Definition 1 (First-Order Logic). In first-order logic, variables are interpreted as ranging over individual entities in a domain, and quantifiers ($\forall$, $\exists$) apply to these entities. Predicates represent properties of or relationships between entities, while functions map entities to other entities.

Example: Consider the statement "Every dog has a tail." In first-order logic, we might represent this as: \[\forall X (dog(X) \rightarrow \exists Y (tail(Y) \land has(X, Y)))\] where:

$dog(X)$ is a unary predicate meaning "X is a dog."
$tail(Y)$ is a unary predicate meaning "Y is a tail."
$has(X, Y)$ is a binary predicate meaning "X has Y."

Limitations of First-Order Logic

While powerful, first-order logic has limitations. It cannot quantify over predicates or functions. For instance, we cannot express the statement "For every property, there exists an entity that has that property" directly in first-order logic. This would require second-order logic, which allows quantification over predicates.

First-order logic allows quantification over entities only. Higher-order logics allow quantification over sets, predicates, functions, and other higher-order constructs. For example, second-order logic allows quantification over predicates.

Validity and Satisfiability

In the realm of logic, understanding the concepts of validity, satisfiability, and contradiction is fundamental. These concepts help us classify formulas based on their truth values across different interpretations.

Definition 2 (Validity). A formula is considered valid (or a tautology) if it is true under every possible interpretation. In other words, no matter how we interpret the symbols in the formula, the formula always evaluates to true.

Definition 3 (Satisfiability). A formula is satisfiable if there exists at least one interpretation under which the formula evaluates to true. This means we can find at least one way to interpret the symbols that make the formula true.

Definition 4 (Contradiction). A formula is a contradiction (or unsatisfiable) if it is false under every possible interpretation. No matter how we interpret the symbols, the formula always evaluates to false.

A formula is valid if and only if its negation is unsatisfiable.
A formula is satisfiable if and only if its negation is not valid.
A formula is a contradiction if and only if its negation is valid.

Example: A Valid Formula

Recall the formula representing Aristotle’s syllogism from Section [eq:aristotle_syllogism]:

\[(\forall X (A(X) \rightarrow B(X)) \land A(Y_0)) \rightarrow B(Y_0)\]

This formula is valid. No matter what sets we choose for $A$ (humans) and $B$ (mortals), and no matter what entity we choose for $Y_0$ (Socrates), the formula will always evaluate to true. This is because the syllogism captures a logically sound argument form.

The diagram illustrates why the syllogism is valid. If $Y_0$ is in set $A$, and $A$ is a subset of $B$, then $Y_0$ must also be in $B$.

Example: A Contradiction (Russell’s Paradox)

Let’s consider a famous example of a contradiction known as Russell’s Paradox. The paradox arises from the following statement:

There exists a set that contains all and only those sets that do not contain themselves.

We can attempt to translate this into a logical formula:

\[\label{eq:russell_paradox}\exists X \forall Y (C(X, Y) \leftrightarrow \neg C(Y, Y))\]

where $C(X, Y)$ is a binary predicate meaning "$X$ contains $Y$".

This formula is a contradiction. It leads to a paradox when we consider the case where $Y$ is equal to $X$. Let’s analyze this:

Assume the formula is true. Then there exists a set $X$ such that for all sets $Y$, $X$ contains $Y$ if and only if $Y$ does not contain itself.
Now, let’s substitute $X$ for $Y$. We get: $C(X, X) \leftrightarrow \neg C(X, X)$.
This statement says that $X$ contains itself if and only if $X$ does not contain itself, which is a direct logical contradiction.

Therefore, the formula [eq:russell_paradox] cannot be true under any interpretation, making it a contradiction.

Assume $\exists X \forall Y (C(X, Y) \leftrightarrow \neg C(Y, Y))$ is true. Let $R$ be the set such that $\forall Y (C(R, Y) \leftrightarrow \neg C(Y, Y))$. Substitute $R$ for $Y$: $C(R, R) \leftrightarrow \neg C(R, R)$. This is a contradiction. Therefore, the assumption is false, and $\exists X \forall Y (C(X, Y) \leftrightarrow \neg C(Y, Y))$ is a contradiction.

Russell’s Paradox had a profound impact on the foundations of set theory and logic. It demonstrated the need for more rigorous axiomatic systems to avoid such contradictions.

Example: Temporal Properties

Let’s explore how to represent temporal properties using first-order logic. Consider the following statement:

Every incoming order is eventually processed.

This statement describes a system where orders are received and subsequently processed at some later point in time. We can translate this into a logical formula as follows:

\[\label{eq:temporal_property}\forall O \forall T (A(O, T) \rightarrow \exists T' (T < T' \land B(O, T')))\]

where:

$O$ is a variable representing an order.
$T$ and $T'$ are variables representing time points.
$A(O, T)$ is a binary predicate meaning "order $O$ is incoming at time $T$".
$B(O, T')$ is a binary predicate meaning "order $O$ is processed at time $T'$".
$<$ is a binary predicate representing the temporal precedence relation "is before" between time points.

Explanation

Let’s break down the formula:

"Every incoming order": This part of the statement is translated as $\forall O \forall T (A(O, T) \rightarrow \dots)$. It states that for every order $O$ and for every time point $T$, if order $O$ is incoming at time $T$ (represented by $A(O, T)$), then some condition holds.
"Eventually processed": This is translated as $\exists T' (T < T' \land B(O, T'))$. It means that there exists a time point $T'$ such that $T'$ is strictly after $T$ (represented by $T < T'$), and the order $O$ is processed at time $T'$ (represented by $B(O, T')$).

The diagram illustrates the temporal relationship. An order $O$ is incoming at time $T$ and processed at a later time $T'$.

Sorted First-Order Logic

In the formula [eq:temporal_property], we used variables $O$, $T$, and $T'$. In sorted first-order logic (also known as typed first-order logic), we can explicitly specify the sort or type of each variable. This means we can declare that $O$ can only be interpreted as an order and $T$ and $T'$ as time points.

Improved Readability: Sorts make formulas easier to understand by explicitly stating the intended types of variables.
Error Detection: Sorts can help detect errors during formula construction by preventing type mismatches.
Efficiency: Some automated reasoning systems can exploit sort information to improve efficiency.

However, it’s important to note that sorted first-order logic does not add expressive power compared to unsorted first-order logic. Any formula in sorted first-order logic can be translated into an equivalent formula in unsorted first-order logic by introducing unary predicates to represent the sorts.

For example, we could rewrite the formula [eq:temporal_property] in unsorted first-order logic as:

\[\forall O \forall T (Order(O) \land Time(T) \land A(O, T) \rightarrow \exists T' (Time(T') \land T < T' \land B(O, T')))\]

where $Order(O)$ and $Time(T)$ are unary predicates that check if an entity belongs to the sort of orders and time points, respectively.

find $T'$ such that $T < T'$ $B(O, T') \gets \text{true}$

Algorithm [alg:order_processing] represents a high-level procedure for processing orders based on the temporal property. It demonstrates how the logical formula can be interpreted procedurally.

Exercise: Translating a Temporal Statement

Let’s put our knowledge of temporal logic to the test. Consider the following statement:

If I keep studying, I will eventually pass the exam.

Your task is to translate this statement into a logical formula using the concepts we’ve learned.

Solution

The correct translation of the statement into a logical formula is:

\[\label{eq:study_exam}(\forall T (Time(T) \land Start < T \rightarrow S(T))) \rightarrow (\exists T' (Time(T') \land Now < T' \land P(T')))\]

where:

$T$ and $T'$ are variables representing time points.
$Time(T)$ is a unary predicate that is true if $T$ is a valid time point.
$Start$ is a constant representing the time point when the studying begins.
$Now$ is a constant representing the current time point.
$S(T)$ is a unary predicate meaning "I am studying at time $T$".
$P(T')$ is a unary predicate meaning "I pass the exam at time $T'$".
$<$ is a binary predicate representing the temporal precedence relation "is before" between time points.

Explanation

Let’s break down the formula:

"If I keep studying": This is translated as $(\forall T (Time(T) \land Start < T \rightarrow S(T)))$. This means for every time point $T$, if $T$ is a valid time point and $T$ is after the starting time of studying, then I am studying at $T$. The original solution missed that we need a starting and current time.
"I will eventually pass the exam": This is translated as $(\exists T' (Time(T') \land Now < T' \land P(T')))$. This means there exists a time point $T'$ such that $T'$ is a valid time point, $T'$ is after the current time (Now), and I pass the exam at $T'$. The original solution missed that we need a current time.
Difference from the previous example: The previous example ("Every incoming order is eventually processed") involved two events (incoming and processed) related to an order. This example involves a continuous activity (studying) and a subsequent event (passing the exam) related to a person. The use of $\forall T(S(T))$ implies studying at *every* time point, which is a simplification. A more accurate representation would involve intervals or a more complex temporal model. Also, in this example we are talking about a specific person, while in the previous one we were talking about every order.

The original solution provided was not entirely accurate because it didn’t account for the continuous nature of "keep studying" starting from a specific point in time. The improved solution introduces a ‘Start’ constant to represent the beginning of the studying period and a ‘Now’ constant to represent the current time. It clarifies that studying happens at all time points after ‘Start’ and that passing the exam happens at some time point after ‘Now’.

$Start \gets \text{initial time point}$ $Now \gets \text{current time point}$ $S(T) \gets \text{true}$ find $T'$ such that $Time(T') \land Now < T'$ $P(T') \gets \text{true}$

Algorithm [alg:study_exam] outlines the process of studying continuously from a starting time and eventually passing the exam at some later time.

Conclusion

In this lecture, we embarked on a journey into the world of logical formalisms. We began by introducing the essential building blocks of any logical system: vocabulary, syntax, and semantics. We then explored a variety of examples, ranging from the classic Aristotle’s syllogism to more complex scenarios involving temporal properties.

We delved into the crucial concepts of validity, satisfiability, and contradiction, which are fundamental for classifying and understanding logical formulas. We saw that some formulas are inherently true (valid) or false (contradictions) regardless of the interpretation, while others can be either true or false depending on the specific meaning assigned to their symbols.

Through examples, we learned how to translate statements expressed in natural language into the precise language of logic, including those involving temporal relationships. We also touched upon the notion of sorted first-order logic and its benefits in terms of readability and error detection.

A logical formalism comprises vocabulary, syntax, and semantics.
Semantics is crucial for connecting symbols and formulas to their intended meanings.
Validity, satisfiability, and contradiction are fundamental properties of logical formulas.
First-order logic provides a powerful framework for representing and reasoning about objects, properties, and relationships.
Temporal properties can be expressed in first-order logic using time points and temporal relations.
Sorted first-order logic enhances readability but does not increase expressive power.

These concepts are not just abstract ideas; they are essential tools for reasoning about the properties of systems, both theoretical and real-world. In subsequent lectures, we will build upon this foundation, further developing our understanding of logic and its applications.

Looking Ahead

To prepare for the next lecture, ponder the following questions:

Formal Semantics of First-Order Logic: How can we rigorously define the semantics of first-order logic? What does it mean to interpret a formula in a model?
Limitations of First-Order Logic: What are the boundaries of first-order logic? When do we need to move beyond it to more expressive formalisms like second-order logic or other higher-order logics?
Applications in System Verification: How can we harness the power of logical formalisms to verify properties of real-world systems, such as software, hardware, and protocols?
Automated Reasoning: How can we automate the process of logical reasoning? What are the techniques and tools used in automated theorem proving and model checking?

By contemplating these questions, you will be well-prepared to delve deeper into the fascinating world of logic and its applications in the next lecture.

The diagram above provides a visual summary of the key concepts covered in this lecture and their relationships.

--- title: "Introduction to Logical Formalisms and Semantics" 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 delves into the concept of a logical language, exploring its fundamental components: **vocabulary**, **syntax**, and **semantics**. We will investigate how logical formalisms serve as tools to represent and analyze statements, with a particular emphasis on the crucial role of semantics in bridging the gap between symbols, formulas, and their intended meanings. Throughout this lecture, we will examine various examples of logical formalisms, including classical first-order logic, and introduce essential concepts such as **validity**, **satisfiability**, and the significance of **quantifiers** and **relations**. The primary goal is to cultivate an intuitive understanding of the construction and interpretation of logical statements, laying the groundwork for more in-depth discussions in subsequent lectures. ::: tcolorbox - **Vocabulary**: The set of symbols that constitute the language. - **Syntax**: The set of rules that govern the formation of well-formed formulas. - **Semantics**: The mechanism for assigning meaning to symbols and formulas, connecting them to the real world or a mathematical structure. ::: # Components of a Logical Formalism A logical formalism is built upon three essential components: 1. **Vocabulary**: This constitutes the set of symbols that are permissible in the language. These symbols can include variables, constants, function symbols, predicate symbols, logical connectives, and quantifiers. - **Example**: In propositional logic, the vocabulary might consist of propositional variables like $p$, $q$, $r$, and logical connectives like $\land$ (and), $\lor$ (or), $\neg$ (not), $\rightarrow$ (implies). 2. **Syntax**: This defines the set of rules that dictate how well-formed formulas (wffs) are constructed from the vocabulary. It specifies the grammar of the logical language. - **Example**: In propositional logic, a rule might state that if $\phi$ and $\psi$ are wffs, then $(\phi \land \psi)$ is also a wff. 3. **Semantics**: This provides the method for assigning meaning to the symbols and formulas of the language. It establishes how formulas are interpreted in a given context or model. - **Example**: In propositional logic, the semantics might define that a formula $(\phi \land \psi)$ is true if and only if both $\phi$ and $\psi$ are true. ::: tcolorbox The components of a logical formalism can be likened to those of a programming language: - **Vocabulary** corresponds to the keywords, identifiers, and operators. - **Syntax** corresponds to the grammar rules that define valid programs. - **Semantics** corresponds to the meaning and execution behavior of the programs. ::: # Example: Aristotle's Syllogism Let's examine a classic example of a syllogism, a form of logical argument attributed to Aristotle: *If all humans are mortal and Socrates is human, then Socrates is mortal.* This statement, expressed in natural language, can be translated into a logical formula using the framework of first-order logic. The translation is as follows: $$\label{eq:aristotle_syllogism}(\forall X (A(X) \rightarrow B(X)) \land A(Y_0)) \rightarrow B(Y_0)$$ where: - $X$ is a **bound variable** representing any entity within the universe of discourse. - $Y_0$ is a **free variable** representing a specific entity, in this case, Socrates. - $A(X)$ is a **unary predicate** that holds true if $X$ belongs to the set of humans. - $B(X)$ is a **unary predicate** that holds true if $X$ belongs to the set of mortals. - $\forall$ is the **universal quantifier**, meaning \"for all\". - $\rightarrow$ represents **logical implication**. - $\land$ represents **logical conjunction**. ## Explanation 1. **First Premise**: \"All humans are mortal\" is translated as $\forall X (A(X) \rightarrow B(X))$. This can be read as: \"For every entity $X$ in the universe, if $X$ possesses the property of being human (represented by $A(X)$), then $X$ also possesses the property of being mortal (represented by $B(X)$).\" 2. **Second Premise**: \"Socrates is human\" is translated as $A(Y_0)$. This asserts that the specific entity represented by $Y_0$ (Socrates) belongs to the set of humans. 3. **Conclusion**: \"Socrates is mortal\" is translated as $B(Y_0)$. This concludes that the entity $Y_0$ (Socrates) belongs to the set of mortals. ::: tcolorbox In the formula [\[eq:aristotle_syllogism\]](#eq:aristotle_syllogism){reference-type="eqref" reference="eq:aristotle_syllogism"}, $X$ is a bound variable because it falls under the scope of the universal quantifier $\forall$. In contrast, $Y_0$ is a free variable because it is not associated with any quantifier. To determine the truth value of a formula with free variables, we need to assign specific entities from the universe to these variables. ::: ::: center ::: The diagram above visually represents the relationships described in the syllogism. Socrates ($Y_0$) is an element of the set of Humans, which is a subset of Mortals, all within the Universe of discourse. # Classical First-Order Logic The preceding example of Aristotle's syllogism is a classic illustration of **classical first-order logic**. This system of logic provides a formal framework for reasoning about objects, their properties, and the relationships between them. ::: tcolorbox - **Quantification over Entities**: Variables in first-order logic represent individual entities within a defined domain or universe of discourse. Quantifiers, such as the universal quantifier ($\forall$) and the existential quantifier ($\exists$), allow us to make statements about all or some of these entities. - **Predicates**: Predicates represent properties of entities or relationships between them. - **Unary Predicates**: These describe properties of single entities. For example, $A(X)$ might represent the property \"X is human.\" - **Binary Predicates**: These describe relationships between two entities. For example, $married(X, Y)$ might represent the relationship \"X is married to Y.\" - **n-ary Predicates**: In general, predicates can have any number of arguments, representing relationships between multiple entities. - **Functions**: Functions map entities to other entities. For example, $fatherOf(X)$ might represent a function that maps a person to their father. - **Constants**: Constants represent specific entities within the domain. For example, $socrates$ might be a constant representing the individual Socrates. - **Logical Connectives**: Standard logical connectives like $\land$ (and), $\lor$ (or), $\neg$ (not), $\rightarrow$ (implies), and $\leftrightarrow$ (if and only if) are used to build complex formulas. ::: ::: definition **Definition 1** (First-Order Logic). *In first-order logic, variables are interpreted as ranging over individual entities in a domain, and quantifiers ($\forall$, $\exists$) apply to these entities. Predicates represent properties of or relationships between entities, while functions map entities to other entities.* ::: ::: mdframed **Example**: Consider the statement \"Every dog has a tail.\" In first-order logic, we might represent this as: $$\forall X (dog(X) \rightarrow \exists Y (tail(Y) \land has(X, Y)))$$ where: - $dog(X)$ is a unary predicate meaning \"X is a dog.\" - $tail(Y)$ is a unary predicate meaning \"Y is a tail.\" - $has(X, Y)$ is a binary predicate meaning \"X has Y.\" ::: ## Limitations of First-Order Logic While powerful, first-order logic has limitations. It cannot quantify over predicates or functions. For instance, we cannot express the statement \"For every property, there exists an entity that has that property\" directly in first-order logic. This would require **second-order logic**, which allows quantification over predicates. ::: tcolorbox **First-order logic** allows quantification over entities only. **Higher-order logics** allow quantification over sets, predicates, functions, and other higher-order constructs. For example, second-order logic allows quantification over predicates. ::: # Validity and Satisfiability In the realm of logic, understanding the concepts of validity, satisfiability, and contradiction is fundamental. These concepts help us classify formulas based on their truth values across different interpretations. ::: {.def:validity .definition} **Definition 2** (Validity). *A formula is considered **valid** (or a **tautology**) if it is true under every possible interpretation. In other words, no matter how we interpret the symbols in the formula, the formula always evaluates to true.* ::: ::: {.def:satisfiability .definition} **Definition 3** (Satisfiability). *A formula is **satisfiable** if there exists at least one interpretation under which the formula evaluates to true. This means we can find at least one way to interpret the symbols that make the formula true.* ::: ::: {.def:contradiction .definition} **Definition 4** (Contradiction). *A formula is a **contradiction** (or **unsatisfiable**) if it is false under every possible interpretation. No matter how we interpret the symbols, the formula always evaluates to false.* ::: ::: tcolorbox - A formula is valid if and only if its negation is unsatisfiable. - A formula is satisfiable if and only if its negation is not valid. - A formula is a contradiction if and only if its negation is valid. ::: ## Example: A Valid Formula Recall the formula representing Aristotle's syllogism from Section [\[eq:aristotle_syllogism\]](#eq:aristotle_syllogism){reference-type="ref" reference="eq:aristotle_syllogism"}: $$(\forall X (A(X) \rightarrow B(X)) \land A(Y_0)) \rightarrow B(Y_0)$$ This formula is **valid**. No matter what sets we choose for $A$ (humans) and $B$ (mortals), and no matter what entity we choose for $Y_0$ (Socrates), the formula will always evaluate to true. This is because the syllogism captures a logically sound argument form. ::: center ::: The diagram illustrates why the syllogism is valid. If $Y_0$ is in set $A$, and $A$ is a subset of $B$, then $Y_0$ must also be in $B$. ## Example: A Contradiction (Russell's Paradox) Let's consider a famous example of a contradiction known as Russell's Paradox. The paradox arises from the following statement: *There exists a set that contains all and only those sets that do not contain themselves.* We can attempt to translate this into a logical formula: $$\label{eq:russell_paradox}\exists X \forall Y (C(X, Y) \leftrightarrow \neg C(Y, Y))$$ where $C(X, Y)$ is a binary predicate meaning \"$X$ contains $Y$\". This formula is a **contradiction**. It leads to a paradox when we consider the case where $Y$ is equal to $X$. Let's analyze this: 1. Assume the formula is true. Then there exists a set $X$ such that for all sets $Y$, $X$ contains $Y$ if and only if $Y$ does not contain itself. 2. Now, let's substitute $X$ for $Y$. We get: $C(X, X) \leftrightarrow \neg C(X, X)$. 3. This statement says that $X$ contains itself if and only if $X$ does not contain itself, which is a direct logical contradiction. Therefore, the formula [\[eq:russell_paradox\]](#eq:russell_paradox){reference-type="eqref" reference="eq:russell_paradox"} cannot be true under any interpretation, making it a contradiction. :::: algorithm ::: algorithmic Assume $\exists X \forall Y (C(X, Y) \leftrightarrow \neg C(Y, Y))$ is true. Let $R$ be the set such that $\forall Y (C(R, Y) \leftrightarrow \neg C(Y, Y))$. Substitute $R$ for $Y$: $C(R, R) \leftrightarrow \neg C(R, R)$. This is a contradiction. Therefore, the assumption is false, and $\exists X \forall Y (C(X, Y) \leftrightarrow \neg C(Y, Y))$ is a contradiction. ::: :::: ::: tcolorbox Russell's Paradox had a profound impact on the foundations of set theory and logic. It demonstrated the need for more rigorous axiomatic systems to avoid such contradictions. ::: # Example: Temporal Properties Let's explore how to represent temporal properties using first-order logic. Consider the following statement: *Every incoming order is eventually processed.* This statement describes a system where orders are received and subsequently processed at some later point in time. We can translate this into a logical formula as follows: $$\label{eq:temporal_property}\forall O \forall T (A(O, T) \rightarrow \exists T' (T < T' \land B(O, T')))$$ where: - $O$ is a variable representing an **order**. - $T$ and $T'$ are variables representing **time points**. - $A(O, T)$ is a binary predicate meaning \"order $O$ is **incoming** at time $T$\". - $B(O, T')$ is a binary predicate meaning \"order $O$ is **processed** at time $T'$\". - $<$ is a binary predicate representing the temporal precedence relation \"is before\" between time points. ## Explanation Let's break down the formula: 1. **\"Every incoming order\"**: This part of the statement is translated as $\forall O \forall T (A(O, T) \rightarrow \dots)$. It states that for every order $O$ and for every time point $T$, if order $O$ is incoming at time $T$ (represented by $A(O, T)$), then some condition holds. 2. **\"Eventually processed\"**: This is translated as $\exists T' (T < T' \land B(O, T'))$. It means that there exists a time point $T'$ such that $T'$ is strictly after $T$ (represented by $T < T'$), and the order $O$ is processed at time $T'$ (represented by $B(O, T')$). ::: center ::: The diagram illustrates the temporal relationship. An order $O$ is incoming at time $T$ and processed at a later time $T'$. ## Sorted First-Order Logic In the formula [\[eq:temporal_property\]](#eq:temporal_property){reference-type="eqref" reference="eq:temporal_property"}, we used variables $O$, $T$, and $T'$. In **sorted first-order logic** (also known as **typed first-order logic**), we can explicitly specify the *sort* or *type* of each variable. This means we can declare that $O$ can only be interpreted as an order and $T$ and $T'$ as time points. ::: tcolorbox - **Improved Readability**: Sorts make formulas easier to understand by explicitly stating the intended types of variables. - **Error Detection**: Sorts can help detect errors during formula construction by preventing type mismatches. - **Efficiency**: Some automated reasoning systems can exploit sort information to improve efficiency. ::: However, it's important to note that sorted first-order logic **does not add expressive power** compared to unsorted first-order logic. Any formula in sorted first-order logic can be translated into an equivalent formula in unsorted first-order logic by introducing unary predicates to represent the sorts. For example, we could rewrite the formula [\[eq:temporal_property\]](#eq:temporal_property){reference-type="eqref" reference="eq:temporal_property"} in unsorted first-order logic as: $$\forall O \forall T (Order(O) \land Time(T) \land A(O, T) \rightarrow \exists T' (Time(T') \land T < T' \land B(O, T')))$$ where $Order(O)$ and $Time(T)$ are unary predicates that check if an entity belongs to the sort of orders and time points, respectively. :::: algorithm ::: algorithmic **find** $T'$ such that $T < T'$ $B(O, T') \gets \text{true}$ ::: :::: Algorithm [\[alg:order_processing\]](#alg:order_processing){reference-type="ref" reference="alg:order_processing"} represents a high-level procedure for processing orders based on the temporal property. It demonstrates how the logical formula can be interpreted procedurally. # Exercise: Translating a Temporal Statement Let's put our knowledge of temporal logic to the test. Consider the following statement: *If I keep studying, I will eventually pass the exam.* Your task is to translate this statement into a logical formula using the concepts we've learned. ## Solution The correct translation of the statement into a logical formula is: $$\label{eq:study_exam}(\forall T (Time(T) \land Start < T \rightarrow S(T))) \rightarrow (\exists T' (Time(T') \land Now < T' \land P(T')))$$ where: - $T$ and $T'$ are variables representing **time points**. - $Time(T)$ is a unary predicate that is true if $T$ is a valid time point. - $Start$ is a constant representing the time point when the studying begins. - $Now$ is a constant representing the current time point. - $S(T)$ is a unary predicate meaning \"I am studying at time $T$\". - $P(T')$ is a unary predicate meaning \"I pass the exam at time $T'$\". - $<$ is a binary predicate representing the temporal precedence relation \"is before\" between time points. ## Explanation Let's break down the formula: 1. **\"If I keep studying\"**: This is translated as $(\forall T (Time(T) \land Start < T \rightarrow S(T)))$. This means for every time point $T$, *if* $T$ is a valid time point and $T$ is after the starting time of studying, then I am studying at $T$. The original solution missed that we need a starting and current time. 2. **\"I will eventually pass the exam\"**: This is translated as $(\exists T' (Time(T') \land Now < T' \land P(T')))$. This means there exists a time point $T'$ such that $T'$ is a valid time point, $T'$ is after the current time (Now), and I pass the exam at $T'$. The original solution missed that we need a current time. 3. **Difference from the previous example**: The previous example (\"Every incoming order is eventually processed\") involved two events (incoming and processed) related to an order. This example involves a continuous activity (studying) and a subsequent event (passing the exam) related to a person. The use of $\forall T(S(T))$ implies studying at \*every\* time point, which is a simplification. A more accurate representation would involve intervals or a more complex temporal model. Also, in this example we are talking about a specific person, while in the previous one we were talking about every order. ::: tcolorbox The original solution provided was not entirely accurate because it didn't account for the continuous nature of \"keep studying\" starting from a specific point in time. The improved solution introduces a 'Start' constant to represent the beginning of the studying period and a 'Now' constant to represent the current time. It clarifies that studying happens at all time points after 'Start' and that passing the exam happens at some time point after 'Now'. ::: :::: algorithm ::: algorithmic $Start \gets \text{initial time point}$ $Now \gets \text{current time point}$ $S(T) \gets \text{true}$ **find** $T'$ such that $Time(T') \land Now < T'$ $P(T') \gets \text{true}$ ::: :::: Algorithm [\[alg:study_exam\]](#alg:study_exam){reference-type="ref" reference="alg:study_exam"} outlines the process of studying continuously from a starting time and eventually passing the exam at some later time. # Conclusion In this lecture, we embarked on a journey into the world of logical formalisms. We began by introducing the essential building blocks of any logical system: **vocabulary**, **syntax**, and **semantics**. We then explored a variety of examples, ranging from the classic **Aristotle's syllogism** to more complex scenarios involving **temporal properties**. We delved into the crucial concepts of **validity**, **satisfiability**, and **contradiction**, which are fundamental for classifying and understanding logical formulas. We saw that some formulas are inherently true (valid) or false (contradictions) regardless of the interpretation, while others can be either true or false depending on the specific meaning assigned to their symbols. Through examples, we learned how to translate statements expressed in natural language into the precise language of logic, including those involving temporal relationships. We also touched upon the notion of **sorted first-order logic** and its benefits in terms of readability and error detection. ::: tcolorbox - A logical formalism comprises vocabulary, syntax, and semantics. - Semantics is crucial for connecting symbols and formulas to their intended meanings. - Validity, satisfiability, and contradiction are fundamental properties of logical formulas. - First-order logic provides a powerful framework for representing and reasoning about objects, properties, and relationships. - Temporal properties can be expressed in first-order logic using time points and temporal relations. - Sorted first-order logic enhances readability but does not increase expressive power. ::: These concepts are not just abstract ideas; they are essential tools for reasoning about the properties of systems, both theoretical and real-world. In subsequent lectures, we will build upon this foundation, further developing our understanding of logic and its applications. ## Looking Ahead To prepare for the next lecture, ponder the following questions: 1. **Formal Semantics of First-Order Logic**: How can we rigorously define the semantics of first-order logic? What does it mean to interpret a formula in a model? 2. **Limitations of First-Order Logic**: What are the boundaries of first-order logic? When do we need to move beyond it to more expressive formalisms like second-order logic or other higher-order logics? 3. **Applications in System Verification**: How can we harness the power of logical formalisms to verify properties of real-world systems, such as software, hardware, and protocols? 4. **Automated Reasoning**: How can we automate the process of logical reasoning? What are the techniques and tools used in automated theorem proving and model checking? By contemplating these questions, you will be well-prepared to delve deeper into the fascinating world of logic and its applications in the next lecture. ::: center ::: The diagram above provides a visual summary of the key concepts covered in this lecture and their relationships.