Intuitionistic predicate logic of constant domains does not have Beth property

TL;DR

This paper demonstrates that Beth's definability theorem fails in intuitionistic predicate logic of constant domains without identity, highlighting limitations in the logical properties of this system.

Contribution

It provides a proof of the failure of Beth's property in a specific intuitionistic logic setting, extending understanding of its logical limitations.

Findings

Beth's property does not hold in the logic

Interpolation failure is demonstrated

Highlights limitations of intuitionistic predicate logic

Abstract

Drawing on the previous work on interpolation failure, we show that Beth's definability theorem does not hold for intuitionistic predicate logic of constant domains without identity.