User talk:Lord Farin

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: $\text {Oct 10, 2010}$ – $\text {Dec 15, 2012}$ Archive 2: $\text {Dec 16, 2012}$ – $\text {Jan 1, 2014}$ Archive 3: $\text {Jan 2, 2014}$ – $\text {May 1, 2022}$

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)

Questions about $\mathsf{Pr} \infty \mathsf{fWiki}$

Hello, nice to see you are still working here after ten years.

I have a some questions. First, sometimes I like to write mathematics offline. Does there exist a LaTeX package defining the specific $\mathsf{Pr} \infty \mathsf{fWiki}$ commands that I can download? --Anghel (talk) 22:12, 7 September 2022 (UTC)

Hi, I am afraid not. However you might be able to craft it yourself using the source from here: MediaWiki:MathJax.js. It is probably some work transforming this to TeX but should be doable with a modest time investment. If you put it on your watchlist (the star symbol) you will be notified of any changes to this page, i.e. new commands being added. — Lord_Farin (talk) 09:30, 8 September 2022 (UTC)

Thanks for the quick answer. I'll see if I can find a way to parse the TeX commands.

Since you know most about the technical operations of the wiki, I figured you were the right person to ask about some possible extensions to the MediaWiki:

• Cirrus Search Extension, which Barto asked about some five years ago. It should improve searching the wiki (so you don't have to match the exact spelling and capitalization of the item you are trying to find with the search bar).
• Hit Counters Extension, which puts hit counters on pages. I remember when I used $\mathsf{Pr} \infty \mathsf{fWiki}$ 10 years ago, we had these counters, and I would frequently check the most popular pages, and boosting my ego by checking how many hits my work got.

Of course, I have no clue how long time it would take to install any of these extension, or if they would stress the servers too much, and so on.

Is it worth looking into? --Anghel (talk) 22:11, 8 September 2022 (UTC)

Sorry for not getting back to you sooner. I'll ask our site admin to have a look if these extensions would run properly. I remember that we disabled the hit counters because of the performance hit (badum-tss). — Lord_Farin (talk) 05:59, 15 September 2022 (UTC)

All links to the Mizar project from the Mizar articles are broken. They have overhauled the mizar.org site, and I believe current version of the Mizar files are now stored at [1]. Maybe it is possible to update the template that links these files. --Anghel (talk) 15:59, 1 October 2022 (UTC)

Fixed -- just needed to take the www off the front. --prime mover (talk) 07:56, 2 October 2022 (UTC)