en:mathematics:logic:predicate-logic

First-order predicate logic is, for example, used for theorem proving, software design and specification, rapid prototyping, user interface design, hardware verification and security testing.

First order logic can be applied to the specification of security policies, but one of the main problems encountered when using first order logic for policy specification arises when negation is used together with recursive rules. Although it is possible to avoid the use of negation or recursion, this is not practical since it diminishes significantly the expressive power of the logical language.

Constants | Things, 2, C, … | |
---|---|---|

Predicates | Brother, sister, >, =, … | |

Functions | Sqrt, leftarmof, … | |

Variables | x, y, a, b, … | |

Connectives | $ \wedge $, $ \vee $, $ \neg $, $ \Rightarrow $, $ \Leftarrow $ | |

Quantifiers | $ \forall$, $\exists$ |

`predicate = (term`

$\vee$ _{1}, … term_{n})`term`

_{1} = term_{2}

`function (term`

$\vee$ _{1}, … term_{n})`variable`

$\vee$ `constant`

Using connectives (works like in propositional logic):

$\neg$ `S` |

`S` $\wedge$ `S` |

`S` $\vee$ `S` |

`S` $\Rightarrow$ `S` |

`S` $\Leftrightarrow$ `S` |

Example:

Sibling (Mutsuraboshi, Krittika) $\Rightarrow$ Sibling (Krittika, Mutsuraboshi)

Where:

- Sibling is a predicate
- Krittika and Mutsuraboshi are terms
- Both statements on left and right side of $\Rightarrow$ are atomic sentences
- The whole thing is a complex sentence

Sentences are true or false *“with respect to models”*, which consist of a **domain** (also called **universe**) and an **interpretation**.

- A
**domain**is a*non-empty (finite or infinite)*set of arbitrary elements. - The
**interpretation**assigns to each**constant**symbol: a**domain**element**predicate**symbol: a relation on the**domain**(of appropriate arity)**function**symbol: a function on the**domain**(of appropriate arity)

An atomic sentence is true in a certain model (consisting of a domain and interpretation) iff (if and only if) the domain elements that are the interpretations of `term`

are in the relation that is the interpretation of _{1}, … term_{n}`predicate`

.

The truth-value of a complex sentence in a model is computed from the truth-values of its atomic sub-sentences in the same way as in propositional logic.

Syntax: ∀ variables sentence

Example: Everyone living in the Universe is paranoia.

∀ x (LivingIn (x, Universe) ⇒ (paranoia, x)

Semantics: ∀xP is true in a model iff for all domain elements d in the model: P is true in the model when x is interpreted by d.

Intuition: ∀xP is roughly equivalent to the conjunction of all instances of P.

Example:

∀ x (LivingIn (x, Universe) ⇒ (paranoia, x)

is equivalent to:

Krittika (LivingIn (Krittika, Universe) ⇒ (paranoia, Krittika) ∧ Mutsuraboshi (LivingIn (Mutsuraboshi, Universe) ⇒ (paranoia, Mutsuraboshi) ∧ …

Note: ⇒ is the main connective with ∀, not ∧

Syntax: ∃ variables sentence

Example: Someone living in the Universe is paranoia.

∃ x (LivingIn (x, Universe) ∧ (paranoia, x)

Semantics: ∃xP is true in a model iff there is a domain element d in the model such that: P is true in the model when x is interpreted by d.

Intuition: ∃xP is roughly equivalent to the disjunction of all instances of P.

Example:

∃ x (LivingIn (x, Universe) ∧ (paranoia, x)

is equivalent to:

Krittika (LivingIn (Krittika, Universe) ∧ (paranoia, Krittika) ∨ Mutsuraboshi (LivingIn (Mutsuraboshi, Universe) ∧ (paranoia, Mutsuraboshi) ∨ …

Note: ∧ is the main connective with ∃, not ⇒

- Quantifiers of same type commute (∀x∀y is the same as ∀y∀x and ∃x∃y is the same as ∃y∃x)
- Quantifiers of different type do not commute (∃x∀y is not the same as ∀y∃x)
- Quantifier duality (∀x Likes(x,Logic) is the same as ¬∃x ¬Likes(x,Logic))

`term`

_{1} = term_{2}

iff term_{1} and term_{2} have the same interpretation.

Validity, satisfiability, unsatisfiablity and entailment are defined in the same way as for propositional logic: x ⊢ y means y is provable from x (in some specified formal system) and x ⊨ y means x semantically entails y.

First order logic calculi:

- Whenever KB ⊨ α, it is also true that KB ⊢ α
- Whenever KB ⊢ α, it is also true that KB ⊨ α

BUT … in propositional logic validity, satisfiability and unsatisfiablity are decidable. In first-order logic the set of valid, and the set of unsatisfiable formulas are enumerable, and the set of satisfiable formulas is not even enumerable. Gödel's completeness theorem asserts that there are logical calculi in which every true formula is provable, and Church's theorem asserts that there is no decision procedure (which always terminates) for deciding whether a formula is true (valid).

en/mathematics/logic/predicate-logic.txt · Last modified: 2018/08/18 15:49 by Digital Dot