One useful logic that defines its own truth

TL;DR

This paper discusses existential fixed point logic (EFPL), highlighting its unique ability to define its own truth within the logic, and provides a proof of this property.

Contribution

It demonstrates that EFPL can define its own truth, a rare property, and emphasizes its potential applications and interesting features.

Findings

EFPL can define its own truth within the logic

The paper provides a formal proof of this property

EFPL has attractive properties for applications

Abstract

Existential fixed point logic (EFPL) is a natural fit for some applications, and the purpose of this talk is to attract attention to EFPL. The logic is also interesting in its own right as it has attractive properties. One of those properties is rather unusual: truth of formulas can be defined (given appropriate syntactic apparatus) in the logic. We mentioned that property elsewhere, and we use this opportunity to provide the proof.