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.)

Share and like (need WordPress account to like):

Leave a ReplyCancel reply

Discover more from Nihal Uppugunduri's Website