Finite Model Theory/Logics and Structures

From Wikibooks, open books for an open world
< Finite Model Theory
Jump to: navigation, search

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

Logics[edit]

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


Fragments of FO[edit]

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

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

Second Order Logic (SO)[edit]

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. That is, the rules are extended 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

Fragments of Second Order Logic[edit]

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

Infinitary Logics[edit]

Notion[edit]

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 ...

Definition[edit]

syntax ...

semantics ...

Properties[edit]

General Quantifier Logics[edit]

Fixed Point Logics[edit]

Counting Logics[edit]

Structures[edit]

Finite Graphs[edit]

Kinds of Finite Graphs[edit]

Strings[edit]