Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\) (Q946579): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Functional interpretation of Aczel's constructive set theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Handbook of proof theory / rank | |||
Normal rank |
Latest revision as of 17:37, 28 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\) |
scientific article |
Statements
Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\) (English)
0 references
23 September 2008
0 references
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}\).
0 references
functional interpretation
0 references
admissibility of rules in \(\text{CZF}^\omega\)
0 references
constructive set theory in all finite types
0 references
q-hybrids of translations
0 references
modified realisation
0 references