Tag: Studies

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 , we note that the classes actually of interest would be of the form “the class of all models of a theory ,” so we can instead talk about logical generation theory of a theory . 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 . 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 . So in what sense could logical generation theory “help”? What would be an application pathway?

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

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

The “familiarity” with the members of 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 of , can we decide it from ? (“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 and can check this for any member of . Namely, say , and say the sentence (call it ) is decidable in each of the . We know that since is an LGS for , by definition the class of all models of is the class of all models that satisfy the common sentences of all members of . So if a sentence is satisfied by every member of , then it must follow from , aka be decidably true from . Conversely, can we show that if a sentence is decidably true from then it must be satisfied by every member of ? If that’s the case then we can say that a sentence is satisfied by every member of if and only if it is decidably true from . Assuming based on our familiarity with the members of that we can quickly check whether a sentence is true in a member of , 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 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 ) is decidably true from . Then it must be true in every model of . So the class of all models of , which is the class of all models that satisfy the sentences common to the members of , must have every member satisfy . So the class of all models that satisfy the sentences common to the members of (call this set of common sentences ) must have every member satisfy . In other words, the class of models of must have every member satisfy . This means that implies . But is commonly satisfied by every member of , so every member of satisfies . 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 .

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

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 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 to maybe be:

• finite sets, , with suitable operations/relations/etc.
• or generally, special subsets of 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 -sized set (or even 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 are LGS’s for a theory , is also? If I have theories and LGS’s respectively, can we form LGS’s for , , and so on in terms of and ? 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 to be an LGS of a theory , all the members of must satisfy .) 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 be a logic, like equational or first-order, formalized generally under a framework like institutions. Is there a cardinality associated to such that for any theory in the logic of , must have a -size LGS? Is there a min such for any logic ? How would this number be related to other measures of expressive strength of ? 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 being generated by a set of axioms .” 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 , 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 would contain/imply, meaning it covers a smaller breadth of all the models/possibilities of , 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 . 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 , a prototype set for is a set of models of such that a sentence is a consequence of if and only if it is true in all members of , 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 has a single prototype if and only if it is complete, and in that case, every model of 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 , 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 ( plus implies .) 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 ,” then the only model of that theory would in fact be , and thus 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 ”? 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.)

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

First, assume and are both finite, so and with (as and come from current knowledge, which is always finite.) Every relation in is symmetric. Querying for problems and whether a certain reduction method applies to them — we can denote this by — is easy (), and similarly querying that for a certain equivalence method is also . Querying whether a problem is in the solved problems set, , should also be fast (.) Given this, what is the fastest algorithm for reducing as many problems in as possible?

There are a couple formalizations of this question. One is the one-problem question: given a particular problem , how quickly can we decide if is solved or not given , and if so what is the solution? (To answer “what is the solution,” we should say that every problem has a solution in a solution set , exactly one solution for each problem, and the solution is known for every problem , 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 can be reduced?” This is similar to the distinction between “find the shortest path between these two given vertices ” and “find all shortest paths in the graph.” Answering this properly would require some enumerability conditions on — in the motivating example, would be infinite and even uncountable to account for all possible equations we could solve, and in general could be unbounded in cardinality. For now, let’s focus just on one-problem decision.

So we are given , with . For each method in or , determining whether it applies to is . For a problem , determining whether (the given-solved set) is . We are given . What is the fastest algorithm to decide whether can now be solved?

Well, first, we can check . If not, then we must know that has a method that applies to it; if not then it can’t be solved. To check this, we would need to check for each , but in general if 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 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 time) whether a problem 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 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.

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

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

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

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