From ProofWiki
Jump to navigation Jump to search

Strong Examples of Concepts

We frequently show that two concepts are equal.

How about showing that two concepts are not equal is that important?

If we were to have an example namespace from the beginning then I would say that:

As soon as the concept of Abelian Group is defined it must be proved that there are groups that are not Abelian otherwise we are unjustified in introducing the concept. In particular we would have to add an example to the examples of groups that we would call a strong example relative to Abelian Group

I need other opinions on this.

I refer you to the P = NP problem for an example where it is very relevant to introduce a new class of concepts (as a sub- or superclass of something bigger), even though we don't know whether or not it is a proper sub- or superclass. Other factors of importance are e.g. conceptual clarity or convenience. OTOH if two classes are not equal then it would be apt to have examples in every appropriate part of the resulting Venn diagram. — Lord_Farin (talk) 18:19, 25 February 2013 (UTC)

What is this in disguise?

A concept $C$ is example admitting if there are examples of it. Write $C \mathsf{ex:} e$ to denote that $e$ is an example of $C$ and $C \overline{\mathsf{ex:}} e$ to denote that $e$ is not an example of $C$.

If we consider "example admitting" as a concept in its own right and denote it by $E$ then we see that it applies to itself. That is, there exists a concept $C$ that is example admitting and so $C$ is an example of $E$ meaning that $E$ is an example of $E$.

Algebraic Structure and Metric Charts

I can't seem to find where but someone proposed a table for all the names of the algebraic structures (or should I say varieties :) ) given which axioms they have.

We could do the same for metrics (and possibly other structures) seeing as how I read today that nearly every possible weakening of those axioms has been studied.

Also speaking of tables you could possibly have a table showing which axioms are independent. Hmm... needs more thought.

I've been seeing these "compound pages" a lot lately with basic properties of a function listed or all the little variations that a word may have and I like them a lot indeed.

--Jshflynn (talk) 16:58, 8 February 2013 (UTC)

Cf. Definition talk:Semiring (Abstract Algebra). Idea needs development. Likely, fields need further development (in terms of both results and sources) to make the exercise worthwhile and less prone to errors. --Lord_Farin (talk) 18:10, 8 February 2013 (UTC)

Checkerboard Matrices

Square matrices partitioned as a checkerboard would be.

Let blacks be zero matrices.

Is this closed under matrix multiplication?

What is the set of left identities?

--Jshflynn (talk) 11:07, 6 February 2013 (UTC)

It looks like the set of square matrices is closed under matrix multiplication. So it's both a vector subspace and a ring. Assuming the standard convention that there is a white square at the lower right corner. --Anghel (talk) 23:11, 6 February 2013 (UTC)
Correct sir! :) --Jshflynn (talk) 16:58, 8 February 2013 (UTC)

What to do?

I am trying to understand just the essence of Double Orthocomplement is Closed Linear Span.

Okay, so I look at $\mathbb R^2$ which is a Hilbert space.

I look at the singleton $\{(1, 0)\}$.

I see the orthocomplement is the whole of the $y$ axis.

I see the orthocomplement of the $y$ axis unioned with $\{(1, 0)\}$ is the $x$ and the $y$ axis. (right?)

Now, what's the span of $\{(1, 0)\}$? Well that's just the $x$ axis isn't it?

What's the closure of the $x$ axis if I think of the usual topology on $\mathbb R^2$?

Surely it's not the $x$ axis unioned with the $y$ axis?

I've made a mistake.

Can anyone help me understand how?

$\{(1,0)\}$ is not in its own orthocomplement. --Lord_Farin (talk) 07:56, 31 January 2013 (UTC)
I get it now $(\{1,0\}^\perp)^\perp$ is the whole of the $x$ axis only which is the closed linear span of $\{(1,0)\}$. It seems I needed sleep :) Thanks LF. --Jshflynn (talk) 11:38, 31 January 2013 (UTC)


In time I'll learn to enjoy posting proofs.

For now I find it most relaxing adding sources and references :)

Onwards ProofWiki!

Quicker Typing Help

If you find yourself typing "Definition:" or some other key sequence repeatedly I have found the program AutoHotKeys to be very good:

AutoHotKeys website
There is also the link in "ProofWiki Specific" right below your edit pane. Saves learning random nonsense. --prime mover (talk) 07:15, 14 December 2012 (UTC)
The act of moving one's hand to the mouse, then the pointer to the link below, then click, then move hand back to keyboard is generally more expensive than simply typing the string yourself. Moreover, it presupposes that one does not use an external editor for PW (which I have started to do just a few days ago, the highlighting and improved search/replace functionality make it worthwhile). Thank you Jshflynn, I'll consider it later, when I get home. --Lord_Farin (talk) 12:04, 14 December 2012 (UTC)
Each to his/her own - but I have less patience with learning new stuff nowadays. Keeping up with tech is becoming a headache and more than. The links below the edit pane are just what I need. --prime mover (talk) 20:13, 14 December 2012 (UTC)


In graph theory I think that connectedness of vertices is an equivalence relation and the elements of the quotient set are the components of the graph. If that's true I don't know if it's worth proving. --Jshflynn (talk) 21:04, 21 December 2012 (UTC)

