Lecture 8. FOL

Slides

∀I

Logical methods for AI

Lecture 8

FOL

This work is licensed under CC BY 4.0

https://forms.gle/JiXXM9eysAZaJMja9

First Order Logic

Background

Logical system for valid inference with quantifiers:

"For all"
"There is"

Benchmark system: strong!
Theoretical limitations

FOL syntax

Alphabet

Non-logical symbols:

Individual constants: $a,b,c,\dots,$ also $Alan$ or $Ada$.
Function symbols: $f,g,h,\dots,$ also $MotherOf$ or $BirthplaceOf$.
Predicates: $P,Q,R,\dots,$ also $Blue$ or $BiggerThan$.

Alphabet

Logical symbols:

Connectives: $\neg,\land,\lor,\to,\leftrightarrow$
Variables: $x,y,z,\dots$
Quantifiers: $\forall,\exists$
Auxilliaries: $(,),\ ","$

Terms

$$\langle const\rangle ::= a \mid b\mid \dots $$ $$\langle var\rangle ::= x \mid y\mid \dots $$ $$\langle fun^n\rangle ::= f^n\mid g^n\mid \dots $$ $$\langle term\rangle::= \langle const\rangle\mid\langle variable\rangle\mid \langle fun^n\rangle(\underbrace{\langle term\rangle,\dots,\langle term\rangle}_{n\text{ times}})$$

Terms

Denote individuals:

Constants: Proper names, like "Utrecht", "Johannes", ...
Variables: Pronouns: "he", "she", "it", ...
Functions: Expressions like "the father of", "the birthplace of"

Atomic formulas

$$\langle pred^n\rangle ::= P^n\mid Q^n\mid \dots $$ $$\langle atom\rangle::= \langle pred^n\rangle(\underbrace{\langle term\rangle,\dots\langle term\rangle}_{n\text{ times}})$$

Atomic formulas

Simple, term-predicate sentences: the robot is smart
Predicate: "... is smart", "... is bigger than ..."
Examples:
- $\mathbf{Smart}(Robot)$
- $\mathbf{LLM}(x)$
- $\mathbf{BiggerThan}(Robot,Johannes)$
- $\mathsf{Lord}(\mathsf{FatherOf}(Ada))$

Quantifiers

$$\langle var\rangle ::= x \mid y\mid \dots $$ $$\langle quant\rangle ::= \forall\mid\exists$$ $$\langle fml\rangle::=\langle atom\rangle\mid\langle unop\rangle\langle fml\rangle\mid$$ $$(\langle fml\rangle\langle binop\rangle \langle fml\rangle)\mid \langle quant\rangle \langle var\rangle\langle fml\rangle$$

Quantifiers

General claims: $$\forall x\exists y\mathsf{BiggerThan}(x,y)$$
For everything there is something, such that it is bigger than it.

Identity/equality

$$t_1=t_2 \qquad \qquad t_1\neq t_2$$ $$\mathsf{FatherOf}(Ada)=Byron$$ $$\exists x\exists y(\mathsf{LLM}(x)\land\mathsf{LLM}(y)\land x\neq y)$$ $$\forall x\forall y((\mathsf{GOAT}(x)\land\mathsf{GOAT}(y))\to x=y)$$

FOL syntax

Domains

Objects we're talking about.
$\mathcal{D}=\Set{o_1,o_2,\dots}$
In KR: representations of the world.
Often graphs.

Denotations

Constants: $c^\mathcal{M}\in\mathcal{D}$
Assignments: $\alpha:\Set{x,y,z,\dots}\to\mathcal{D}$
Variables: $\alpha(x)\in\mathcal{D}$
Functions: $f^\mathcal{M}:\mathcal{D}^n\to \mathcal{D}$
Recursion: $$t^\mathcal{M}_\alpha::= c^\mathcal{M}\mid \alpha(x) \mid f^\mathcal{M}((t_1)^\mathcal{M}_\alpha, \dots (t_n)^\mathcal{M}_\alpha) $$

Extensions

Set of things having a property/standing in a relation: $$P^\mathcal{M}\subseteq \mathcal{D}^n$$
$\mathcal{D}^n=\Set{\langle o_1,\dots,o_n\rangle:o_i\in\mathcal{D}}$
$\mathsf{Sister}^\mathcal{M}=\Set{\langle o_1,o_2\rangle:o_1\text{ is sister of }o_2\text{ in }\mathcal{M}}$

