Week S2.2. Logical Equivalence and Syntactic Re-writing

Order of quantifiers

Order of quantifiers

The order of quantifiers matters depending on the formula. For a sequence of same-type quantifiers, the order does not matter:

$$\forall x\forall y\varphi (x,y)\equiv \forall y\forall x\varphi (x,y)$$

For a sequence of alternating quantifiers, the order matters:

$$\exists x\forall y\varphi (x,y)\not\equiv \forall y\exists x\varphi (x,y)$$Link to original

Example: order of quantifiers

Consider $\exists x\forall y\text{AttendClass}(x,y)$ and $\forall y\exists x\text{AttendClass}(x,y)$.

If there is a student $s$ attending all classes, then each class is attended by at least a student, i.e. $s$; if each class is attended by a student, this does not imply that there is a student attending all classes.

Relationships between quantifiers

Relationships between quantifiers

Consider the formula, “no university has no student”, it is equivalent to “all universities have at least one student”, which shows that quantifiers are linked.

$$\begin{array}{c}\neg (\exists x)(\text{University}(x)\wedge \neg (\exists y)\text{Student}(y,x))\\ (\forall x)(\text{University}(x)\wedge \to (\exists y)\text{Student}(y,x))\end{array}$$

Hence we can produce the following the equivalences:

• $\neg \forall x\varphi (x)\equiv \exists x\neg \varphi (x)$
• $\neg \exists x\varphi (x)\equiv \forall x\neg \varphi (x)$

Link to original

Example 1: Interpreting Negated Formulae 1

Problem: represent and negate “there is a student attending the ELA module”

1. Encode as a formula: $\exists x\text{AttendClass}(x,ela)$
2. Obtain negation: $\neg \exists x\text{AttendClass}(x,ela)$
3. Use rules demonstrated earlier to obtain $\forall x\neg \text{AttendClass}(x,ela)$ This produces two different statements:
   • Negation: “there is no student attending the ELA module”
   • Generated from rule: “all students do not attend the ELA module”

Example 2: Interpreting Negated Formulae 2

Problem: represent and negate “all universities have at least one student”

1. Encode: $(\forall x)(\text{University}(x)\to (\exists y)\text{Student}(y,x))$
2. Negate: $\neg (\forall x)(\text{University}(x)\to (\exists y)\text{Student}(y,x))$
3. Transform using rules: $$\begin{array}{rl}\neg (\forall x)(\text{Uni}(x)\to (\exists y)\text{Student}(y,x))& \equiv (\exists x)\neg (\text{Uni}(x)\to (\forall y)\text{Student}(y,x))\\ & \equiv (\exists x)\neg (\neg \text{Uni}(x)\vee (\exists y)\text{Student}(y,x))\\ & \equiv (\exists x)(\text{Uni}(x)\wedge \neg (\exists y)\text{Student}(y,x))\\ & \equiv (\exists x)(\text{Uni}(x)\wedge (\forall y)\neg \text{Student}(y,x))\end{array}$$ The last formula reads “there is a university without any student”.

Example 3: Showing Equivalence

Problem: show that the following two formulas are equivalent.

$$\begin{array}{c}(\forall x)(\text{University}(x)\to (\exists y)\text{Student}(y,x))\\ \neg (\exists x)(\text{University}(x)\wedge \neg (\exists y)\text{Student})\end{array}$$

In order to show equivalence, we can use double negation:

$$\begin{array}{rl}(\forall x)(\text{Uni}(x)\to (\exists y)\text{Student}(y,x))& \equiv \neg \neg (\forall x)(\text{Uni}(x)\to (\exists y)\text{Student}(y,x))\\ & \equiv \neg (\exists x)\neg (\text{Uni}(x)\to (\exists y)\text{Student}(y,x))\\ & \equiv \neg (\exists x)\neg (\neg \text{Uni}(x)\vee (\exists y)\text{Student}(y,x))\\ & \equiv \neg (\exists x)(\text{Uni}(x)\wedge \neg (\exists y)\text{Student}(y,x))\text{ QED}\end{array}$$

Quantifier Replacement Rules

Quantifier Replacement Rules

From what we just saw in the previous example, we can generate a set of rules used to transform quantifiers:

