26 Syntactic Derivation vs Semantic Entailment, Logic Calculus, Sequent Calculus, Resolution Calculus

Lecture from: 16.12.2024 | Video: Videos ETHZ

Example: Syntactic Derivation vs. Semantic Entailment

Lets recap the relationship between syntactic derivation ($⊢$) and semantic entailment ($\models$), focusing on how to determine if a given derivation is sound.

Soundness asks whether a syntactically correct derivation using a set of rules ($K$) also implies a semantically valid entailment. In simpler terms:

If we can derive $Y$ from $X$ using the rules of our system ($X{⊢}_{K}Y$), does it logically follow that $X$ entails $Y$ ($X\models Y$)?

We’ll explore this through examples, analyzing whether the given derivations are sound.

Example 1:

Derivation: $\{F,\neg F\}{⊢}_{R_1}G$

Question: Is this derivation sound? Does $\{F,\neg F\}\models G$ hold?

Answer: Yes, this derivation is sound.

Reasoning: The left-hand side of the entailment, $\{F,\neg F\}$, represents a contradiction. There is no interpretation $\mathcal{A}$ that can make both $F$ and $\neg F$ true simultaneously. Since the premise is always false, the implication holds vacuously. In other words, a contradiction logically entails anything.

Example 2:

Derivation: $F\to G{⊢}_{R_2}G$

Question: Is this derivation sound? Does $F\to G\models G$ hold?

Answer: No, this derivation is not sound.

Reasoning: We need to find a counterexample – an interpretation where $F\to G$ is true, but $G$ is false.

Counterexample: Let $\mathcal{A}(F)=0$ and $\mathcal{A}(G)=0$. Then $\mathcal{A}(F\to G)=1$, but $\mathcal{A}(G)=0$. Therefore, $F\to G/\models G$.

Example 3:

Derivation: $\varnothing {⊢}_{R_3}(F\to G)\wedge (G\to F)$

Question: Is this derivation sound? Does $\varnothing \models (F\to G)\wedge (G\to F)$ hold? In other words, is $(F\to G)\wedge (G\to F)$ a tautology?

Answer: No, this derivation is not sound.

Reasoning: We need to find a counterexample where $(F\to G)\wedge (G\to F)$ is false.

Counterexample: Let $\mathcal{A}(F)=1$ and $\mathcal{A}(G)=0$. Then $\mathcal{A}(F\to G)=0$, and consequently, $\mathcal{A}((F\to G)\wedge (G\to F))=0$. Therefore, $(F\to G)\wedge (G\to F)$ is not a tautology.

Example 4:

Derivation: $\{F\vee G,\neg G\}{⊢}_{R_4}F\vee H$

Question: Is this derivation sound? Does $\{F\vee G,\neg G\}\models F\vee H$ hold?

Answer: Yes, this derivation is sound.

Reasoning: Let’s consider an arbitrary interpretation $\mathcal{A}$ where both $F\vee G$ and $\neg G$ are true. If $\mathcal{A}(F\vee G)=1$, then either $\mathcal{A}(F)=1$ or $\mathcal{A}(G)=1$ (or both). Since $\mathcal{A}(\neg G)=1$, we know $\mathcal{A}(G)=0$. Therefore, if both premises are true, it must be the case that $\mathcal{A}(F)=1$. If $\mathcal{A}(F)=1$, then $\mathcal{A}(F\vee H)=1$, regardless of the truth value of $H$. Thus, under any interpretation where the premises are true, the conclusion is also true.

General Approach

To determine the soundness of a derivation $X{⊢}_{K}Y$, we need to check if $X\models Y$ holds. This involves:

1. Understanding the Rules: Knowing the derivation rules ($K$) used in the syntactic derivation.
2. Considering Interpretations: Analyzing whether there exists any interpretation $\mathcal{A}$ where all formulas in $X$ are true, but $Y$ is false.
3. Constructing Counterexamples: If such an interpretation exists, we’ve found a counterexample, and the derivation is not sound.
4. Demonstrating Entailment: If no such interpretation exists, the derivation is sound, and we need to demonstrate why $X\models Y$ holds, usually by considering the truth conditions of the formulas involved.

Example: Proving with a Logic Calculus

Let’s consider a logic calculus with the following derivation rules:

• R1: $\{F\to G,F\}{⊢}_{R_1}G$
• R2: $\varnothing {⊢}_{R_2}F\to (G\to F)$
• R3: $\varnothing {⊢}_{R_3}(\neg F\to \neg G)\to ((\neg F\to G)\to F)$

We are given that these rules are sound.

Goal: Show that $\{A,\neg A\}{⊢}_{K}B$ is derivable using these rules, where $K=\{R_1,R_2,R_3\}$.

Note: We already know that $\{A,\neg A\}\models B$ holds (a contradiction entails anything). Our task here is to demonstrate this derivation syntactically using the given rules.

Derivation

Since the final goal is to derive $B$, and R1 is the only rule that can directly derive a formula that is not an implication, our final step will likely involve R1.

Let’s work backward, aiming to use R3 and R2 to construct the necessary premises for R1.

1. $\varnothing {⊢}_{R_3}(\neg B\to \neg A)\to ((\neg B\to A)\to B)$ (1)

   • This is an instance of R3, with $F=B$ and $G=A$.

2. $\varnothing {⊢}_{R_2}\neg A\to (\neg B\to \neg A)$ (2)

   • This is an instance of R2, with $F=\neg A$ and $G=\neg B$.

3. $\{(2),\neg A\}{⊢}_{R_1}\neg B\to \neg A$ (3)

   • From (2) and the premise $\neg A$, we can derive $\neg B\to \neg A$ using R1.

4. $\{(1),(3)\}{⊢}_{R_1}(\neg B\to A)\to B$ (4)

   • From (1) and (3), we can derive $(\neg B\to A)\to B$ using R1.

5. $\varnothing {⊢}_{R_2}A\to (\neg B\to A)$ (5)

   • This is an instance of R2, with $F=A$ and $G=\neg B$.

6. $\{(5),A\}{⊢}_{R_1}\neg B\to A$ (6)

   • From (5) and the premise $A$, we can derive $\neg B\to A$ using R1.

7. $\{(4),(6)\}{⊢}_{R_1}B$ (7)

   • From (4) and (6), we can derive $B$ using R1.

Final Step:

Since we have derived $B$ using the premises $\{A,\neg A\}$ and the rules $K$, we can conclude:

$\{A,\neg A\}{⊢}_{K}B$

Derived Rule:

This derivation demonstrates that we could add a new rule to our calculus:

• R4: $\{F,\neg F\}{⊢}_{R_4}G$

This rule would be sound, as we’ve shown that it can be derived from the existing sound rules R1, R2, and R3.

Sequent Calculus: An Alternative to Hilbert Calculi

The calculi we’ve examined so far, where we derive new formulas from existing ones using syntactic rules, are known as Hilbert-style calculi. There are other types of calculi, including sequent calculi.

Note: We won’t delve into the details of sequent calculi or natural deduction in this course, but it’s important to be aware that alternative formalisms for logical reasoning exist. They offer different perspectives and can be more convenient for certain types of proofs or applications.

Key Difference

Instead of manipulating sets of formulas, sequent calculi operate on sequents. A sequent is a pair $(M,N)$, where $M$ and $N$ are sets of formulas. The intuitive reading of a sequent is that the conjunction of the formulas in $M$ entails the disjunction of the formulas in $N$. We could write this as $M⊢N$.

Derivation Rules

Derivation rules in a sequent calculus transform sequents into other sequents:

$(M_1,N_1),(M_2,N_2),...,(M_k,N_k){⊢}_R(M^{\prime },N^{\prime })$

A rule of this form can be read as follows:

If all sequents $(M_i,N_i)$ are given for $1\le i\le k$, then we can derive the sequent $(M^{\prime },N^{\prime })$.

This notation is similar to the notation $M⊢G$ from before, but now $M$ and $G$ themselves are sets of formulas.

Correctness

The correctness of such a rule means that if the premise sequents are valid (i.e., the conjunction of formulas on the left-hand side entails the disjunction of formulas on the right-hand side), then the conclusion sequent must also be valid.

Natural Deduction

One example of a sequent calculus is natural deduction. Natural deduction systems aim to mimic the way humans reason naturally, often using introduction and elimination rules for each logical connective.

Resolution Calculus for Propositional Logic

