25 Skolem Normal Form, Russell's Paradox, Cantor's Diagonalization, Existence of Uncomputable Functions, Higher-Order Logic, Calculi

Lecture from: 11.12.2024 | Video: Videos ETHZ

Skolem Normal Form

Skolem Normal Form is a specific prenex normal form used in predicate logic, particularly useful for automated theorem proving and techniques like resolution. While converting a formula to Skolem Normal Form doesn’t preserve logical equivalence, it does preserve satisfiability. This means a formula is satisfiable if and only if its Skolem Normal Form is satisfiable. This weaker form of equivalence, called equisatisfiability, is sufficient for many applications.

Skolemization, the process of converting a formula to Skolem Normal Form, plays a role in resolution calculi. Resolution operates on formulas in a specific format (clauses), and Skolemization helps transform arbitrary predicate logic formulas into a suitable form for resolution. As we’ve seen, satisfiability and unsatisfiability are closely linked to logical consequence and tautologies.

Skolemization: Eliminating Existential Quantifiers

The core idea behind Skolemization is to eliminate existential quantifiers ($\exists$) by introducing new function symbols, called Skolem functions. These functions effectively “choose” values for the existentially quantified variables, based on the values of the universally quantified variables that precede them.

Examples

Example 1: Simple Skolemization

Consider the formula $\forall x\exists yF(x,y)$. To Skolemize this formula, we remove $\exists y$ and replace $y$ with a Skolem function $f(x)$, resulting in $\forall xF(x,f(x))$.

These two formulas are not logically equivalent.

The original formula asserts that for every $x$, there exists some $y$ (which might depend on $x$) such that $F(x,y)$ holds. The Skolemized version asserts that there’s a specific function $f$ that, for every $x$, gives us a value $f(x)$ such that $F(x,f(x))$ holds. However, if one of them is satisfiable then the other one must also be satisfiable. If the initial formula is satisfiable, it means we can construct a model $\mathcal{A}$ and corresponding universe $U^{\mathcal{A}}$ where for every $u\in U^{\mathcal{A}}$ we have some $v$ such that ${\mathcal{A}}_{[x\to u][y\to v]}(F(x,y))=1$. This $v$ depends on $x$. Thus we can simply construct our Skolem function $f(u)=v$ which chooses the $v$ which makes the formula true.

Conversely, if there is a interpretation which satisfies the second, then we can also be sure that we can select such a $v$ from our universe using the interpretation of $f^{\mathcal{A}}$ which satisfies the second formula. Thus, we can conclude they are equisatisfiable.

Example 2: Multiple Quantifiers

Now, let’s consider a more complex formula: $\forall s\exists t\forall x\forall y\exists zF(s,t,x,y,z)$.

To Skolemize this, we proceed as follows:

1. Prenex Normal Form: Ensure the formula is in prenex normal form (all quantifiers at the beginning). Our example is already in PNF.
2. Replace Existential Quantifiers: Replace each existential quantifier with a Skolem function whose arguments are the universally quantified variables that precede it.
   • $\exists t$ becomes $f(s)$.
   • $\exists z$ becomes $g(s,x,y)$.

The Skolemized form is $\forall s\forall x\forall yF(s,f(s),x,y,g(s,x,y))$.

Example 3: Existential Quantifier without Preceding Universal Quantifiers

What about a formula like $\exists xP(x)$? In this case, the Skolem function has no arguments, effectively becoming a constant. We replace $\exists x$ with a new constant symbol, say $a$, resulting in $P(a)$.

Theorem: A Tautology in Predicate Logic

The following formula is a tautology in predicate logic, meaning it’s true under every interpretation:

This theorem is significant because it holds without any prerequisites or assumptions. It’s a universal truth within predicate logic.

Proof of Tautology

