4 citations · 12 across the 20 of their papers we have counts for
6 papers · 1 filter
Strong negation in the theory of computable functionals TCF
Nils Köpp, Iosif Petrakis
We incorporate strong negation in the theory of computable functionals TCF, a common extension of Plotkin's PCF and Gödel's system , by defining simultaneously strong n…
The Role of the Fifth Postulate in the Euclidean Construction of Parallels
Iosif Petrakis
We ascribe to the Euclidean Fifth Postulate a genuine constructive role, which makes it absolutely necessary in the parallel construction. For that, we present a reconstruction of…
Sets completely separated by functions in Bishop Set Theory
Iosif Petrakis
Within Bishop Set Theory, a reconstruction of Bishop's theory of sets, we study the so-called completely separated sets, that is sets equipped with a positive notion of an inequali…
Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
Iosif Petrakis, Max Zeuner
Bishop's measure theory (BMT) is an abstraction of the measure theory of a locally compact metric space , and the use of an informal notion of a set-indexed family of complement…
Univalent typoids
Iosif Petrakis
A typoid is a type equipped with an equivalence relation, such that the terms of equivalence between the terms of the type satisfy certain conditions, with respect to a given equiv…
Constructive Combinatorics of Dickson's Lemma
Iosif Petrakis
We study constructively the relations between the finite cases of Dickson's lemma. Although there are many constructive proofs of them, the novel aspect of our proofs is the extrac…