We’ll now explore the resolution calculus, a proof system specifically designed for formulas in Conjunctive Normal Form (CNF). Recall that a formula in CNF is a conjunction of clauses, where each clause is a disjunction of literals.

Visualizing CNF

Example:

The formula $(A\vee \neg B\vee C)\wedge (\neg A\vee C\vee D)\wedge (\neg A\vee \neg D)$ in CNF can be represented as a set of clauses:

$\mathcal{K}=\{\{A,\neg B,C\},\{\neg A,C,D\},\{\neg A,\neg D\}\}$

Clause Sets and Satisfiability

Technically, a clause set represents an equivalence class of formulas, as the order of clauses and literals within a clause doesn’t affect the formula’s meaning.

We can check the satisfiability of a clause set by finding an interpretation that makes all clauses true. For example, in the clause set above, the interpretation $\mathcal{A}(A)=1$, $\mathcal{A}(C)=1$, $\mathcal{A}(D)=0$ satisfies all clauses.

The SAT Problem

The SAT problem asks whether a given formula in CNF (or equivalently, a clause set) is satisfiable. This problem is NP-complete, meaning it’s considered computationally difficult to solve in general.

Proving Unsatisfiability

While finding a satisfying interpretation demonstrates satisfiability, proving unsatisfiability is generally much harder. There is no known efficient proof system that can provide short, easily verifiable proofs of unsatisfiability for arbitrary CNF formulas (unless $P=NP$, which is considered unlikely). This is analogous to the difficulty of proving primality versus proving compositeness by simply finding a factor.

Why Focus on Unsatisfiability?

Proving unsatisfiability is a powerful technique because it makes a statement about all possible interpretations. It asserts that no interpretation can satisfy the formula. This is a much stronger claim than demonstrating satisfiability, which only requires finding a single satisfying interpretation.

Connection to Tautologies

To check if a formula $F$ is a tautology, we can negate it ($\neg F$), convert it to CNF, and then check for unsatisfiability. If $\neg F$ in CNF is unsatisfiable, then $F$ is a tautology. This is because a formula is a tautology if and only if its negation is unsatisfiable.

The Resolution Rule

The resolution calculus for propositional logic in CNF has a single inference rule, called the resolution rule.

Rule Definition

The resolution rule states that from two clauses containing a complementary literal (one containing $L$ and the other containing $\neg L$), we can derive a new clause called the resolvent.

More formally:

Let $C_1$ and $C_2$ be two clauses, and let $L$ be a literal such that $L\in C_1$ and $\neg L\in C_2$. Then the resolvent $C$ of $C_1$ and $C_2$ with respect to $L$ is:

$C=(C_1\cup C_2)\setminus \{L,\neg L\}$

We write this as:

$\{C_1,C_2\}{⊢}_{res}C$

Example:

Consider the clauses $\{A,\neg B,C\}$ and $\{\neg A,C,D\}$. We can resolve these clauses on the literal $A$, obtaining the resolvent:

$\{\neg B,C,D\}$

Important: The resolution rule eliminates only one complementary pair of literals at a time.

Resolution and Unsatisfiability

The resolution calculus is particularly useful for proving the unsatisfiability of a clause set.

Empty Clause and Unsatisfiability

• If we can derive the empty clause (denoted by $\square$ or $\{\}$) from a clause set using the resolution rule, then the original clause set is unsatisfiable.
• An empty set of clauses is always satisfiable (it imposes no constraints) and is a tautology. An empty clause is always false and is hence unsatisfiable.

Why the Empty Clause Implies Unsatisfiability

The empty clause represents a contradiction. It’s a disjunction with no literals, meaning it cannot be satisfied by any interpretation. If we can derive the empty clause, it means the original set of clauses logically entails a contradiction, and therefore, it must be unsatisfiable. This is because the resolution rule preserves satisfiability, meaning if the resolvent is satisfiable, then the clauses from which is derived are also satisfiable, which is a contradiction, since the empty clause is not satisfiable.

In the next lecture, we will prove the soundness and completeness of the resolution calculus, demonstrating that it’s a correct and complete proof system for propositional logic in CNF.

Examples of Resolution

Example 1: Continuing the Previous Example

Let’s continue with the clause set from our previous example:

