User talk:TheoLaLeo

Welcome to ProofWiki! Since you're new, you may want to check out the general help page. It's the best first stop to see how things are done (next to reading proofs, of course!). Please feel free to contribute to whichever area of mathematics interests you, either by adding new proofs, or fixing up existing ones. If you have any questions please feel free to contact one of the administrators, or post your question on the questions page.

Here are some useful pages to help get you started:

• Community Portal - To see what needs to be done, and keep up to date with the community.
• Recent Changes - To keep up with what's new, and what's being added.
• Check out our house style if you are keen on contributing.
• Main Page talk - This is where most of the main discussions regarding the direction of the site take place. If you have any ideas, please share them!

Cheers! prime mover (talk) 22:37, 21 November 2021 (UTC)

joke

Apologies, but I have had to delete one of your logicians jokes because it is already there, under "Beerlogical".

No attempt has been made to gather these jokes into categories, which IMO is how it should be (it enhances the reader experience to get jokes in an unpredictable and unstructured order). --prime mover (talk) 06:46, 22 November 2021 (UTC)

No problem, I considered reading through them first to see if I'd be putting down repeats but was too lazy. --TheoLaLeo (talk) 06:48, 22 November 2021 (UTC)

I suggest you may want to do so, you've just entered another one we've already got. --prime mover (talk) 06:58, 22 November 2021 (UTC)

Ah just saw that, I'll read through --TheoLaLeo (talk) 07:00, 22 November 2021 (UTC)

on rolling back

a) If you have a new proof, then please add it as a new proof.

b) Please try and craft your edits so as to retain our house style both of visual presentation and of coding style.

c) If you can fix your editing --prime mover (talk) 20:22, 22 November 2021 (UTC)approach so as not to remove blank lines that would be top notch.

Apologies, I will try to read through the house style pages before doing more edits, it's a lot of info to take in. --TheoLaLeo (talk) 20:26, 22 November 2021 (UTC)

A good way to get to grips with our style is to study existing pages and follow. Most of them are in house style, although there may still be a few wildly non-compliant pages created by undisciplined mavericks which we are still in the process of finding and cleaning up. --prime mover (talk) 06:49, 23 November 2021 (UTC)

Sources

I suggest you take some time to contemplate the structure of the "Sources" section.

a) If you copy the entire content from one page to another, please take the time to remove the content of the "Sources" section from the new page. Bet you bombs to biscuits that the new page is *not* in the source (at least, not in the specific location pinned down by the detail) where the original page came from.

b) Even if it is, please note the nature of the "prev" and "next" links. It is intended that the source work is arranged in the form of a total ordering (in fact, a well-ordering). Copying the contents of the "Sources" section, as I'm sure you will perceive, compromises this construction.

If and only if you actually have direct unfettered access to a copy of the specific edition of the source work in question, then you may feel inspired to contribute towards the maintenance of those source citations in that section. Otherwise bring it to the attention of someone who actually does have such a source work, and you do that by adding an invocation of {{SourceReview}} strictly above the sources whose content needs to be reviewed.

I apologise for what appears to be unnecessary fussiness and attention to trivial details. When this project was started, it was assumed was that mathematicians are self-starting autodidacts who pick this stuff up directly. Many contributors are able to do this, and produce presentation-perfect pages right from the get-go; others have less success (and still others scorn the fact that we have a standard style in the first place and insist on doing it their own way, which causes friction, tension and all sorts of other unwelcome concepts from applied mathematics).

The philosophy is: any fool can post mathematics up on the web (the vast number of such websites is proof of that). It takes time and effort and considerable hard work to present something that is consistent and rigorously structured (the fact that a vast number of that vast number of websites look terrible is proof of that). --prime mover (talk) 06:49, 23 November 2021 (UTC)

I will try to look more at the house style guide and familiarize myself with the technical aspects of editing, sorry if cleaning up after me has been a nuisance. Hopefully I'll learn the conventions here with time. --TheoLaLeo (talk) 06:57, 23 November 2021 (UTC)

Is there a way to see this ordering of citations for a book other than continually clicking previous and next in citations? Clicking on "what links here" from a book page gives the pages citing the book, but they aren't in order.--TheoLaLeo (talk) 20:09, 23 November 2021 (UTC)

No there isn't. Why would you need it?

