24 Evaluating and Proving Formulas in Predicate Logic, Equivalences, Transformations, Variable Substitution, Universal Instantiation, Equality, Prenex Normal Form

Lecture from: 09.12.2024 | Video: Videos ETHZ

Recap: Formalizing Logic and Proof Systems

In previous lectures, we established the framework for formalizing logic and proof systems. Recall that a proof system $\Pi =(\mathcal{S},\mathcal{P},\tau ,\varphi )$ comprises:

• Statements ($\mathcal{S}$): The set of all possible statements, which can be formalized e.g., as bitstrings.
• Proofs ($\mathcal{P}$): The set of all possible proofs.
• Semantic Interpretation Function ($\tau$): Assigns truth values to statements ($\tau :\mathcal{S}\to \{0,1\}$).
• Proof Verification Function ($\varphi$): Checks the validity of proofs ($\varphi :\mathcal{S}\times \mathcal{P}\to \{0,1\}$).

We focused on statements of the form $M\models G$, expressing logical consequence: $G$ is derivable from the set of formulas $M$.

Syntax and Semantics of Formulas

We’ve explored the syntax and semantics of formulas, defining how they’re constructed and interpreted.

• Syntax: Defines the allowed structure of formulas, ensuring well-formedness.

• Semantics: Assigns meaning to formulas through interpretations.

  • Interpretations ($\mathcal{A}$): Define a universe ($U^{\mathcal{A}}$) and assign meanings to predicate symbols, function symbols, and free variables.
  • Valuation Function ($\sigma$ or $\mathcal{A}(F)$): Determines the truth value of a formula under a given interpretation. It checks if $\mathcal{A}$ models $F$.

Key Concepts and Properties

We’ve also introduced important logical concepts:

• Satisfiability: A formula is satisfiable if there exists an interpretation that makes it true.
• Insatisfiability: A formula is unsatisfiable if it’s false under every interpretation.
• Tautology: A formula is a tautology if it’s true under every interpretation.
• Logical Consequence (Entailment): $\{F_1,...,F_k\}\models G$ means $G$ is true under every interpretation where all $F_i$ are true.

Defining Logical Consequence

It’s essential to understand how we define logical consequence. We use natural language (“for all interpretations…”) to define this concept precisely. While we use symbols like $\models$ to represent logical consequence, the underlying definition relies on natural language.

The Role of Natural Language

We could imagine a “meta-logic” with symbols representing “for all interpretations,” but ultimately, even that meta-logic would need to be grounded in natural language. At some level, we rely on human understanding to interpret the meaning of logical symbols and concepts.

Unsatisfiability and Logical Consequence

Last time we established a connection between unsatisfiability and logical consequence:

If $\{F,\neg G\}$ is unsatisfiable, then $F\models G$.

Proof:

This proof relies on our natural language understanding of logical concepts:

1. $\{F,\neg G\}$ is unsatisfiable: No interpretation makes both $F$ and $\neg G$ true simultaneously.
2. Suppose $\mathcal{A}(F)=1$: For any interpretation $\mathcal{A}$ that makes $F$ true, $\neg G$ must be false (due to the unsatisfiability of $\{F,\neg G\}$).
3. Therefore, $\mathcal{A}(G)=1$: If $\neg G$ is false, then $G$ must be true.
4. Hence, $F\models G$: Since any interpretation that makes $F$ true also makes $G$ true, $G$ is a logical consequence of $F$.

Evaluating Predicate Logic Formulas Under Interpretations

Let’s illustrate the process of evaluating predicate logic formulas under specific interpretations using examples.

Example 1: Evaluating a Formula with a Function

Consider the formula $F=\exists xP(f(x))$. We can represent its structure with a syntax tree:

Now, let’s define an interpretation $\mathcal{A}$:

• $\mathcal{A}$:
  • $U^{\mathcal{A}}=\mathbb{N}$ (natural numbers)
  • $P^{\mathcal{A}}(n)=1⟺n\text{ is even}$
  • $f^{\mathcal{A}}(n)=n+5$

