Allowed definitions in some intuitionistic formal system

35 Views Asked by At

I want to introduce a definition, while working with intuitionistic mathematics. I was told that I can define anything, as long as the proofs are valid intuitionistically. But how do I work with a new definition? What if the description of the definition cannot be expressed with intuitionistic logic? Do I make it a set, as in, $x$ is an element defined as $A$ when $x \in A$?