User Tools

Site Tools


en:mathematics:logic:predicate-logic
 
 

Cheat sheet first-order 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.

Symbols

Constants Things, 2, C, …
Predicates Brother, sister, >, =, …
Functions Sqrt, leftarmof, …
Variables x, y, a, b, …
Connectives $ \wedge $, $ \vee $, $ \neg $, $ \Rightarrow $, $ \Leftarrow $
Quantifiers $ \forall$, $\exists$

Atomic sentences

predicate = (term1, … termn) $\vee$ term1 = term2

Terms

function (term1, … termn) $\vee$ variable $\vee$ constant

Complex sentences

Using connectives (works like in propositional logic):

$\neg$ S
S1 $\wedge$ S2
S1 $\vee$ S2
S1 $\Rightarrow$ S2
S1 $\Leftrightarrow$ S2

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

Truth

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 term1, … termn are in the relation that is the interpretation of 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.

Universal quantification

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 ∧

Existential quantification

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 ⇒

Properties of quantifiers

  • 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))

Equality

term1 = term2

iff term1 and term2 have the same interpretation.

Properties of first order logic

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