Logic for Computer Science/Logics

Sub-FO Logics

Modal Logic

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

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

Fixed-Point Logics

Fixed-Point Logics augment the syntax of FO by a fixed-point operator, 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}=\emptyset ;J_{i}=\varphi (J_{i-1}),i>0$

that clearly gives the transitive closure for some k, i.e. the sequence converges (i.e. J_k = J_k+j, for all j > 0) and its 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 J₃ = J₄ = ... .

♣

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)

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, positiveness and inflation of the recursion.

Inflationary Fixed-Point Logics (IFP)

Notion

TODO Life-Game

Definition

TODO

Least Fixed-Point Logics (LFP)

Notion

TODO

Definition

TODO

♣

Comparison of IFP and LFP

TODO

♣