Project Page Index Table of Contents
  • Finiteness
    • Pigeonhole principle
    • Definitions of finiteness, weak and strong
    • Finite quotient by a decidable equivalence
  • Synthetic Computability
    • Reductions
    • PCP as defined in the synthetic undecidability library
    • The Binary Post correspondence problem
    • Utilities
    • Decidability and discreteness and closure properties
    • Enumerability and closure properties
  • 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
    • Reduction from BPCP to specialized FSAT
  • Model Discreteness and Interpreted Equality
    • FSAT and FSAT over discrete model are equivalent
    • FSATEQ reduces to FSAT
    • The first order theory of membership
    • Construction of the Hereditarily Finite Sets model
  • Compressing n-ary Relations to binary Membership
    • Kleene's greatest fixpoint of omega-continous operators
    • Binary trees as concrete Hereditarily Finite Sets
    • The Type of Hereditarily finite sets
    • From Σ=(ø;{R^n}) to Σ=(ø;{R^2})
  • 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
    • Decidability results for FSAT
    • Removing constant propositions from monadic signatures
    • Removing constant functions from monadic signatures
    • Removal of function symbols from propositional signatures
  • 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
Generated by coqdoc and improved with CoqdocJS