Talk:Main Page/Archive 16

This is an article of past discussions, from 1-Jan-2022 to 1-Jul-2022. Do not edit the contents of this page. If you wish to start a new discussion or revive an old one, please do so on the current talk page.

New $\LaTeX$ macros for your convenience and our internal consistency

There are a number of new $\LaTeX$ macros which have been developed recently as a result of a lot of discussion some time back which never ended up happening at the time.

They can be found on the page Symbols:LaTeX Commands/ProofWiki Specific, also accessible from the sidebar.

A thing or two

I thought I'd dump some ideas here since my activity may wane a bit over the next few months and I might as well say these things while they're fresh. (then I'll have exams late April-mid June, after that I'll resume to current levels with another semester's knowledge) First I wanted to say that I'm planning on maintaining the page User:Caliburn/Job List as well as I can. The intention is for new contributors to be able to come along and find what still needs working on and gaps that people may not have noticed. Also a handy list for myself so I know what still needs to be done. People are free to add to the list or take off stuff they've completed. I am not sure where to put it for maximum visibility, but I'll display it on my userpage and post it here.

There are already a number of contributors who have their own way of managing their to-do lists, but a global one may have a use. I say: go for it, but beware that it's just another thing that needs maintenance. There are currently few enough active contributors that this could be extremely useful, especially if they are in the same approximate areas of activity. I can see the points of overlap between measure theory, metric spaces, topology, normed spaces, prob theory, matroid theory etc. etc. where this would be worth applying, in particular. --prime mover (talk) 07:19, 4 January 2022 (UTC)

It seems that I am going to tackle some of your topics simply by following Sasane. Namely, I am almost done with distributions. One thing that has been nagging me is the definition of Dirac delta through limits of various functions. This was one of the main reasons why I decided to work on these topics. However, Sasane does not cover this at all. Hence, after I am done with a couple of exercises, I will briefly switch to a different source (not sure which one) to establish how definitions through limits work out in the distributional sense. Then I will work a bit on the Lebesgue integral and resume where I left off (this can be seen by inspecting hyperlinks in Sasane's book page). Most of the work will be less abstract involving normed vector spaces.--Julius (talk) 12:32, 4 January 2022 (UTC)

I was looking under Category:Distributions so I didn't realise how much you have got through, fair enough. (I think any category containing results about distributions should be a subcategory of this category) Distributions are a huge topic that have only just started getting worked on, so it is probably worth noting as an area to expand anyway. If you need ideas on sources for more work on distributions, the module at Warwick on distributions recommends Friedlander & Joshi's Introduction to the Theory of Distributions, among some Fourier analysis texts by Duoandikoetxea and also by Grafakos. I haven't looked at these myself yet, learning more about distributions is on my "to-do" list for the summer. Wikipedia's page on distributional limits gives an example of a sequence of functions converging in the distributional sense to $\pi \delta_0$ (not sure if it's the canonical one, if there is one) so that might also be a good jumping off point. Looking forward to seeing how it all turns out. Caliburn (talk) 15:50, 4 January 2022 (UTC)

Second I'm wondering how theorems could be catalogued so that they don't get lost. While having a descriptive name for each theorem makes the most sense, it can make navigation difficult since some pages have to be given unintuitive names, some more so than others. (sometimes leading to mistakenly duplicate pages) I like pages like Properties of Beta Function for this purpose. I'm wondering whether we could branch this out to have easily navigable collections of other results. No specific format to mind yet. My contribution backlog at the moment is massive, so I doubt I will get to this soon, (especially as it's a significant undertaking) I will return to this idea when it's been whittled down a bit. Caliburn (talk) 00:19, 4 January 2022 (UTC)

I too am a fan of the "Properties of ..." sort of page. The archetype is Subset Equivalences, which I have found very useful indeed.

While duplicate pages are a problem, it's not a serious one. It happens for minor stepping-stone results when multiple source are being used to flesh out an area -- but when we implement categories more incisively, these duplicates are usually caught. The problem mainly happens when a contributor puts every result in a high-level all-inclusive category called, e.g. "Real Analysis" or "Metric Spaces", then it's easier to miss stuff.

Best advice while an area is being fleshed out is: if you see a potential duplication, slap a template in there to flag it up and move on with what you're doing, then after all is in place, take a step back to see whether there is a common thread that would need to be refactored out. --prime mover (talk) 07:19, 4 January 2022 (UTC)

I think once measure theory is fleshed out I'll have pages like "Limit Theorems for (Riemann/etc.) Integrals" and "Properties of Measures", etc. As an aside - should we archive a few older discussions here? My browser is starting to lag a bit typing this response. Caliburn (talk) 15:50, 4 January 2022 (UTC)

Aside -- job done. Good call. --prime mover (talk) 17:16, 4 January 2022 (UTC)

Slow

I don't want to be irritating, but the site has been extremely slow on and off for the past few days. Could this be looked in to? It is making refactoring very sluggish. Caliburn (talk) 18:44, 18 January 2022 (UTC)

Haven't noticed it myself. I do hope I'm not the problem. --prime mover (talk) 20:23, 18 January 2022 (UTC)

Doesn't seem like it, happens on and off even if I'm the only one editing. Doesn't seem as bad right now. Caliburn (talk) 19:13, 19 January 2022 (UTC)

Weak convergence

Can we get macros for $\rightharpoonup$ (weak convergence) and $\stackrel \ast \rightharpoonup$ (weak-* convergence)? Caliburn (talk) 13:11, 30 January 2022 (UTC)

Yes okay, I'll get to it in a bit. --prime mover (talk) 14:03, 30 January 2022 (UTC)

... all good? --prime mover (talk) 18:19, 30 January 2022 (UTC)

Yes that's great cheers Caliburn (talk) 18:24, 30 January 2022 (UTC)

Proofs of unsolved conjectures

Without trying to be rude to certain contributors, I'm wondering if codifying disallowing claimed proofs of famous conjectures (Goldabch's, Collatz, RH, etc.), and otherwise obvious crankery, (eg. the Bibhorr nonsense) is a reasonable step. Obviously we shouldn't discard the possibility of original theorems and proofs, (that being one of our selling points over Wikipedia of course - posting interesting-but-not-particularly-useful toy theorems should be encouraged) but I would draw the line before proofs that would very possibly win the poster a Fields Medal (or at least shoot them into international fame) if correct, on the basis that it almost certainly isn't. If by sheer miracle their proof is correct, they can get it published in a peer-reviewed journal, (I know this all might be harder for "outsiders", but Yitang Zhang managed despite being virtually unknown) claim their $\$1$ million dollar prize/Fields Medal/international infamy, and post it here. Thoughts? Caliburn (talk) 22:18, 31 January 2022 (UTC)

A well-crafted and coherently-written page to $\mathsf{Pr} \infty \mathsf{fWiki}$ standards (or at least in literate $\LaTeX$) will always be given greater credence than an ungrammatical and careless page written by someone who does not care enough about the target audience to bother to communicate properly.

It is a matter of fact that the more unusual and improbable a claim of success at proving an unattainable, the more bletheringly incoherent and incomprehensible the language it is written in. This is not a matter of fluency in what may not be one's native language, this is either the complete inability to string thoughts together, or the writer's belief that they are so cool and awesome that they can write in their own version of street slang and as a result everyone will bow down in worship of the awesome light, brighter than a thousand suns, that emerges from their nether orifice.

Hence I give short shrift to crackpots. Life's too short to bother. --prime mover (talk) 23:43, 31 January 2022 (UTC)

We are not a peer-reviewed scientific journal. Even if we know a thing or two about maths, we are far from being competent to say anything solid about your favourite unsolved world-class problem. If anyone has proof, please go through the usual peer-review process, get your prize and recognition, and then we can discuss posting your result here. To my understanding, here we are interested in well-established results with anything we can interpolate in between. As for Bibhorr, I could see a historical reason if this was derived thousands of years ago, but to my knowledge, this is a claim to a revolutionary new result, which is not. It is simply an inspiration derived from approximation of standard trig functions.--Julius (talk) 07:46, 1 February 2022 (UTC)

This specific exchange was triggered by a recent posting about Collatz. If the post in question is written using standard mathematical symbols in $\LaTeX$ then maybe we'd have been able to have a stab at poking the necessary holes in it like we did Senojesse some months back. But the symbols used were non-printing and non-displaying and hence of zero value. Seriously, I may be getting old, but I have neither time, headspace nor tolerance. As for the request on my user talk page to discuss it over the phone, there's an orifice for such to be inserted. :-/ --prime mover (talk) 09:07, 1 February 2022 (UTC)

Handling TORI as a source

With TORI being offline for approximately 10 years now (according to Wayback Machine https://web.archive.org/web/*/http://tori.ils.uec.ac.jp/TORI/index.php*) I think it is time that we decide what to do with it.

My suggestion would be to:

• Remove the (broken) direct links
• Include a reference to the Wayback Machine for TORI in general

For me it is up to debate whether or not we want to keep the reference to the licence. We might want to change the wording at least, since it will not be clear any more what part is actually reproduced.

Thoughts welcomed. — Lord_Farin (talk) 16:03, 16 March 2022 (UTC)

Considering how very few pages there are which reference TORI, I wonder whether to just delete the template and references and pretend they never existed. :-)

There appear to be a number of primary sources cited in the talk page, which we can plant on the main page after checking them out (these pages date from way before {{Citation}}.)

If the user who originally posted these pages up returns to us, then he may be invited to link to whatever resources that may contain his work -- although if it was original, such may not exist.

If we can explore Wayback and successfully identify the precise source pages from which the $\mathsf{Pr} \infty \mathsf{fWiki}$ pages were generated, then we may be able to amend the template accordingly, but I've not got this anywhere near the top of my Things To Do list.

As for the license, I'd say just remove it; the license refers directly to TORI which seems no longer to exist. --prime mover (talk) 16:25, 16 March 2022 (UTC)

Good call, I have eliminated the references. As a signpost I have left Template:TORI with a general link to the Wayback Machine. It was not possible to retrieve the content in reliable fashion. — Lord_Farin (talk) 19:55, 16 March 2022 (UTC)

Differentiating levels of refactoring

As you might have noticed, I have been cherrypicking from Category:Refactoring In Progress recently (i.e. {{Refactor}}).

It quickly occurred to me that it contains an overly broad spectrum of tasks, from elementary to highly complex.

To that end, I have introduced Category:Basic Refactoring, Category:Intermediate Refactoring and Category:Advanced Refactoring. It should help to get a better grasp of the level of problem that needs to be addressed.

This brings several questions:

1. Is this useful in general?
2. Is the usage sufficiently explained on the relevant pages or does the wording need to be tweaked?
3. Should we take it further and introduce similar mechanisms for {{Tidy}} and the rest? Personally I feel it's a bit early.

Thoughts welcomed. — Lord_Farin (talk) 09:43, 20 March 2022 (UTC)

I like it. In particular I like the categorisation.

I wouldn't go with doing the same for {{Tidy}}, as this ought to be straightforward to keep under control -- except that last time I did a concerted effort to tidy everything I lost my sanity. --prime mover (talk) 09:47, 20 March 2022 (UTC)

The process has been completed. In adding the categorisation, some 30% of the originally about 800 refactor calls have been replaced with more explicit calls (particularly {{ExtractTheorem}}) and/or resolved immediately. 500-something template invocations remain. Of those, a very limited number defied clear categorisation, mostly because the offending page had content problems that refactoring could not easily resolve.

Going forward, you can utilise Category:Basic Refactoring, Category:Intermediate Refactoring and Category:Advanced Refactoring to find a task at the level you're looking for, making the process less frustrating. — Lord_Farin (talk) 14:52, 5 May 2022 (UTC)

I will every so often pick up on one or two of these refactoring tasks, but I am finding it tedious. Times of day in which my brain is fresh enough to allow me to get on with stuff are fewer than they used to be. Good job and many thanks. --prime mover (talk) 16:58, 5 May 2022 (UTC)

Seth Warner's Modern Algebra exercises

I've been making heavy weather of solving the exercises in sections 11 and 12 of Seth Warner's Modern Algebra, where he derives general results concerning quotient structures and quotient mappings usually introduced in the context of group theory and normal groups. His approach is to investigate structures with the most general properties and derive results which can then be used to further derive the corresponding statements in group theory.

I have documented all of the results in these chapters, but left some of them undone because of lack of ability to concentrate (and I confess also patience).

During the course of this I have been trying to categorise and structure the results in this area so as to make them easier to find, with more or less success.

I'm going to move on from this (to the next chapter, but still in the same area of work), and I would welcome a second pair of eyes to see whether there may be a way to better structure the results in this area so as to make the whole area easier to perceive as the richly patterned structure that it is, rather than as a patchwork of similar-but-not-quite-the-same results.

In particular, the correspondence between groups quotiented both by normal subgroups and congruence relations needs to be better emphasised.

Does anyone want to see whether we can make something really useful here? I would hope that incomplete proofs could be completed using the same approach they have been started with -- the exercises in Warner often say "Use this result to derive (some other result)", where I can see the pattern of what is to be achieved, but have not been able to focus adequately on the fine detail.

I have been asking questions on MathStackExchange a lot recently, and I fear the experts there are losing patience with me. --prime mover (talk) 17:29, 22 March 2022 (UTC)

I'll take a shot, but I'll have to ask for a few days of patience till I find a timeslot of sufficient size to really get into it. — Lord_Farin (talk) 07:36, 23 March 2022 (UTC)

Update: done. As you noticed I left remarks and maintenance templates where I felt they were appropriate. Nice job, crisp presentation! — Lord_Farin (talk) 12:16, 27 March 2022 (UTC)

Heh! Sorry, slight misunderstanding: my point was that a number of the exercises have been left incomplete. I was hoping someone was going to do my homework for me add the finishing touches to the incomplete proofs, e.g. $11.12$, $11.16 - 20$, and so on. No worries, I'll return to them later, when I've cleared my head from the current confusion.

Internal Group Direct Products

It will be noticed that I have done a bit of work chewing over the definitions and equivalence proofs of Definition:Internal Group Direct Product.

In particular, the definitions are identified by name rather than number, so as (I hope) to make it clearer which one is under discussion at any one time.

The question will be asked: why does it have to be quite as complicated as this?

The answer is: I have a few source works which introduce this concept from different directions:

Seth Warner: Modern Algebra leaves it implicitly understood as a special case of the general abstract algebraic structure: an isomorphism from the cartesian product of two substructures onto the parent structure. He then goes on to demonstrate that if the substructures are subgroups of a group are subgroups, then Definition:Internal Group Direct Product/Definition by Subset Product follows.

John D. Dixon: Problems in Group Theory defines the concept in an introduction on notation as Definition:Internal Group Direct Product/Definition by Subset Product and leaves it at that.

John F. Humphreys: A Course in Group Theory takes the general approach of Definition:Internal Group Direct Product/General Definition/Definition by Unique Expression, deriving the $n$-tuplar Internal Direct Product Theorem thence.

I also have a vivid memory of my course pamphlets from my degree course which went over the subject finely in detail, which formed the basis of the initial work on $\mathsf{Pr} \infty \mathsf{fWiki}$ on this subject, but I was new to the game and did not do a very good job of it.

My strategy here is to identify those 3 approaches to the definition and generate a $2$-subgroup and $n$-subgroup version of all of these. I appreciate that it may not be the case that all are explicitly documented in the literature, but in order to offer consistency and thoroughness to the approach, I am including them as definitions even if this may not be the case, which is counter to our stated guidelines.

I am now in the process of rationalising all the results which go towards proving the equivalence of all these approaches, with a view towards making them more accessible and internally consistent.

It's a long-overdue job, and at the moment I am getting more frequent periods of an hour or more at a time when I am mentally lucid enough to attack such problems, and I am not wasting them. (Getting old sucks.) --prime mover (talk) 23:34, 24 March 2022 (UTC)

Update after brain failure: I have completely lost the thread.

Can anyone explain why, from:

"Let $\struct {S, \circ}$ be an algebraic structure with $1$ operation.

"Let $\struct {A, \circ {\restriction_A} }, \struct {B, \circ {\restriction_B} }$ be closed algebraic substructures of $\struct {S, \circ}$, where $\circ {\restriction_A}$ and $\circ {\restriction_B}$ are the operations induced by the restrictions of $\circ$ to $A$ and $B$ respectively.

"Let the mapping $\phi: A \times B \to S$, where $A \times B$ denotes the Cartesian product of $A$ and $B$, defined as:

$\forall \tuple {a, b} \in A \times B: \map \phi {a, b} = a \circ b$

be an isomorphism."

... it can be deduced that:

"$\forall \tuple {a, b}, \tuple {c, d} \in A \times B: \tuple {a, b} \circ \tuple {c, d} = \tuple {a \circ c, b \circ d}$"

?

It seems to be taken for granted in all the books I've managed to find on this subject (there aren't many) -- but I don't see why. --prime mover (talk) 23:23, 25 March 2022 (UTC)

