User talk:Lord Farin

From ProofWiki
Jump to navigation Jump to search
Welcome to my talk page.
Here, you can leave messages intended specifically for me. If the topic is of site-wide interest, please consider using the Main Page Talk.


User talk:Lord_Farin Archives

Archive 1: Oct 10, 2010 to Dec 15, 2012
Archive 2: Dec 16, 2012 to Jan 1, 2014


Template for Gentzen proofs?

Since we have a template for non-Gentzen tableau proofs, it might be worth constructing one for the new Gentzen ones you're constructing at the moment. It should save some considerable effort and page space. What say? --prime mover (talk) 15:05, 2 April 2014 (UTC)

I don't expect many proofs in this style, since even Ben-Ari tries to move on to different proof systems quickly. It is not a proof system that is very common or popular (other Gentzen systems are, however). I deem it wise to not create a template specifically for this proof style.
Nonetheless, given that we can expect more and more proof systems in the future, it might be a good idea to generalise Template:BeginTableau to arbitrary proof systems, and provide a generic template which can act as a semantic hull around the MediaWiki syntax, just like Template:Eqn and Template:Axiom do. This will make it easier to adapt to future needs. — Lord_Farin (talk) 17:36, 2 April 2014 (UTC)
More challenging ... I'm not immediately planning on doing all that much more in this area (I only raised it in the first place so as to have something to plant ZFC in back in 2008 and it all got a bit unwieldy) so for the moment I'll leave this until I have another manic episode. --prime mover (talk) 19:28, 2 April 2014 (UTC)

Boolean Algebra

I have been investigating the "Wanted Pages" list and clearing out dead links to superseded pages. One such is Category:Boolean Algebra, where there is still a link from the Algebra page. Is it appropriate to replace this with Definition:Boolean Algebra in your opinion, or to remove it from that particular list in which it appears? --prime mover (talk) 08:23, 2 May 2014 (UTC)

... or indeed replace with Category:Boolean Algebras? --prime mover (talk) 08:27, 2 May 2014 (UTC)
I think it'd be best to remove it. A link to Definition:Boolean Algebra could be added to the "Algebra (Abstract Algebra)" subpage. — Lord_Farin (talk) 21:11, 2 May 2014 (UTC)

Question about Definition:Smallest Element

Back in December 2013 you placed an "expand" template onto Definition:Smallest Element saying:

Some links to this page are actually referring to the smallest element of a subset. This has to be defined, and the links changed to the resulting subpage.

I've looked at this, and raised such a subpage Definition:Smallest Element/Subset, but I'm unclear as to how well this serves us.

After all, a subset is a set, and has the same properties as a set, and so the smallest element of a subset is defined in the same as the smallest element of a general set -- whether that set is a superset of it or not.

Hence a page containing something like "the smallest element of $T$ where $T \subseteq S$" is equally well served by Definition:Smallest Element as it is to a separate page defining the concept of "smallest" in the specific context where the set in question happens to be the subset of an ordered superset. None of the works I have raise it in a separate definition (however I see you have access to the Munkres and Birkhoff works which I don't, so while I can't check them, maybe you can).

The only circumstance I can think of where the concept may be worth separating out and emphasising is the one where $S$ is partially-ordered while $T$ is totally ordered -- but we have that covered by the page Definition:Chain (Set Theory).

Can you take a look at this and add some thoughts? I should have asked the question at the time, but back in Dec. 2013 I was freezing my nuts off in $-10 \cels$ blizzards, and the brain was less well disposed to think about it. :-) --prime mover (talk) 08:34, 5 April 2015 (UTC)

The most apparent definition arises in the context of a woset. While it is ultimately the same definition, a reader may fail to recognise that the ordered set one is talking about is actually the subset.
One might add that Munkres explicitly defines this on subsets. It is also relevant in the intuitive coupling of largest element and supremum.
I'm pretty sure, though, that Munkres triggered me to create the expand template. Does that address your concerns in an adequate manner? — Lord_Farin (talk) 21:55, 6 April 2015 (UTC)
Okay, given that I'm unfamiliar with the Munkres, has the treatment I have offered on the subpage I added consistent with his treatment? --prime mover (talk) 22:01, 6 April 2015 (UTC)
Most definitely, although he doesn't bother with the formalism of writing $\preceq \restriction_T$. — Lord_Farin (talk) 22:39, 6 April 2015 (UTC)
The above is being refactored for ongoing simplicity and increased modularity with a view to implementing more rigorous separation of Class Theory and Set Theory.

mathbin, mathrel, mathop

Recommend we go through and change "mathop" to "mathbin" and "mathrel" as appropriate, as we progress? I confess it's not a job I fancy doing in one go. :-) I picked up on the differences when I went through the work on TeX codes at the weekend, so I'm fairly well up to speed on it and I appreciate that it "ought" to be done, but it's not something I can nerve myself up to.

Gradual seems like just fine to me. Or "as noticed". — Lord_Farin (talk) 21:56, 7 April 2015 (UTC)

While I'm here, I wonder whether the "mathbin" entries on Inverse of Order Isomorphism is Order Isomorphism should actually be "mathrel" as $\preceq_1$ etc. is technically a relation not an operation. What say? --prime mover (talk) 18:13, 7 April 2015 (UTC)

It was a subconscious thought after changing that page (among others) that this was actually wrong that triggered me bringing this up in the first place. I have fixed it.
Further investigation ... in places where we have x \mathop{\preceq_1} y and so on, we can in fact just remove the mathop altogether, and just have x \preceq_1 y, because it appears that MathJax may have fixed the bug whereby subscripted relations were not being treated as relations.
Check out:
The $\LaTeX$ code for \(x \mathop{\preceq_1} y\) is x \mathop{\preceq_1} y .
The $\LaTeX$ code for \(x \mathrel{\preceq_1} y\) is x \mathrel{\preceq_1} y .
The $\LaTeX$ code for \(x \preceq_1 y\) is x \preceq_1 y .

So not only is mathop now demonstrably different from and inferior to mathrel, mathrel is not even needed.

IIRC the reason we started using mathop in the first place was because it was the only one of these modifiers that had actually been implemented on MathJax adequately at the time. The new version of MathJax seems to have resolved all of this. --prime mover (talk) 06:44, 8 April 2015 (UTC)

Awesomeness (TM). — Lord_Farin (talk) 14:59, 8 April 2015 (UTC)
... although another reason we started using mathop was to put some spacing between summation limits. Neither mathrel nor mathbin do the job here, only mathop does what we want it to:
The $\LaTeX$ code for \(\ds \bigcap_{\alpha \mathbin \in I}\) is \ds \bigcap_{\alpha \mathbin \in I} .
The $\LaTeX$ code for \(\ds \bigcap_{\alpha \mathrel \in I}\) is \ds \bigcap_{\alpha \mathrel \in I} .
The $\LaTeX$ code for \(\ds \bigcap_{\alpha \mathop \in I}\) is \ds \bigcap_{\alpha \mathop \in I} .
The $\LaTeX$ code for \(\ds \bigcap_{\alpha \in I}\) is \ds \bigcap_{\alpha \in I} .
--prime mover (talk) 14:58, 8 April 2015 (UTC)
Hmm... Some cursory search and testing have convinced me that continuing to use \mathop is the way to go, although it is not an elegant solution. There is simply no other option I know of, except manually fiddling around with spacing. — Lord_Farin (talk) 15:18, 8 April 2015 (UTC)