• $\exists x\varphi (x)\equiv \neg \neg \exists x\varphi (x)\equiv \neg \forall x\neg \varphi (x)$
• $\forall x\varphi (x)\equiv \neg \neg \forall x\varphi (x)\equiv \neg \exists x\neg \varphi (x)$

Link to original

Distribution of quantifiers over $\wedge$ and $\vee$

Distribution of existential quantification over disjunction

Existential quantification distributes over dis-junction:

$$\exists x(P(x)\vee Q(x))\equiv \exists x(P(x))\vee \exists xQ(x)$$Link to original

Distribution of universal quantification over conjunction

Universal quantification distributes over conjunction:

$$\forall x(P(x)\wedge Q(x))\equiv \forall x(P(x))\wedge \forall xQ(x)$$Link to original

Note however that:

• $\exists x(P(x)\wedge Q(x))\not\equiv \exists xP(x)\wedge \exists xQ(x)$ We can find that $\exists x(P(x)\wedge Q(x))\models \exists xP(x)\wedge \exists xQ(x)$ but not the converse.
• $\forall xP(x)\vee \forall xQ(x)\not\equiv \forall x(P(x)\vee Q(x))$ We can find that $\forall xP(x)\vee \forall xQ(x)\models \forall x(P(x)\vee Q(x))$ but not the converse.

Example 4: Equivalent with distribution

Show that $\exists x(P(x)\to Q(x))\equiv \forall xP(x)\to \exists xQ(x)$.

$$\begin{array}{rl}\exists x(P(x)\to Q(x))& \equiv \exists x(\neg P(x)\vee Q(x))\\ & \equiv \exists x\neg P(x)\vee \exists xQ(x)\\ & \equiv \neg \forall xP(x)\vee \exists xQ(x)\\ & \equiv \forall xP(x)\to \exists xQ(x)\end{array}$$

Vacuous quantification

Vacuous quantification

Vacuous quantification is when a variable $x$ has no occurrence in a formula $\varphi$, hence then binding $x$ with a quantifier in $\varphi$ has no effect. Or when the variable $x$ is already bound by another quantifier in a formula $\varphi$, hence binding $x$ again has no effect.

$$\begin{array}{rl}\forall x\forall y(P(y)\to Q(y))& \equiv \forall y(P(y)\to Q(y))\\ & \equiv \exists x\forall y(P(y)\to Q(y))\\ & \\ \forall x(\forall x(P(x)\to Q(x)))& \equiv \forall x(P(x)\to Q(x))\\ \exists x(\forall (P(x)\to Q(x)))& \equiv \forall x(P(x)\to Q(x))\end{array}$$

title: not sure if the last example is correct, check if it should $\equiv \exists$

Link to original

Renaming quantified variables

Renaming quantified variables

If $y$ is a new variable that does not occur in $\varphi$, then the following equivalences hold:

$$\begin{array}{rl}\exists x\varphi (x)& \equiv \exists y\varphi (x/y)\\ \forall x\varphi (x)& \equiv \forall y\varphi (x/y)\end{array}$$

Where $\varphi (x/y)$ is obtained from $\varphi (x)$ by replacing all free occurrences of $x$ in $\varphi (x)$ with $y$.

Link to original

Equivalences with restrictions

Equivalences with restrictions

Provided that $x$ does not occur in $\varphi$ (or that $x$ is bound by another quantifier in $\varphi$), then the following equivalences hold:

Simplification: $\exists x\varphi \equiv \forall x\varphi \equiv \varphi$

Regarding disjunction:

• $\exists x(\varphi \vee \phi (x))\equiv \varphi \vee \exists x\phi (x)$
• $\forall x(\varphi \vee \phi (x))\equiv \varphi \vee \forall x\phi (x)$

Regarding conjunction:

• $\exists x(\varphi \wedge \phi (x))\equiv \varphi \wedge \exists x\phi (x)$
• $\forall x(\varphi \wedge \phi (x))\equiv \varphi \wedge \forall x\phi (x)$

We can also show similar equivalences for implications:

• $\exists x(\varphi \to \phi (x))\equiv \varphi \to \exists x\phi (x)$
• $\forall x(\varphi \to \phi (x))\equiv \varphi \to \forall x\phi (x)$
• $\exists x(\phi (x)\to \varphi )\equiv \forall x\phi (x)\to \varphi$
• $\forall x(\phi (x)\to \varphi )\equiv \exists x\phi (x)\to \varphi$