1. Equivalence Transformation: We start by applying an equivalence transformation using quantifier negation and De Morgan’s law for quantifiers:

   $$\neg \exists x\forall y(P(y,x)⟺\neg P(y,y))\equiv \forall x\neg \forall y(P(y,x)⟺\neg P(y,y))\equiv \forall x\exists y\neg (P(y,x)⟺\neg P(y,y))$$

2. Analyzing the Inner Part: Now let’s focus on the inner part: $\neg (P(y,x)⟺\neg P(y,y))$. The biconditional ($⟺$) is true if and only if both sides have the same truth value. Negating the biconditional means the two sides must have different truth values. We can express this as:

   $\neg (A⟺B)\equiv (A\wedge \neg B)\vee (\neg A\wedge B)\equiv A⟺\neg B$

   Here’s a truth table demonstrating this equivalence:

   $A$	$B$	$A⟺B$	$\neg (A⟺B)$	$A⟺\neg B$	$(A\wedge \neg B)\vee (\neg A\wedge B)$
   0	0	1	0	0	0
   0	1	0	1	1	1
   1	0	0	1	1	1
   1	1	1	0	0	0

3. Substituting Back: Substituting this back into our formula, we get:

   $\forall x\exists y(P(y,x)⟺P(y,y))$

4. Proving the Transformed Formula: Now we need to show that $\forall x\exists y(P(y,x)⟺P(y,y))$ is a tautology. See below…

Proving of Tautology

Let’s consider an arbitrary interpretation $\mathcal{A}$ and an arbitrary element $u\in U^{\mathcal{A}}$. We need to show that there exists a $v\in U^{\mathcal{A}}$ such that ${\mathcal{A}}_{[x\to u][y\to v]}(P(y,x)⟺P(y,y))=1$. This means we have to show ${\mathcal{A}}_{[x\to u][y\to v]}(P(y,x))={\mathcal{A}}_{[x\to u][y\to v]}(P(y,y))$.

Let us choose $v=u$ then we get $P^{\mathcal{A}}(u,u)⟺P^{\mathcal{A}}(u,u)$ which is $1⟺1$ which is $1$, thus the formula holds for all $x$ if we select our $y$ appropriately.

Since this holds for any arbitrary interpretation $\mathcal{A}$, the formula is a tautology. Therefore, the original formula $\neg \exists x\forall y(P(y,x)⟺\neg P(y,y))$ is also a tautology.

Interesting Interpretations of a Tautology

We’ve proven that the following formula is a tautology:

Now, let’s explore some interesting interpretations of this tautology, revealing its connections to fundamental concepts in mathematics and computer science. We will see how this seemingly abstract logical statement embodies profound ideas about concepts from maths and computer science.

Example 1: Russell’s Paradox

• Universe: $U=\{\text{all sets}\}$
• Predicate: $P(s,t)=1⟺s\in t$ (set membership)

Under this interpretation, the formula becomes:

This can be interpreted as:

“There does not exist a set $x$ such that for all sets $y$, $y$ is a member of $x$ if and only if $y$ is not a member of itself.”

In simpler terms: This denies the existence of a set that contains precisely those sets that are not members of themselves. This is the crux of Russell’s Paradox. Let’s analyze why such a set leads to a contradiction:

1. Hypothetical Existence: Suppose such a set $x$ exists. Then, for any set $y$, either $y\in x$ or $y\notin x$.

2. The Crucial Test: Consider y = x: What happens when we apply this rule to the set $x$ itself?

3. Case 1: Self-Membership ($x\in x$): If $x$ is a member of itself, then by the very definition of x (containing only sets that do not contain themselves), $x$ should not be a member of itself. Contradiction!

4. Case 2: Non-Self-Membership ($x\notin x$): Conversely, if $x$ is not a member of itself, then according to the definition of $x$ (containing all sets that do not contain themselves), it must contain itself. Contradiction again!

Resolution: Both possibilities lead to contradictions. Therefore, the initial assumption—that such a set $x$ exists—must be false. Our tautology precisely captures this impossibility, formally expressing the resolution of Russell’s paradox.

