Finite Model Theory/Logics and Structures

From Wikibooks, the open-content textbooks collection

Jump to: navigation, search

FMT studies logics on finite structures. An outline of the most important of these objects of study is given here.

Contents

[edit] Logics

The logics defined here and used thoughout the book are always relational, i.e. without function symbols, and finite, i.e. have a finite universe, without further notice.


[edit] Fragments of FO

The subsequent restrictions can analogously be found in other logics like SO.

  • MFO ...
  • ESO and USO ...
  • FOn ...

[edit] Second Order Logic (SO)

Second-order logic extends first-order logic by adding variables and quantifiers that range over sets of individuals. For example, the second-order sentence \forall S \, \forall x \, ( x \in S \lor x \not \in S) says that for every set S of individuals and every individual x, either x is in S or it is not. I.e. the rulesareextended by:

  • If X is a n-ary relation variable and t1 ... tn are terms then X t1 ... tn is a formula
  • If φ is a formula and X a relation variable then \exists_X \varphi is a formula

[edit] Fragments of Second Order Logic

  • The fragment monadic second-order logic (MSO) only unary relation variables ("set variables")are allowed.
  • The existential fragment (ESO) is second-order logic without universal second-order quantifiers, and without negative occurrences of existential second-order quantifiers.
  • USO ...

[edit] Infinitary Logics

[edit] Notion

The intention is to extend FO by an infinite disjunction element over a set ψ of formulas (of infinitary logic)

\bigvee \psi

So the following infinitary logics can be defined

  • L_{\infty \varpi} where ψ is an arbitrary set of formulas, e.g. uncountable
  • L_{\varpi \varpi} where ψ is a countable set of formulas
  • L_{\infty \varpi}^n ...

[edit] Definition

syntax ...

semantics ...

[edit] Properties

[edit] General Quantifier Logics

[edit] Fixed Point Logics

[edit] Counting Logics

[edit] Structures

[edit] Finite Graphs

[edit] Kinds of Finite Graphs

[edit] Strings