Categories
Tech

Customer Support and Data Privacy

One “natural” good intention that can end up undermining data privacy is enabling customer support. For example, say a website was built so that its website owners could not access passwords even if they wanted to (no “master users” or “superusers” of the database.) This would seem to be a great design decision from the perspective of security and privacy. But if a customer forgot their password and wanted to get back into their account, without such “superuser” access this could technically be impossible (depending on the technical architecture of the website.) So companies do end up introducing such “database superusers” since users end up making mistakes in this vein or wanting to undo their actions. To aid customer support personnel further, they often introduce “God Mode” tools that allow them to perform any actions on behalf of any user. But the problem is that such tools then get abused by employees, far beyond the purpose they were created for, for example to stalk users. This is further exacerbated by smaller companies de-prioritizing proper controls on such tools because of pressure to deliver quickly, and even for companies that do have such controls, I believe those may not be enough; for example, some companies do auditing and after-the-fact disciplining, but I would argue that by that time the damage is already done. Scandals connected to this have in fact happened in major companies like Uber.

Also, from a development perspective, developers would like to test and analyze their apps in environments that are as close to the “real world” as possible (how users would actually use them.) It is well-known that even with developers’ best efforts to guess all the scenarios of possible usage patterns, they can fall short of the breadth of what happens in reality when the app is released. This means that developers would like test data to be as close to real user data as possible, even possibly a small randomized sample of actual user data. Also, when troubleshooting real customer issues, the more information developers have to work with, the more effective they can be in helping out. This leads to incentivizing the hoarding of user data, with the reasoning that “it could be used later to make the user experience better and help users more.” But such troves of data that are amassed are then attractive targets for hackers and bad actors, and in companies that store even more data, the potential for subsequent damage from any hack is far greater. And as a company operates for longer and longer, the probability that they could slip up gets higher, especially with the necessity of continual maintenance of their systems.

Companies usually address this with internal data privilege enforcement systems, where only certain employees are specially authorized to deal with user data, and only the data that they specifically need for a legitimate business purpose. Use of “God Mode” tools is tracked, producing detailed audit trails, and the price of any misuse is severe disciplinary action, including termination. However, while this is well-intentioned as a setup, it still doesn’t feel adequate to me: after-the-fact disciplinary action is not enough when the damage is already done, and there does not usually seem to be much external transparency into who internally is granted access to user data internally for what purpose — this is all owned within the company, and for the purpose of a smoother customer experience it is supposed to be invisible to the customer (as if it is something they shouldn’t need to worry about.) A more robust system towards the requirement of providing the transparency that customers deserve would be one that externally exposes and audits these internal data privilege grants better.

I also have a few general points on communication and discussion of this issue. First, I think too much of the discussion is symptoms-focused rather than root cause-focused. It’s easy to criticize a certain company for having data privacy violations, but the more interesting and important question to me is what incentives led to those violations happening, especially if such incentives could apply to anyone and redirect them, even those who started with good intentions. This especially applies to companies that were once hailed as privacy supporters, and then in sudden heel turns (often derived from one or a few news articles) condemned as privacy saboteurs. This point can also be generalized beyond data privacy to many other issues people often criticize the tech industry on today.

That said, I think there is too much pressure rampant throughout the industry to deliver quickly, and while some of that pressure is a good thing, it cannot be to the point that it crosses certain fundamental boundaries, especially for example those concerning security and privacy. I do believe these boundaries can be crossed too often sometimes these days, and while this doesn’t necessarily happen with malicious intentions (“We’ll fix it later”), regardless it is not acceptable, and we should be much stricter in upholding those boundaries, no matter what.

In companies that do have proper controls (what I described with an internal grant system and a thoroughly audited God Mode tool), I wonder if a “God Mode” tool could be built that has customer consent technically baked in. At first glance, this seems to not make much sense — say for example that such a tool was built, where a customer support agent technically could not access it without a customer’s consent. How would the customer provide that consent, and how would their provision of it be technically verified? After all, if the customer is the one who forgot the very thing that allows them to access their account (e.g. their password), then from the perspective of the website, how can it know that they are who they claim they are, and therefore that the consent was valid? And if they are able to prove that, then they could just access the website directly using that proof without any customer support in the loop. In fact, this would essentially just be the same as logging into the app directly, possibly with a “forgot password” flow that still requires some other authentication. With a robust enough “forgot password” flow (which must be secure in requiring enough alternative proof but also covering enough cases of what users could forget — this seems actually to be a tricky problem that we’re glossing over here), this could presumably work for many cases, but for those customers where that flow doesn’t work, they would never be able to get back into their account again, no matter how much a human tried to help. Maybe some partial technical verification of consent could be possible: for example, the system could use voice parsing via AI to check whether the customer agent is speaking to the intended user, and if so then grant consent; but with AI today this could also potentially be faked, and this would also require storing user voice data in order to perform the comparison. In general, any alternative authentication mechanism would require storing user data along the lines of that authentication method in order to perform such a comparison.

