- Finiteness
- Synthetic Computability
- First-Order Logic
- Notations
- First order operators and their semantics
- First order signatures and models
- First order terms, syntax and semantics
- The syntax and semantics of FO logic
- Enumerability of the type of FO formulas
- First order theory of congruences
- Definition of first order satisfiability
- First order definability and closure properties
- Trakthentbrot's Theorem
- Model Discreteness and Interpreted Equality
- Compressing n-ary Relations to binary Membership
- Further Signature Transformations
- From binary singleton to n-ary singleton with n >= 2
- From Σ=(ø;{R^n}) to any signature
- Expanding from Σ=({f^n};{P^1}) to any signature
- Signature reduction for symbol free formulas
- Converting functions symbols into relations symbols
- Uniformize the arity of relations
- From signatures with only constants functions to function symbol free signatures
- From several relations to one, arity incremented by 1
- Mapping a formula into a finitary signature
- Decidability Results
- Signature Classification
- Decidability of FSAT for monadic signatures
- Removal of function symbols from full monadic signatures
- From binary singleton to a n-ary function and a unary relation
- Common Tools for reductions
- Collection of high-level synthetic decidability results
- Collection of high-level enumerability results
- Collection of high-level synthetic undecidability results
- Summary File