Families

Advice needed on where to go with this one.

Munkres is the only author I've seen who defines the terminology of indexing sets using definitions which are intuitively clear:

a) An Definition:Indexing Function is the actual mapping from $x: I \to S$
b) A Definition:Indexed Family is the set of elements of $S$, together with the mapping itself.

Every other source I've seen calls the mapping itself the "family", despite giving it the intuitively-suggestive notation $\langle x_i \rangle$ (or whatever notation used).

Consequently I have decided to go with Munkres's definition, despite the fact that he appears to be in a minority.

Or do you see this as: everybody else has failed to define the concept precisely enough, and has made a mistake by failing adequately to distinguish between the mapping itself and its codomain?

It is also interesting that Munkres is the only one who specifies that the mapping itself needs to be a surjection -- a point which I still have yet to address in the definitions.

As a practical matter, however, I have changed the links on Halmos and Givant so as to allow it to point to Definition:Indexing Function instead of Definition:Indexed Family. You may wish to review this in order to make sure the flow accurately reflects the specific treatment of Halmos and Givant here: do they define a "family" as the mapping, or the mapping together with its codomain?

I also need to consider whether to include the "also defined as" on Definition:Indexing Set/Family on a separate page and then transclude it onto other pages in the same way as Notation and Note on Terminology.

Are you able to cast an eye over this area? I just need a second opinion on it. Thanks. --prime mover (talk) 09:09, 25 April 2015 (UTC)

There are basically two points of view at work here which are conceptually quite different. The majority of writers takes the indexing set $I$ as the starting point; from this point of view, it is more natural to define the concept in the way they do (e.g. Halmos/Givant do it in this fashion), as simply the function $x: I \to S$.
On the other hand, we have Munkres (and it's inconceivable he is alone). The viewpoint now is radically different: We start with a set $S$ (in Munkres' case, a set of sets), which we want to index. In this view, it makes sense to bring $S$ along explicitly, and to require an indexing function to be surjective -- after all, it was not merely a subset of $S$ that was to be indexed.
With this in mind, I think it is not warranted to choose between the two. Rather, we should aim for an exposition that somehow manages to unify these treatments. I'm sorry to burden you with this task, but ultimately I think this is the best way to go. — Lord_Farin (talk) 09:53, 25 April 2015 (UTC)
Are you happy with the approach which I have just taken? --prime mover (talk) 21:49, 26 April 2015 (UTC)
Except for the note I left on one of the talk pages, the content looks good. Regarding presentation, it is maybe a bit awkward to have Indexing Set as the master page. Perhaps Indexed Family ought to be the parent page, with all related concepts as subpages; in this way, subpages will describe portions of the entire thing, which is the Indexed Family. (But I understand if you don't want to embark on that journey right now.) — Lord_Farin (talk) 08:08, 27 April 2015 (UTC)
You're right, it does appear as thought "indexed family" is the main concept, and all the other parts of it should perhaps be subpages. It's not quite as big a job as it looks on the surface, though, because our redirect strategy is a good one. --prime mover (talk) 15:31, 27 April 2015 (UTC)
All instances of Definition:Family have now been reviewed and replaced by a link to the appropriate instance of "indexed family", be it "of sets" or "of subsets" or neither. Time for a break; Definition:Family can now become a disambiguation page as suggested in a conv with Joel on Definition talk:Indexing Set/Function a while back. --prime mover (talk) 20:03, 27 April 2015 (UTC)

Eqn template: puzzling

So one of the rules of the game is: do not have adjacent {{ or }} in an Eqn template, or it will break.

So I'm puzzled at how this:

{{begin-eqn}}
{{eqn | l = \gcd \left\{{F_{k+1}, F_{k+2}}\right\}
      | r = \gcd \left\{{F_{k+1}, F_{k+2} - F_{k+1}}\right\}
      | c = [[Common Divisor Divides Integer Combination]]
}}
{{eqn | r = \gcd \left\{ {F_{k+1}, F_k} \right\}
      | c = Definition of [[Definition:Fibonacci Numbers|Fibonacci Numbers]]
}}
{{eqn | r = \gcd \left\{{F_k, F_{k+1}}\right\}
      | c = 
}}
{{eqn | r = 1
      | c = [[Consecutive Fibonacci Numbers are Coprime#Induction Hypothesis|Induction Hypothesis]]
}}
{{end-eqn}}

manages all right.

I think the fact that the {{ and }} come in pairs very close together may have something to do with it -- but had you noticed this?

It's on page Consecutive Fibonacci Numbers are Coprime if you're interested. --prime mover (talk) 21:24, 2 June 2015 (UTC)

It's definitely a fluke, and should be expected to break at any moment. Thanks for spotting, you're sharp :). — Lord_Farin (talk) 21:26, 2 June 2015 (UTC)

More on the eqn template

Check out Inverse Cosecant is Odd Function.

Note how the $\pi$ on one line is overlapped by the $2$ on the line above.

This is the source of the comment I made about adding some top and bottom padding to the eqn template.

I tried experimenting with this but could not get it to work.

Are you able to do some magic here? --prime mover (talk) 22:22, 5 June 2015 (UTC)

I've added 3px bottom and top margin. If you feel it should be 2 or 4 (5 is a bit too much I think, it adds up to 10 total in that case), just change the 3px occurrences to whatever you deem suitable. But 3px works fine for me. — Lord_Farin (talk) 22:49, 5 June 2015 (UTC)
That looks perfect. Good job. --prime mover (talk) 04:54, 6 June 2015 (UTC)

Help needed with eqn-intertext

The current Template:Eqn-intertext is all very well, but it puts all text into the first column, which then expands to fill it and compromises the appeal of the page.

Is there a way of making the text spread over all the columns of the table, perhaps using a "merge columns" technique? A good example of a page where it is to be made use of is Primitive of p x + q over Root of a x + b. --prime mover (talk) 06:17, 11 June 2015 (UTC)

Sorry for not minding my own business, but I solved it. --kc_kennylau (talk) 06:29, 11 June 2015 (UTC)
Brilliant! I knew it was simple, I just didn't care to look up how to do it ... :-) --prime mover (talk) 06:38, 11 June 2015 (UTC)

Jacobson's treatment of Peano axioms

1951: Nathan Jacobson: Lectures in Abstract Algebra: Volume $\text { I }$: Basic Concepts treats the Peano structure in considerable detail, but uses a $1$-based approach, not $0$-based.

How do you envisage this being treated?

a) State "Some treatments define the unique non-successor element as $1$ instead of $0$", and leave it at that

b) Provide a full definition of each addition, multiplication, etc. in the 1-based schema, and separately demonstrate the commutativity / associativity / distributivity laws?

c) A combination of the two?

