A note on inconsistencies caused by fixpoints in a cartesian closed category (Q749648): Difference between revisions

From the note: ``The results indicate the different nature of domain theory and \(set=topos\) theory or, in other words, that programming requires other foundations than even a constructive set theory.... Domain theory provides a semantics for recursive programs via least fixed points. Categories of domains are typically cartesian closed in order to accommodate functions of higher type where the parameter passing mechanism is call by name.... Hence cartesian closed categories [CCC] with fixed points axiomatize the paradigm of recursive programming with higher types. The inconsistent results explain why such a language cannot be enriched by certain infrastructure [typical for set or topos theory] as disjoint sums.'' A category C is called inconsistent if all its objects are (isomorphic to) terminal (1). An object A has fixpoint property if for every morphism f: \(A\to A\) there exists a morphism Y(f): \(1\to A\) such that \(f\circ Y(f)=Y(f)\). Then it is proved that: 1. CCC with fixpoints is inconsistent if it has either an initial object, or coproduct \(1+1\), or equalizers, or natural number object. 2. CCC such that the coproduct \(1+1\) has the fixpoint property is a preorder category and \(A\cong 1\) iff A has a global element a: \(1\to A\). 3. Heyting algebra objects H are trivial in any CCC with fixpoints. 4. A CCC with finite coproducts is a preorder category if for some object D either [D\(\Rightarrow 2]\) is a retract of D, or \(D\cong 1+[D\Rightarrow D]\). Moreover, in this case \(D\cong 1\).