Link to original

Deduction rules in First-order Logic

Similarly to propositional logic, we can obtain logical consequences in FOL using deduction rules. All natural deduction rules involving the propositional connectives and seen for the propositional logic case are still valid. New deduction rules need to be provided for the quantifiers.

Universal Instantiation ($\forall$-elimination)

Universal instantiation

A universal instantiation means for each and every entity $c$ in the domain we have a correct inference rule of the form: $$\boxed {\begin{array}{c}\underline{\forall xP(x)} \\P(c)\end{array}}$$

For example,

$$\begin{array}{lc}& \underline{\text{Everyone in the class is feeling miserable today.}}\\ \therefore & \text{Agi is feeling miserable today.}\end{array}$$

By universal instantiation, given the premise $(\forall x)\varphi (x)$, we may derive the conclusion $\varphi (x/t)$, where $t$ is any object in the domain:

$$\frac{(\forall x)\varphi (x)}{\varphi (x/t)}(\text{UI})$$

If $\varphi (x)$ holds for all the elements of the domain, it holds in particular for the element $t$ as well. Universal instantiation can be seen as $\forall$-elimination.

Link to original

title: Example
Validate the following inference:
- Every boy likes Mary
- John is a boy
- **Therefore**: John likes Mary
 
$$
	\begin{aligned}
		&1. &&\forall x(\text{Boy}(x) \rightarrow \text{Likes}(x, mary)) &&\text{data} \\
		&2. &&\text{Boy}(john) &&\text{data} \\
		&3. &&\text{Boy}(john) \rightarrow \text{Likes}(john, mary) &&\text{from } (1.) \text{ and } \forall E: x / john \\
		&4. &&\text{Likes}(john, mary) &&\text{from } (2.), (3.), \text{ and } (\rightarrow E)
	\end{aligned}
$$

Universal Generalisation ($\forall$-introduction)

Universal generalisation

A universal generalisation is $$ \boxed{\begin{array}{c} \underline{P(c) \textsf{ for any arbitrary entity } c \textsf{ in the domain}} \\ \forall x P(x)\end{array}} $$

By universal generalisation, given the premise $\varphi (x/t)$ takes place for a generic object $t$ of the domain, we may derive $(\forall x)\varphi (x)$:

$$\frac{\varphi (x/t)}{(\forall x)\varphi (x)}(\text{UG})$$

The object $t$ in the premise of $(\text{UG})$ must not be specific but arbitrary, i.e. we cannot make any assumption about $t$ other than it comes from the domain. Universal generalisation can be seen as $\forall I$.

Link to original

title: Example
Validate the following inference:
- All humans are mammals
- All mammals are vertebrates
- **Therefore**: All humans are vertebrates
 
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&\forall x (\text{Human}(x) \rightarrow \text{Mammal}(x)) &&\text{data} \\
			&2. &&\forall x (\text{Mammal}(x) \rightarrow \text{Vertebrate}(x)) &&\text{data} \\
			&3. &&\text{Human}(a) \rightarrow \text{Vertebrate}(a) &&\text{subcomputation}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{\text{Vertebrate}(a)} \\
				&3.1 &&\text{Human}(a) &&\text{assume} \\
				&3.2 &&\text{Human}(a) \rightarrow Mammal(a) &&\text{from } (1.), \text{ and } \forall E: x/a \\
				&3.3 &&\text{Mammal}(a) &&(3.1), (3.2), \text{ and } \rightarrow E \\
				&3.4 &&\text{Mammal}(a) \rightarrow \text{Vertebrate}(a) &&(2.), \text{ and } \forall E: x/a \\
				&3.5 &&\text{Vertebrate}(a) &&(3.3), (3.4), \text{ and } \rightarrow E
			\end{aligned}
		} \\
		\begin{aligned}
			&4. &&\forall x (\text{Human}(x) \rightarrow \text{Vertebrate}(x)) &&(3.), \text{ and } \forall I: a / x
		\end{aligned}
	\end{array}
$$

Existential Generalisation

Existential generalisation