Actually I think I may have worked it out.

The external direct product is defined as $\tuple {a, b} \circ \tuple {c, d} = \tuple {a \circ c, b \circ d}$ but the internal direct product is not the same thing at all, it is in fact defined as $\tuple {a, b} \circ \tuple {c, d} = \tuple {a circ b, c \circ d}$ and they are not the same.

I'll try and make some sense of this tomorrow. --prime mover (talk) 23:32, 25 March 2022 (UTC)

Codifying a category structure

I'm wondering if we should codify categories, which is a bit fragmented as things stand. My idea is that categories such as Category:Measure Theory, Category:Galois Theory, Category:Functional Analysis should on the first level contain the fewest results possible, limiting only to major theorems that are too wide-reaching to fit in a specific subcategory. The next level down, contained in the topic category, should then consist of the fundamental objects of that field of study, for example Category:Measure Theory should contain stuff like Category:Measures, Category:Sigma-Algebras, and so on. These categories should then contain the bulk of the results, (bar Corollaries, I think there is established convention that these should be categorised as theorems) but not subpages thereof. Pictorially we have for example:

Category:Proofs by Topic

Category:Measure Theory

Category:Complex Measures

Category:Variation of Complex Measure (have not created this yet)

Category:Variation of Complex Measure is Finite Measure

