LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:predicate_logic_informally [2008/02/21 14:41]
vkuncak
sav08:predicate_logic_informally [2015/04/21 17:30]
Line 1: Line 1:
-====== First-Order Logic ====== 
  
-First-order logic is a very powerful notation that extends [[Propositional Logic Informally|propositional logic]]. ​ Here we give only an informal overview of first-order logic, which should be enough for you to understand the meaning of first-order logic formulas based on mathematics and natural language. ​ In future lectures we study first-order logic as a formal system and discuss algorithmic questions in more detail. 
- 
-On top of propositional operations, first-order logic adds: 
-  * constructs to represent the structure of propositions:​ 
-     * equality ( = ) 
-     * predicate symbols ($P$, $Q$, ...) 
-     * function symbols ($f$, $g$, ...) 
-     * first-order variables ($x$, $y$, ...) denoting entities in some domain $D$ 
-  * quantifiers "​forall"​ ($\forall$),​ "​exists"​ ($\exists$) 
- 
-Uses of first-order logic: 
-  * precisely describe arbitrary mathematical statements (theorems, conjectures,​ properties) 
-  * specify program properties 
-  * represent the meaning of programs 
-  * represent knowledge about the world (e.g. knowledge bases, semantic web) 
- 
-**Examples** 
-  * An ancestor of my ancestor is also my ancestor: $\forall x. \forall y.\ ((ancestor(x,​I) \land ancestor(y,​x)) \rightarrow ancestor(y,​I))$ 
-  * Grandparent is the parent of a parent: $\forall x. \forall y.\ (grandparent(x,​y) \leftrightarrow (\exists z. parent(x,z) \land parent(z,​y)))$ 
-  * Property $P$ holds for infinitely many natural numbers: $\forall n. \exists m.\ m > n \land P(m)$ 
-  * $f$ is continuous in point $x_0$: $\forall \varepsilon > 0. \exists \delta > 0. \forall x.\ |x-x_0| < \delta \rightarrow |f(x)-f(x_0)| < \varepsilon$ 
-  * first $k$ array elements are strictly positive, remaining elements are zero: $\forall i. ((0 \le i \land i < k \rightarrow a(i) > 0) \land ((k \le i \land i < N) \rightarrow a(i)=0)$ 
- 
-===== First-Order Logic Formulas ===== 
- 
-We build first-order logic formulas by starting from //atomic formulas// (defined below) and applying //​propositional operators// and //​quantifiers//:​ 
-  * atomic formulas are first-order logic formulas 
-  * if $P$ and $Q$ are first-order formulas, so are $\lnot P$, $P \land Q$, $P \lor Q$, $P \rightarrow Q$, $P \leftrightarrow Q$ 
-  * if $P$ is a first-order formula, so is $\forall x.P$ and $\exists x. P$ 
- 
-For a given value of variables, each formula evaluates to //true// or //​false//​. ​ The rules for propositional operators are exactly as in [[Propositional Logic Informally|propositional logic]]. ​ Quantifiers can be seen as a way of generalizing conjunction and disjunction. ​ First-order variables range over some domain $D$.  In the special case of finite domain $D = \{d_1,​\ldots,​d_k\}$,​ we have that 
-\[\begin{array}{l} 
-    (\forall x. P(x)) \ \leftrightarrow\ P(d_1) \land \ldots \land P(d_k) \\ 
-    (\exists x. P(x)) \ \leftrightarrow\ P(d_1) \lor \ldots \lor P(d_2) \\ 
-\end{array}\] 
-which corresponds to the intuitive definition of terms "for all" and "there exists"​. ​ Note, however, that $D$ can be infinite in general (for example: the set of integers or reals). 
- 
-Atomic formulas evaluate to //true// or //​false//​. ​ We build atomic formulas by applying //predicate symbols// and //​equality//​ to //terms//: 
-  * if $t_1$ and $t_2$ are terms, then $t_1 = t_2$ is an atomic formula; 
-  * if $t_1$, ..., $t_n$ are terms and $P$ is a predicate symbol that takes $n$ arguments, then $P(t_1,​\ldots,​t_n)$ is an atomic formula. 
-Predicates represent relations, for example, we can represent $\leq$ as a binary relation. 
- 
-Terms denote elements of the domain $D$.  We build them starting from variables and constants and applying //function symbols//: 
-  * each first-order variable is a term 
-  * a constant is a term 
-  * if $t_1,​\ldots,​t_n$ are terms and $f$ is a function symbol that takes $n$ arguments, then $f(t_1,​\ldots,​t_n)$ is also a term. 
-Example of constants are numerals for natural numbers, such as $0, 1, 2, \ldots$. ​ Examples of function symbols are operations such as $+, -, /$. 
- 
-From above we see that the set of formulas depends on the set of predicate and function symbols. ​ This set is is called //​vocabulary//​ or //​language//​. 
- 
-==== Bounded Quantifiers ==== 
- 
-In general all quantifiers range over some universal domain $D$.  To restrict them to subsets of $D$, we can use bounded quantifiers:​ 
- 
-  * $\exists x \in S. P(x)$ means $\exists x. (x \in S \land P(x))$ 
-  * $\forall x \in S. P(x)$ means $\forall x. (x \in S \rightarrow P(x))$ (note implication instead of conjunction) 
- 
-More generally, if $\rho$ is some binary relation written in infix form, such as $<, \le, >, \ge$ we write 
-  * $\exists x \mathop{\rho} t. P(x)$ meaning $\exists x. (x \mathop{\rho} t \land P(x))$ 
-  * $\forall x \mathop{\rho} t. P(x)$ means $\forall x. (x \mathop{\rho} t \rightarrow P(x))$ (note implication instead of conjunction) 
- 
-===== Evaluating First-Order Logic Formulas ===== 
- 
-To evaluate first-order logic formulas we need to know: 
-  * the domain set $D$ 
-  * values of first-order variables in the formula 
-  * interpretation of predicate symbols and function symbols (e.g. does predicate symbol $R$ denote $\leq$ or $<$ or $>$, does binary function symbol $f$ denote $+$ or $-$) 
- 
-=== Examples === 
- 
-Consider formula $F$ given by $\forall x. (P(x) \lor P(f(x))$. ​ The formula has one predicate symbol $P$ that takes one urgument (we call it unary) and one unary function symbol $f$.  Assume that the domain $D$ is the set of integers and consider two possible interpretations:​ 
-  * $P$ denotes property of being an even integer and $f$ denotes the successor function $f(x)=x+1$. ​ Is formula true under this interpretation?​ 
-  * $P$ denotes property of being an even integer and $f$ denotes the squaring function $f(x)=x^2$. ​ Is formula true under this interpretation?​ 
- 
-Now consider formula $\forall x. \forall y. ((P(x) \land x=f(y)) \rightarrow P(f(y))$ in each of these two interpretations. 
- 
-===== (Finite) Validity and Satisfiability of First-Order Logic Formulas ===== 
- 
-Formula is //valid// if and only if it evaluates to //true// for //all// domains, values of its variables and interpretations of predicate and function symbols. 
- 
-Formula is //​satisfiable//​ if and only if it evaluates to //true// for //some// domains, values of its variables, interpretation of predicate and function symbols. 
- 
-Formula is //​unsatisfiable//​ if and only if it is //false// for //all// domains, values of its variables and interpretations of predicate and function symbols. 
- 
-Note 
-  * a formula $F$ is //​unsatisfiable//​ if and only if it is not satisfiable 
-  * a formula $F$ is //valid// if and only if $\lnot F$ is unsatisfiable 
- 
-Answers to some important algorithmic questions (not immediate): 
-  * There is no algorithm that given a first-order logic formula outputs "​yes"​ when the formula is valid and "​no"​ otherwise - //validity of first-order logic formulas is undecidable//​ 
-  * There exists an enumeration procedure that systematically lists //all// valid formulas (and only valid formulas) - //validity of first-order logic formulas is enumerable//​ 
- 
-If instead of considering all domains we only consider finite domains (no natural numbers but only e.g. prefixes of natural numbers of the form $\{1,​\ldots,​ n\}$) then we obtain notions of //finite validity//, //finite satisfiability//​ and //finite unsatisfiability//​. 
- 
-Note that because finite domains are a special case of possible domains, we have the following: 
-  * if a formula is finitely satisfiable,​ then it is satisfiable 
-  * if a formula is valid, then it is also finitely valid 
- 
-Answers to some important algorithmic questions about finite satisfiability:​ 
-  * There is //no algorithm// that given a first-order logic formula outputs "​yes"​ when the formula is satisfiable and "​no"​ otherwise - //finite satisfiability of first-order logic formulas is undecidable//​ 
-  * There exists an enumeration procedure that systematically lists //all// finitely satisfiable formulas (and only finitely satisfiable formulas) - //finite satisfiability of first-order logic formulas is enumerable//​ 
- 
- 
-===== Some Valid First-Order Logic Formulas ===== 
- 
-If we take a [[Propositional Logic Informally#​propositional tautologies|propositional tautology]] and replace equal propositional variables with equal atomic formulas, we obtain a valid formula. ​ Such formula is called //an instance of a tautology//​. 
- 
-But there are many other valid formulas. ​ Such formulas are valid laws of thinking that we often use in mathematics (explicitly,​ or implicitly without mentioning them). 
- 
-\[\begin{array}{l} 
-   ​(\forall x. (P(x) \land Q(x)) \leftrightarrow ((\forall x. P(x)) \land (\forall x. Q(x))) \\ 
-   ​(\exists x. (P(x) \land Q(x)) \rightarrow ((\exists x. P(x)) \land (\exists x. Q(x))) \\ 
-   ​(\exists x. (P(x) \lor Q(x)) \leftrightarrow ((\exists x. P(x)) \lor (\exists x. Q(x))) \\ 
-   ​((\forall x. P(x)) \lor (\forall x. Q(x))) \rightarrow (\forall x. (P(x) \lor Q(x)) \\ 
-   ​(\exists x. \forall y. R(x,y)) \rightarrow (\forall y. \exists x. R(x,y)) \\ 
-   ​(\lnot (\exists x. P(x))) \leftrightarrow (\forall x. (\lnot P(x)) \\ 
-   ​(\lnot (\forall x. P(x))) \leftrightarrow (\exists x. (\lnot P(x)) \\ 
-   ​(\lnot (\exists x \rho t. P(x))) \leftrightarrow (\forall x \rho t. (\lnot P(x)) \\ 
-   ​(\lnot (\forall x \rho t. P(x))) \leftrightarrow (\exists x \rho t. (\lnot P(x)) \\ 
-   ​(\forall x. (x=t \rightarrow F(x))) \leftrightarrow F(t) \\ 
-   ​(\exists x. (x=t \land F(x))) \leftrightarrow F(t) \\    
-\end{array}\] 
- 
-===== More information ===== 
- 
-  * forthcoming lectures 
-  * [[Calculus of Computation Textbook]], Chapters 2, Chapter 3 
-  * [[:Gallier Logic Book]], Sections 5.1, 5.2, 5.3  ​