Our recommendation for contributing to this site is from extant printed sources, in the way that you can see it already being done. We are uncomfortable about people pasting up stuff which comes completely from their own heads. We have had trouble before from people who are much cleverer than the stupid dusty old-fashioned boring old printed stuff, who know that what they are doing is far, far better than the rubbish that already exists, and so set themselves up on a mission to change every aspect of the site into their own dream. Unfortunately we have far too often had to reverse out large amounts of this because it is basically wrong. --prime mover (talk) 22:21, 23 November 2021 (UTC)

When citing sources I want to be able to insert them in the correct spot in the ordering, it's hard to do that as is. --TheoLaLeo (talk) 22:24, 23 November 2021 (UTC)

Difficult how???? every single citation is (or ought to be) identified with chapter and section. --prime mover (talk) 22:26, 23 November 2021 (UTC)

The citations are but they don't display on the what links here page. So if I want to cite something, I have to click around on the book's what links here page until I find something close to the right section, then click next or previous until I hit the exact right spot in the ordering. It would be easier if the what links here page was in order of the book's table of contents, or if some such ordering was displayable. --TheoLaLeo (talk) 22:34, 23 November 2021 (UTC)

I tried to attack this problem manually by linking chapters in the book to the very first item from the given chapter (like here). Maybe you could do this for your own source? I would also like to have the option to see all the pages for a given book ordered according to how they are linked to each other by prev and next, but this is tricky due to errors, loops and missing pages. Maybe a script could be written such that it receive the first and the last page as inputs (where the ordering is fine) to generate an ordered list of links to pages, and post it on the book's page. But this is beyond me.--Julius (talk) 23:01, 23 November 2021 (UTC)

Next question: what are you actually trying to do?

The entries in the Sources section are effectively complete for a given source work. The editor of the page in question has made an attempt to work through the entirety of a given work. Unless something in a particular work you hold in your hand is actually missing, and you want to add it, you should not need to click around to look for it, as you should already be on the page before and the page after the missing place that you want to add something in.

In what other circumstances do you want to search through the citations? They are there to provide the user an experience parallel to reading the actual book.

What other reason do you have to be mucking about with the (existing) ordering of a source's citations? --prime mover (talk) 23:04, 23 November 2021 (UTC)

I was trying to cite something from Suppes Axiomatic Set Theory.--TheoLaLeo (talk) 23:07, 23 November 2021 (UTC)

I'm confused -- why do you want to cite a specific result from a specific work? Can't you just link to the result from the page you want?

Note that there's a note on the page of the book that says "redo from start" which means a poor job was done on the citations of this work in the first place. The person who did this hasn't bothered to, oh never mind --prime mover (talk) 23:14, 23 November 2021 (UTC)

jech set theory

Good job taking on the Jech set theory work.

Suggestions for going forward:

a) It is generally a better idea to give a result page its own title, rather than as a corollary of an existing page. There are reasons for this, including:

1. You can more easily find the page you want by reading the title, as the content is more likely to match the title if it is custom.

2. Such a result may have a proof which takes a different approach, and hence may be a "corollary" of a completely different result.

b) If you need a page to be renamed, it is suboptimal to create a new page, copy everything across, and then delete the old page. This is because if you do it that way you lose all the page editing history, which is a bad thing. I realise you don't have access to the "Move" tool, because it requires "trusted user" status, which as at this moment you don't have. So the requested approach is that you use the {{Rename}} template to flag up that a given page needs to be renamed, and (assuming the request is a good one) one of the admins will do it. --prime mover (talk) 08:25, 24 November 2021 (UTC)

All noted. I'm currently working through Jech so I'll try to systematically add that source to pages. --TheoLaLeo (talk) 08:31, 24 November 2021 (UTC)

Adding material to established pages

You have been around long enough to know how this place works. If not, then spend some time browsing.

A definition page contains a definition, and nothing but a definition. We do not include results that are derived from that definition.

In particular, we do not add results to such pages, especially when such materials already exist.

Hence I am going to reverse out the changes you made to Definition:Restricted Existential Quantifier and Definition:Restricted Universal Quantifier and request that you may want to refer to existing pages which cover the material you are adding to them. --prime mover (talk) 19:16, 26 November 2021 (UTC)

Fair enough about excluding results from definition pages. I see plenty of pages about negated quantifiers but none about negated restricted quantifiers. I may be missing something, but I don't see these particular results anywhere. --TheoLaLeo (talk) 23:36, 26 November 2021 (UTC)