This is a matching interpretation, as it provides meanings for all free variables (the predicate symbol $P$ and the function symbol $f$). To evaluate $\mathcal{A}(F)$, we need to determine if there exists an $x\in \mathbb{N}$ such that $P(f(x))$ is true under $\mathcal{A}$.

• Evaluation:
  1. We are looking for an $x$ such that $f^{\mathcal{A}}(x)$ is even.
  2. $f^{\mathcal{A}}(x)=x+5$.
  3. If we choose $x=1$, then $f^{\mathcal{A}}(1)=1+5=6$, which is even.
  4. Thus, $P^{\mathcal{A}}(f^{\mathcal{A}}(1))=P^{\mathcal{A}}(6)=1$.
  5. Since we found an $x$ that satisfies the formula, $\mathcal{A}(F)=1$.

Example 2: Proving Logical Consequence

Now, let’s analyze logical consequence. Consider the statement:

Is this statement true? Intuitively, it seems plausible. If there exists an $x$ such that $P(f(x))$ is true, then there must exist some value in the universe (namely, $f(x)$) for which $P$ is true. Thus the statement $\exists xP(x)$ is also true. The left-hand side has a more restricted universe than the right hand side. The universe of the left hand side are values that can result from an application of $f$. Thus, if the LHS is true then surely the RHS which has less restriction on the universe is also true.

Formal Proof

To prove this formally, we need to show that for any interpretation $\mathcal{A}$ where $\mathcal{A}(\exists xP(f(x)))=1$, it must also be the case that $\mathcal{A}(\exists xP(x))=1$.

1. Assume $\mathcal{A}(\exists xP(f(x)))=1$: This means there exists a $u\in U^{\mathcal{A}}$ such that ${\mathcal{A}}_{[x\to u]}(P(f(x)))=1$.
2. Evaluate the term: This means $P^{\mathcal{A}}(f^{\mathcal{A}}(u))=1$.
3. Let $v=f^{\mathcal{A}}(u)$: Since $f^{\mathcal{A}}$ maps elements from the universe to the universe, $v$ must also belong to $U^{\mathcal{A}}$. Furthermore from step 2, $P^{\mathcal{A}}(v)=1$.
4. Therefore, ${\mathcal{A}}_{[x\to v]}(P(x))=1$: This means $P^{\mathcal{A}}(v)=1$, which we already know from step 3.
5. Hence, $\mathcal{A}(\exists xP(x))=1$: Since we found a $v$ such that $P(x)$ holds under modified interpretation ${\mathcal{A}}_{[x\to v]}$, this means there exists such a value hence $\exists xP(x)$ must be true.

Since we’ve shown that if $\mathcal{A}(\exists xP(f(x)))=1$, then $\mathcal{A}(\exists xP(x))=1$ for any interpretation $\mathcal{A}$, we have proven the logical consequence: $\exists xP(f(x))\models \exists xP(x)$.

Equivalences in Predicate Logic and Parameterized Statements

Recall that the valuation function $\sigma (F,\mathcal{A})$, or $\mathcal{A}(F)$, is defined recursively. Evaluating a formula under an interpretation might involve evaluating subformulas under modified interpretations. For example, $\mathcal{A}(\forall xG)$ is determined by evaluating ${\mathcal{A}}_{[x\to u]}(G)$ for all $u\in U^{\mathcal{A}}$.

We’ll now explore and prove some equivalences in predicate logic. These equivalences allow us to manipulate and simplify formulas, which is crucial for automated reasoning and theorem proving.

Lemma 6.7 and Parameterized Statements:

Before diving into the main equivalence, let’s establish a helpful principle regarding parameterized statements. We often encounter statements that depend on a parameter. Let $S_u$ and $T_u$ be statements parameterized by $u\in U$.

Parameterized Statements

If $S_u$ is true for all $u\in U$ and $T_u$ is true for all $u\in U$, then the statement ”($S_u$ and $T_u$)” is also true for all $u\in U$.

This principle seems obvious but is formally important for our subsequent proof.

Proving an Equivalence (Lemma 6.7.8 Example)

Consider the following equivalence from Lemma 6.7:

