Church's thesis from the point of view of provability interpretation (Q1823243)

The paper considers a natural extension of one usual way to provide a provability interpretation for the intuitionistic logical language in the arithmetical language as follows. For each arithmetical formula F let tr(F) be a result of prefixing \(\square\) to each subformula of F, and let \(F^*\) be the result of an interpretation \(\square Q\) as Q\&Pr[Q] in a formula tr(F). Here Pr[Q] is the standard formula of provability of Q in Peano Arithmetic. The paper demonstrates that if F is one of the following formal versions of Church's thesis: CT, CT!, ECT, nCT, then the arithmetic formula \(F^*\) is false in the standard model of arithmetic.