@JorgeStolfi @dymaxion @whknott
Part of understanding these systems and their tremendous power is recognizing that there are undefined terms and knowing exactly what you have assumed through the consensus of language and conventions of meaning.
Do you want to purge subjectivity from mathematics? Good luck with that.
But I think it's also worth asking WHY so much of the mathematics of a century ago was focused on this goal? Why did otherwise brilliant people burn up so much time chasing it?