where $x$ is not a free variable in $H$. Let’s prove this equivalence.

Proof of Equivalence

We’ll show that the two formulas have the same truth value under any interpretation $\mathcal{A}$.

1. $\mathcal{A}((\forall xF)\wedge H)=1$: This means $\mathcal{A}(\forall xF)=1$ and $\mathcal{A}(H)=1$.
2. $\mathcal{A}(\forall xF)=1$: This means ${\mathcal{A}}_{[x\to u]}(F)=1$ for all $u\in U^{\mathcal{A}}$.
3. $\mathcal{A}(H)=1$: Since $x$ is not free in $H$, the truth value of $H$ is unaffected by modifying the interpretation with respect to $x$. Thus, ${\mathcal{A}}_{[x\to u]}(H)=\mathcal{A}(H)=1$ for all $u\in U^{\mathcal{A}}$.
4. Combining (2) and (3): Using the principle of parameterized statements (with $S_u={\mathcal{A}}_{[x\to u]}(F)=1$ and $T_u={\mathcal{A}}_{[x\to u]}(H)=1$), we have ${\mathcal{A}}_{[x\to u]}(F)=1$ and ${\mathcal{A}}_{[x\to u]}(H)=1$ for all $u\in U^{\mathcal{A}}$.
5. Semantics of $\wedge$: From (4), we have ${\mathcal{A}}_{[x\to u]}(F\wedge H)=1$ for all $u\in U^{\mathcal{A}}$.
6. Semantics of $\forall$: From (5), we have $\mathcal{A}(\forall x(F\wedge H))=1$.

Since we’ve shown that $\mathcal{A}((\forall xF)\wedge H)=1$ if and only if $\mathcal{A}(\forall x(F\wedge H))=1$ for any interpretation $\mathcal{A}$, the two formulas are equivalent.

Transforming Formulas and Equivalences

We often want to transform formulas into equivalent forms for simplification or to apply specific proof techniques. These transformations rely on logical equivalences. For example, consider the equivalence:

We can demonstrate this equivalence using transformations based on Lemma 6.7 and other logical equivalences:

1. Implication Elimination: $(\exists xP(x))\to Q(y)\equiv \neg (\exists xP(x))\vee Q(y)$
2. Quantifier Negation and De Morgan’s Law: $\neg (\exists xP(x))\vee Q(y)\equiv (\forall x\neg P(x))\vee Q(y)$
3. Quantifier Distribution (Lemma 6.7 variant): $(\forall x\neg P(x))\vee Q(y)\equiv \forall x(\neg P(x)\vee Q(y))$ (since $x$ is not free in $Q(y)$)
4. Implication Introduction: $\forall x(\neg P(x)\vee Q(y))\equiv \forall x(P(x)\to Q(y))$

Variable Substitution and Universal Instantiation

Variable Substitution:

We define the notation $F[x/t]$ to represent the formula obtained by replacing all free occurrences of the variable $x$ in formula $F$ with the term $t$.

• Example: If $F=\forall y(Q(x,y,z))$ and $t=f(g(w),h(w))$, then $F[x/t]=\forall y(Q(f(g(w),h(w)),y,z))$.
• Quantifier Renaming Another example $\forall xG\equiv \forall yG[x/y]$. The reason this holds is due to how the semantics are defined.

Universal Instantiation:

Universal instantiation is a crucial inference rule. It states:

This means that if a formula $F$ holds for all $x$, then it must also hold for any specific term $t$ substituted for $x$. This can be viewed as a syntactic derivation rule ($⊢$) in a sound proof system.

Extending Predicate Logic with Equality

We extend predicate logic with the equality symbol ($=$).

• Syntax: If $t_1$ and $t_2$ are terms, then $(t_1=t_2)$ is a formula.
• Semantics: $\mathcal{A}(t_1=t_2)=1$ if and only if $\mathcal{A}(t_1)$ and $\mathcal{A}(t_2)$ are the same element in the universe $U^{\mathcal{A}}$.