$\mathcal{K}=\{\{A,\neg B,C\},\{\neg A,C,D\},\{\neg A,\neg D\}\}$

We can apply the resolution rule as follows:

1. Resolve $\{A,\neg B,C\}$ and $\{\neg A,C,D\}$ on $A$ to get $\{\neg B,C,D\}$.
2. Resolve $\{\neg B,C,D\}$ and $\{\neg A,\neg D\}$ on $D$ to get $\{\neg A,\neg B,C\}$.

The derivation is visualized below:

Example 2: Logical Consequence

Let’s revisit the example from the beginning of the chapter:

Formulas:

1. $A\vee Z\to C$
2. $B\to A$
3. $E\to Z$
4. $(A\wedge C)\to (D\vee E)$
5. $(D\wedge A)\to Z$
6. $A\wedge B$

Question: Is $Z$ a logical consequence of this set of formulas?

Approach:

1. Convert to CNF: We’ll convert each formula to CNF.
2. Negate the Goal: Since we want to show that the formulas entail $Z$, we’ll add $\neg Z$ to our clause set.
3. Apply Resolution: We’ll apply the resolution rule repeatedly, attempting to derive the empty clause. If we succeed, it means the original set of formulas, together with $\neg Z$, is unsatisfiable, implying that the original formulas entail $Z$.

Conversion to CNF:

1. $A\vee Z\to C\equiv \neg (A\vee Z)\vee C\equiv (\neg A\wedge \neg Z)\vee C\equiv (\neg A\vee C)\wedge (\neg Z\vee C)$

   • Clauses: $\{\neg A,C\},\{\neg Z,C\}$

2. $B\to A\equiv \neg B\vee A$

   • Clause: $\{\neg B,A\}$

3. $E\to Z\equiv \neg E\vee Z$

   • Clause: $\{\neg E,Z\}$

4. $(A\wedge C)\to (D\vee E)\equiv \neg (A\wedge C)\vee (D\vee E)\equiv (\neg A\vee \neg C\vee D\vee E)$

   • Clause: $\{\neg A,\neg C,D,E\}$

5. $(D\wedge A)\to Z\equiv \neg (D\wedge A)\vee Z\equiv (\neg D\vee \neg A\vee Z)$

   • Clause: $\{\neg D,\neg A,Z\}$

6. $A\wedge B$

   • Clauses: $\{A\},\{B\}$

7. $\neg Z$ (Negated goal)

   • Clause: $\{\neg Z\}$

Clause Set:

$\mathcal{K}=\{\{\neg A,C\},\{C,\neg Z\},\{\neg B,A\},\{\neg E,Z\},\{\neg A,\neg C,D,E\},\{\neg D,\neg A,Z\},\{A\},\{B\},\{\neg Z\}\}$

Now we can apply the resolution rule to this clause set, attempting to derive the empty clause. If we succeed, we’ve proven that the original formulas entail $Z$.

Let’s apply the resolution rule.

Derivation:

Conclusion:

Since we derived the empty clause, we have shown that the set of formulas $\mathcal{K}$ is unsatisfiable. This means that the original set of formulas, together with the negation of $Z$, leads to a contradiction. Therefore, the original formulas do entail $Z$.

Limitations of Resolution

While resolution is a powerful technique, it has limitations:

• Combinatorial Explosion: The number of possible clauses that can be formed from $n$ atomic formulas is exponential (roughly $4^n$, considering that each literal can be positive, negative, absent or present both as a positive and negative). In the worst case, we might need to explore all possible resolvents before deriving the empty clause or determining that it’s not derivable.
• Efficiency: While resolution is complete (it will always find the empty clause if the formula is unsatisfiable), there’s no guarantee of efficiency. Finding a short resolution proof can be challenging. It is not guaranteed that there exists an efficient derivation, and finding an efficient derivation is even more difficult.

Open Questions:

Whether there exist more efficient, general-purpose methods for proving unsatisfiability remains a major open question in computer science. The potential existence of such methods is closely tied to the P versus NP problem.

Despite its limitations, resolution remains a fundamental technique in automated theorem proving and has practical applications in areas like software verification and artificial intelligence. It provides a systematic way to reason about propositional logic formulas in CNF and to determine their satisfiability or unsatisfiability.