Atomic truth

$$\nu_\alpha(\mathsf{Parent}(\mathsf{FatherOf}(Ada),Clara))=1$$ $$\Leftrightarrow$$ $$\langle\mathsf{FatherOf}^\mathcal{M}(Ada^\mathcal{M}),Clara^\mathcal{M}\rangle\in \mathsf{Parent}^\mathcal{M}$$ $$=\Set{\langle o_1,o_2\rangle:o_1\text{ is parent of }o_2\text{ in }\mathcal{M}}$$

Atomic truth

$$\nu_\alpha(\mathsf{Blue}(x))=1\Leftrightarrow \alpha(x)\in\mathsf{Blue}^\mathcal{M}$$

Atomic truth

$$\nu_\alpha(P(t_1,\dots,t_n))=1\Leftrightarrow \langle (t_1)^\mathcal{M}_\alpha, \dots, (t_n)^\mathcal{M}_\alpha\rangle\in P^\mathcal{M}$$

Identity truth

$$\nu_\alpha(\mathsf{FatherOf}(Ada)=x)=1$$ $$\Leftrightarrow$$ $$\mathsf{FatherOf}^\mathcal{M}(Ada^\mathcal{M})=\alpha(x)$$

Identity truth

$$\nu_\alpha(t_1=t_2)=1\Leftrightarrow t_1^\mathcal{M}=t_2^\mathcal{M}$$

Universal truth

$$\nu\_\alpha(\forall x\mathsf{Blue}(x))$$ $$=_{\mathbf{o}^\mathcal{M}=o}$$ $$\nu_\alpha(\mathsf{Blue}(\mathbf{o}_1))\times\nu\_\alpha(\mathsf{Blue}(\mathbf{o}_2)\times\dots$$ $$=$$ $$\prod_{o\in\mathcal{D}}\nu_\alpha(\mathsf{Blue}(\mathbf{o}))$$

Existential truth

$$\nu\_\alpha(\exists x\mathsf{Blue}(x))$$ $$=_{\mathbf{o}^\mathcal{M}=o}$$ $$\nu_\alpha(\mathsf{Blue}(\mathbf{o}_1))+\nu\_\alpha(\mathsf{Blue}(\mathbf{o}_2)+\dots$$ $$=$$ $$\sum_{o\in\mathcal{D}}\nu_\alpha(\mathsf{Blue}(\mathbf{o}))$$

$$\nu_\alpha(P(t_1,\dots,t_n))=1\Leftrightarrow \langle (t_1)^\mathcal{M}_\alpha, \dots, (t_n)^\mathcal{M}_\alpha\rangle\in P^\mathcal{M}$$ $$\nu_\alpha(\neg A)=-\nu_\alpha(A)$$ $$\nu_\alpha(A\land B)=\nu_\alpha(A)\times \nu_\alpha(B)$$ $$\nu_\alpha(A\lor B)=\nu_\alpha(A)+\nu_\alpha(B)$$ $$\nu_\alpha(A\to B)=\nu_\alpha(A)\Rightarrow\nu_\alpha(B)$$ $$\nu_\alpha(\forall xA(x))=\prod_{o\in\mathcal{D}}\nu_\alpha(A(\mathbf{o}))$$ $$\nu_\alpha(\exists xA(x))=\sum_{o\in\mathcal{D}}\nu_\alpha(A(\mathbf{o}))$$

FOL consequence

$$P_1,P_2,\dots \vDash C$$ $$\Leftrightarrow$$ $$\text{ for all }\mathcal{M},\nu,\alpha,$$ $$\text{ if }\nu_\alpha(P_1)=1,\nu_\alpha(P_2)=1,\dots\text{, then }$$ $$\nu_\alpha(C)=1.$$

Quantifier laws

Duality $\exists/\forall$		$\exists xA\vDash \neg\forall x\neg A\qquad \neg\forall x\neg A\vDash \exists xA$
Duality $\forall/\exists$		$\forall xA\vDash \neg\exists x\neg A\qquad \neg\exists x\neg A\vDash \forall xA$

Quantifier laws

Distr. $\forall/\land$		$\forall x(A\land B)\vDash \forall xA\land \forall xB\quad \forall x A\land \forall x B\vDash \forall x(A\land B)$
Distr. $\exists/\lor$		$\exists x(A\lor B)\vDash \exists xA\lor \exists xB\quad \exists x A\lor \exists x B\vDash \exists x(A\lor B)$