English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We study finite first-order satisfiability (FSAT) in the constructive settingof dependent type theory. Employing synthetic accounts of enumerability anddecidability, we give a full classification of FSAT depending on thefirst-order signature of non-logical symbols. On the one hand, our developmentfocuses on Trakhtenbrot's theorem, stating that FSAT is undecidable as soon asthe signature contains an at least binary relation symbol. Our proof proceedsby a many-one reduction chain starting from the Post correspondence problem. Onthe other hand, we establish the decidability of FSAT for monadic first-orderlogic, i.e. where the signature only contains at most unary function andrelation symbols, as well as the enumerability of FSAT for arbitrary enumerablesignatures. To showcase an application of Trakhtenbrot's theorem, we continueour reduction chain with a many-one reduction from FSAT to separation logic.All our results are mechanised in the framework of a growing Coq library ofsynthetic undecidability proofs.

Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens