Differences
This shows you the differences between two versions of the page.
sav08:predicate_logic_informally [2008/02/20 15:46] 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 ((\exists x. P(x)) \land (\exists 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 |