I’m not sure what a better solution here could be. But external auditing of internal data privilege grants would be a start, and in general more external transparency around how these systems are built and why the tradeoffs exist would be important to provide customers with the fundamental knowledge that they should have when navigating technology.

Categories
Math

Teaching Abstraction’s Purpose in Math

I’ve recently been rethinking my approach to teaching abstraction in math. The approach I used to take — which I also think is the dominant one amongst math teachers, based on what I’ve often seen (not based on a scientifically analyzed comparison per se, but still seemingly so anecdotally and experientially) — is to present abstraction as enabling greater applicability: if I identify a few properties obeyed by the concrete system currently under my study and look at just the consequences of those properties, I’m now much more powerful, since my conclusions apply to any system that satisfies those properties. But if someone protests, “what is the use? what other system would we apply this to?”, the default response would be to label this as a lack of skill/imagination. We say that abstraction is an important skill for pursuing mathematics at a higher level, and you just need to have the imagination to see ahead that systems could exist that that abstract theory yields fruit for, without needing specific examples right now.

I do still believe that some amount of greater imagination in this vein is necessary to succeed in and truly avail of the fruits of mathematics, and that this is an important skill for people in general to develop regardless of whether they go on to actually be mathematicians. But that is a topic for a different post. With regards to abstraction, I now think a more effective way to justify it is based on clarity: the reason why we isolate certain properties is just to help us see what behavior is truly dependent on what characteristics. With a whole soup of functionality swirling around in a particular concrete system, this helps us truly “pin things down” and gain a greater conceptual understanding in the process. This is aligned with programs like reverse mathematics, which are “natural” in their desire to simply gain greater understanding, regardless of whether the increased abstraction is actually applied later. And the greater clarity has “real” applications not in the math itself, but in our cognitive understanding of it, as math is ultimately performed by humans. (And AI agents these days, but still in a way that was constructed by humans in the first place — but I digress. My thoughts on AI for math are best left to another post.)

As a concrete example, take model theory. I’ve often thought about what would be the best ways to teach various concepts in model theory, and earlier I would have emphasized the greater abstraction (for example, topics like the general definitions of homomorphism and isomorphism for a first-order structure) as enabling greater applicability. But while this is technically true, if I really look back at it, look back at my own model theory-oriented projects (like prototype model theory), that’s not truly the reason I even wanted to go into model theory in the first place. Instead, the reason was the clarity gained by working at that level and stripping away all the details that don’t matter in that context. When we see so many different instances of the concept of homomorphism or isomorphism in different abstract structures, it is a natural desire to pin down a more general formulation of the concept to really “capture” what it means, regardless of whether I actually have another system in mind I want to apply that general definition to right after.

This connects to philosophy too: why do humans study the subjects in math they choose to study? Now, there are multiple reasons and factors here, and part of the breadth and diversity of math comes from the fact that different topics can be reached and studied from a variety of underlying philosophical motivations. For example, historically, some abstractions did in fact arise from mathematicians seeing multiple examples for them, and it makes sense that some of these examples are just hard to cover in an introductory course where you still want to discuss the abstract theory to prepare the student better for later, so you would then just ask the student to suspend their disbelief. But another important reason, and one that I now think should be emphasized more pedagogically, is simply clarity, regardless of greater applicability. Part of the motivation for Bourbaki’s program, as well as other abstraction-oriented programs, can be seen as providing greater clarity on ideas rather than true application-enabling setup, and maybe presenting subjects with this motivation can help students for the same reasons that these mathematicians sought that very sort of presentation themselves.

Categories
Math

Non-Standard Axioms for Various Math Structures 10

Under the title of this series, in 2023 I had investigated a particular math idea of mine. My last post on this was the ninth in the series. My thoughts on this topic as well as adjacent topics have evolved since, and I’m coming back to this after some time. I will summarize some of the thoughts I’ve had since and continue this thread.