Example 2: Cantor’s Diagonalization and Uncountability

Our tautology also connects to Cantor’s diagonalization argument, a powerful technique used to prove the uncountability of certain infinite sets, like the set of all infinite binary sequences.

Cantor’s Argument (Brief Review):

The goal is to show that the set of natural numbers, $\mathbb{N}$, is smaller than the set of infinite binary sequences, $\{0,1{\}}^{\infty }$ (denoted as $\mathbb{N}\prec \{0,1{\}}^{\infty }$). The proof proceeds by contradiction:

1. Assumption of Countability: Assume a bijection exists between $\mathbb{N}$ and $\{0,1{\}}^{\infty }$, implying we can list all infinite binary sequences:

   s_1: b_11 b_12 b_13 ...
   s_2: b_21 b_22 b_23 ...
   s_3: b_31 b_32 b_33 ...
   ...
   

   where each $b_{ij}$ is either 0 or 1.

2. Diagonalization: Constructing the “Rogue” Sequence: Cantor cleverly constructs a new sequence s’ by flipping the diagonal bits: $s_i^{\prime }=1-b_{ii}$. This new sequence differs from every sequence in the list in at least one position (the i-th position for sequence $s_i$).

3. The Contradiction: s’ is a valid infinite binary sequence, yet it’s not in our supposedly complete list. This contradicts the initial assumption of a bijection.

Connecting to the Tautology:

• Universe: $U=\mathbb{N}$ (natural numbers)
• Predicate: $P(s,t)=1⟺\text{the }s\text{-th bit of the }t\text{-th sequence is 1}$

The formula $\neg \exists x\forall y(P(y,x)⟺\neg P(y,y))$ now translates to:

“There is no natural number $x$ (representing a sequence) such that for all natural numbers $y$ (representing bit positions), the $y$-th bit of the $x$-th sequence is 1 if and only if the $y$-th bit of the $y$-th sequence is 0.”

The Deeper Meaning: This statement perfectly encapsulates the impossibility of “capturing” all infinite binary sequences in a countable list. The tautology asserts that no sequence can be constructed (as Cantor did) that systematically differs from every other sequence in a predictable way. It reflects the core principle of diagonalization: any attempt to enumerate all infinite binary sequences will inevitably miss at least one.

Example 3: Existence of Uncomputable Functions

Our tautology can also be interpreted to demonstrate the existence of uncomputable functions, a fundamental concept in computer science with profound implications for what computers can and cannot do.

• Universe: $U=\{0,1{\}}^{\ast }$ (all finite binary strings, representing programs). We assume a fixed programming language where programs take a single binary string as input and output a single bit (0 or 1).
• Predicate: $P(s,t)=1⟺\text{program }t\text{ outputs 1 on input }s$.

The formula $\neg \exists x\forall y(P(y,x)⟺\neg P(y,y))$ becomes:

“There is no program $x$ that acts as a perfect complementer for all programs $y$ when given their own code as input.”

While this relates to the Halting Problem, we’re exploring a more general concept of uncomputability here. A perfect complementer would be a program that could flawlessly determine the opposite output of any program when fed its own code.

Proof by Contradiction: The Impossibility of a Perfect Complementer

Let’s rigorously prove the non-existence of such a complementer program using our tautology:

1. The Hypothetical Complementer: Assume, for the sake of contradiction, that a program $H$ exists such that for any program $y$, $H(y)$ simulates $y(y)$ and outputs the opposite. If $y(y)$ outputs 1, $H(y)$ outputs 0. If $y(y)$ outputs 0, $H(y)$ outputs 1. If $y(y)$ doesn’t halt, neither does $H(y)$.

2. Self-Reference: The crucial step is to consider $H(H)$ — what happens when we feed $H$ its own code?