Variation of Complex Measure is Finite Measure

Do people agree on this? To clarify, my picture is that Characterization of Left Null Space should be contained only in Category:Null Spaces, and Category:Linear Algebra should primarily contain other categories rather than the 100 or so pages it does now.

Caliburn (talk) 17:57, 3 May 2022 (UTC)

This is exactly the structure that I have more recently been trying to evolve $\mathsf{Pr} \infty \mathsf{fWiki}$ into. Note that the bottom line of what you put has recently been formalised by adding another use case for {{SubjectCategory}} where you have a result parameter which is the page title of the result being documented. --prime mover (talk) 18:26, 3 May 2022 (UTC)

Agreed, this makes sense. We might allow ourselves reasonable time to tackle this by an appropriate maintenance template that can be used on categories needing to be subcategorised. — Lord_Farin (talk) 18:44, 3 May 2022 (UTC)

Progress on generalized functions and Dirac Delta

Dear all, I think I am done with covering the basics of generalized functions, distributions, Dirac delta etc. Obviously there is much more to cover, but I have accomplished my two little goals - absorption of the last chapter of Sasane and some clarification of Dirac delta properties, sequences and connection to the sketchy presentation in standard applied literature. The majority of the work is based on Sasane, Arfken and Kanwal. I tried to stick to $1D$ to understand basic arguments before we jump into arbitrary dimensions since this will require invention of a few arguments. Also, in my work I chose to denote the distribution as $\map {T_f} \phi$, while many books choose $\innerprod f \phi$. I wonder if this is legible and how this is presented in other people's studies. I may still add additional material, but I won't steamroll it anymore. So, if someone feels that something is really worth adding, please be specific with your wishes. Otherwise I am coming back to continuous and linear mappings on normed vector spaces.---Julius (talk) 21:50, 4 May 2022 (UTC)

What you've done seems pretty solid. The opportunity is now there for anyone to build on it who wants to and is able to. I think if anyone has questions from here on in, it will take a while for them to evolve. Lots of study will be needed, and that will take time, at least from my perspective. Good job . --prime mover (talk) 05:07, 5 May 2022 (UTC)

I think we should rename the current dirac $\delta$ page "the physicists dirac $\delta$" and create a {{PhysicistsDiracDelta}} or similar giving appropriate health warnings. Worthwhile including on this site I think. Caliburn (talk) 18:07, 5 May 2022 (UTC)

As it was said some time ago, abuse of notation it not a problem as long it has a solid background. I agree that we should have a page for physicist's Dirac delta, because this notation simply exists and is in use everywhere. I think we could use this page to host various properties of Dirac delta as they are usually presented together with more rigorous structure backing up all of this.--Julius (talk) 21:03, 5 May 2022 (UTC)

Progressive Mapping -- the cat jumps

I have taken the radical decision to amend the terminology concerning "inflationary mappings" and "progressing mappings".

While I am retaining the name "inflationary mapping" when in the context of the general ordered set (although this may change), I am moving the class-theoretical definition of "Inflationary Mapping/Subset" completely over to the pave Definition:Progressing Mapping.

Rationale:

The concept of "progressing mapping" is used extensively in class theory in the development of the principle of induction to a much more general footing than on the natural numbers. The work which I am using to do this job is Smullyan and Fitting, which is the only one I have to hand which defines the concept. I have found no mention of "inflationary mapping" in any of the works I've seen (which is not saying much, I haven't studied all that many), and no other $\mathsf{Pr} \infty \mathsf{fWiki}$ contributor has actually provided any other sources on the subject.

I note that the concept of an "inflationary mapping" appears to be used in Measure Theory, but again, no sources are cited and I have come across none myself.

Because the concepts are basically the same, I am going to continue to keep them nested one within the other as a structure, but weasel-word my way around it by saying that the two things have different names in the different mathematical contexts: "In the development of class theoretical approaches to development of the natural numbers, an inflationary mapping is better known as a progressing mapping" or some such.

Forefront in this development is because the concept of a "slowly progressing mapping" appears not to be mirrored in the context in which "inflationary mappings" are raised, and of course, in the context of the latter, on a close-packed domain, such a concept cannot be realised.

Please feel free to offer your thoughts. --prime mover (talk) 07:44, 5 May 2022 (UTC)

The reason inflationary (also: "extensive") mappings do not get a lot of love separately is because they are mostly interesting in combination with other properties. It is therefore not a concept which is carefully named and explored. Personally I find "inflationary" and "progressing" clearer names than "extensive" which bears too much reference to the set-theoretic case (and even there is not very clear). I have no real preference for either name except "inflationary" being already established and therefore requiring less work. But sourced names trump easy names, so I support your endeavour for "progressive" in covering S&F. — Lord_Farin (talk) 08:00, 5 May 2022 (UTC)

Thanks L_F -- this work will progress (no pun intended) progressively. --prime mover (talk) 08:07, 5 May 2022 (UTC)