While we use the same symbol ($=$) for equality within the logic and equality within the universe of the interpretation, these are conceptually distinct. We assume we have a notion of equality within the universe (e.g., equality of natural numbers, equality of sets). The equality symbol within the logic refers to this underlying equality in the universe. If we base our logic on axiomatic set theory we have a very rigorous notion of equality, two sets are equal if they are subsets of each other.

Example: Group Axioms

Using equality, we can express the group axioms:

• G1 (Associativity): $\forall x\forall y\forall z(f(f(x,y),z)=f(x,f(y,z)))$
• G2’ (Right Identity): $\forall x(f(x,a)=x)$
• G3’ (Right Inverse): $\forall x(f(x,g(x))=a)$

Let $GA=\{\text{G1, G2, G3}\}$ be the set of these group axioms.

Proving Group Properties from Minimal Axioms (Standard Notation)

We will now show how these minimal axioms entail other important group properties. First, we use standard algebraic notation, then we’ll revisit the proof using predicate logic.

1. Left Inverse: We want to show that every element has a left inverse. $\forall x\exists y(y\circ x=e)$. Let $x$ be an arbitrary element. By G3 we have a right inverse $x^{\prime }$ such that $x\circ x^{\prime }=e$. Then, there exists also $(x^{\prime }{)}^{\prime }$ by G3 such that $x^{\prime }\circ (x^{\prime }{)}^{\prime }=e$. Thus: $(x^{\prime }\circ x)\circ x^{\prime }{=}_{\text{G1}}{x}^{\prime }\circ (x\circ x^{\prime })=x^{\prime }\circ e{=}_{\text{G2}}{x}^{\prime }$. Multiplying both sides with $(x^{\prime }{)}^{\prime }$ yields $((x^{\prime }\circ x)\circ x^{\prime })\circ (x^{\prime }{)}^{\prime }=x^{\prime }\circ (x^{\prime }{)}^{\prime }=e$ thus $(x^{\prime }\circ x)\circ (x^{\prime }\circ (x^{\prime }{)}^{\prime }){=}_{\text{G1}}(x^{\prime }\circ x)\circ e=x^{\prime }\circ x=e$. Thus $x^{\prime }$ is also a left inverse of $x$.

2. Left Identity: We want to show that the right identity $e$ is also a left identity: $\forall x(e\circ x=x)$ Let $x$ be an arbitrary element. $e\circ x=(x\circ x^{\prime })\circ x{=}_{\text{G1}}x\circ (x^{\prime }\circ x)=x\circ e{=}_{\text{G2}}x$ which proves the claim.

3. Uniqueness of Identity: Suppose there exists another identity $e^{\prime }$ such that $e^{\prime }\circ x=x\circ e^{\prime }=x$. Since $e^{\prime }$ is an identity, we have $e\circ e^{\prime }=e$. But since e is also an identity we also have $e\circ e^{\prime }=e^{\prime }$, thus $e=e^{\prime }$, proving uniqueness.

4. Uniqueness of Inverse: Let $x^{\prime \prime }$ be another inverse of $x$, meaning $x^{\prime \prime }\circ x=x\circ x^{\prime \prime }=e$. Since $x^{\prime }$ is an inverse of $x$, we also have $x\circ x^{\prime }=e$. Thus $x^{\prime \prime }\circ x=e$. Multiplying with $x^{\prime }$ gives us $(x^{\prime \prime }\circ x)\circ x^{\prime }=e\circ x^{\prime }=x^{\prime }$ thus $x^{\prime \prime }\circ (x\circ x^{\prime })=x^{\prime \prime }\circ e=x^{\prime \prime }=x^{\prime }$ thus $x^{\prime \prime }=x^{\prime }$, proving uniqueness.

Predicate Logic Proof of Left Identity (Predicate Functions Notation)

Now, we’ll prove the Left Identity property using a more formal approach with predicate logic, assuming only G1, G2’, and G3’. We want to show $GA\models \forall x(f(a,x)=x)$.

Let $x$ be an arbitrary element. Then $f(x,g(x))=a$ (right inverse) We multiply both sides with $x$ to get $f(f(x,g(x)),x)=f(a,x)$. Then, using associativity we also have $f(x,f(g(x),x))=f(a,x)$.