3. Case 1: $H(H)$ outputs 1: If $H(H)$ outputs 1, then by $H$‘s definition, $H$ simulating itself ($H(H)$) must output 0 (or not halt). This is a blatant contradiction! $H(H)$ cannot simultaneously be 1 and 0 (or not halt).

4. Case 2: $H(H)$ outputs 0 (or doesn’t halt): The same logic applies. If $H(H)$ outputs 0 (or doesn’t halt), then $H$‘s definition dictates that $H(H)$ should have output 1. Contradiction again!

5. The Inevitable Conclusion: $H$ Cannot Exist: Both cases lead to contradictions, dismantling our initial assumption. No program $H$ can act as a perfect complementer.

6. Uncomputable Functions Emerge: This impossibility directly implies the existence of uncomputable functions. The function that $H$ was meant to compute – perfectly complementing any program’s self-application – is uncomputable. No algorithm can solve this problem for all possible inputs. This result highlights fundamental limits on the power of computation.

   

Implications for Firewalls: An Undecidable Problem

The existence of uncomputable functions has significant practical consequences, particularly for network security. Firewalls attempt to differentiate between benign and malicious network traffic, essentially trying to decide if a given program (or code segment) will behave safely.

The Undecidable Challenge: This task, however, is analogous to the Halting Problem and is therefore undecidable in the general case. No firewall can perfectly classify all possible programs as safe or unsafe.

Inherent Limitations: This limitation isn’t a flaw in firewall design, but a consequence of the fundamental limits of computation revealed by our tautology. Some malicious code will inevitably slip through, while some benign code might be erroneously blocked.

Limitations of Predicate Logic (First-Order Logic)

While predicate logic (also known as first-order logic) is a powerful tool for expressing and reasoning about mathematical statements, it has inherent limitations. One key limitation relates to the expressiveness of quantifiers.

In predicate logic, quantifiers ($\forall$ and $\exists$) can only range over individuals within the universe of discourse. We can quantify over objects, but we cannot quantify over properties or relations (represented by predicates) or functions.

Expressing Dependencies between Quantifiers

Consider the formula $\forall w\forall x\exists y\exists zF(w,x,y,z)$. This states that for all $w$ and $x$, there exist $y$ and $z$ such that $F(w,x,y,z)$ holds. However, this formula doesn’t capture potential dependencies between the quantifiers. We might want to express that $y$ depends only on $w$, and $z$ depends only on $x$, while the overall truth of $F$ depends on all four variables. In other words, we’d like to express something like: “For all $w$, there exists a $y$ (dependent on $w$), and for all $x$, there exists a $z$ (dependent on $x$) such that $F(w,x,y,z)$ holds.”

Standard predicate logic doesn’t allow us to directly express this dependency. The order of quantifiers matters, but we can’t explicitly specify how the existentially quantified variables depend on the universally quantified ones.

The Temptation of Quantifying over Functions

One might be tempted to introduce function symbols to capture these dependencies, similar to how we use Skolem functions. We might try to write something like:

$\exists f\exists g\forall w\forall xF(w,x,f(w),g(x))$

This formula attempts to express the desired dependency: $y$ is determined by a function $f$ applied to $w$, and $z$ is determined by a function $g$ applied to $x$. However, this is not a valid first-order logic formula. In first-order logic, we cannot quantify over functions. The quantifiers $\exists$ and $\forall$ can only range over individuals in the universe, not over functions or predicates themselves.

Second-Order Logic (and Higher)

To express such statements about functions or predicates, we need a more powerful logic: second-order logic. Second-order logic allows quantification over relations and functions, enabling us to express dependencies between quantifiers directly. In second-order logic, the formula $\exists f\exists g\forall w\forall xF(w,x,f(w),g(x))$ would be well-formed and would capture the intended meaning. However, constructing and working with second-order logic comes with increased complexity.

