Post #1889742

@carloangiuli But I do wonder about this, for a long time. Gordon Plotkin proved, using classical mathematics, that an element of a dcpo in the domain of discourse of PCF is computable if and only if it is PCF definable from parallel-or and parallel-exists. Can this be formulated and proved constructively?