We know there exists $g(w)$ for all elements $w$ in our universe such that $f(w,g(w))=a$. Likewise such a $g(g(x))$ exists. Multiplying $f(g(x),x)=w$ with $g(g(x))$ gives us $f(g(g(x)),f(g(x),x))=f(g(g(x)),w)$. Using associativity we get $f(f(g(g(x)),g(x)),x)=f(f(g(g(x)),g(x)),x)$. By G3’ we know $f(g(x),x)=w$ and $f(g(w),w)=a$, using this we get $f(a,x)=f(x,f(g(x),x))$.

Since we proved that every element has a left inverse and we know that $f(x,f(g(x),x))=f(a,x)$ and $f(g(x),x)=e$, we also know $x\circ e=x$ and hence $f(x,e)=x$, thus $f(a,x)=x$.

Prenex Normal Form (PNF)

In predicate logic, it’s often beneficial to express formulas in a standardized format called Prenex Normal Form (PNF). A formula is in PNF if all its quantifiers appear at the beginning, followed by a quantifier-free part. This structure simplifies many logical operations and is essential for some automated reasoning techniques.

A key question is whether every predicate logic formula can be converted into an equivalent formula in PNF. The answer is yes, and we’ll explore the process of converting formulas to PNF.

Variable Renaming and Clashes

A crucial step in the conversion process is handling potential variable clashes. A clash occurs when the same variable name is used for different purposes (e.g., bound by different quantifiers or appearing both free and bound).

• Example: In the formula $\neg \forall xP(x,y)\wedge \exists yQ(x,y,z)$, the variable $y$ appears both free (in $P(x,y)$) and bound (by $\exists y$). This can lead to ambiguities during transformations.

To avoid clashes, we rename variables. We use the notation $[x/u]$ to denote the substitution of all free occurrences of variable $x$ with a new variable $u$.

Conversion to PNF: An Example

Let’s convert $\neg \forall xP(x,y)\wedge \exists yQ(x,y,z)$ to PNF.

1. Original Formula (with syntax tree):

   

2. Rename Bound Variables to Eliminate Clashes: We rename the bound $y$ in $\exists yQ(x,y,z)$ with $v$. And since we also have a $\forall x$ on the left branch, which is implicitly also applied on the second conjunct on the right, we replace $x$ by $u$ in $Q(x,y,z)$. This gives us: $\neg \forall xP(x,y)\wedge \exists vQ(u,v,z)$. Note that the $x$ on the left and the $u$ are distinct and thus are two independent free variables. We have no more clashes. This is the bereinigte (cleaned-up) form. This is just for us to see that we are dealing with completely independent variables.

3. Move Quantifiers to the Front:

   We can move the quantifiers $\forall x$ and $\exists v$ to the front. Since the $x$ is not free in the second conjunct we can put it to the left or right. Since the variable names do not clash we can put the quantifiers in any order. One possible PNF is $\forall x\exists v(\neg P(x,y)\wedge Q(u,v,z))$. Note that we have $\neg \forall xP(x,y)\equiv \exists x\neg P(x,y)$. Thus another way to write this is $\exists x\neg P(x,y)\wedge \exists vQ(u,v,z)$. Then moving quantifiers to front yields $\exists x\exists v\exists u(\neg P(x,y)\wedge Q(u,v,z))$ where $y,z$ are free.

Future Directions: Skolem Normal Form

In future lectures, we’ll encounter another normal form called Skolem Normal Form. While converting a formula to Skolem Normal Form doesn’t preserve full equivalence ($\equiv$), it does preserve satisfiability. This means that a formula is satisfiable if and only if its Skolem Normal Form is satisfiable. This weaker notion of equivalence is sufficient for certain proof techniques, particularly those based on resolution. The key transformation in Skolemization is eliminating existential quantifiers ($\exists$) by introducing new function symbols (Skolem functions).

Continue here: 25 Skolem Normal Form, Russell’s Paradox, Cantor’s Diagonalization, Existence of Uncomputable Functions, Higher-Order Logic, Calculi