It seems to be correct (assuming that connectedness means "exists path" and the graph is undirected). Worth adding, I think. --Lord_Farin (talk) 21:58, 21 December 2012 (UTC)
Only in an undirected graph. Funny but I thought I'd already proved this. If not, then go for it because (though trivial) it's important. --prime mover (talk) 22:15, 21 December 2012 (UTC)
Aha - seems I have done. Graph Connectedness is Equivalence Relation. --prime mover (talk) 22:17, 21 December 2012 (UTC)
Excellent. Had I simply Ctrl F'd 'Equivalence' on the proof index page I would have found it and the corollary that alphabetically precedes it. If you would like a break from the topology section (which is coming along fantastically btw) here's another easy one: "The deletion of a cyclic edge in a complete graph is a complete graph" (the book I am reading at the moment though calls cycle's circuits and what you might think would be called a 'circuitous edge' is just a 'circuit edge', it is from 1981 however so there could have been a terminological shift since then). --Jshflynn (talk) 23:23, 21 December 2012 (UTC)


I will have to deposit this here for the future:

$\displaystyle\left\vert{ \prod_{j \in J} \left\vert{ \prod_{i \in J} \left\vert{ \left({\mathcal{P}\left({S / \mathcal{R}_f}\right)_j}\right)_i }\right\vert }\right\vert}\right\vert$

Emerging Trends

I am keeping a note here of emerging phenomena on ProofWiki for me to think about. I am aware it is not organised.

  • Theorems that are special cases of other theorems.
  • Definitions that are special cases of other definitions.
  • Processes to generate new theorems (duality principles, the machinery of category theory (corollary spaces?)).

Other undeveloped thoughts:

  • Some theorems are not used in the proof of anything else. Perhaps have community consequence challenges? The players have to prove something else using the theorem at least once.
Just noticed this. I don't see this as being a problem. Certain theorems are "end points" in that they exist as an end in themselves. FLT is an example I can think of (although you'll tell me it has a use now).
  • Lemma (or Exercise) namespace? The idea being that people store answers to questions in books so that more people can have a go of using LaTeX and wikis (the book in question of course not having the answers). Reward users by saying that their work has been "promoted" to the theorem namespace and let them know that they too can do mathematics. This way the theorem namespace isn't cluttered and it's getting others involved.
Lemmas should carry on existing in the Theorems namespace, because it's not a hard-and-fast rule as to what is a lemma and what is a theorem. Lemmas are identified (usually) by having "Lemma" at the top instead of "Theorem".
Examples I'm less sure about. What I am sure of is that I would rather they did not clutter up a definition page (or proof page, come to that) but should have standalone pages. What we could do is have example categories as subcategories of either theorem or definition categories (but I understand that the namespace paradigm may be compromised by the latter - does that matter?) There could be a specific template that would go into an "example" category like we have in the existing categories and subcategories. But I haven't gone down that route because the concept of examples in general (except for the instances of topologies and groups etc.) does not interest me much. --prime mover (talk) 19:46, 18 January 2013 (UTC)
I am trying to categorise the 'complaints' into broad categories and see if there is a sweeping solution for each of them. You may improve the list if you wish:
  • People that want the site to be completely different (as in like an encyclopedia or a wikiversity offshoot): If new direct them to the relevant help page. If persistent tell them to make their own. If demanding tell them to piss off.
  • People that want the site to have extra stuff: I have been studying databases and the concept of views has helped me think about this. Perhaps someday in the distant future PW will have views that take full advantage of the idea of transclusion. A 'concept page' for example could have a definition at the top, then 3 or 4 examples, 3 or 4 'featured theorems' etc. People who disliked the idea could simply turn their view of them off. But this is very difficult and not worth looking into at the moment I think.
  • People that want the site to look different: Disturbing that people seem to be genuinely offended by different notation. They will have to get used to it. Some people are bothered by excess notation which is understandable. PW is moving in the direction now where it suppresses notation if it has no use in the proof. So I think their complaints are as a whole attended to.

Antitransitive Implies Antireflexive


$xy,yz \vert \overline{xz}$




$aa,aa \vert \overline{aa}$

A contradiction.


$(xy,yz \vert \overline{xz}) \vert (\vert \overline{xx})$


Deposit 2

$\begin{xy} <0em,0em>*+{M_n(\mathbb{R})} = "S1", <5em,0em>*+{M_n(\mathbb{R})} = "S2", <5em,-5em>*+{\mathbb{R}} = "S3", "S1";"S2" **@{-} ?>*@{>} ?*!/_1em/{t}, "S2";"S3" **@{-} ?>*@{>} ?*!/_1em/{\operatorname{det}}, "S1";"S3" **@{-} ?>*@{>} ?<>(.4)*!/^1em/{\operatorname{det}}, \end{xy}$
I would advise you to use xymatrix instead. It allows to focus more on semantics rather than syntax. --Lord_Farin (talk) 08:15, 16 January 2013 (UTC)
Good advice. You may want to change the Definition:Commutative Diagram page if this is the case as this is where I got it from. :) --Jshflynn (talk) 09:46, 16 January 2013 (UTC)
Thanks for the pointer. Done. --Lord_Farin (talk) 19:03, 16 January 2013 (UTC)