... there we go, does that make more or less sense? --prime mover (talk) 22:20, 5 May 2022 (UTC)

Sets or Classes -- it comes down to the wire

There is no way to avoid this, we really do have to decide how to handle class theory.

I don't like it, for reasons of "tidiness" more than anything else, but that does not excuse us from posting it up.

The basic facts of what a class is, and how it behaves is all well and good. The strategy we have devised for putting that in the context of foundational set theory (ZFC and NBG and the like) is in place and is evolving (not complete, this will happen as the books are worked through).

What I have trouble with (and what we have always had trouble with) is how to handle structures and results which are "basically the same thing" for sets and classes, except that one result, say, has a set as the underlying collection, and the other has a class.

Take for example set unions and intersections, and class unions and intersections. They are the same thing, except that we also define them on power sets (the concept of which is not applicable to classes: you can't have a "power class") and families (about which I'm not sure but I believe also the concept can't be applied to classes, haven't thought it through). Now a set is a class. Do we use as a master page Definition:Class Union, say "a set is a class" and then implement "set union" only in the cases where class theory does not apply (i.e. the "set of sets" versions)? Advantages: this simplifies the structure greatly and we don't have to duplicate results between sets and classes, once the class theory results have been established, we "know" they apply to sets as well. Disadvantages: renaming and refactoring will be a mammoth task; people who know set theory but haven't encountered classes are going to be compromised, which is against our site philosophy.

The other option, to set up a parallel set of definitions and results for "class theory" versions of the stuff which applies only for class theory? (Or at least, until it has been established that once the class-theoretical material has been explored, and it is proved, for example, that the empty class is the same as the empty set, and the results concerning unions and intersections are "the same" in set theory as they are in class theory: commutativity, associativity, idempotence, distributivity and so on.) The advantage to this is that the existing set theoretical results stand as they are, and all we have to do is bolt on the class theory stuff on the side, which may take some work to do but should be limited in scope -- and such scope can be worked out by studying the literature. The disadvantage of this is that it will then make class theory look like a great big air-conditioning unit bolted onto the side of an antique historical building, and it offends my sense of aesthetics.