Since I have the book and have been tasked with the source review, I suppose it devolves to me to do whichever approach is decided. --prime mover (talk) 07:13, 22 September 2015 (UTC)

I feel we can get away with a). Therefore, I think it is more valuable to dedicate our limited resources to other areas of PW. In an ideal world, b) would be preferable, but due to the declining importance of the 1-based approach this does not have priority for me at the moment. (A similar thing will go for meticulously proving the equivalence of the defined operations in the various axiomatisations -- I'm going to postpone it.)
If in due time we find a good number of sources on the 1-based approach, which furthermore make the top of the list of books to be covered, we can reconsider.
Until then, a) suffices in my book. I feel that once multiplication and the ordinal entanglement are revisited, the section about $\N$ is sufficiently coherent to serve as a stable basis for further development of other areas of PW. — Lord_Farin (talk) 15:15, 22 September 2015 (UTC)
I implemented a template "Non-Successor Element 1" which states the case and has been used in various places and in particular Definition:Addition/Peano Structure and Definition:Multiplication/Natural Numbers -- the latter of which now has a muce clearer boundary between $0$-based and $1$-based.

Further number theory axiom question

This page: Axiom:Axiom Schema for 1-Based Natural Numbers is what I renamed Axiom:Axiomatization of 1-Based Natural Numbers, as there were already some pages linking to that directly. It fixed a load of redlinks.

What's the plan here? Leave it at that? --prime mover (talk) 19:23, 22 September 2015 (UTC)

The plan was to rename it because it's not a "schema", it's a finite set of axioms. Apparently I somehow forgot to address the pages linking to it. — Lord_Farin (talk) 20:06, 22 September 2015 (UTC)
In general I've been quite tired from this refactoring endeavour, so I'm patching up the final pieces that really need to be done and then I'll move somewhere else. — Lord_Farin (talk) 20:06, 22 September 2015 (UTC)
All those are done except for a few links from your backup pages etc. I haven't done Definition:1-Based Natural Numbers yet as it's not so contentious. --prime mover (talk) 21:16, 22 September 2015 (UTC)
The last thing on my list is to address multiplication. I'll try to make time these days, it'll feel good to be done. — Lord_Farin (talk) 15:31, 23 September 2015 (UTC)

Recreating links to moved pages

There are a lot of pages in your backup area which were moved from their main pages without leaving a redirect. Trouble is, these have left some redlinks, in particular the source flow from Well-Ordering Principle which had not had all its links changed.

I have gone through and replaced a few of the redirects, but I realise the problem is more widespread as there are many pages in your backup with no redirects to them, and I am worried we are going to lose the flow (specially around the Induction proofs).

My preferred technique is never to move without leaving a redirect, and never delete the redirect until all links via the redirect have been repointed. I use "What links here" to check, and then go through and change each one methodically.

Hope this hasn't put you out too badly, as I say there were some redlinks to non-redirected moved pages and it wasn't clear to me exactly where they were supposed to go. I worked it out in the end, but I want to make sure everything is linking before we clear out redirects. --prime mover (talk) 22:23, 22 September 2015 (UTC)

I know that the rule is to have redirects. However, I treat the backup area as special. Namely, it is a backup area. Everything there is a snapshot from before an important change, so that if need be, we can easily restore everything by removing the appropriate prefix from the page title. I don't care for redlinks on these pages; they shouldn't be visited anyway, and in theory should be regularly purged.
At times, I furthermore take the liberty to spawn redlinks on talk pages, where in my head, they indicate that the section they're in can safely be regarded as obsolete and can in principle be deleted.
For all other links, I always try to make sure they are changed appropriately.
With this procedure I preserve the structural integrity of the site with minimal effort. I'm not inclined to change it. But perhaps it would've been good to make these assumptions more explicit, as they apparently led to some confusion on your part -- sorry for that. — Lord_Farin (talk) 15:31, 23 September 2015 (UTC)
Point is that not all the live pages had been amended so that the links had all been updated, so the redlinks (well, one, anyway) were on live pages not on backup pages. Hence and so. I still prefer not to delete a redirect till all the pages that link to it have been addressed. Even backup pages, because at least if you've got a redirect to a backup page, you have a chance at working out where the link ought to go to, otherwise one is lost. --prime mover (talk) 16:18, 23 September 2015 (UTC)
There's a valid point there. I'll consider it next time. I'll also try not to screw up the redirecting of live links. — Lord_Farin (talk) 16:48, 23 September 2015 (UTC)

Deletion of Natural Numbers form Naturally Ordered Semigroup

I've been tidying up some of my Source Review tasks, and have come upon Natural Numbers form Naturally Ordered Semigroup.

There are a number of pages dependent upon this, from when the definition of Natural Numbers was based on that analysis. Without this page, there is no longer an explicit page defining the link between the Naturally Ordered Semigroup and the Natural Numbers. There is a definite place for a page that links up the derivations that state:

a) The Natural Numbers fulfil the requirements for being a Natural Ordered Semigroup
b) The Naturally Ordered Semigroup is unique under isomorphism

thereby allowing us to identify the natural numbers with the NOS.

We already have a transcluded link on the Natural Numbers page which defines the $\N$ as an instance of an NOS, but I am afraid that if we are not careful we will (under the guise of tidying up) remove some important links in the chain of reasoning that allow us to define $\N$ from the NOS axioms. It's not a mainstream derivation, but I believe it has some benefit, if nothing because Seth Warner is so delightfully thorough in everything he does, and his construction is a paradigm of such attention to detail.

So, in short, can we either leave this, or make an effort to restructure all the pages which depend on it so as to allow alternative reasoning (e.g. Peano-based) for their justification? There's a huge pile of pages (just do "What links here" from it, you'll see the extent of the task) which I'm not in a position to address right now, I'm supposed to be packing to leave for Romania in a couple of hours. --prime mover (talk) 10:41, 11 October 2015 (UTC)

