is this true for any FOL structure or am I missing something?
I think it's true for any FOL structure
@alexthecamel Yep. One caveat is that it often has to be constructive first order logic rather than classical first order logic, because the law of excluded middle fails in many useful categories. E.g. law of excluded middle can be used to define discontinuous functions, and so doesn't hold topologically.
@alexthecamel First order logic structures in general requires toposes, not just products. However, it is true for any algebraic structure (monoids, groups, rings, ... BUT NOT fields because fields aren't a true algebraic structure due to having a != 0 condition on division).
is there anything nontrivial here? I guess we are now allowed to write "topological" before anything in FOL and have it make sense
similarly things with some kind of symmetry