First, I now support removing proper classes from mathematics (see the linked article for more justification of this approach.) Thus, instead of talking about logical generation theory for a class of models C, we note that the classes actually of interest would be of the form “the class of all models of a theory T,” so we can instead talk about logical generation theory of a theory T. There is also another usage of “class” in “logical generating subclass”; we can get rid of this by noting that anytime we want to describe a class (like a subclass), we would want to do so by a particular property (the class/subclass of models with that property) — this always makes sense if we interpret the word “property” generally enough. And such a property would always be formalizable in some sufficiently expressive logic, just possibly not the logic that we started with when describing T. For example, when we say that “a logical generating subclass for the class of groups is the class of symmetry groups,” we can instead say that “a logical generating theory for the theory of groups is the theory of symmetry groups.” If needed, we can change the logic in question to accommodate this. (I don’t even think such a change of logic is needed for that group example, since to say that, we don’t need to formalize the logic that can express the property of being a symmetry group; we already have a formal definition of symmetry groups, and we can talk about their “theory” as the common equational theory of them, in equational logic.)

But actually, for the ensuing discussion here nothing would change anyway if we just assumed logical generating theories identified set-sized collections of models. So for now, we will talk about logical generating sets (LGS’s) of theories.

As we already know, any equational theory has a singleton logical generating set as a free object over an infinite set. (Actually, I think I should write out my proof more formally sometime. But I’m convinced of the truth of this result for now.) But the model in this singleton really “contains no more utility” in deriving consequences of the theory, given its very definition — proving something in this singleton is just as hard as proving something directly from T. So in what sense could logical generation theory “help”? What would be an application pathway?

Let T be a theory in our chosen logic L, and say we know an LGS S for T. One possible application goal is:

1. Prove results about T, given our familiarity with the members of S.

The “familiarity” with the members of S is the key here: that’s why saying that the free object is a singleton LGS isn’t really more “useful.”

Let’s check how this could work. Given a statement (sentence) in the language \mathcal{L} of T, can we decide it from T? (“Decide” here could mean by computational algorithm as in decidability theory or by human effort.)

Well, this is actually pretty simple now, assuming we have finite S and can check this for any member of S. Namely, say S = \left\{ S_{1},\ldots,S_{n} \right\}, and say the sentence (call it \phi) is decidable in each of the S_{i}. We know that since S is an LGS for T, by definition the class of all models of T is the class of all models that satisfy the common sentences of all members of S. So if a sentence is satisfied by every member of S, then it must follow from T, aka be decidably true from T. Conversely, can we show that if a sentence is decidably true from T then it must be satisfied by every member of S? If that’s the case then we can say that a sentence is satisfied by every member of S if and only if it is decidably true from T. Assuming based on our familiarity with the members of S that we can quickly check whether a sentence is true in a member of S, we can then judge for sure whether any sentence is decidably true. If our logic includes negation (e.g. first-order logic), then we can use this to judge whether any sentence is decidably false. Hence, we could judge any sentence to be either true, false, or undecidable from T in a logic that includes negation, and either decidably true or not in a more restrictive logic (like equational logic.)