You make a fair point. But, and this will remain my point of view, there is no such thing as "the natural numbers" in existence with the adequate mathematical precision. Therefore, the NOS was invented as an adequate or at least plausible axiomatisation of $\N$.
Now of course the axiomatisation may be strengthened if it's proven equivalent to some other prevalent and so far highly successful treatises of $\N$ in a precise way. But it cannot and will not ever replace the intuition everyone has on $\N$.
Therefore I think the only viable option is to rephrase all the linking pages. It needn't be hard. We only need to say "consider $\N$ defined as a NOS" instead of referring to said theorem. I'll try to find the time. — Lord_Farin (talk) 15:13, 11 October 2015 (UTC)
I still think there is a disconnect -- we have "consider $\N$ defined as a NOS" but do we have a page establishing why we can do this? My original thinking behind this page was purely so there is a direct link to a page which says "... and we can use the NOS as a model for the natural numbers because ..."
You're right, it all boils down to an "intuitive" understanding of what makes $\N$ what it is -- but exactly how to establish this I'm not sure, beyond a vague "... and this is a model for $\N$ because it's infinite and it's got addition, multiplication and ordering and they act like ..."
Do we need a separate page again for the "axioms" of what define natural numbers from an "intuitive" perspective?
If this isn't all done by the time I get back, I'll continue giving it some thought, but at the moment (on 3 hours sleep and inadequate coffee) I'm not able to summon enough grey cells. :-) --prime mover (talk) 05:10, 12 October 2015 (UTC)
There is no reason why we can do that beyond proving a lot of results with NOS that we expect to hold for $\N$, as well as not managing to prove anything that is false for $\N$ (the latter being critical to the axiomatisation's success). There is no such list of "axioms" beyond the vague sentence you wrote down. Anything more is simply philosophy of maths, which is admittedly beyond the scope of this site.
It's admittedly a leap of faith. But it's all we've got, because there cannot be a rigorous jump from our intuition to the safe confines of mathematical rigour -- such would prove all instances of "our intuition" are equivalent which is contradicted by the existence of open problems about the natural numbers. Sad but true. — Lord_Farin (talk) 16:05, 12 October 2015 (UTC)

The discussed references have been appropriately replaced, and the page under discussion is no longer among us. — Lord_Farin (talk) 14:40, 25 October 2015 (UTC)

Yes, thanks for sorting that one out, I was going to but got sidetracked again by a different book. --prime mover (talk) 15:46, 25 October 2015 (UTC)

Refactor of Ordered Pair

I have refactored the definition of Ordered Pair, setting the Kuratowski formulation as a second definition, and establishing an equivalence proof page. There are another couple of pages which need to be source-reviewed for the Howson and the Halmos / Givant, which you may be able to attend to. Silly me, I've been getting new books. --prime mover (talk) 16:50, 24 December 2015 (UTC)

I've been away lately, but I'll try to keep up to speed now. I'll keep a tab open on the Source Reviews until it nags me enough to make me attend to them. Next year, I might start cracking on PredLog and subsequently Model Theory. We're seriously lacking proper coverage in especially the latter category, although an earlier endeavour of mine at least put consistent nomenclature in place. — Lord_Farin (talk) 15:55, 28 December 2015 (UTC)
Having just got hold of a great pile of books on logic and foundations of mathematics and all that, I expect to be thundering around this area again myself in the immediate future. Given that I have a massive heap of refactoring to do, I will address each one during the course of running up against it during the course of ploughing through whatever work I am studying at the time (at the moment it's Tarski, it's light and fairly easy -- so far -- and goes into model theory later on) so be aware of that. I hope we don't clash too badly. --prime mover (talk) 21:16, 28 December 2015 (UTC)

New departure: Specific Axiom Systems

I have finally established the context into which specific axiom systems for Propositional Logic are to be placed. Please feel free to take a look and see whether it makes sense. Note the page Definition:Axiom System and its subpage (to be expanded). The source work I am using which I found at the bottom of a pile of books the other day is somewhat vague, but it does make clear what its starting axioms are (once it gets down to business). Some of its definitions need to expanded and made rigorous, and some of them may need to be merged into others. As I say, feel free to add any input you may feel appropriate. --prime mover (talk) 07:43, 12 January 2016 (UTC)

Hm, looks interesting. However, what I notice immediately is that the distinction between Definition:Proof System and Definition:Axiom System is very opaque. The way I interpret it, the two are identical. Both specify axioms and rules of inference (= rules of transformation). Interesting is the introduction of "Definitions". The why and how of integrating these into the appropriate dissertations has been bugging me for quite some time. One of the problems is that these definitions often only work within the context of some given proof system (and fail in e.g. intuitionistic calculus).
For now, I would be content with the following set-up:
1. Merging Proof System and Axiom System
2. Setting up a page "Proof Systems for PropLog"
It remains an open problem how to present the various formal languages for PropLog. The same issues arise with PredLog, as I'm encountering now. — Lord_Farin (talk) 15:23, 13 January 2016 (UTC)
Are you okay with me ploughing ahead with this as it is, on the understanding that the outstanding issues get resolved as and when the insight comes? I note, for example, that the "rules of transformation" (not explicitly defined in Basson & O'Connor, but taken for granted as truths) can be considered to be "universal" and always to sit on top of the axioms and proof system as metarules. This is consistent with their treatment in Lemmon, which I believe also borrows from Principia Mathematica, but is even less clear than Basson & O'Connor. This is also to be reconciled with Hamilton, which "does" Hilbert's 3-axiom, 1-transformation-rule system which I kept promising myself I'd return to and then I see that I keep running across it wherever I turn ... --prime mover (talk) 22:50, 13 January 2016 (UTC)
Indeed, such "rules" are written in the metalanguage. For, they contain statements about $\vdash_{\mathscr P}$ in one way or another (it's always a bit messier to make things precise, especially in absence of detachment ($\vdash p \to q$ iff $p \vdash q$)). But in the end I would consider them part of the proof system. I can see your point, though. Perhaps it's just the names that I found confusing on first glance. We'll reconcile in due time. Once my job grants me some head space I'll come up with something. — Lord_Farin (talk) 23:09, 13 January 2016 (UTC)

PropLog: Changes made

Mighty changes made in PropLog. Immediately relevant:

a) All "proof rule" logical formulae have been extracted into their own pages: each per formula, so as better to separate out those which are used in a particular exposition's "proof rule list" or "axiom list", which work will start properly in due course. (There are still a few to do, but it is mostly there.)

b) All "proof rule" templates have been amended so as to pick up these changes. The templates themselves use your "TableauLine" template, which has been enhanced so as to add a small gap either end of the elements in the table for better presentational style. This has also served to consolidate and make consistent the presentation of tableau proofs, so that any future changes can be done in just one place.

c) Note that I have changed the name of some of the rules: "or-elimination" is now "proof by cases", and has been merged with the existing PBC pages. "Rule of Bottom-elimination" (never liked that name) is now "Rule of Explosion", I would have called it "quodlibet" if I thought I could get away with it. (And I think there may have been another one. Can't remember. Been a long weekend.) I think all pages have been renamed as appropriate -- but please be aware that I have renamed some stuff on your user pages so as to keep consistency throughout.

Still plenty to do in this area to get where I want to be before I can build the axiom frameworks for the various different structures, but it is very more in line with where I see it going. But I wanted you particularly to be aware of the renaming I did. --prime mover (talk) 21:58, 17 January 2016 (UTC)

I like what I see. Especially the distinction between Proof Rule and Theorem is a nice step forward. I have been contemplating PredLog recently, still haven't come up with a universally satisfying solution. I naturally won't start working until I've marked such a target on the horizon.
I expect the idea for PredLog to drop in the coming week or so, I can slowly start to feel it materialise in my head. Fortunately there's much less stuff on PredLog than on PropLog, making any restructuring much easier. I'll keep you posted. — Lord_Farin (talk) 23:28, 17 January 2016 (UTC)
Well, I got so far with it, but now (having ill-advisedly started ploughing through the utter unreadable sludge that is Principia Mathematica) I am suddenly sick of the sight of symbolic logic. I'm going to take a break from it once more and work on something lighter again. --prime mover (talk) 21:52, 18 January 2016 (UTC)

Interesting quirk to subst:Subpage technique

I offer you:

== [[Faà di Bruno's Formula/Historical Note|Historical Note]] ==
{{:Faà di Bruno's Formula/Historical Note}}

Interestingly, it swapped the apostrophe for its html encoding but not the accented a. :-) Have fun. --prime mover (talk) 01:33, 16 August 2016 (EDT)

Luckily, this helped :). I also fixed Template:Subproof to use Template:Subpage, simplifying future maintenance. — Lord_Farin (talk) 11:49, 16 August 2016 (EDT)
Many thanks -- every improvement is an improvement. --prime mover (talk) 14:39, 16 August 2016 (EDT)

Colons in templates

I remember some talk about this but cannot remember its resolution ...

I've been tidying the Template:Citation so as to make the colon in "Vol. 12: 123 - 456" comes out correctly. As it is there is a space (a nbsp in fact) before it, because if you have a colon immediately as the start of a conditional clause it interprets it as a page break.

Now I remember you mentioning a technique that can be used to prevent this happening, but cannot remember what it was, and can't find it in the discussion archives.

Can you remember? Cheers. --prime mover (talk) 01:11, 12 September 2016 (EDT)

I guess you refer to Template:! which renders the pipe |. I don't think there current exists an equivalent for the colon. You could use nowiki, or define Template:; to yield a colon. Those are the two options I see (a third being their combination). Does that answer your question? — Lord_Farin (talk) 11:47, 12 September 2016 (EDT)
(NB. MW 1.24 introduced the ! as a magic word, so the template is now unnecessary. But the effect is identical.) — Lord_Farin (talk) 11:48, 12 September 2016 (EDT)
nowiki did the trick. Many thanks. --prime mover (talk) 15:07, 12 September 2016 (EDT)
Np yw. — Lord_Farin (talk) 15:13, 12 September 2016 (EDT)

MSC template

Why did you delete the MSC template? Yes I know I never got round to doing anything with it, but the plan and the possibility are still there. Are we getting short of space? --prime mover (talk) 17:37, 12 September 2016 (EDT)

Because in its current form it took an unnecessarily large chunk of screen estate, gave no explanation, and only linked to some random list of mathematical subjects. So I figured that if we are ever going to start this task (we $\ne$ me), we'd be better off starting from scratch. — Lord_Farin (talk) 00:55, 13 September 2016 (EDT)
O very well. --prime mover (talk) 01:47, 13 September 2016 (EDT)

Contour Integration by Substitution

LF, I am going to need to invoke Contour Integration by Substitution, which I'm not in a position to prove yet.

To clarify: I'm allowed to do $\ds \int_{z_0}^{z_1} f (z) \rd z = \int_{u^{-1}(z_0)}^{u^{-1}(z_1)} f (u (z))u'(z) \rd u$ if $u$ is a homotopy, right? Is that enough? What conditions do I need on $f$? The integral I'm working on is in my sandbox, the one that I need for Laplace Transform of Complex Power. Feel free to answer my question on Stack Exchange if you feel like sharing the answer with others. Thanks in advance! --GFauxPas (talk) 07:22, 7 December 2016 (EST)

You have to keep in mind that we're talking contour integration here. So in fact there is no such thing as $\d z$, because the integral is defined as $\int_0^1 f(\gamma(t))\gamma'(t) \rd t$ for a suitable parameterisation $\gamma$, and the $\d z$ is just for resemblance. Therefore I think there is no general substitution theorem of the kind you allude to (and I can't remember ever seeing one). Rather one has to resort to Cauchy's theorem and/or perform the substitutions after the transition to the complex Riemann integral has been made. In special cases such substitutions might result in a contour integral of a different curve, but I think this should be seen as incidental.
Caveat: it has been some time since I concerned myself with complex analysis (and admittedly it has never been my forte), so please don't thoughtlessly take my words for fact. — Lord_Farin (talk) 12:05, 7 December 2016 (EST)
Hmm... Just thinking. It might be possible to phrase a theorem like this with biholomorphic functions. Maybe that will lead you somewhere. — Lord_Farin (talk) 12:11, 7 December 2016 (EST)
So what allows me to make the substitution to change the integrand into one that resembles the gamma function integrand? Isn't it "just" a coordinate transformation? Intuitively I should be able to change the contour if the substitution function is biholomorphic and homotopic. --GFauxPas (talk) 12:36, 7 December 2016 (EST)
Should I split the integrand into real and imaginary parts for the proof? --GFauxPas (talk) 12:41, 7 December 2016 (EST)
I'm sorry, I'm seriously out of my depth with this stuff. You'll have to figure it out on your own :(. — Lord_Farin (talk) 13:35, 7 December 2016 (EST)

Someone responded with a proof! It looks like the mapping doesn't even need to be bijective. I'll try to put it up on $\mathsf{Pr} \infty \mathsf{fWiki}$ this week. --GFauxPas (talk) 14:49, 11 December 2016 (EST)

Everyhere

Yes I know I made a mistake. I had a domestic interruption before I was able to correct it. I had to attend to needs of the household. I could not avoid that, and I was going to come back and delete it as soon as I had done it. Apologies. --prime mover (talk) 07:39, 14 January 2018 (EST)

No problem. I saw it, I thought I'd correct it in case you didn't notice. Apologies are totally unnecessary here. — Lord_Farin (talk) 07:54, 14 January 2018 (EST)

Quick question about Definition:Constructed Semantics/Instance 1

I notice we have this sort of construct:

$v \left({ \neg \phi }\right) := \begin{cases} 1 &: \text{if $v (\phi) = 2$} \\ 2 &: \text{if $v (\phi) = 1$}\end{cases}$

where we have $\LaTeX$ nested inside a text element (only there to allow an "if".

Is there a reason:

a) why not to just do, for example, "$\text{if } v (\phi) = 1$" (thereby "just" rendering the "if" in the text box;
b) doing away with the "if" altogether, and merely rendering it as:
$v \left({ \neg \phi }\right) := \begin{cases} 1 & : v (\phi) = 2 \\ 2 & : v (\phi) = 1 \end{cases}$
... which is how we usually construct a "cases" statement -- the "if" is implicit in the structure? (IMO the "if" just adds clutter.)

Meanwhile, the general structure of the page has been given the usual makeover. --prime mover (talk) 05:47, 24 March 2018 (EDT)

I'm happy to explain my considerations here:
a) is suboptimal because I prefer to let the parser handle the layout. Note how the space needs to be taken care of manually. In this choice we are relying on some spacing interaction between the \text and the math. Whereas "my" solution is unambiguous from a semantic perspective and thus more likely to be rendered correctly at all times.
b) I have considered to be less great because not every reader might be familiar with the formal meaning of the colon in such expressions. Especially in more complicated situations it is not as insightful as having the extra "if" there. As such it is not clutter to me, but instead adding extra clarity. It is additionally more in line with the use of "otherwise".
Also I have no problems with the appearance of the nested construct in the source code. In conclusion I see no need to change the approach. Instead I would argue to make it the standard, but I would understand if you'd be hesitant to that.
Finally, as to the \left\right paradigm your change has implemented, I have taken on a more lenient approach of late, because in single-symbol cases, it is adding clutter to the source code. I consciously consider the use at any moment and generally tend to including them. Just not everywhere anymore. I appreciate that we might have a difference of opinion here, but let's discuss that and find a way forward. — Lord_Farin (talk) 06:47, 27 March 2018 (EDT)
The left-right thing.
Compare and contrast: $f(x)$ with $f \left({x}\right)$ with $f({x})$ with $f \left(x\right)$.
This is on a par with your preference to let the parser handle the layout. Using left-right (the braces seem to have no direct effect), the spacing is subtly adjusted accordingly. I have noticed there are other subtle differences between using our "fussy" style to our simple one. In this case the parser makes a difference.
We also need to acknowledge that parsers evolve (MathJax has evolved several times during the course of our using it), and such subtle differences in presentation gradually appear. It is probable that the extra gap in the left-right version of the above is deliberate, and (in my opinion) welcome. (I may be alone in my preference for the bigger gap between the $f$ and the $(x)$ -- I know for certain that Barto does not like the extra gap -- but the difference unarguably exists.)
Hence my preference for the left-right -- it future-proofs us. --prime mover (talk) 07:33, 27 March 2018 (EDT)
I appreciate your considerations. There is a defensible case for keeping \left\right. I suggest that, to alleviate the concerns of me and others, we spend time to automate the whole effort. That is to say, we automate the process of adding \left\right to pages. I guess MediaWiki makes it possible to write bots that "clean up" after each edit by adding the delimiters using some clever regular expressions.
Would this be something that could alleviate your concerns while at the same time ensuring an easier editing experience? — Lord_Farin (talk) 12:05, 1 April 2018 (EDT)
I happened upon a contributor's user page recently which described how to set up hotkeys, including for our beloved \left\rights. I was deep in the middle of thinking about something else at the time and so postponed taking any action on it. I have now re-found it: User:HumblePi.
I'm conflicted on the idea of using a bot to convert (x) to \left({x}\right) etc, because it may convert more than we want. For a start, it would remove the "amnesty" that we currently have for equation labels, like:
$(1): \quad 1 = 2$
and so on -- but that's not necessarily a bad thing in itself. I can't immediately see any reason not to do it, although I would prefer us to start with a bot which would simply list all non-compliances which we could then scan to see if there are cases we specifically want to exclude from being given the left/right treatment.
It bears further thought. --prime mover (talk) 14:36, 1 April 2018 (EDT)

DefinitionCategory template

The {{DefinitionCategory}} template seems to be working differently from how it did (as you seem to have recognised) -- if there was no "disp" field, it used to take its default description string from the category name, but now it seems to take it from the "def" field. I initially intended it to take its default description from the category name. Is there a reason for the change, or might this have been an oversight? --prime mover (talk) 16:58, 14 May 2018 (EDT)

You are correct, thanks for noticing the pattern. I made a mistake; it has been addressed. — Lord_Farin (talk) 13:58, 16 May 2018 (EDT)

Tidying up

I'm doing a bit of tidying up, seeing which redlinks can be cleared. There's one on here to Template:Lw. I'm thinking to remove references to it so it does not continue to clutter. There's one such reference on this page. Care to remove the section pertaining to it? --prime mover (talk) 14:25, 12 January 2019 (EST)

Good riddance. — Lord_Farin (talk) 12:52, 13 January 2019 (EST)

Index Laws

I have added a master page to this. No I know it doesn't render neatly at the moment. We can address this once we have that merge exercise complete. (Not immediately about to take it on, I'm inching my way through chap $11$ of Warner at the moment, the index laws are 9 chapters away). I will get there in due course.

In the meantime, I reworked your "source of name" as you see. Although it seems like more work and less benefit to specifically *not* include the title in the onlyincludes, it makes the result more portable and allows for the page itself to appear as a clickable link in that header -- otherwise it is not directly accessible from the parent pages. Minor other rearrangements of sections according to what has evolved into house style -- "source of name" comes after "Also see" along with linguistic and historical notes.

Good to see you back. --prime mover (talk) 22:09, 15 March 2022 (UTC)

Also want to say welcome back! I have been continuing your work on functional analysis and measure theory. Caliburn (talk) 23:03, 15 March 2022 (UTC)
Thank you both. It is heartwarming to see how quick you both were to notice my presence and drop a message. And yes, I have noticed my editing is a bit rusty, and yes, please clean up after me. E.g. I noticed the issue with the transclusion and the heading but I didn't manage to produce a proper solution.
My activities will probably be limited due to, well, life, but I intend to be more present than I was the past years. — Lord_Farin (talk) 07:01, 16 March 2022 (UTC)

Example subpages

I know it looks immediately suboptimal, but the paradigm in which "Examples" subpages of definition pages are not in the Definition namespace is deliberate.

In many (in fact, most) instances, such examples are results to be proved, and hence require to be in the Results namespace.

My view is that it is good to be consistent in such cases, and furthermore, deciding whether such examples are "definitions" or "results" is a sufficiently grey area as to make the decision in which to put them problematical.

Maybe there is a case for a new "Examples" namespace, but at this stage it would be a lot of work for uncertain benefits, as there have been a lot of examples appearing on $\mathsf{Pr} \infty \mathsf{fWiki}$ in recent years.

I'd welcome your thoughts on the matter. --prime mover (talk) 19:13, 23 March 2022 (UTC)

I concur with the following:
  • Examples lie somewhat in between definitions and results (also see: every maths book)
  • It is more important to be consistent, even if the standard is somewhat arbitrary
  • It would not be productive to take on a big burden of work to change the current consensus
What is however confusing and problematic about some pages is that the page name is structured like a subpage, but it is not actually a subpage. In summary my current proposal would be to keep them in the results namespace, but potentially settle on the name "Examples of X" instead of "X/Examples".
How does the above sound to you? — Lord_Farin (talk) 07:07, 24 March 2022 (UTC)
A colossal amount of rework on the current examples.
The big question is: how "confusing and problematic" is it? For me it's no more than a minor annoyance that I barely notice it.
If we're going to change all instances of "X/Examples" to "Examples of X" this is going to be just as much work as changing them all to "Examples:X".
The big, I may even say big or even BIG advantage of an Examples namespace is that the ordering of the examples in the category listing alphabetises "Examples:X" and "Examples:Y" under X and Y and not under "E". Otherwise everything in an Examples category would then be under "E", which would be beyond ugly.
My view is that if the existing paradigm is truly unacceptable, then we do a complete and thorough job, and move everything forward to an "Examples" namespace (for which I believe we would have to bring Joe on board) -- which is a hefty package of work, but (as we have all the examples in one place already) manageable and quantifiable. It will also give us the opportunity of reviewing the examples we already have with a view to ensuring that all existing examples are truly presentationally and structurally consistent.
We may even be able to templatise some of the structural commonalities, which will increase the streamlined nature of the website.
I confess that my mathematical abilities have atrophied recently (and in fact weren't particularly spectacular in the first place -- I was just good at following rules and applying already existing knowledge) and so rather than expanding and extending what we already have, I may be better placed for this maintenance work -- if we undertake it in the first place.
And something else I thought of: should we continue to distinguish between "definition examples" and "result examples"? Something else I've been conflicted about. --prime mover (talk) 08:24, 24 March 2022 (UTC)
Bringing to memory that I wrote "It would not be productive to take on a big burden of work to change the current consensus", I propose that we stick with the current standard until we have a level of argumentation and certainty that justifies the amount of work involved.
In the meantime, aside from the work on moving everything around, I think that a painless first step would be to templatise the page structure. An appropriate thing to do then would be to write up Help:Examples to codify the standard.
I would not distinguish between definition examples and result examples for the same reasons. Let us wait until we are sufficiently satisfied with a standard to move forward. The templates might then help us to automate more of the efforts. — Lord_Farin (talk) 10:03, 24 March 2022 (UTC)

Create a template for terminology etc. that was coined by $\mathsf{Pr} \infty \mathsf{fWiki}$

I offer you {{Neologism}}. --prime mover (talk) 09:16, 24 March 2022 (UTC)

Nice job! I've added some suggestions. Instinctively I would feel the need to add more discussion/elaboration/fluff for each of these instances, but let's have this evolve naturally and incrementally. — Lord_Farin (talk) 10:03, 24 March 2022 (UTC)
I concur with both of your suggestions, in particular that of implementing a category. Feel free to implement both or either. Iif it's still undone by the time I get to it, then I may work on it, but at the moment I'm in the wrong headspace. --prime mover (talk) 10:15, 24 March 2022 (UTC)

Recent refactoring

I expect you may notice that I have refactored the material around Properties of Ordered Group and Properties of Relation Compatible with Group Operation.

In particular:

I have renamed everything so as to give it a descriptive name rather than a number
I have rationalised the categories these results are grouped into
I have internally restructured to use the more conventional {{eqn}} template rather than {{axiom}} for presentational consistency and (IMO) improvement
I have removed the somewhat artificial and arbitrary labels (stuff like $\operatorname {OG}' 4$ and the like) because:
a) they didn't seem to bring anything useful to the table
b) none of it was corroborated by anything in the literature
c) arbitrary as it seemed, it introduced a precedent (identifying results by letter/number codes) which would lead to an unwelcomely hefty and headache-inducing maintenance burden.

