Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\) (Q946579)

By means of translation technique, the author investigates admissibility of various rules in \(\text{CZF}^\omega\) -- constructive ZF in all finite types. All five translations used are in the spirit of Gödel's Dialectica translation. Three are based on realizability. The author's \({}^ \times\)-translation is a modification of \textit{W. Burr}'s one [cf. Ann. Pure Appl. Logic 104, No.~1--3, 31--73 (2000; Zbl 0959.03043); also, the details of \(\text{CZF}^\omega\) can be found here], and his \({}^ {\times q}\)-translation is a further variation à la \textit{J. Diller} and \textit{W. Nahm} [Arch. Math. Logik Grundlagenforsch. 16, 49--66 (1974; Zbl 0277.02006)]. The author investigates five rules: weak axiom of choice, independence of Harrop premises, Markov principle for \(\Delta_0\) formulas, the existence property (EP), and the existence definability (ED). Here, ED claims: if \(\vdash\exists x F(x)\) then there is a term \(t\) (of the same type as \(x\)) such that \(\vdash F(t)\). EP is a weaker rule, just saying that there are \(S\) and \(V\) such that \(\vdash S\neq\emptyset\wedge\forall y\in S\,F(Vy)\). The first four rules are shown to be admissible. Needless to say, one translation can show the admissibility of more than one rule, and one rule can be handled by different translations. The admissibility of (ED) is still unsettled, but the author reduces it to the special case where \(F\) is a \(\Delta_0\) formula and \(x\), \(t\) are of type \(o\). He also gives a detailed proof of the interpretation theorem for the \({}^ {\times q}\)-translation: if a formula \(A\) is provable, so is \(A^ {\times q}\).