My view is that the first of these options is probably the best way to go. From my limited perspective (I've read round the subject but have only just now started to dig into it) I'm beginning to get a feel for the enormity of both of the above tasks (and I use the word "enormity" in its true sense -- I'm being ironic here) but I haven't yet got a feel for its full extent.

Further implications:

• How does class theory interleave with ordinal theory? I believe that in general you can cover ordinal theory completely within set theory until you start to talk about the collection of all ordinals. I think the same may apply to cardinals. Infinity theory as dipped into by Rudy Rucker's Infinity and the Mind will have to wait.
• Axiom of Choice -- does this apply solely to sets, or is there again a class-theoretical version of this? I believe that the former is correct -- that there is no "class theory" AoC. Again, haven't explored in detail, this is my intuition talking.

My current mode of thinking is: add a load of class-theoretical results on top of / in parallel with the set theoretical versions (that is: prove commutativity, associativity, distributivity for class union and intersection, set up pages for ordered classes, totally ordered classes, well-ordered classes, perhaps transcluding, perhaps just linking) and then, when we have the full scope of how far class theory needs to be extended into set theory, we take another view on how to (and indeed, whether to) merge the concepts further together into their own pages.

A hybrid approach is to keep the set theoretical results as they are, add "(or class)" to everywhere it says "set", and retain inaccurate page names so that (for example) "Set Union is Commutative" would cover both set theory and class theory, but I have a nasty taste in my mouth just thinking about that (and in fact that I have already done this in places, and it pains me). And again, the disadvantage to that approach is correlating it with the "set of sets" versions which specifically do not apply to class theory.

This will of course be a weekend-only job for me, as I won't be able to expend much mental energy on this during the week. My best working hours are from 06:00 through till mid-morning, but after that I can't sustain the level of concentration and commitment for stuff which needs attention to detail and application of thought. Evenings after a day's work are increasingly becoming no-go areas for me, and the older I get the more time-sucky social commitments I seem to accumulate.

Thoughts on this? And does someone care to set up a discussion area, where we can include this and all the other wrangling and squabbling on the subject over the last decade and a half? --prime mover (talk) 06:48, 8 May 2022 (UTC)

My 2 cents: The level of work we put in to a restructuring needs to be proportional to the level of conviction we have it is the right thing to do. Right now, we don't have a clear enough vision of the end result to warrant enormous refactoring. So keeping the class stuff separate is currently the right thing to do.

Going forward we should definitely try to keep the stuff on classes away from the basic pages. I get similar vibes like between relations and mappings, where many results hold for arbitrary relations but are also proved separately for mappings. The mappings version then usually has one of the proofs saying "mapping is relation, link, qed".

Good on you for acknowledging when is, and when is not, the time to work on these things. It can grow very complex very fast, trying to grasp multiple approaches from multiple books and perspectives so that we can present it coherently. So take your time.

As for a discussion place, I would suggest to keep it over here for now, and later on we can think of placing the whole discussion somewhere under Definition:Class (Class Theory) or some such for archival purposes. — Lord_Farin (talk) 07:47, 8 May 2022 (UTC)

I am ignorant as to class theory, (I only understand a class as something that is too large to be a set) so this will be from the perspective of someone who has read set theory but not class theory. I think I agree with you and LF. Personally, I think there is value in covering subcases individually, rather than just having an uber-powerful extremely general theorem and saying "This is immediate because every X is a Y and we have this result for all Y". If the reader is taking a first course and knows nothing about Y, they have not learned anything. And it might be the case that the proof for sets gives a more elegant presentation than that for classes because of the upgraded regularity. So I think we should have separate results about classes and sets, with the proofs of the latter not usually invoking theorems on the former, unless it is absolutely unavoidable. I personally don't mind if this results in a lot of duplication, so I am on board with the current approach. Ultimately we ask the question over whether we are writing a treatment of mathematics that is for the sake of mathematics, or a treatment of mathematics that is viable supplement to learning mathematics. I prefer the latter. Caliburn (talk) 13:24, 8 May 2022 (UTC)

This is the strategy I will go with. I will take some time being ultra-careful about links to whichever of the versions of theorems and definitions (have already cleared up some inaccuracies concerning Definition:Class and Definition:Empty Class and some others) and go through this extremely slowly, starting from Chapter 2 of S&F again.

This weekend's run away with me because I've had to entertain visitors most of today, which is just one of those things that happens when you're unfortunate enough to live in society. --prime mover (talk) 14:54, 8 May 2022 (UTC)

Right, 2 weeks on and I have completely reworked S&F (what exists on $\mathsf{Pr} \infty \mathsf{fWiki}$ so far, that is) according to the philosophy discussed above. It is likely that there are still some inconsistent links way in the depths of the mix, but as we progress through, we should catch these.

I have no plans in the short or medium term to do a closer job of "merging" set theoretical and class theoretical results. Having seen what it is starting to look like, I think what we have now is camera-ready, so to speak (except where I have exercises to complete, which will take as long as it takes for me to get down on it). That is, our "parallel track" of class definitions and set definitions is maintainable and (as far as I can tell) rigorous, and (by way of {{ClassContext}}), definitions are appropriately cross-linked. We also have Subset Relation is Transitive/Proof 2, which shows how we can cross-link results as well. We have the freedom of space to be able to do this now.

In fact I'm guardedly going to go so far as to suggest, up to a certain definition of the word "like", that I actually like it. --prime mover (talk) 09:59, 21 May 2022 (UTC)

Indeed, the result turned out nice and manageable I would say. Which is a great achievement considering the amounts of confusion that can easily arise in foundational matters such as classes. Thanks a lot! — Lord_Farin (talk) 08:41, 22 May 2022 (UTC)

Sub-discussion: the future of Takeuti/Zaring

In the current efforts of restructuring class theory, we run into continuous problems with integrating the material from 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory. Many of the pages are incomprehensible and lacking in adherence to the evolved $\mathsf{Pr} \infty \mathsf{fWiki}$ style.

Additionally, the original contributor (Asalmon) who offered us the material has not been sighted in almost 10 years. Not being able to easily check the compatibility of results when notation, choice of wording, etc. are notoriously ambiguous in this area compromises our ability to salvage the material in a confident way.

While I am not saying that T/Z does not deserve to be covered on $\mathsf{Pr} \infty \mathsf{fWiki}$, I am now ready to take the leap and declare the current implementation deprecated. I consider the best way forward to first remove all the material, and then cover it again based upon the current structure on PW. This will enable us to write up results that actually contribute to the clarity of the site as opposed to detracting from it, as is now often the case. Illustrative of this problem is that the {{NotZFC}} template has been littering our pages for many years now, without satisfactory resolution.

Seeing as this proposal (removing the T/Z material that is not up to par or backed by other sources) is admittedly radical, I would like to gather some other opinions before proceeding. Other proposals are more than welcomed and I would gladly give up my plan for a better one. — Lord_Farin (talk) 19:03, 13 May 2022 (UTC)

Yes I see what you're saying -- but hang fire on it at the moment, ordinals (which is the mainstay of T/Z's coverage) is just one chapter away from where I am in S/F, and it is probably going to be the case that I can progressively supersede the T/Z work as soon as I get there. I am fairly sure that T/Z itself is not at fault so much as the fact that the early chapters of T/Z have not been covered to quite the level of tooth-grinding detail that I have scraped from S/F. I have flashes of zen enlightenment on the topic where I see the tree with branches and roots and I know what the shape of the frame is, and everything is just one small part of the root structure. I can see where the T/Z stuff is going, it's just where it comes from that's obscure.

There's 2 things going on here: class theory and ordinals. Both extend our coverage of set theory, both are "new" (and so not quite bedded down yet) and both have multiple viewpoints. I still think we can evolve a synergy and hence grasp and present the essence. I have already done a good deal of that with the axioms, it's just a matter of time before I get the ordinals sorted out. --prime mover (talk) 23:49, 13 May 2022 (UTC)

I would dearly love to spend more time on Devlin, which again covers the same ground, but he's difficult to penetrate.

In other news ...

... you might have noticed I've started rendering important linked definition pages in bold, so as to emphasise them. I find it makes the page easier to assimilate because your eye is drawn to the important stuff.

Can't lay down a rule on the subject, just sometimes I find it make a page better.

Follow or discuss. I'll continue here after I've sobered. Had a night on the town. --prime mover (talk) 23:54, 13 May 2022 (UTC)

Mechanism for reporting errors without creating an account

Often mistakes here are only reported on Maths StackExchange and so may remain unnoticed for quite a while - I search "ProofWiki" on there every once in a while to make sure we haven't missed something. The usual process would be to flag it up on the talk page and put up a maintenance notice. I'm wondering if having to request an account, and then put yourself out doing this puts up a "high barrier to entry". Might it be worth investigating ways where someone could suggest corrections or improvements without having to make an account? (and that would be obvious to anyone looking at the page) I'm unsure how to put any feelers out since we're talking about people without accounts... Caliburn (talk) 15:59, 16 May 2022 (UTC)

I try to monitor MSE but I'm not very good at keeping up with it. We're not liked on MSE for blindingly obvious reasons, but fortunately there is some feedback we can glean from there. And every so often people do say something like: "starting an account in order to fix such-and-such a mistake." We did at one stage have to disable anonymous editing because of a spam attack, but I wonder whether we can re-enable it on the grounds that we are no longer noticeable enough to attract spammers. --prime mover (talk) 18:48, 16 May 2022 (UTC)

I don't think ProofWiki is massively disliked... For many theorems it is on the first two pages and is sometimes the second result after Wikipedia, you don't get that from low-quality without some sort of visible backlash. Of course it being a wiki the quality is not uniform and there are imaginable reasons why people would dislike the style. An old-fashioned suggestion would be some mailing list that people can email and that email will be forwarded to people who opt in. A slightly more modern solution would be some kind of webform/google form people can fill in. I have no problems with the current model of requesting an account, but the fact that users go to an external site to identify mistakes and don't notify us directly of it is troubling as a wiki. (I guess you could say the same of Wikipedia) Just thought it was worth fielding this. Caliburn (talk) 20:19, 16 May 2022 (UTC)

Here is what Wikipedia suggests one to do: [[1]]. I wonder how much we can limit rights and message sizes to avoid spam. I also have a reddit page for Proofwiki that I had no time to manage and am willing to give away if needed.--Julius (talk) 20:53, 16 May 2022 (UTC)

That sounds like an option. Not sure that we might already have something of the sort. --prime mover (talk) 21:26, 16 May 2022 (UTC)

Maybe we should have the subreddit more clearly advertised, like on the front page? Caliburn (talk) 21:28, 16 May 2022 (UTC)

There's a trade-off between allowing non-registered people to be able to report errors conveniently and efficiently and laying us open to being bombarded with undesirable communications. But I will leave it to someone else to decide on the details of what we do about this exactly. --prime mover (talk) 05:03, 17 May 2022 (UTC)

Tying things together: PropLog and PredLog

To those who care (probably just me), please observe Propositional Tautology is Tautology in Predicate Logic.

That is to say, we have the first page formally proving that propositional logic carries over to predicate logic. In this case on the model-theoretic side. I expect a similar proof for the proof-theoretic side in due course (although using completeness theorem on both sides would suffice). — Lord_Farin (talk) 18:26, 17 May 2022 (UTC)

I also care big time but the philosophical complexities of logic defeat me. So glad you're doing this and not me. --prime mover (talk) 19:41, 17 May 2022 (UTC)

Impassable mental block in Class Theory

I'm going to have to abandon my attempt to impose some meaning and consistency into the coverage of class theory and set theory, because I can't make any sense of it.

It all boils down to an understanding of what is meant by the domain of a relation.

For a mapping it's clear: if $f$ is a mapping on $S$, then the domain of $f$ is incontrovertibly $S$, by the definition of $f$.

But suppose $\RR$ is a relation on $S$. The domain of $\RR$ is defined as: $\set {x \in S: \tuple {x, y} \in \RR}$

Thus the domain of a relation is a subset of $S$, and of course therefore may not equal $S$.

But then we have no name for $S$ in relation to $\RR$. Hence if we have a relation $\RR: S \to T$ we can always call $T$ the codomain of $R$. But $S$ is not necessarily the domain of $\RR$.

It seems to me that the great thinkers in this area have missed a subtle detail here in migrating from mapping theory to relation theory.

This has the following repercussion: when you define a reflexive relation, you define $\RR$ as reflexive iff $\forall x \in S: \tuple {x, x} \in \RR$.

Now when you go and look at Smullyan & Fitting's definition of "reflexive relation", you get this:

A (class-theoretical) relation is nothing more nor less than a subclass of the Cartesian product of $V \times V$ where $V$ is the basic universe.

A reflexive relation is a relation $\RR$ such that for all $x$ in the domain of $\RR$ we have $\tuple {x, x}$ in $\RR$.

To my understanding, these are not the same thing.

Suppose you have a class $A$ (which of course may be a set, as a set is a class). Then you would think that a reflexive relation ought to be defined as a relation such that $\forall x \in A: \tuple {x, x} \in \RR$.

But (according to Smullyan and Fitting), they define a reflexive relation as $\forall x \in \Dom \RR: \tuple {x, x} \in \RR$.

This is not the same thing at all, as the domain of a relation is (as we have seen above) the subset of $A$ such that $\exists x \in A: \tuple {x, y} \in \RR$.

If we define a relation like this, then Symmetric and Transitive Relation is not necessarily Reflexive no longer holds, because then automatically every $\tuple {x, x} \in \RR$ is such that $x \in \Dom \RR$.

Now either S&F have come up with a definition of a reflexive relation which is inconsistent with the "conventional" way of defining a reflexive relation, or there is a subtlety somewhere that I'm missing, or everybody in the world has not noticed the stumbling-block over which I have fallen in the definition of the "domain of a relation" above.

Does anyone know of an online resource which can help self-taught mathematicians with technical problems like this? --prime mover (talk) 09:37, 19 May 2022 (UTC)

A new problem has been highlighted: I seem to have lost the ability to follow explanatory examples. I am beginning to feel concerned that I may be reaching the end of my useful life, at least as a mathematician. Things that normal people take in their stride as obvious and trivial, and hence impossible to explain, I see as an insurmountable barrier. I don't know what to do. --prime mover (talk) 11:55, 19 May 2022 (UTC)

Upon closer reading of S&F (found an online copy) I do contend that their interpretation of relation is nonstandard according to what we are used to on $\mathsf{Pr} \infty \mathsf{fWiki}$. I would therefore choose to amend the disputed Definition:Reflexive Relation to be the sensible definition in deviation from S&F, and add an explanatory note that some sources choose to define it differently.

It is my understanding that these subtleties are foundational only, and that there should not be an issue once we ascend to higher concepts. But I'm not sure. It is clear to me that our definition is the safer one, and avoids unwanted pathologies. As $\mathsf{Pr} \infty \mathsf{fWiki}$'s coverage is wider than S&F's, we should choose the more universal approach. — Lord_Farin (talk) 12:48, 19 May 2022 (UTC)

The Wikipedia article on Reflexive Relation, defines

Quasi-Reflexive: $\tuple{x,y} \in \RR \implies \tuple{x,x}, \tuple{y,y} \in\RR$

a search of Quasi-Reflexive further shows up:

Left Quasi-Reflexive: $\tuple{x,y} \in \RR \implies \tuple{x,x} \in\RR$

Right Quasi-Reflexive: $\tuple{x,y} \in \RR \implies \tuple{y,y} \in\RR$

I don't know how pervasive these terms are, but the S&F Reflexive definition coincides with Left Quasi-Reflexive and they seem to be on their own with this as the definition of Reflexive. --Leigh.Samphier (talk) 13:42, 19 May 2022 (UTC)

I don't understand some more, doesn't the S&F definition coincide with fully quasi-reflexive? This is difficult for me. --prime mover (talk) 15:53, 19 May 2022 (UTC)

If $\forall x \in \Dom \RR: \tuple {x, x} \in \RR$ and $\tuple{x,y} \in \RR$ then $\tuple{x,x} \in \RR$ as $x \in \Dom \RR$, but there is nothing to say that $y \in \Dom \RR$ so its not guaranteed that $\tuple{y,y} \in\RR$ --Leigh.Samphier (talk) 16:08, 19 May 2022 (UTC)

Ah, there's the misunderstanding, my copy of S&F has that "a relation $R$ is called reflexive if $x R x$ for every $x$ in the field of $R$." The field here is the union of $\Dom R$ and $\Img R$.

In which case, the S&F definition does indeed coincide with Quasi-Reflexive. --Leigh.Samphier (talk) 16:59, 19 May 2022 (UTC)

A transitive, symmetric relation is quasi-reflexive, but not necessarily reflexive. A symmetric quasi-reflexive relation is reflexive on $\Dom \RR \times \Dom \RR$ --Leigh.Samphier (talk) 16:19, 19 May 2022 (UTC)

Yes, this was the root of my confusion, this is what I surmised from the S&F definition of a reflexive relation. Follows trivially. One of the first exercises in relation theory is proving that a symmetric transitive relation is not necessarily reflexive. My contention is that under S&F's definition of reflexive, it necessarily is.

A quasi-reflexive relation is reflexive on $\paren{\Dom \RR \cup \Img \RR} \times \paren{\Dom \RR \cup \Img \RR}$ --Leigh.Samphier (talk) 16:26, 19 May 2022 (UTC)

Is that the same as saying a quasi-reflexive relation is a relation that is reflexive on its field? It is, isn't it? --prime mover (talk) 16:45, 19 May 2022 (UTC)

Yes --Leigh.Samphier (talk) 16:54, 19 May 2022 (UTC)

Cutting through all the fiddly stuff, we now have comprehensive pages on quasi-reflexivity, just needs the equivalence proofs to finish, which will happen after supper. Busy evening, sorry. --prime mover (talk) 19:22, 19 May 2022 (UTC)

Many thanks. The world makes sense again. You had every right to bring this up as S&F were sloppy in this regard. I added a suggestion to Definition:Relation (Class Theory) that might aid understanding. Thoughts welcomed. — Lord_Farin (talk) 08:26, 20 May 2022 (UTC)

I thought about doing that, but I'd rather wait until I find that the class-theoretical approach specifically needs it. As it stands, the concepts as they have been so far developed appear not to require this level of detail -- but as I continue this microscopically-detailed analysis of S&F I will see how it pans out. I am going to be really careful not to make any assumptions about anything in the class-theoretical model until I see it approached formally.

In due course I will study further works that cover class theory, and consolidate what we have. It's well probable that it is worth doing what you suggest, but at the moment I'm treating this area like a minefield. --prime mover (talk) 08:48, 20 May 2022 (UTC)

Upper / Lower Set / Section

I have changed the names "lower set" and "upper set" to "lower section" and "upper section".

A fairly radical move which needs lots of further rework which is under way.

Reasons:

The term "lower section" is used in Smullyan & Fitting, and none of the existing definitions of "lower set" or "upper set" are referenced anywhere. Hence "cited" beats out "uncited".

The term "lower section" can also be used in the class-theoretical context with more convenience.

Work is in progress to do the appropriate rework, of which, yes I know, there is quite a lot. This will happen in due course. --prime mover (talk) 05:23, 25 May 2022 (UTC)

I would've preferred to discuss this before all the work is done. However in hindsight I am sufficiently able to rationalise it, so that it does not need to be reverted.

Please do note that there are other mathematical notions of "section", so we might want to check if a disambiguation is in order. — Lord_Farin (talk) 05:31, 25 May 2022 (UTC)

That was a big whack of rework, but I think it's completed. Gave me the opportunity of reviewing and tidying a considerable body of pages, and consistency is improved.

I can now continue with my development work. But first I take a break. --prime mover (talk) 09:50, 26 May 2022 (UTC)

Axiom invocation

When we invoke a standard axiom, I wonder whether it would be a general enhancement to house style to render its main words starting uppercase:

"Using the Axiom of Choice, we can set up ..."

which I think emphasises its nature as an Important Axiom, and looks better than:

"Using the axiom of choice, we can set up ..."

This could be a rule generally applied, or does anyone genuinely prefer the lowercase rendition? Anyone go for bold? "Using the Axiom of Choice, we can set up ..."

--prime mover (talk) 05:30, 27 May 2022 (UTC)

AFAIK Axiom of Choice is already standard. I don't like bold. — Lord_Farin (talk) 07:44, 27 May 2022 (UTC)

Definition:Chain (Order Theory), Definition:Nest, Definition:Nested Sequence: terminological consistency

I recently changed Definition:Chain (Set Theory) to Definition:Chain (Order Theory), as we have to take on the concept of chains in the context of classes which are not necessarily sets.

The idea was then to subpage it to include the specific instance where the ordering is the subset or subclass ordering.

Then I notice that this is already initiated, using Definition:Nested Sequence, which is also sort of the same thing as a Definition:Nest. All can of course also be categorised as totally ordered sets.

A number of pages link to Definition:Chain (Set Theory) instead of the more accurate Definition:Nested Sequence, so those are being amended as I reach them.

The plan will be to merge the concepts of chain, nested sequence and nest, and gather them all together into one place which I propose to be:

a) Chain (Order Theory): the general subset of a totally ordered set. A totally ordered set itself is itself a chain. However, I would rather keep Definition:Totally Ordered Set and reserve the concept of chain to be a subset of such.