So is this true? Is our conjectured converse true? Assume a sentence (call it \phi) is decidably true from T. Then it must be true in every model of T. So the class of all models of T, which is the class of all models that satisfy the sentences common to the members of S, must have every member satisfy \phi. So the class of all models that satisfy the sentences common to the members of S (call this set of common sentences T^{'}) must have every member satisfy \phi. In other words, the class of models of T^{'} must have every member satisfy \phi. This means that T^{'} implies \phi. But T^{'} is commonly satisfied by every member of S, so every member of S satisfies \phi. QED.

So we can use LGS’s of theories and information about the members of the LGS’s to decide whether sentences are true, false, or undecidable from the theories, at least in a logic with negation, and otherwise to decide whether sentences are true from the theories.

After this, our next goal in the application pathway is:

2. Derive information about specific models of T.

This is very doable very naturally following on goal 1! In fact, remove T from consideration and just say we want to study a specific system s. This system will be a model of many different theories. We can derive information about s by picking one such theory, T, and then seeing whether a particular sentence about s is decidable from T. If it is, then we’ve decided that sentence for s too. If it is undecidable, then further study is needed. We can rinse and repeat that approach with multiple theories T. With some ingenuity in picking T and application of logical generation theory, we can hopefully eventually decide our target sentence for s.

Note that this shows that we’d like to find LGS’s in a logic with negation since that’s the most powerful, but if the theory for equational logic is simpler / easier to classify more fully then that can still help partially too.

But remember that this hinges on our familiarity with the members of an LGS. So we should base these members off of numbers and other primitive concepts — if a member of an LGS was described purely abstractly, like for the free object, then satisfaction in that model wouldn’t be easier than theorem proving with T itself. We need specific models based on primitives that we have better insight into the decidability of, and we need to understand why we have better insight there — the asymmetry here in the “familiar” vs “unfamiliar” is what would allow logical generation theory to be useful.

We’d like the members of S to maybe be:

  • finite sets, \left\{ 0,\ldots,n - 1 \right\}, with suitable operations/relations/etc.
  • or generally, special subsets of \mathbb{R} with suitable operations/relations/etc., or sets directly based on these

But with cardinality theory, this is the same as just picking any finite, countable, or \left| \mathbb{R} \right|-sized set (or even 2^{\left| \mathbb{R} \right|} sized, or so on with increasing powers of 2) if we allowed the operations/relations/etc. to be whatever. So it wouldn’t actually increase familiarity.

Or maybe we can turn that back around: we can study any set of such a cardinality productively by defining it in terms of numbers and operations/relations/etc. on those numbers, and then applying number theory and/or real analysis. Let’s say henceforth that this is possible.

Decidability for members of the LGS would then fall under number theory, real analysis, and derivatives of these. Philosophically, this eventually boils down to the primitive acceptance of numbers, which we then join all other branches of mathematical logic in applying numbers as primitive concepts to the study of logic. To the level that logical generation theory can yield algorithmic answers to decidability — the fundamental question of computational proof theory — we should ask how the direction we’re heading in differs from what exists already in this subject, to facilitate newer results. We can also work that back around and possibly use existing proof theory to say something about LGS’s, but that doesn’t provide any more applicability value then.

In general, we can say that logical generation theory would reduce questions about abstract systems to questions in number/primitive-based subjects like number theory and real analysis. In education, so much of the theme of motivating abstract algebra and other abstract subjects is to apply them back to specific systems that they were inspired by; this in some sense would be a reversal of that!

Also, logical generation theory is not useful as a theory, rather just a collection of interesting results, if there is no systematization. E.g., if A,B are LGS’s for a theory T, is A \cap B also? If I have theories T_{1},T_{2} and LGS’s S_{1},S_{2} respectively, can we form LGS’s for T_{1} \cup T_{2}, T_{1} \cap T_{2}, and so on in terms of S_{1} and S_{2}? If we have some “interesting” / “useful” LGS examples and then this systematic theory that allows us to derive more, that is where logical generation theory could truly be useful. Otherwise we would just be proving each result “on its own” and logical generation theory would just be a header for a few related and interesting-on-their-own theorems. (This is what my investigations seem to have produced so far — cool results but independently for specific cases.)

For this application pathway to work, we would need to check that the models we’re defining are actually more familiar, and if we can define operations/relations/etc. however we’d like, then we have flexibility but at the possible cost of familiarity. If we are dealing with the familiar models like all of the integers or all of the reals, then these satisfy specific properties that mean they could only apply to a very small subset of all possible theories (since for S to be an LGS of a theory T, all the members of S must satisfy T.) But actually, this could be addressed by identifying certain subsets of familiar sets; for example, for the integers, we know that the integers are an integral domain while the rationals are a field, and the positive integers don’t satisfy certain properties that the integers do (invertibility wrt addition) and the prime numbers don’t satisfy certain properties that the positive integers do (like closure under addition.) If the identified subsets are “interesting” or “familiar” enough but the diversity of such subsets is enough to reflect the breadth of possible sets of properties in a logic, then this could work — although it remains to be seen exactly how that theory would play out.

Another application pathway approach, that could align better with abstract constructions like the free object, could be in relation to universal logic. We know that equational logic has the property that every theory has a singleton LGS, while first-order logic doesn’t, thus it presumably requires a greater number of models to say something like “every first-order theory has an (abstractly constructed) LGS of this size,” if such a result is true. (Earlier I had conjectured the size 2.) If this is true, going further, maybe we can classify the “expressive power” / “diversity” of a logic by the minimum LGS size of a theory in the logic? There are ways to formalize logics abstractly, such as with institutions. (Institutional model theory and institution-independent model theory are keywords here. I personally prefer the former term, as it is less verbose and already communicates the meaning naturally and effectively.) The basic form of the question would be: let L be a logic, like equational or first-order, formalized generally under a framework like institutions. Is there a cardinality c associated to L such that for any theory T in the logic of L, T must have a c-size LGS? Is there a min such c for any logic L? How would this number be related to other measures of expressive strength of L? Is this number guaranteed to be finite?

Also, on second thought, “logical generation” is not a great name; it’s easy to suspect that it could refer instead to a proof-theoretic notion of a “sentence s being generated by a set of axioms A.” Furthermore, logical generation is a closure operator, as we have seen previously in the series, and we suspect that there could be great fruit in applying linear-algebraic notions, yielding terms like “logical basis” or “logical generating basis” and “logically independent” or “logically generatively independent.” (See my series on an abstract approach to generating sets.) These are either clunky or definitely ambiguous.

Instead, a new term I’m using now is “prototype model theory.” This emphasizes that this discussion is part of model theory, and the name itself suggests a suitable, accurate interpretation: given a theory T, all its prototype models are the models of that theory that “are prototypes of different aspects of it, that together cover the full breadth of it,” in a sense analogous to the parable of the blind men and the elephant. Each model has some more specificity (potentially) beyond what T would contain/imply, meaning it covers a smaller breadth of all the models/possibilities of T, but together the models cover everything, so they are worthy of together being called a “prototype model set” (or even “prototype set” for short), even if one of them on their own isn’t fully a prototype in terms of capturing the diversity of T. Applying linear-algebraic notions, we can then talk about prototypal independence and prototype model bases (and we can again drop “model” here to talk about “prototype bases,” if the context of prototype model theory is clear.) We will use this name instead of “logical generation theory” from now on. Thus, writing it out: for a theory T, a prototype set for T is a set S of models of T such that a sentence is a consequence of T if and only if it is true in all members of S, and we can define linear-algebraic notions like prototypal independence and prototype basis on top of this.

I recently asked a question on Math Stack Exchange to gain a deeper understanding of the free object (see the discussion there for more details.) Based on that, I have some references that I can use to learn more; my next step in this project will then be to (broken into sub-steps): (1) produce a more careful proof that any equational theory has a single prototype (via a free object over an infinite set), and (2) with the analogous notion to free object for arbitrary first-order theories (I’m hearing “syntactic category” now), see how this result could be generalized to first-order theories (e.g., can we say that “there is a single prototype if and only if the syntactic category satisfies this property,” in a way where that property is obviously true for equational theories and other first-order theories with single prototypes?)

Actually, we already know what the first-order theories with single prototypes are: restating a previous result more concisely and elegantly, we have that a first-order theory T has a single prototype if and only if it is complete, and in that case, every model of T is a prototype. I suspected earlier that for non-complete first-order theories, 2 prototypes are sufficient, and I thought that this could be established as follows (informal sketch): we have 2 models where for each sentence not implied by T, it holds in one model and not the other. We can pick by say Axiom of Choice which sentence goes to which model, in a way that respects implication (T plus \rho implies \rho^{'}.) Maybe we can take the set of all sentences not implied by the theory, separate them via the Axiom of Choice into two subsets where each is “closed under implication” (and if one subset contains a sentence the other contains its negation), and then syntactically construct two models that each satisfy one equivalence class plus the negation of the other.

If that’s the case, then the “universal logic” application pathway could be moot since maybe the same reasoning could trivialize it: maybe we have that in any logic closed under negation (including first-order logic as well as other logics like second-order and higher-order logic), 2 models are sufficient by the same argument. But actually, if the logic is expressive enough, would this work for any logic? Could a sufficiently expressive logic for example encode the sentence “this is the actual model of the real numbers,” not just “this model is elementarily equivalent to the real numbers,” and thus break the feasibility of syntactically constructing models? What would prototype model theory look like in such a logic? Actually, it seems that if a logic could encode the sentence “this is the specific model M,” then the only model of that theory would in fact be M, and thus M would trivially be a single prototype and in fact the only prototype. Can second-order logic encode “this is the actual model of real numbers” or more generally “this is the specific model M”? What about other well-known logics beyond first-order? Would we still have an “expressive strength cardinality” for well-known logics or would the number be either 2 or trivially 1?

Looking this up, for second-order logic this seems to be exactly the concept of categoricity — and there are theories that are categorical and theories that are not. If we take general theories in a logic like second-order logic, it still seems that this question isn’t moot.

It remains to continue this (at some time — this project is interesting but not currently a priority for me.)

Categories
Math

Problem Reduction Theory

Suppose you have a class of problems you want to solve — the motivating example is differential equations. Say you have a number of reduction methods that reduce one problem to another, or even establish equivalence of problems — for example, say that (1) given a differential equation, we can express the solution function as a power series and transform to a corresponding difference equation (assuming e.g. we only care about sufficiently “nice” / real-analytic / etc. solutions), but also (2) given a difference equation we can relate it to a corresponding differential equation via time-scale calculus. We could imagine we could iterate these reduction methods and keep transforming differential equations to other differential equations as well as other difference equations, potentially yielding great solutions to a number of equations just with these transformations. We could then imagine that for all the reduction methods we know, we could try to understand systematically what all problems we can solve given all possible combinations of these methods. So far, before the advent of AI for math, applying such methods was manual and ad-hoc, with one particular sequence of methods manually derived out for a particular problem, and based on whether the person studying it knew about the methods (so not necessarily optimal.) Is there some kind of general theory we could come up with for the systematic application of problem reduction and equivalence methods? Can AI take advantage of such a theory to solve problems at a scale beyond what humans could achieve alone? This is in keeping with other similarly-themed ideas that are yielding rapid advances today in AI for math.

Let’s formalize this. Say we are dealing with a collection of problems P. We have a collection of reduction methods R, where each method r \in R identifies some problems in P that can be reduced to others in P (essentially, a binary relation on P, which we can denote by a \rightarrow b for problems a,b.) (For e.g. the case above with differential and difference equations, we put both differential and difference equations in P and just identify the reduction method as having “domain” only a subset of P — in general the set of first coordinates of a binary relation is just a subset of P.) The reduction methods must be transitive — or maybe we can just identify R as “easy to query” / not transitive, and then have our theory essentially computationally work with the transitive closure of R. More precisely, we can model it as R being “easy to query” in some algorithmically defined way, and then work on algorithms that can systematize the knowledge represented by R, which essentially reduces to fast computability of concepts related to the transitive closure. So we have P and R, and we can also have a set of equivalence methods E, where each equivalence method is just a binary relation but that also must be symmetric. We can then have a set of solved problems S \subseteq P (which are already given / known as solved.) Starting from S, and given R and E (and some conditions on the “easy query-ability” of R and E), what all problems can now be “effectively” solved in P?

First, assume R and E are both finite, so r_{1},\ldots,r_{n} and e_{1},\ldots,e_{m} with n,m \in \mathbb{Z}_{+} (as R and E come from current knowledge, which is always finite.) Every relation in E is symmetric. Querying for problems a and b whether a certain reduction method r applies to them — we can denote this by a \rightarrow_{r}b — is easy (O(1)), and similarly querying that for a certain equivalence method e is also O(1). Querying whether a problem p \in P is in the solved problems set, p \in S, should also be fast (O(1).) Given this, what is the fastest algorithm for reducing as many problems in P as possible?

There are a couple formalizations of this question. One is the one-problem question: given a particular problem p \in P, how quickly can we decide if p is solved or not given R,E,S, and if so what is the solution? (To answer “what is the solution,” we should say that every problem p \in P has a solution in a solution set O, exactly one solution for each problem, and the solution is known for every problem p \in S, also for each reduction method or equivalence method it must carry information on how it “propagates” the solution forward. So “what is the solution” can be a later follow-up question; we think the decision question is more fundamental first, and intuition suggests that it may not be hard to tack on the additional data if the method pathways must already be followed to address the decision question successfully.) Another question that can be different from the one-problem question is “what all problems in P can be reduced?” This is similar to the distinction between “find the shortest path between these two given vertices a,b” and “find all shortest paths in the graph.” Answering this properly would require some enumerability conditions on P — in the motivating example, P would be infinite and even uncountable to account for all possible equations we could solve, and in general P could be unbounded in cardinality. For now, let’s focus just on one-problem decision.

So we are given R,E,S, with R = \left\{ r_{1},\ldots,r_{n} \right\},E = \left\{ e_{1},\ldots,e_{m} \right\}. For each method in R or E, determining whether it applies to a,b \in P is O(1). For a problem p \in P, determining whether p \in S (the given-solved set) is O(1). We are given p \in P. What is the fastest algorithm to decide whether p can now be solved?

Well, first, we can check p \in S. If not, then we must know that p has a method that applies to it; if not then it can’t be solved. To check this, we would need to check r_{i}(p,q) for each q \in P, but in general if P isn’t finite and without additional structure this wouldn’t be feasible. Actually, we should be able to tell whether a reduction method applies to a particular problem p without needing to identify the problem we think it reduces to — for example, in the motivating example, we know the Taylor series method applies to any differential equation if we restrict to sufficiently nice solutions. And really, there is only one problem each individual method reduces a problem to; different methods yield different problems that are reduced to. So really, the reduction methods aren’t just binary relations, they’re partial functions. But if we model it that way, then is it too restrictive to assume the list of methods is finite? Could a family of reduction methods be “parameterized” by some uncountable variable that yields uncountably many reductions of a given problem or something like that (if it’s only one possible image of the reduction function)? Do we model this as one reduction method (conceptually) or an uncountable family?

Maybe we have finitely many methods to represent finite knowledge, as with an unbounded set we lose the encoding of “how much knowledge we’re working with” — with finitely many methods, each method represents one “conceptual idea” of a method. And each method then can have multiple possible reductions of a given problem. We should be able to query easily (in O(1) time) whether a problem p can be reduced, and then if it can we should be able to get one of the reductions “easily.” But if there are a possibly unbounded number of reductions then how can this be modelled?

Also, it seems with this model that it’s almost like a graph where the problems are vertices and reduction methods are edges, but if the set of problems is possibly unbounded and we don’t have more structural information about the reduction methods then we can’t really say much besides a generic graph algorithm on a possibly infinite graph. Instead, maybe we should see how systematic solution finding can depend on the structure of the methods in some way — this could be a more abstract theory than just a generic ultimately-graph-theoretic algorithm.

Actually, both could be valuable; for our motivating example, the generic framing is not enough, but it could work well in cases where we have less information but the set of problems is finite. So let’s say that we have a branch of our theory which is finite problem reduction theory, where P is finite, and we have another branch which is infinite, and for the infinite case we need more structure (aka some kind of parametrization where we can computationally work with the parameters.)

It remains to continue this.

Categories
Math

Questioning Axiomatic Set Theory

After thinking about it more, the current standard approach to and interpretation of axiomatic set theory seem questionable to me. Of course, the strict logic of the results is not in dispute, but it seems we should be able to assume axioms like ZFC implicitly (as most mathematicians in practice do anyway) and move on. There are a number of reasons to do this, which we will discuss now.

First, the question of a result’s dependence on a certain axiomatic set theory axiom, like the Axiom of Choice, is not as consequential as it is often presented to be. The axioms that have been controversial are those with unintuitive consequences, even when the axioms themselves seem reasonable, but rather than framing those consequences as dependent on choice of axiom, we should understand them as exposing unintuitive but “real” truths about reality. For example, the Banach-Tarski paradox is not something we can just “turn off” by rejecting the Axiom of Choice; instead, it results from using non-measurable sets in the process of deriving something about measure. In general, we should expect that if a process’s steps don’t explicitly preserve an invariant, then that invariant may not hold in the end, though the application of this to that particular scenario is hard to grasp at first.

Second, we should be able to perform the rest of math without ever really mentioning axiomatic set theory anyway, by simply reworking our language to avoid such issues. In this way, we can avoid follow-up topics like classes and Grothendieck universes, which stem from an “unenlightening syntax issue” rather than offering additional “meaningful semantic insight.” For example, instead of talking about the class of all sets satisfying a property P, take an arbitrary “universal working” set U and talk about all the subsets of U satisfying P, or talk about P itself and mention particular sets satisfying P without mentioning the whole class of such sets (for example, in universal algebra, it seems we can avoid talking about equational classes by just focusing on equational theories.) And we don’t need to mention the “larger collection” that all these sets and sets derived from them (e.g. via the power set operation) are in (aka the Grothendieck universe), just as we don’t need to mention the collection of all sets but can still pick out and work with any set in that collection (like we do in abstract algebra and other abstract math subjects: “let S be any set satisfying these axioms …”) To generalize that last point, for any proper class we can talk about as many individual members of that class as we please, without mentioning the full collection of all those members. In this way, we should be able to avoid axiomatic set theory-derived language in all further math without missing anything semantics-wise.

Concerning axiomatic set theory’s ability to formalize the mathematical universe, as I mentioned in my article on separating mathematical logic and set theory, no axiomatic theory can capture all the properties of a type of mathematical object like the integers. The most it can achieve is completeness in a particular logic, which fundamentally doesn’t correspond to the full theory of a concept. But it further happens to be the case that because of Godel’s incompleteness theorem, any “practical” system, including all currently prominent axiomatic set theories, must be incomplete. (“Practical” here corresponds to a particular formalization, which may or may not fully capture an intuitive intended meaning. Nevertheless, the point stands.)

Also, encoding in terms of sets is not the only way to encode mathematics. For example, we can encode mathematical language and thus mathematical information (expressed via language) via bits or numbers, as we do all strings. Sets are not really more “privileged” then than these other encoding schemes.

Finally, if we hold that the “domain of all sets” is a “real thing,” then statements like the Continuum Hypothesis must have a truth value — we just don’t know the answer yet. Over-emphasizing ZFC or another system as being the “complete list” of axioms hinders progress in coming up with proofs of statements like these that can involve “rigorous informal reasoning” (which I consider to still be rigorous, see my post on the definition of mathematical rigor), which together with formal arguments form the practice of math, not one without the other. This is true more generally: an over-reliance on motivating a particular concept as an intended-to-be-complete formalization of a particular intuition misses a more accommodating approach of making the intuitive idea the “primitive” and then treating various formalizations of its properties as just different avenues to glean information about it. This is more historically accurate (as definitions have evolved over time), as Richard Hamming discussed, and opens up the possibility of different formalizations down the road that can yield additional insights.

From a perspective of how to reconcile this point with formal proof checking software, which we would like to serve as a basis for automated verification of math in the future, we have always had a history in software engineering of modifying interfaces when user preferences / intended feature sets change (see my article on the non-mathematical aspects of real-world systems), and we can always do so here as well when we come up with new axioms that we motivate outside of formal logic, but that can then be great tools for further formal proofs on top of them.

To summarize, the main aspects of current approaches to axiomatic set theory that seem “not semantically valuable” to me are: (1) over-emphasizing its importance, (2) introducing notions like classes and Grothendieck universes that arise only from syntactic error resolution in unenlightening ways, and (3) treating set theory axiom lists as “full.” We can avoid these points in treatments of math by simply showcasing Russell’s paradox (and its variants), showing methods for avoiding such issues, mentioning “reasonable” and “intuitively clear” axioms like ZFC, taking these axioms as self-evident, and moving on. I hold that if we do this, we can elucidate math better for both researchers and students, helping accelerate progress further.

Written February 2026, edited April 2026 for clarity.

Edit (March 2026): After thinking more about my points on model-theoretic results on axiomatic set theories, I have some further questions in that area too. Note that I’m not familiar with all the details of the proofs of these results, so my thinking could be wrong here.

As far as I understand, the proof of a statement like “Choice is independent of ZF” relies on set-sized models of ZF, and in fact has been established only for set-sized models. But it is then unclear how applicable such a result is to the standard model of ZF (ordinary sets), as it is unclear whether a collection of sets satisfying ZF with the standard interpretation of \in could be set-sized. Indeed, this is equivalent to the question of existence of a Grothendieck universe, which is tricky (as the Wikipedia article on the topic elaborates.) Of course, the question of independence is moot for a specific model — any specific statement is either true or not true in the model — which traces back to my point above that over-emphasizing independence hinders progress in determining the truth value of statements for specific models. But independence established model-theoretically is often interpreted in a proof-theoretic way: I can’t use these axioms to decide this statement, so additional properties of my specific model are needed to decide it. But how accurate is this really when applied to ordinary sets, when the independence result, dealing with any possible interpretation of \in and a set-sized model, is effectively about a kind of system that we don’t even know sets form?

Instead, more proof-theoretic arguments that don’t point to set-sized models (just don’t mention the whole collection that the axioms take as domain) would be preferable in truly helping us understand how we can get closer to a resolution of a statement like the Continuum Hypothesis, helping elucidate which proof paths would definitely not work so we could eliminate them.

Categories
Math

Sine Angle Product Formula 3

In this post, we continue the discussion from a previous post about the existence of a suitable sine angle product identity.

Categories
Math

Generalization of the Group Ring to Other Algebraic Structures

It seems natural to try to generalize the group ring construction to algebraic structures other than groups and rings. We do so here.

Categories
Math

Removing Proper Classes via Universal Sets

Can we avoid ever needing to mention proper classes in math by restricting to subsets of a universal working set?

Categories
Math

Subsets of Algebras, Subalgebras, and Preserving Concepts

Let F be a field and S \subseteq F be closed under addition and multiplication; under these operations, say S is a field. Is it then necessarily true that the other field concepts on S (identities and inverse) agree with those on F? What about for other algebras?

Categories
Math

Rings as Modules Over Themselves

In this note, we address some questions I had concerning rings when viewed as modules over themselves.