Okay I see what you mean, I get what you see is missing, but I'm at a loss to understand why you really *need* the complication of using these "restricted quantifiers" in the first place. Seems like a messy and overcomplicated way of proving Smullyan's Drinking Principle in the first place. Define $P$ as being a universe. --prime mover (talk) 06:03, 27 November 2021 (UTC)

Oh and while I'm about it, from your latest edit of Smullyan's Drinking Principle you can see directly why we do not allow "bare" parentheses in the $\mathsf{Pr} \infty \mathsf{fWiki}$ house style. Please use whichever of the various custom $\LaTeX$ constructs is relevant to your need of the time. --prime mover (talk) 06:13, 27 November 2021 (UTC)

If you want I can change Smullyan's Drinking Principle to a proof without the restricted quantifiers, googling around it seems that both formulations are used on other sites. Regardless, should I add pages with the negated restricted quantifier proofs? --TheoLaLeo (talk) 06:41, 27 November 2021 (UTC)

The concept of the "restricted quantifiers" appears to me to be more a concept used in the development of the foundations of set theory, when one is establishing the properties of ZF, for example.

Using them to prove a quirky veridical paradox in logic seems to be using the "wrong" technique.

Maybe I'm being naive, but it feels inelegant and top-heavy.

Is there a way this theorem can be proved without using such heavy artillery?

I'm happy for there to exist pages to prove the negations, as long as they are on their own theorem pages, not bolted onto the existing definition pages. --prime mover (talk) 07:55, 27 November 2021 (UTC)

Yes I'll take the restricted quantifiers out of the theorem and add the negation proofs as their own pages. --TheoLaLeo (talk) 08:12, 27 November 2021 (UTC)

Aah! Hits the spot. Allow me to refactor. --prime mover (talk) 09:23, 27 November 2021 (UTC)

There. Perfect. --prime mover (talk) 09:46, 27 November 2021 (UTC)

Nice I like what you did there, that page is really thorough and accessible at multiple levels now --TheoLaLeo (talk) 17:11, 27 November 2021 (UTC)

the moral of the story is: don't remove stuff just because you know that the material you provide is eleventy-billion times better than what it replaces. If you have a different approach, place it alongside. --prime mover (talk) 22:08, 27 November 2021 (UTC)

fair enough --TheoLaLeo (talk) 22:14, 27 November 2021 (UTC)

using "permanent redirects"

You will have noticed that there are many definitions which are implemented in subpages of parent pages, and as such have titles implemented as page/subpage etc.

It is the intention that all such subpages have redirects which do not have slashes in them whose name encapsulates the fullness of the intent of the page title.

It is highly-recommended-to-mandatory that all such "permanent redirects" be used in preference to the full ugly end-page title.

This makes refactoring easier. --prime mover (talk) 07:49, 28 November 2021 (UTC)

Do you just want me to link to redirects instead of the ugly titles when citing theorems/definitions etc, or should I also make redirects for subpages? --TheoLaLeo (talk) 16:09, 28 November 2021 (UTC)

yes --prime mover (talk) 18:47, 28 November 2021 (UTC)

be interested to know what subpages you think you're going to make. Usually applies to definitions, thinking behind this is obvs --prime mover (talk) 18:48, 28 November 2021 (UTC)

So far I've mostly been picking low hanging fruit, adding simple proofs or making proofs in close proximity to axioms more rigorous, and I've also taken a random interest in paradoxes. But I've been wanting to beef up the class theory content by going through a book like Jech, which would be a more long term project. Definition:Von Neumann-Bernays-Gödel Set Theory is incomplete, and I don't think Axiom:Axiom of Limitation of Size should be taken as part of Definition:Gödel-Bernays Axioms. In the context of the other axioms, it's equivalent to the combo of replacement, union, and global choice, which is a stronger version of the ZFC axiom of choice. So taking Axiom:Axiom of Limitation of Size as an axiom means that to do choice free proofs you either can't use replacement or union, or you have to add them back as redundant axioms. It seems like a better idea to just prove Axiom:Axiom of Limitation of Size as a theorem from the other three and maybe make a page about the equivalent formulations of the theory. Also, I've been shopping around for NBG formulations and have not found any textbooks that use it as an axiom, they all use the other three.

I have Bernays' Axiomatic Set Theory on my shelf but I find it difficult to penetrate. One day, when I know the subject better.

His notation is horrendously ugly, tends to be like that for older logic books --TheoLaLeo (talk) 21:09, 28 November 2021 (UTC)

