[16:53] <YYZ> Cale, I think of the same "leveling" between objects in physics, including theoretical "objects", and a metaphysical language to describe the physical objects and theories (as objects)
[16:53] <Cale> So that interpretation will let us translate formal proofs in the first order theory of groups (which are trees or sequences of symbols, typically encoded using set theory or type theory), into informal proofs of various properties of an arbitrary group.
[16:53] <nikoma> I find it interesting that purely algebraic structures seem to be studied a lot (universal algebra), but purely relational structures don't seem to be studied that much.
[16:53] <YYZ> nikoma: what defines a purely relational structure?
[16:54] <Cale> nikoma: That's a reasonably valid observation. There's a lot of order theory out there though.
[16:54] <YYZ> "order theory" defines relational structure ?
[16:54] <Cale> (but even that's not usually purely relational)
[16:54] <Cale> YYZ: nikoma is referring to these ingredients we add to our rules of first order logic -- function and relation symbols
[16:59] <YYZ> nikoma: you asked, but Cale's elaboration about theorems as objects in models is precisely the required sort of scientific model needed, one which ranges as a model over the entire field of scientific "objects" and arguments


Can I assume these people are discussing "a prison break" from mathematical logic?   (I'll get back to this later)