Deposit 3

Captain's log: I have managed to open the database. There is a lot of excess data in there.

Managed to create a program which can output:
Set: Object, Element, Comprehension Principle, ...
I am leaving it to run in the background. It will take about 6 hours.
Ugh. Came back to PC and there was an error with the 2000th file. Getting there though...

From there I will see if I can make the GML script.

Deposit 4

Definition:Lambda Term


So I have the necessary data to make the graph.

For phase 1 I will just be making a simple graph that shows the connections between the definitions.

For phase 2 I'm going to colour the nodes according to their category. There are two problems though:

1. Deciding on the colouring scheme.
2. One very notable contributor on here is colour blind so I will have to find some way around that.

Stay tuned.

Progress 2

So here is what I'm working with:


It is incomplete because proofwiki is not yet perfectly monolithic (in the words of PM) and I want to get the project moving. I believe it is sufficient to give a simple overview :)

First impression: very smart.
Can you find places in it where it is inaccurate / incomplete because of ProofWiki's lack of being completely monolithic? That is, can it be used to provide direct feedback on PW's tightness and internal cohesiveness? --prime mover (talk) 19:38, 18 January 2013 (UTC)
Very cute, indeed.
One apparent problem: the dictionary doesn't look at subpages. For instance, the entry for the word coprime is empty. This is because the page Definition:Coprime has been refactored to a degree that it doesn't link to anything but subpages, which isn't registered in the dictionary.--Anghel (talk) 19:47, 18 January 2013 (UTC)
Essentially my Macro is hunting for sections on definition pages that are headed by either "== Definition ==" or "== Formal Definition ==". It then pulls out what it sees as valid links from inside those sections.
There are some sections that are headed by "== General Definition ==" instead which is perfectly valid, I just had never seen them before.
I think I should take back what I said as looking further into it the whole problem seems to be with my program handling redirects and subpages. I think I will leave this for phase 2 though as I'm rather impatient to see if the "convert list to graph" stage of the project is actually doable. --Jshflynn (talk) 19:54, 18 January 2013 (UTC)
Neat stuff. Might be good to look into the fact that some listings end with a comma while others don't. --Lord_Farin (talk) 22:08, 18 January 2013 (UTC)
Another one: rendering of non-UTF8 chars like letters with accent and Scandinavian, Polish letters. --Lord_Farin (talk) 22:10, 18 January 2013 (UTC)
How coincidental that I was attending to the comma issue just now before I read this. You have the instincts of a programmer it seems. Thanks for the heads up on those accents, I don't think anybody would be to pleased seeing "G?nter" or something of that sort where their name should be :) --Jshflynn (talk) 22:17, 18 January 2013 (UTC)


Script checks out.

Computer's compiling it.

Progress: 1%

It's going to be slow because it's an applying algorithm to optimise the layout.

Stay tuned.

--Jshflynn (talk) 19:46, 19 January 2013 (UTC)

On how it turned out


If A points to B then A is defined in terms of B.

The graph was produced using XGMML (approximately 75000 lines generated by a macro). There are some problems and explanations due of how they may be handled in the future:

  • All node labels are in lower case English with no spaces or UTF-8 characters: This was because the program I made relied on using the node labels as IDs. Unfortunately it was my mistake that it simplified the strings when deciding what the node label would actually be. This is a simple error and can be fixed. It would take another 6 hours of compilation however and I wanted to finish in some respect tonight.
  • It's difficult to read the nodes: This may be fixed if I can find a way to adjust the width of the nodes and not their height. It is another relatively simple problem I believe.
  • It's difficult to see the directed edges: This may not be fixable. With words like 'iff' for example it is probably completely impossible.
  • There are edge missing and nodes with the label "object": For no obvious reason 6 edges had to be removed because cytoscape didn't like it. The nodes with object on them do in fact represent words but there is no obvious reason in the code as to why this is.
  • There are words floating at the bottom and tiny components at the top: This is because the data I was working with was inadequate from the beginning. I will have to return to that phase and find a way to handle redirect structures.
  • There is no pinch and zoom feature: I cannot upload SVG on this wiki. This is the closest I could get.

If you dislike it in its entirety I would politely ask that you withhold your tongue as in spite of how poorly it turned out it did require a lot of work to make.

I'd like to thank Joe for directing me to the DB dump along with the rest of you for your encouragement along the way.

And now I shall get some rest :)

--Jshflynn (talk) 02:02, 20 January 2013 (UTC)

Interesting! --prime mover (talk) 06:17, 20 January 2013 (UTC)
That's really neat! If you feel like uploading a .svg somewhere and posting a link, I'd certainly download it. --GFauxPas (talk) 02:34, 7 February 2013 (UTC)
Sure thing GFauxPas. I'm going to tweek it so that the words fit and aren't all run together. I assume you are [email protected]? If not just email me at [email protected] to set up a comm. link. --Jshflynn (talk) 00:53, 8 February 2013 (UTC)