This distinction between quantifying over individuals (first-order), relations/functions (second-order), and so on, leads to a hierarchy of higher-order logics. Each level in the hierarchy increases expressiveness but also increases complexity. While higher-order logics can capture more nuanced mathematical concepts, first-order logic remains a widely used and powerful tool due to its balance between expressiveness and tractability.

Calculi: Formalizing Proof Systems

Our goal is to formalize proof systems within logic, creating a clear and rigorous way to verify the validity of proofs. This structured approach is what we call a calculus. A calculus provides a set of rules for manipulating formulas and deriving new formulas from existing ones.

Defining Rules

A calculus consists of a set of derivation rules. A derivation rule specifies how to derive a new formula (the conclusion) from a set of existing formulas (the premises). Mathematically, a rule $R$ can be viewed as a relation between sets of formulas. If $R$ relates a set of formulas $H=\{H_1,H_2,...,H_k\}$ to a formula $H_{k+1}$, we can write this as $H{⊢}_R{H}_{k+1}$. This notation indicates that $H_{k+1}$ can be derived from the set $H$ using the rule $R$.

• Example: A rule $R$ might be defined as $\{F\to G,F\to H\}{⊢}_{R}F\to (G\wedge H)$. This rule allows us to derive the formula $F\to (G\wedge H)$ if we already have the formulas $F\to G$ and $F\to H$.

Rule Validation

To validate a derivation rule, we need to ensure its correctness. This means that for any interpretation $\mathcal{A}$, if all the premises are true under $\mathcal{A}$, then the conclusion must also be true under $\mathcal{A}$. In other words, the rule must preserve truth under all interpretations.

Calculi and Derivation

A calculus $K$ is a set of derivation rules: $K=\{R_1,R_2,...,R_s\}$. Given a set of formulas $M$ and a formula $G$, we say that $G$ is derivable from $M$ within the calculus $K$, denoted as $M{⊢}_{K}G$, if and only if there exists a finite sequence of rule applications that leads from the formulas in $M$ to the formula $G$. This sequence represents a derivation or proof of $G$ from $M$.

It’s important to note the concept of finite composition of rules. Formally, $M{⊢}_{K}G$ means there’s a finite sequence of formulas $F_1,F_2,\dots ,F_n$ where $F_n=G$, and each $F_i$ is either an element of $M$ or is derived from some previous formulas in the sequence using a rule from $K$. This notion of a sequence of rule applications, each producing a new formula from earlier ones, is fundamental to Hilbert-style calculi. There are other types of calculi where the history of the derivation matters, but in Hilbert-style calculi only the final result $M{⊢}_{K}G$ matters.

Hilbert-style Calculi

The type of calculi we’ve described, based on sets of derivation rules and sequences of rule applications, is known as Hilbert-style calculi. Other types of calculi exist, such as Gentzen-style calculi (sequent calculi), which explicitly represent the derivation history using sequents.

Correctness (Soundness) and Completeness of a Calculus

A well-defined calculus should be both correct (sound) and complete.

• Correctness (Soundness): If a formula $G$ is derivable from a set of formulas $M$ within the calculus $K$ ($M{⊢}_{K}G$), then $G$ must be a logical consequence of $M$ ($M\models G$). This ensures that the calculus only derives true statements. Formally: $M{⊢}_{K}G⟹M\models G$.

• Completeness: If a formula $G$ is a logical consequence of a set of formulas $M$ ($M\models G$), then $G$ must be derivable from $M$ within the calculus $K$ ($M{⊢}_{K}G$). This ensures that the calculus can derive every true statement. Formally: $M\models G⟹M{⊢}_{K}G$.

These properties are crucial for ensuring that the calculus accurately captures the notion of logical consequence. A sound and complete calculus provides a reliable tool for proving theorems and reasoning about logical statements.

Continue here: 26 Syntactic Derivation vs Semantic Entailment, Logic Calculus, Sequent Calculus, Resolution Calculus