There are two other problems I've run into. The first is an annoyance inherent to class theory, that sets and classes have to be dealt with separately. One solution is to have multiple sorts and treat the domain as containing fundamentally different objects, but that's pretty tedious and non mainstream. Another is to take the domain as all classes and introduce a definition like "$x$ is a set iff $\exists y : x \in y$" and "$x$ is a proper class iff it isn't a set". This makes axioms and theorems pretty ugly to state rigorously, as you have to start adding in random intrusive predicates. A third way I've seen is to denote classes with uppercase variables and sets with lowercase variables. It's a nice convention but I don't really understand why some people use it as the formal way to distinguish between classes and sets, since it just seems like if you tried making it more explicit and rigorous you'd end up with one of the first two solutions. Also I kind of doubt that it could be guaranteed to be consistently followed on a site like this that takes public edits. One idea I kind of like is to take as a constant the universe $V$ defined to be the superset of all classes, so that saying something like "for all sets $x$ ..." can be stated "$\forall x \in V : ...$", which seems both more natural than "$\forall x : set(x) : ...$" and more rigorous than stating in natural language that "the following statement applies only to sets". But the only place I've seen this done is in the smullyan book (I don't have access to the 2010 edition btw), and firstly it isn't completely explicit in its definition and use of the constant $V$ from what I've skimmed, and secondly it's a very non standard approach that I haven't seen anywhere else, despite it seeming elegant. A kind of hacky workaround could be to just define the predicate $set(x)$ to be the syntactic notation $x \in V$, then prove that the elements of the defined class $V$ have all the properties of the sets $x$, justifying the notation. But this is kind of hacky and misleading and also isn't really done anywhere that I've seen.

I get that annoyance, but see what I started doing with Smullyan and Fitting. I got part way through that exercise before getting sidetracked by something else and not getting back to it. Basically we have two instances: the set theory version of the axiom and the class theory version.

S&F's approach is the most accessible one I have found, as they are between them *very* good at explaining and structuring. IIRC they approach the problem by the $\forall x \in V$, which they can get away with because $V$ has been defined with the reader's confort in mind.

The second issue is that since Class Comprehension Schema does not allow the properties to quantify proper classes, it can be replaced with a list of finite axioms that can be proven to imply Class Comprehension Schema for any predicate that doesn't quantify over proper classes, justifying the schema. The issue is that it seems very inelegant and annoying to have to set up all that apparatus just to use Axiom:Class Comprehension Schema, [[1]] sketches out how you'd do it and its pretty ugly. It's an interesting piece of math that can be added as a separate page but it seems better to just use the schema for the actual axiomatization, since it's easier to use, equivalent, would reduce the axiom size by a lot, and wouldn't require setting up the class existence theorem just to be able to use NBG rigorously. Thing is some of the books that nicely solve the issue of dealing with sets and classes separately use this approach. For instance, Mendelson's Introduction to Mathematical Logic has an otherwise nice version of NBG, but does this whole finite axiomatization thing.

Whatever is done in the source works.

I haven't found one unified text whose formalization solve both these issues well. Jech gives a formalization but doesn't actually seem to rigorously use it, he does the whole "we're gonna talk about classes but let's pretend we're using ZFC" shtick and gives a version of NBG only in passing, and anyways his version has some of the issues above. So all in all I'm not really sure how to proceed. I think I kind of know what my ideal formalization would look like, but I haven't found a text with such a formalization, and I assume you don't want me frankensteining an axiom system for this site. How do you think I should approach this? --TheoLaLeo (talk) 20:09, 28 November 2021 (UTC)

Like what I do, and that is, follow an exposition as rigorously as possible, adding alternative presentations by means of parallel definitions and equivalence proofs, and documenting everything that is out there. In such a way the "definitive" approach emerges from analysing where these match -- and where they do not match, then we have the option of "also defined as" and we can then do a formal comparison of the various approaches. But first let's get the stuff out there.

I beseech you to conform rigorously to the style of page structuring that already exists. If you need to backtrack and approach things from a different angle, pepper your pages with "rename" and "delete" templates, and just see how far you get.

