I’m a mathematical fictionalist, so I’m happy to grant that there’s a good sense in which mathematical discourse isn’t strictly true, and doesn’t need to be.
Are you asking for a definition of an intuitionistic ‘exists’ predicate, or for the intuitionistic existential quantifier?
First, if you accept that mathematical constructs are fictional, why do you consider it valid to define a concept in terms of them? Second, I admit I wasn’t clear on this issue: The salient part of intuitionistic type theory isn’t intuitionism, but rather that it is a structural theory. This means that statements of the form “exists x, P(x)” are not well defined, but rather only statements of the form “exists x in A, P(x)” can be made.
I’m a mathematical fictionalist, so I’m happy to grant that there’s a good sense in which mathematical discourse isn’t strictly true, and doesn’t need to be.
Are you asking for a definition of an intuitionistic ‘exists’ predicate, or for the intuitionistic existential quantifier?
(Note: I added a link in my previous comment)
First, if you accept that mathematical constructs are fictional, why do you consider it valid to define a concept in terms of them? Second, I admit I wasn’t clear on this issue: The salient part of intuitionistic type theory isn’t intuitionism, but rather that it is a structural theory. This means that statements of the form “exists x, P(x)” are not well defined, but rather only statements of the form “exists x in A, P(x)” can be made.