In logic non-existing objects have all properties, including contradictory ones. This follows from the fact that in propositional calculus from a contradiction (or from False) everything can be concluded. I.e., P /\ ~ P -> Q.
One could conclude that the definition of -> is not very logical but if one is to attach a formal meaning to -> it would seem hard to avoid this. One would need conditions like that when P -> Q we have to have that P and Q are related in some way but that does not sound like something that is very easy to formalize.
It also does not matter whether one uses intuitionistic logic. P /\ ~ P -> Q still holds.
In type theory False is the empty type and proving something about it can be done with case analysis. Since it is the empty type there are zero cases and one is immediately done and can prove anything.
One could conclude that the definition of -> is not very logical but if one is to attach a formal meaning to -> it would seem hard to avoid this. One would need conditions like that when P -> Q we have to have that P and Q are related in some way but that does not sound like something that is very easy to formalize.
It also does not matter whether one uses intuitionistic logic. P /\ ~ P -> Q still holds.
In type theory False is the empty type and proving something about it can be done with case analysis. Since it is the empty type there are zero cases and one is immediately done and can prove anything.