b) Definition:Nested Sequence to be renamed to Definition:Chain of Sets, but it could so easily be redirected to Definition:Nest, whose current definition (in the non-class-theoretic context) exactly the same as the Smullyan and Fitting definition which is next on my list to be paged up.

c) Don't know what to do about Definition:Nest as it is tantamountly the same thing as Definition:Chain of Sets, and it is most definitely an actual Definition:Chain (Order Theory), except that it class theoretical version appears not to be classifiable as a "chain" as such.

I welcome thoughts and ideas. How to bring all this into the same place, but at the same time respect the traditional terminology by keeping the term "nest" in there somewhere -- or do we dispose of the concept of "nest" completely, and couch everything in the language of "chains" and "totally ordered sets" (or "tosets")? --prime mover (talk) 12:23, 29 May 2022 (UTC)

Good to see that this is finally cleared up. Thanks for your efforts. As for two cents, my understanding is that "nest" is specialised language and "chain" is standard language. I would therefore suggest to stick with "chain" and use "nest" as a redirect. All accompanied by the usual AKA and other sections enlightening the reader.

But perhaps the set/class distinction reveals some subtleties that will guide us in a better direction. — Lord_Farin (talk) 06:27, 30 May 2022 (UTC)

I think this is now complete.

I have retained the concept of Definition:Nested Sequence, and $\mathsf{Pr} \infty \mathsf{fWiki}$ now uses it exactly where appropriate. We have Definition:Nest as a main page, with Definition:Nest (Class Theory) as its subpage in the context of class theory, while the set-theory version of nest is Definition:Chain of Sets, which is also a direct subpage of Definition:Chain (Order Theory).

