Limitations of knowledge according to the Intuitionist Type Theory

I've started reading a book on Intuitionist Type Theory, by J.G. Granstrom. More than half of it goes over my head but some remarkable ideas occasionally get stuck between the ears. For example, when he makes a definition of a set, he states that an element can be defined "in any way whatever, but always without reference to the totality of sets."
On the one hand, I understand that this technical limitation addresses the Russell's Paradox. On the other hand, it says loud and clear that we even theoretically can't handle the totality of all sets. Moreover, we should not even make an assumption that we might know the totality.

Another interesting statement from the book is that the Law of Excluded Middle is a not a matter of logic, but rather of existence. Therefore, if a proposition is true, it does not logically follow that its negation is false, and vice versa.

upd: due to the logical limitations described above, assumptions like this one "Пусть совокупность всевозможных состояний вселенной описывается набором параметров V1,V2 .... VN" look highly suspicious. If we can't handle the totality of all sets, we can't describe all possible states of the world in a logically consistent way.

Плодородная американская почва

Был как-то у меня знакомый голландец - Ян. Женился рано, по любви и все такое, но после восьми или десяти лет брака не было у них детей. И так старались, и эдак, а дети не получаются. Просто беда. Они расстраивались, конечно, но ничего сделать не могли, а в пробирке не хотели - значит, не судьба. Решили, раз такое дело, будем жить в свое удовольствие, путешествовать, жить и работать, где попало. Для начала, приехали в Америку по контракту на 3 года. Через два месяца после приезда, жена забеременела и родила мальчика. Через год опять забеременела и родила девочку. Контракт кончился и они, счастливые, уехали обратно к себе в Голландию с двумя детьми-американцами. Что бы им такое привезти в подарок?

Absolutely beautiful

If in an expression, whose content need not be capable of becoming a judgement, a simple or compound sign has one or more occurrences and if we regard that sign as replaceable in all or some of those occurrences by something else (but everywhere by the same thing), then we call the part that remains invariant in the expression a function, and the replaceable part the argument of the function. - Frege.

Now imagine that we are talking about a piece of infrastructure, e.g. a road. Cars are replaceable (transient), the road is not. Nevertheless, there are certain times when the type of cars changes in some interesting way, e.g. from the horse-driven carriage to the automobile. As a result, the road becomes replaceable, i.e. it becomes an argument relative to the car type. From this perspective, a purpose of innovation is to create a type of variable that requires a new type of function. I wonder if this stuff can be formalized.

upd: it follows that the electric car is a smaller innovation, if any, than the self-driving car.