With regard to that last point, I know you and DFeuer spent quite some time and effort hammering these out, but it seems to me that it is probably better to leave name / number / label systems to axioms only.

The results above are no more special or significant than any others. All we need to do is reference them as appropriate. Grouping them under umbrella pages, as they are now, is perfectly adequate and precedented. And all of them follow trivially from the basic definition of relation compatibility.

I gather that DFeuer may have been trying to make a point about the prevalence of "trivial" results that take no more than $2$ or $3$ lines each, by following the practice through to an absurd conclusion. I may be wrong in this inference, but then again, such slavish attention to detail over a bunch of such simple results seems somewhat uncharacteristic of his approach.

Still. What is done is now done. In the course of this, a few annoying maintenance tags have been cleared. --prime mover (talk) 08:04, 18 April 2022 (UTC)

Inspecting the result, I absolutely agree that the current presentation is crisp and clear; nice job. Additionally I completely agree that {{axiom}} was misused in these cases. And finally I agree that we should stick to naming results explicitly instead of resorting to numbered systems.
As to what lead to this setup in the first place, I don't recall and given the improvement that has been made it is also no longer relevant. In conclusion, great job all around! — Lord_Farin (talk) 08:56, 18 April 2022 (UTC)

Ordinals and all that

As you have seen, I am making my mark on the work to define ordinals. Revisiting S&F, I am filling in gaps and (where I can) merging pages where there is parallel development.