Definition:Chain (Order Theory) is the master page of the general chain (in the set theoretical context) of the general ordered set. As and when I see it in a source work, I will enter the class-theoretic analogue of the general Definition:Chain (Order Theory), but for the moment, S&F are only interested in chains of subsets.

From a result in Devlin, all these distinctions don't matter too much because any ordering on a set is isomorphic to a subset ordering. --prime mover (talk) 20:50, 31 May 2022 (UTC)

Our relevance in the academic world

I wonder if any of you have ever tried using Google Scholar to gauge our relevance outside the forum discussion level. At this moment GS shows 222 items, which refer to us in one way or the other. I have checked all of them, and Proofwiki appears in various degrees from just a passing mention or a source for a proof to proof generators with applications in education. I find the work of Welleck et al. particularry interesing. I almost wonder if there would be any gain from contancing them (scientists in general)? At the moment our interaction with the outside world is rather indirect.--Julius (talk) 20:21, 7 June 2022 (UTC)

The sterling work of the late Grzegorz Bancerek bringing $\mathsf{Pr} \infty \mathsf{fWiki}$ closer to his Mizar project is probably the closest we have actually collaborated with another site. I don't know whether such work is still going on, but they have been experimenting with tools to automatically parse $\mathsf{Pr} \infty \mathsf{fWiki}$ pages into an automatic theorem prover. This had originally been the hope all along. I don't know how far it got. I met up with some of that team at the symposium at Radbout back in 2011 when $\mathsf{Pr} \infty \mathsf{fWiki}$ was in its infancy. Sometimes I look at $\mathsf{Pr} \infty \mathsf{fWiki}$ now and wonder if it has actually got much further along. --prime mover (talk) 21:22, 7 June 2022 (UTC)

Trivial enhancement -- Featured Proof icon

Currently we have a smiley-face logo to illustrate the "featured proof". See Banach-Tarski Paradox for an example.

I would love this to be replaced with something more "personal" to $\mathsf{Pr} \infty \mathsf{fWiki}$. Smiley faces are so passé .

So, let's throw this open: can anyone come up with a better "featured proof" icon?

Apologies for wasting everyone's time and energy on such a trivial matter, but that's just the sort of person I am . --prime mover (talk) 11:17, 8 June 2022 (UTC)

We now have --prime mover (talk) 05:54, 21 June 2022 (UTC)

And another thing -- that Well-Ordering Theorem

The current status of the Well-Ordering Theorem is that it has a loose, woolly and handwavey proof dating back to when the page was first raised some 11 years ago (almost to the day) when the world was new-and-all.

My personal view is that maybe we should dispose of the given proof, and instead replace it with a link to Set with Choice Function is Well-Orderable, which is based on the more-or-less rock-solid foundation that is the first 4 chapters of Raymond M. Smullyan and Melvin Fitting: Set Theory and the Continuum Problem (revised ed.), all of which (up to this point, and apart from a few exercises whose solutions have not been done) is now covered completely on $\mathsf{Pr} \infty \mathsf{fWiki}$.

(Seriously, if you have a spare weekend when it's pouring down and there's nothing else to do, I'd recommend starting at the start and stepping through the "next" links till the end, it's really rather good.) (This will also give a few extra pairs of eyes on it.)

I intend to gather this Well-Ordering Theorem together with Zermelo's Theorem (Set Theory) in the same page structure, which can be renamed Zermelo's Well-Ordering Theorem to improve the name of each.

Thoughts? --prime mover (talk) 11:46, 8 June 2022 (UTC)

No objections so off I go --prime mover (talk) 19:13, 8 June 2022 (UTC)

Good job, nice improvement! — Lord_Farin (talk) 09:56, 10 June 2022 (UTC)

$L^p$ spaces

$L^p$ spaces are pretty much set up. Major step for analysis here. I will also need to put up the non-negative case for Radon-Nikodym derivatives (a huge roadblock in probability theory) but that's a job for another day. Caliburn (talk) 18:56, 8 June 2022 (UTC)

Keep up the good work. Way over my head right now as I'm at absolutely the other end of the mathematical spectrum at the moment. --prime mover (talk) 22:19, 8 June 2022 (UTC)

Looking good, great milestone! — Lord_Farin (talk) 09:56, 10 June 2022 (UTC)

Maximal Principles - further development

Using S&F as a keywork, I am gradually hacking through the undergrowth of the Maximal Principles, completely divorcing the principles themselves from the Axiom of Choice to which they are equivalent, stating this equivalence in separate proof pages as these proofs come to light.

This seems to simplify not only the pages themselves, but also the paths to the proofs, as there is now no need to worry about what rests on what in the actual pages stating the principles themselve -- these can now be left to the various assorted proofs stating specific implications.

This has the side-effect of making, for example, the "proof" of Zorn's Lemma considerably simpler than it appears, because all the heavy detail is now hidden away in the multitude of small results building up to the concepts of Principle of Superinduction and closure under chain unions and so on.

The mega-proofs can still live on, once they are tidied and restructured as need be, but now they will sit alongside the results that establish them as mere corollaries of the fundamental properties of well-orderings.

I don't know about you, but all this is now becoming much clearer in my mind to an extent that I am finally able almost to see their shapes.

I am considering how to generate diagrams to illustrate the steps along the way. --prime mover (talk) 21:32, 13 June 2022 (UTC)

Everything definitely has become clearer by the revisiting based on a rigorous source, so thanks a lot for that. I do have to say that it itches me a bit that there is now Zorn's Lemma/Formulation 1 and Zorn's Lemma/Formulation 2 where obviously they are not identical. As "my" version of Zorn is definitely Formulation 1, it is a bit difficult to see Formulation 2 also bearing the same name. Although I also don't really know a better way of doing it. Oh well, we learn every day I suppose. — Lord_Farin (talk) 19:47, 14 June 2022 (UTC)

