Finite Model Theory/Logics and Structures

From Wikibooks, open books for an open world
Jump to navigation Jump to search

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

Logics[edit | edit source]

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 | edit source]

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

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

Second Order Logic (SO)[edit | edit source]

Second-order logic extends first-order logic by adding variables and quantifiers that range over sets of individuals. For example, the second-order sentence 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 is a formula

Fragments of Second Order Logic[edit | edit source]

  • 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 | edit source]

Notion[edit | edit source]

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

So the following infinitary logics can be defined

  • where ψ is an arbitrary set of formulas, e.g. uncountable
  • where ψ is a countable set of formulas
  • ...

Definition[edit | edit source]

syntax ...

semantics ...

Properties[edit | edit source]

General Quantifier Logics[edit | edit source]

Fixed Point Logics[edit | edit source]

Counting Logics[edit | edit source]

Structures[edit | edit source]

Finite Graphs[edit | edit source]

Kinds of Finite Graphs[edit | edit source]

Strings[edit | edit source]