OK, maybe if we look at some other definitions of equality we can get a grip on it? In set theory, you say that two sets are equal if they've got the same elements. How do you know the elements are the same i.e. equal? You just know.
If we have the axiom of foundation -- or, more perspicuously maybe, the principle of epsilon-induction its equivalent to in presence of other usual axioms -- the picture is less mysterious.
Yes, in order to tell if A and B are equal, we need to see if they have the same elements, but in order to do that we need to already know how to tell if any two elements are the same, and so on, which does not seem to actually get us anywhere.
Except that when A or B has no elements, we don't need to have already figured out any way to tell two elements apart -- if A has no elements but B does, then A and B are not equal, and if both A and B have no elements, its trivially true that all their elements are equal, so A is equal to B, and they are both the unique empty set. Given foundation, all membership chains terminate at the empty set, so we've now got a way to use extensionality -- the principle that two sets are the same if they have got exactly the same elements -- to give us a non-circular notion of equality by grounding in the empty case.
(If we don't have foundation, or if we indeed actively welcome non-well-founded sets, we do need something beyond extensionality to give a well-defined notion of equality, e.g. bisimulation in case of the anti-foundation-axiom.)
It's sometimes thought or said that the second incompleteness theorem shows that formal systems such as PA are in some sense "incapable of self-reflection", and their incapability to prove their own consistency reflects this lacuna in their "cognitive capabilities" or something along those lines.
Löb's theorem highlights how this is a much deeper phenomenon: it's not just that these formal systems lack abilities, or formalizations of relevant mathematical insight, or whatever; no, it's that it's formally impossible for any consistent system of the relevant sort to even baldly assert their own consistency, on pain of inconsistency!
That is, we can for instance construct, using the diagonal lemma, a sentence A such that A is, provably in PA, equivalent to "PA + A is consistent" -- thus creating, in a sense a theory that just asserts its own consistency, in the form of a random assertion about Diophantine equations or however we carry out the arithmetization of syntax, for no particular legible reason whatever -- but we then find that PA + A is inconsistent! (This is an immediate consequence of the second incompleteness theorem.)
I recommend Torkel Franzén's excellent "Inexhaustibility -- a non-exhaustive treatment" for anyone pondering these matters.
It's heavily implied in the novels we only see the "disaffected" lot -- people who experience ennui, etc. and are drawn to find meaning out of a sense of meaninglesness even in somewhat inadvisable ways -- and the whole of Culture is mostly exploring the state space of consciousness and the nature of reality, sort of LARPing individual humanity as a mode of exploration -- you can for instance upgrade yourself from a humanoid into something resembling a Mind to a degree if you want to, it just seems this is not the path we mostly see mentioned. It's just that that sort of thing is not narratively exciting for most people, and Banks is, after all, in the entertainment business in a sense.
There are interesting themes explored in the books that go beyond just the "cinematic fireworks and a sense of scale". For instance, it is suggested that the Culture could have the option to simply opt out of Samasara, but refuses to do this out the suspicion that the possibility of Sublimation -- collectively entering Nirvana -- would be to cop out, preventing them from helping sentient beings. (There's a conflation of sapience and sentience in the books, and disregard for the plight of sentient beings who are not "intelligent" to a sufficient degree, but otherwise there's an underlying sentientist/truth-seeking slant to it.)
The Minds of Culture are also represented to be basically extremely sophisticated consequentialists with appreciation for "Knightian uncertainty" and wary about total certainty about their understanding of the nature of reality, although it's not clear if they're e.g. super intelligent negative utilitarian Boddhisattva beings -- in the Culture world there seems still be belief in individual, metaphysically enduring personal identity extending to the Minds themselves, but it might also be that this is again a narrative device -- or some sort of anti-realists about ethics but on the side of the angels just for the heck of it, because why not, what else could there be to do? Or some combination of both -- like, if you've solved the problem of suffering, in the sense of having calibrated your efforts correctly, why not dance super gracefully and blissfully through it all, creating positive experiences in the course of this process? One theme that suffuses the work is the ethical responsibility of super-intelligent beings, cooperation strategies and a sort of irreverent spirit of ethical seriousness and truth seeking that's very EA like.
That said, personally I think the work of suffering-focused ethicists -- including those long past in many contemplative traditions -- including "Those who walk away from Omelas" are a very important part of the "heritage of humanity", in a sense a testament to our ability to see beyond our evolutionary programming and into what really matters: the well-being of all sentient beings. But a Culture Mind of the ship named "Boddhisattva" representing a fictional culture that refuses the easy way out out of suspicion to do so would to shirk one's ethical duties would not be amiss either. This especially so if LLMs are making the world slightly fictional in some weird sense and might latch on into the most sophisticated and interesting attractors...
Right, but models of set theory without equality can contain many indistinguishable "copies" of the same set, and in this sense the "extensionally equivalent" predicate does not define equality (in the sense of the identity relation on the universe of the model).