In answer to your earlier question, yes I am replacing the terminology Minimal Infinite Successor Set with Minimally Inductive Set. The former was pulled out of my, er, the air when I was trying to piece together some terminology to make things consistent. Devlin's approach also didn't come in from it from the direction of abstract notions, it came straight in to the definition of the ordinal from nothing, so to speak, and as such is difficult to grasp the abstract concept behind it. So I could have called it "smallest finite ordinal" but then the wider and more general picture as introduced by S&F would have been compromised.

So, Minimally Inductive Set seems to be the "best" term for this, as it is then consistent with "inductive set", "minimally inductive class", and even "inductive semigroup" which is so closely related to the concept of "inductive set" you wouldn't trust them to have children together. :-) --prime mover (talk) 11:59, 2 May 2022 (UTC)

I am in agreement. Nice job bringing things together! (Too bad we still have the Takeuti mess in between. I am often tempted to delete the material outright. Oh well.) — Lord_Farin (talk) 12:49, 2 May 2022 (UTC)
We may one day be in a position to. It's not all unsalvageable, though. At the very least I'm able to merge some of the stuff that's mergeable (some already done) and second-proof other parallel stuff.
As I said somewhere else, I expect it probably is internally consistent, but unfortunately a) we don't have the exposition going back to the first page of that work, and b) we don't have a link thread (which is more regrettable).
I have that Takeuti work "Proof Theory" but it's a heavily technical exposition of Gentzen theory and so far I've been too pusillanimous to crack it open. I doubt he would lend his name to a work which is itself badly flawed.
As for the Smullyan and Fitting work, it's the only work on the subject I've seen which is both thoroughly comprehensible and accessible, and probably benefits through being relatively recent -- the authors have clearly distilled the essence of previous works and made considerable further abstractions which allow all the fluff to be blown away.
Please continue casting a critical eye over stuff; I take appearances of {{Mistake}} to heart and try to address them when I see them. --prime mover (talk) 16:26, 2 May 2022 (UTC)