I'm hoping to find that the two formulations are equivalent, but don't hold your breath waiting for that. --prime mover (talk) 20:29, 14 June 2022 (UTC)

Refactoring of Proof Rules

I am getting to a point in covering Kunen's Foundations book where I really need a proper basis for proof systems and rules of inference, to build successive results upon.

To that end, I have picked up the ambition to restructure the area around Definition:Proof Rule, Definition:Rule of Inference, and Definition:Natural Deduction. This was attempted in the past but I would say that by now we have the surroundings in place due to previous refactoring and rigorous foundation from other sources in the logic department (particularly PropLog).

As usual this endeavour amounts to separating the generic and the specific. No proofs depending on the specifics of natural deduction should be affected.

The details of my plans are at User:Lord_Farin/Sandbox/Proof Rules. I expect more content and some drafts to appear there in the coming time. Thoughts welcomed, either here or there. — Lord_Farin (talk) 21:03, 17 June 2022 (UTC)

It all sounds good.

The only reason PropLog is based on Huth and Ryan is because that's what I first laid my hand on when setting it all up to start with. It was the first time I had experienced "natural deduction" and seen it properly expanded upon. It was not until processing it that I began properly to understand Lemmon and Basson/O'Connor (the latter which I'd had since college but never properly cracked it).

Points where I part comprehensional company:

Model Theory and discussion about semantics. Metalanguage and formal language.

the philosophical meaning of if and only if and Definition:Logical Equivalence.

Making absolute sense of the Rule of Substitution and the SI rule -- they're how you drop completed subformulas into larger more complex structures, but I was never happy about how rigorous the proof is (proving the obvious is the hardest task ever).

Enjoy. --prime mover (talk) 22:21, 17 June 2022 (UTC)

Progress report: The page Definition:Natural Deduction is available as a draft under User:Lord_Farin/Sandbox/Proof Rules/Definition:Natural Deduction. Up next is Definition:Rule of Inference. — Lord_Farin (talk) 18:03, 18 June 2022 (UTC)

That was easy: User:Lord_Farin/Sandbox/Proof Rules/Definition:Rule of Inference. — Lord_Farin (talk) 18:29, 18 June 2022 (UTC)

Rules for limits of real functions

To be clear, we don't have pages for stuff like $\ds \lim_{x \to a} \paren {\alpha \map f x} = \alpha \lim_{x \to a} \map f x$ right? I'm quite surprised to be not able to find it, but I will put up pages for it very soon. Caliburn (talk) 13:26, 19 June 2022 (UTC)

Combination Theorem for Limits of Functions. — Lord_Farin (talk) 13:41, 19 June 2022 (UTC)

Great, not sure why I couldn't find that. I will change the categorisation so it's much clearer. Caliburn (talk) 13:55, 19 June 2022 (UTC)

Actually it seems fine the way it is, I don't know how I managed to miss it/forget about it. The pages for limits at $\pm \infty$ are up now anyway. Caliburn (talk) 13:57, 19 June 2022 (UTC)

Good work. Might I suggest that they be interlinked with the non-$\infty$ pages for easier navigation? — Lord_Farin (talk) 14:38, 19 June 2022 (UTC)

Ordinals

I am now making tracks into the material in Raymond M. Smullyan and Melvin Fitting: Set Theory and the Continuum Problem (revised ed.) concerning ordinals.

This may take some time.

I am also shivering on the brink of plunging in to remove the material (or some of it) from Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory. But rather than go through and wipe it all and start again, I am "just" going to replace any suspect definitions and results and replace them with S&F versions as I encounter them.

I would greatly appreciate anyone following this carefully to fill in any incomplete and unattempted proofs as I put them in place.

However, naturally all this material is based strongly on the heavily abstract analysis on well-orderings and superinduction, and this is not trivial to absorb. It makes for very short proofs, but each of those proofs is itself based on a teetering tower of abstraction into which the Von Neumann construction is dropped into the middle like a fish in the ocean. --prime mover (talk) 19:28, 23 June 2022 (UTC)

I am definitely intent on following the work you are doing, but other responsibilities interfere with my available time. I hope to not test your patience too much. — Lord_Farin (talk) 08:36, 26 June 2022 (UTC)

I found some extra time and reviewed most of the work; I focused mainly on refactored and/or new pages. Comments left where appropriate, but as usual the quality was great. Thanks for your efforts! — Lord_Farin (talk) 12:02, 26 June 2022 (UTC)

Be warned: recent work on ordinals may be a little ragged, as S&F are starting to cut corners and use results that they appear not to have specifically demonstrated. While some of those do exist on $\mathsf{Pr} \infty \mathsf{fWiki}$ they are proved from the T&Z or Devlin paradigm, which may lead to circular or unsound reasoning. I need to go through and tighten it up and fill in those gaps, but for the moment I want to make sure the results being demonstrated are actually in there. --prime mover (talk) 05:19, 29 June 2022 (UTC)

Notational paradigm review: $\ds \bigcup C$ as opposed to $\cup C$

Consider the concept of the union of a set of sets.

$C$ is a set of sets:

$\ds \bigcup C$ is the union of $C$.

In order to render the above consistently, we need $\ds \bigcup C$ which is unwieldy and clumsy.

But if we just use $\bigcup C$ it looks better: $\bigcup C$, but then continues to be rendered $\ds \bigcup C$ when it appears in {{eqn}} or {{Axiom}} etc.

So the question is: can we go through and render this construct just as $\cup C$, which is compact in presentation and efficient to type?

We do of course keep the $\ds \bigcup$ form when using $\ds \bigcup_{i \mathop \in I} S_i$ or $\ds \bigcup_{i \mathop = 1}^n S_i$.

Thoughts?

Same of course applies to $\ds \bigcap$ and similarly defined operators. --prime mover (talk) 09:50, 24 June 2022 (UTC)

I don't like $\cup C$ at all. To me the "lower-case" $\cup$ should be used with finite unions ie. $A \cup B$, and $\bigcup$ (though maybe not displaystyled) should be should be the one that works over a set of sets. I think in stuff I've written for myself I've just used $\bigcup C$ for union of $C$, not displaystyled, so would support that option here. Caliburn (talk) 12:01, 24 June 2022 (UTC)

Thanks for your input.

The problem with using $\bigcup C$ without displaystyle is that it automatically gets displaystyled up when in the {{eqn}} environment. So we have this layer of inconsistency which may be viewed as a lack of consistency. --prime mover (talk) 12:41, 24 June 2022 (UTC)

For me the "inconsistency" is fine. I don't think it will lead to confusion. The distinction between normal and subscripted variants would lead to more confusion overall I would say.

Additionally, losing the \ds has the benefit of nicer, more proportional parentheses: $\paren{\bigcup C}$ vs. $\paren{\ds\bigcup C}$. — Lord_Farin (talk) 08:34, 26 June 2022 (UTC)

I will concede that $\paren {\bigcup C}$ vs. $\paren {\ds \bigcup C}$ is an improvement. I can live with the inconsistency if everyone else can. --prime mover (talk) 09:21, 26 June 2022 (UTC)

Something's gone tits-up in the software -- menu items reporting QINU errors

An image capture:

And when you click on one of the links above the menu (either Definition:Image (Relation Theory)‎ or Mapping next to it, you get "Internal Error":

[440d5e46b7a25368c8a76cb2] 2022-07-01 18:54:09: Fatal exception of type "Error"

Presume something has changed for the worse. --prime mover (talk) 18:54, 1 July 2022 (UTC)

Looks like an issue with the latest MediaWiki software I updated to this morning. I've reverted the update for now and will take a look to see what's happening. --Joe (talk) 18:59, 1 July 2022 (UTC)

It seems to be when you have embedded $\LaTeX$ in the heading. --prime mover (talk) 19:03, 1 July 2022 (UTC)