If you have the patience to plough through the earlier edition of smullyan and fitting, entering what will probably be a whole number of duplicated citations, that would actually be really useful (See how this is done for the 2 editions of the Penguin Dictionary of Mathematics (amusing though it is, the name is not a joke) and see that mostly they are parallel but on the places where they diverge, so do the citation chains. It would be expected that there are actually few differences between the editions, so the work needed is the minimal (though tedious) task of just editing each page and placing the citation there. A contents list for the page specifying that first edition would of course be expected.

Yes, all this is boring and tedious and can be mind-sapping, but the end result is a good-looking and well-structured site (or at least, better-looking and better-structured, it has a long way to go before it can be regarded as "good").

I happen also to have that first edition of the Kelley work which expounds the Morse-Kelley approach, and one day I will take the time to present it on $\mathsf{Pr} \infty \mathsf{fWiki}$, but today is not that day, I'm kicking back and tackling some of the outstanding refactoring tasks. --prime mover (talk) 20:46, 28 November 2021 (UTC)

The original MK is in a topology appendix or something right? I haven't looked at Morse Kelley much, it's strictly stronger than ZFC and NBG whereas the theorems NBG proves about sets are the same as ZFC, so I don't think its as popular.

Yeah I gather it's discredited as obsolete, having been superseded by the stuff which works better. As such, it's still worth documenting it so that when people come to look for it to see what it's all about, they can get the full story. We try to be so inclusive on $\mathsf{Pr} \infty \mathsf{fWiki}$ that we dont' shy away from the historical material, despite the fact that it is no longer in fashion (*coughEuclidBook10cough*). At the very least, we can make pretty pages which have some intrinsic interest.

I'm not sure it's been discredited exactly but for some reason no one uses it, it's not thought to be inconsistent or anything it's just stronger than need be. A more modern book that seems to use MK is [Book of Set Theory by Charles Pinter], I haven't looked at it closely but the way it formulated its comprehension axiom was as MK from what I saw --TheoLaLeo (talk) 21:42, 28 November 2021 (UTC)

I may just use the Jech NBG bc I'm reading that book anyways, I'll just have to make his implicit sethood predicate explicit. It will be the same exposition, he's just a bit lazy with the rigor, I think bc he doesn't officially use NBG in his book despite him talking about classes all the time. --TheoLaLeo (talk) 21:01, 28 November 2021 (UTC)

I also at some point want to beef up the Modal Logic stuff, there's almost nothing. I don't know the subject super well but know enough that I could probably add some basic axiom systems and theorems and stuff. Issue is I'd be structuring it from scratch which I don't want to start doing as of yet --TheoLaLeo (talk) 21:04, 28 November 2021 (UTC)

When you're ready, fill your boots. I myself have been standing shivering on the brink of studying modal logic for decades.

Doing derivations in propositional modal logic is fairly easy, and the semantics of it are quite beautiful and elegant. Apparently it's the first order stuff that becomes a nightmare --TheoLaLeo (talk) 21:28, 28 November 2021 (UTC)

examples

When setting up examples, I try to limit my contributions to those I see in the sources from which I am working.

It's tedious to set up all the supporting architecture: the category, the transclusions, the links, the proofs, the heading and so on and so forth.

Making up your own examples is just asking for hard work, and I for one am reluctant do it, as it's time I'm never going to see again. --prime mover (talk) 07:22, 30 November 2021 (UTC)

Sorry about that. You mean source to textbooks? How thoroughly should i source/prove examples? something like the derivative example seems kind of trivial --TheoLaLeo (talk) 07:40, 30 November 2021 (UTC)

Yes, that is what I mean about sources. --prime mover (talk) 18:35, 30 November 2021 (UTC)

Rule 34

I did that "Rule 34" joke in my stand-up spot last night. The audience appreciated it. So thx for that. --prime mover (talk) 06:06, 23 December 2021 (UTC)

lol i found it deep on some reddit thread, the full exchange was something about proving the riemann hypothesis like this, then making porn out of the grad student getting fucked trying to solve it. I didn't see a good way to extend the joke on the page to include that but maybe it could be included in a stand up. --TheoLaLeo (talk) 07:34, 23 December 2021 (UTC)

Mine was: "Come here, big boy, give me that number that forms a counterexample to the Collatz conjecture." "$1$. $9$. $3$. $3$. $2$. $8$. $7$. $0$." each number being accompanied by a pantomime "thrust". Audience rocked. --prime mover (talk) 09:05, 23 December 2021 (UTC)

Lol that's good, also pretty cool that you do stand up comedy, it's something I admire from afar but don't have the guts to try.

I've found unironic 10 hour quantum mechanics lecture series and such on porn sites but there's no porn aspect to them. Would make for an interesting addition to the math tutor genre. --TheoLaLeo (talk) 17:53, 23 December 2021 (UTC)