Formal systems and all that

Many thanks for attacking the matter of formal systems. In its way, it seems to me far more challenging than class-set theory, and far more important from the point of view of establishing the foundations of mathematics. --prime mover (talk) 05:16, 12 May 2022 (UTC)

Having spent a lot of time on it during my studies, I am quite attuned to the formalities associated with that. The biggest risk I see is to become unintelligible for those who haven't seen the concepts before. This is always a concern on $\mathsf{Pr} \infty \mathsf{fWiki}$, however I would particularly appreciate your pair of eyes reading along and making sure that I don't mess things up and it becomes just the next idiosyncratic mess. — Lord_Farin (talk) 05:22, 12 May 2022 (UTC)
I will trundle through the few books I have which cover axiomatics and see how well it all hangs together. In due course. --prime mover (talk) 05:51, 12 May 2022 (UTC)

Class-Set Theory -- some rationalisation

I have reworked the basic basic fundamentals of Class-Set Theory based on a microscopically close reading of Smullyan and Fitting, from which I worked out that I had unwittingly glossed some of the finer detail. I have also fixed some horrible mistakes, particularly around the declaration of Axiom of Pairing. The latter is now considerably cleaner and consistent than it was.

To that end, I believe I have worked out the following:

  • The Axiom of Extension (in fact better named as "extensionality" despite the fact that the longer name is uglier) and Axiom of Specification are fundamental, and all workings of class-set theory will have these right at the bottom. Hence (via Specification) everything rests on a bedrock of logic.
  • The Axioms of Unions, Empty Set, Pairing and Powers are the next most basic stuff, being the basis of the Basic Universe. The latter also requires Transitivity and Swelledness as axioms, but with this in place the other four axioms are completely equivalent to the set-theoretical versions: that is, what Set Theory declares as existing as sets, Class Theory constructs from the Axiom of Specification, proves is unique, and declares to be Sets. These axioms are common to ZF Set Theory and NBG Class Theory -- although many treatments of ZF deduce Axiom of Empty Sets from other axioms. (At this stage I am not too concerned about that.)
  • The Axiom of Infinity is next on my list to be scrutinised at this level. This is introduced by S&F in parallel with Peano's Axioms and the Natural Numbers, which again may get yet another workover. Still not entirely sure I'm happy about all this.

