Logic for Computer Science/Logics

From Wikibooks, open books for an open world
< Logic for Computer Science
Jump to: navigation, search

Sub-FO Logics[edit]

From Propositional Logic to FO[edit]

Propositional Logic[edit]

Monadic FO[edit]

Existential FO[edit]

Universal FO[edit]

Modal Logic[edit]

Modal logic expands propositional logic by operators for the modalities possibility and necessity. These basic modal operators are usually written \Box (or L) for necessarily and \Diamond (or M) for possibly. Each can be defined from the other in the following way:

\Diamond P \leftrightarrow \lnot\, \Box\, \lnot\, P.

Conjunctive Logic[edit]

Conjunctive Logic is a fragment of FO that is restricted to atomic FO expressions joined by conjunctions that can be preceded by existential quantifiers. It is especially important in Database theory.

Definition CON

  1. Atom
  2. \varphi \land \psi
  3. \exists_x \varphi

Remarks

  1. In other words: a CON-formula is a (relational) FO-formula built from atomic formulas using only conjunction and existential quantification.
  2. The semantics of FO applies here correspondingly.
  3. The 'usual' notions of free and bound variables also apply here.
  4. A formula of the form \exists_{x_1} ... \exists_{x_n} \varphi_1 \land ... \land \varphi_m, where each φ is quantifier free, is said to be in Normal Form
  5. Each CON formula is equivalent to one in Normal Form
  6. All CON formulas are satisfyable

Examples

  1. \exists_x (\varphi(x, y) \land \psi(x, y)) has a bound x and a free variable y
  2. \exists_x (\varphi(x) )\land \exists_y (\psi(y)) is equivalent to \exists_x \exists_y (\varphi(x) \land \psi(y)). The latter is said to be in normal form.

Equality

Additionally Equality between variables or constants can be be introduced by

  • x \equiv y

Example. Not always satisfiable. Each satisfiable CON formula is equivalent to one without equality.

Higher-order Logics[edit]

Fixed-Point Logics[edit]

Fixed-Point Logics augment the syntax of FO by a fixed-point opreator, a mechanism that enables recursion on expressions, and so allows higher expressive power. This idea is quite similar to adding the construct of while-loop to an imperative programming language.

Example Transitive Closure

Transitive Closure illustrated

Consider the transitive closure of a graph G. For distance one we have:

G(x, y)\,

for distance up to two:

G(x, y) \lor \exists_z ( G(x, z) \land G(z, y) )

so we can go on by expanding this disjunction for further fixed distances (only). In order to express transitive closure for an arbitrary distance (what is vital for most situations) recursion can be introduced employing:

\varphi(T) = G(x, y) \lor T(x, y) \lor \exists_z ( T(x, z) \land G(z, y) )

where T is the transitive closure up to some i. Thus φ(T) gives the transitive closure up to i + 1. So it can be defined a sequence

J_0 = \empty ; J_i = \varphi(J_{i-1}) , i > 0

that clearly gives the transitive closure for some k, i.e. the sequence converges (i.e. Jk = Jk+j, for all j > 0) and it's limit is the transitive closure.

In the illustration we have an initial graph G as in (a) and thus

(a) as J_1 = G(x, y)\,

(b) as J_2 = G(x, y) \lor \exists_z ( G(x, z) \land G(z, y)

and the fixed point (c) as

J_3 = G(x, y) \lor \exists_z ( G(x, z) \land G(z, y) ) \lor \exists_z ( \exists_t ( G(x, t) \land G(t, z) ) \land G(z, y) )

and thus J3 = J4 = ... .

As we have seen in this example, recursion can be used to express formulas of arbitrary length. But since we are always dealing with finite formulas here some terminator must be given for the recursion. This role can be played by the fixpoint. In the above example such a fixpoint exists. But this is not always the case, as we see next.

Example

TODO Jumper

As we have seen in this example, a fixpoint of a recursion not always exists. So we must be careful defining a recursion-based logic. We extend FO by a fixpoint operator to PFP for cases where a fixpoint exists.

Partial Fixed-Point Logics (PFP)[edit]

TODO

The above assumption that a fixpoint exists it not really satisfying, so one now can think of restrictions on the recursion in order to enforce the existence in every case. Therefore three ideas are introduced: monotonicity, positivness and inflation of the recursion.

Inflationary Fixed-Point Logics (IFP)[edit]

Notion

TODO Life-Game

Definition

TODO

Least Fixed-Point Logics (LFP)[edit]

Notion

TODO

Definition

TODO

Comparison of IFP and LFP[edit]

TODO

Characteristics of FO[edit]

Completeness Theorem[edit]

Compactness Theorem[edit]

Löwenheim-Skolem Theorem[edit]