An existential generalisation means that for every entity $c$ in the domain, we have a correct inference rule of the form $$ \boxed{ \begin{array}{c} \underline{P(c)} \\ \exists x P(x) \end{array} } $$

For example:

$$\begin{array}{lc}& \underline{\text{Marla is reading the lecture notes.}}\\ \therefore & \text{There is someone in the class reading the lecture notes.}\end{array}$$

By existential generalisation, given that $\varphi (x/t)$ is known to hold for a particular object $t$ of the domain, we may derive $(\exists x)\varphi (x)$:

$$\frac{\varphi (x/t)}{(\exists x)\varphi (x)}(\text{EG})$$

This can be seen as $\exists I$.

Link to original

title: Example
Validate the following inference:
- Anne likes Bob
- **Therefore**: Someone likes Bob
 
$$
	\begin{aligned}
		&1. &&\text{Likes}(ann, bob) &&\text{data} \\
		&2. &&(\exists x) \text{Likes}(x, bob) &&(1.), \text{ and } \exists I: ann/x
	\end{aligned}
$$

Existential Instantiation ($\exists$-elimination)

Existential instantiation

By existential instantiation, given the premise $(\exists x)\varphi (x)$, we may derive $\varphi (x/t)$ where $t$ is a particular object of the domain:

$$\frac{(\exists x)\varphi (x)}{\varphi (x/t)}(\text{EI})$$

Note: we cannot select an arbitrary object in $(\text{EI})$ but rather it must be an object $t$ for which $\varphi (x/t)$ is true. Usually, we have no knowledge of what the actual object is, we only know that it does exist. Since it exists, we can give it a new name, not used anywhere before, say $t$, and continue the derivation. Existential instantiation can be seen as $\exists E$.

Link to original

title: Example
Validate the following inference:
- Everyone who likes Bob likes Charles
- Someone likes Bob
- **Therefore**: Someone likes Charles
 
$$
	\begin{aligned}
		&1. &&\forall x(\text{Likes}(x, bob) \rightarrow \text{Likes} (x, charles)) &&\text{data} \\
		&2. &&(\exists x) \text{Likes}(x, bob) &&\text{data} \\
		&3. &&\text{Likes}(t, bob) &&\text{from } (2.), \text{ and } \exists E: x/t \\
		&4. &&\text{Likes}(t, bob) \rightarrow \text{Likes}(t, charles) &&\text{from } (1.), \text{ and } \forall E: x/t \\
		&5. &&\text{Likes}(t, charles) &&\text{from } (3.), (4.), \text{ and } \rightarrow E \\
		&6. &&(\exists x) \text{Likes}(x, charles) &&(5.), \text{ and } \exists I: t/x
	\end{aligned}
$$

Identity Introduction ($II$)

Identity introduction

By identity introduction, for any term $t$, we can assert that $t=t$:

$$\frac{}{t=t}(\text{II})$$Link to original

Identity Elimination ($IE$)

Identity elimination 1

By identity elimination (substitution of identicals), if $t$ and $t^{\prime }$ are terms, from $t=t^{\prime }$ and $\varphi (x/t)$, we may derive $\varphi (x/t^{\prime })$ (we substitute $t$ for $t^{\prime }$ since they are identical):

$$\frac{t=t^{\prime },\varphi (x/t)}{\varphi (x/t^{\prime })}(\text{IE})$$Link to original

Symmetry Proof of $IE$

We can prove that the equality relation is symmetric, i.e. prove that:

$$\models \forall x\forall y(x=y\to y=x)$$ $$\begin{array}{l}\begin{array}{rlrlrl}& 1.& & a=b\to b=a& & \text{subcomputation}\end{array}\\ \boxed{\begin{array}{rlrlrlrl}& & & & & & & \underline{b=a}\\ & 1.1& & a=b& & \text{assume}& & \\ & 1.2& & a=a& & II& & \\ & 1.3& & b=a& & (1.1),(1.2)(\varphi (x):x=a;x/a),\text{ and }IE:x/b& & \end{array}}\\ \begin{array}{rlrlrl}& 2.& & \forall x(x=b\to b=x)& & \text{from }(1.)\text{ and }\forall I:a/x\\ & 3.& & \forall x\forall y(x=y->y=x)& & \text{from }(2.)\text{ and }\forall I:b/y\end{array}\end{array}$$