Note that I am not completely happy with the treatment of Axiom of Empty Set. There are two set-theoretical versions, differing only in the quibble over the specification. I am wondering whether to sideline these (bearing in mind it's not truly axiomatic) and revert to S&F's treatment where they do not specify a set-theoretical "there exists an empty set" but instead "the universal class has at least one element" and equivalence that with "the empty class is a set", based on Axiom of Transitivity and Axiom of Swelledness.

From all the above I am trying to piece together a "minimal" axiomatic framework in which we need to work. I raise the hypothesis that S&F's "Basic Universe" along with Extension and Specification is that minimal framework. All I need to do now is demonstrate that all other frameworks are either equivalent to or subsume this. (I thought I could get away with asking just that question on MathStackExchange but after a sarcastic comment "Not clever enough to understand the Wikipedia page on the subject?" I deleted it.)

I've tried the Wikipedia page but find it impenetrable. May have another go.

Anyway, feel free to take a good look at what I've done, and also to comment on the set theory / class theory distinction between the definitions and theorems. I think we're still far from perfect, but we're a lot closer to where we want to be. --prime mover (talk) 21:32, 12 May 2022 (UTC)

Thank you for your work clarifying this area. I'll read through it the coming time to see if things make sense. I'll gather the questions/remarks here to keep a good overview of them, rather than scattering them around the various pages. If we cannot address them right away, we might still put the maintenance templates on there. That being said:
  1. Is S&F defining the formal language (i.e. Definition:Language of Predicate Logic c.q. Definition:Language of Set Theory) explicitly? If so that would be valuable to include (currently the page Definition:Class (Class Theory)/Zermelo-Fraenkel is sourceless).
    1. They don't cover logic at all. The closest they come is to define a propositional function.
    2. Can't comment on Definition:Class (Class Theory)/Zermelo-Fraenkel as it's not one of mine and I don't know where it came from. Checking up on it, it seems to be one of yours. :-)
  2. The category Category:Axioms/Von Neumann-Bernays-Gödel Axioms is applied to axioms which also apply to ZF Class Theory. How to deal with this? I think every axiomatisation (ZF, ZF Class, NBG) should have its own page as we would otherwise get into conflicts. This might mean that we would actually need to disambiguate Class (ZF) and Class (NBG) everywhere. Not looking forward to that, so happy to hear your thoughts.
    1. The plan would be that you'd get a master page Axiom:Von Neumann-Bernays-Gödel Axioms which would transclude each of the axioms needed, and present them as a list according to the source work we get them from. Same as we do with ZF / ZFC axioms. Bear in mind there is a nasty complication here in that different sources include different axioms in them. Hence multiple formulation pages needed. With our modular technique of building pages by the transclusion technique, which I am of course very personally proud of, it should then be straightforward to build up these pages by transcluding exactly which axioms are needed. The underlying equivalence routines tie the schemata together, because at base, when you analyse all these different systems, you find that to a greater or lesser extent, that all roads lead to Rome.
    2. Yes I know, your question was about categories. Simples: we include in the category those axioms which contribute towards that axiom schema. If they belong in more than one schema, put them in all that apply.
    3. Oh, and while I think about it, I believe we might want to discontinue the use of, deprecate, and then finally delete {{NotZFC}}, as I don't believe it really has any concrete purpose.
  3. I love the comparison subpages such as Axiom:Axiom of Powers/Set Theoretical and Class Theoretical. They are greatly enlightening. — Lord_Farin (talk) 08:31, 13 May 2022 (UTC)
    1. Taking a step back from that specific point: I wonder whether there is a case for adding a new page "subtype": that is, for discussion / exposition, so we have a standard style of transclusion. Then we could be slightly more relaxed about the lame "Comment" or "Remark" sections, and merely turn them into "Discussion" or "Exposition" subpages. To paraphrase our good friend Caliban pointed out: is this website a teaching aid (designed specifically to provide useful stuff for people to learn from) or just a complicated exercise in mathematical structure? --prime mover (talk) 09:54, 13 May 2022 (UTC)
More questions will be added here as I progress. — Lord_Farin (talk) 07:56, 13 May 2022 (UTC)
Ad 2.3: see Main talk for my admittedly more far-reaching proposal. Further discussion of that to be held there. — Lord_Farin (talk) 19:04, 13 May 2022 (UTC)

Singleton Image of Element under Many-to-One Relation

Seriously, I'm having difficulty working out exactly what we need to do with this: Definition:Image (Relation Theory)/Relation/Element/Singleton

It seems that a great big meal is being made of the fact that if a relation is many-to-one, then the image set of a single element of its domain is at most a singleton.

This just seems to me as though it ought to be a result (trivial though it be) rather than a definition. What are your thoughts?

I took a peek at T/Z which is cited as a source, and all that is written there is the definition of their notation $\RR ` s$, which they only consider defined if indeed there is a unique $t$ such that $s \RR t$.
Incidentally they refer to a many-to-one relation as "single valued", which I consider quite elegant. Personally I also find "partial mapping" to be a very useful description, depending on the context.
Coming back to the issue at hand, there is no need to keep this page as a subpage of Image. If anything it should be under "value under relation" or whatever the thing is called.

As you see, incidentally, I have moved all these big definition pages for Domain, Range, Codomain and Image from being (Set Theory) to (Relation Theory) as I am preparing to jump out into space with class theory versions of these concepts. I'm quite pleased that our "permanent redirect" technique has paid off big time, as the task to change the links was minimal (except for where they pointed directly to the page, and those have all now been fixed).

Happy to see that it pays off. It also makes navigating the site (much) easier. Good luck on the next chapter of the Class journey!

Other news: still waiting to see when / if someone on MathStackExchange is feeling philanthropic enough to share some thoughts on the proof of Addition in Minimally Inductive Set is Unique from the principle of recursive definition -- been looking at that for ages and I can't seem to get my head round how this is done. It occurred to me that we still do not have a rigorous demonstration that this addition function is valid (although we have done this for the naturally ordered semigroup, this is covered in Warner.

What about Principle of Recursive Definition for Minimally Inductive Set? Of course, this moves the problem to providing a proper proof of that, but hey, we got ahead by one step... — Lord_Farin (talk) 06:57, 16 May 2022 (UTC)