User talk:Kingdon

From Wikiproofs
Revision as of 04:22, 17 May 2012 by Kingdon (Talk | contribs) (no need for an isomorphism)

Jump to: navigation, search


Hi Kingdon, welcome to Wikiproofs! Feel free to mess around a little with JHilbert. You can also download the program for local use from There, you can find some preliminary documentation. There is also some very preliminary concept documentation in Category:JHilbert. Unfortunately, I've been very busy in RL, so nothing much has happened on this site the last few months. But I'm still checking for activity every few days.--GrafZahl (talk) 08:06, 6 January 2010 (UTC)

Proof and interface modules in user space

Hi Kingdon, just so you know: the JHilbert parser is also enabled in the User module and User interface namespaces where you can write your private/testing stuff with more flexibility than in the sandboxes.--GrafZahl (talk) 10:25, 8 January 2010 (UTC)

Thanks. I just tried it out and it seems to work nicely. Kingdon 19:41, 8 January 2010 (UTC)


Thank you for starting a JHilbert manual!--GrafZahl (talk) 20:27, 10 January 2010 (UTC)


Wow, you're really making great progress with Principia Mathematica propositional logic!

I wanted to direct your attention to User:GrafZahl/Definitions in JHilbert. This little essay contains a suggestion of mine to weaken the JHilbert definition mechanism for the sake of simplicity. As you might or might not know, the current definition mechanism is in a bit of a sorry state, with unsoundness lurking everywhere. Maybe you have some input you'd want to share.

Oh, and don't worry about your current work on propositional logic. It is neither affected by any unsoundness in the current definition mechanism, nor would the particular definitions in that proof module cease to work due to my suggested weakening.

--GrafZahl (talk) 23:05, 11 February 2010 (UTC)

Yes, most of Principia Mathematica propositional logic is on my laptop and needs to be uploaded (and debugged, which I have been doing as I upload each theorem). I've been travelling and off the internet which is why I haven't been doing the edits in the usual way. I also am working on (1) a set of suggestions for improvements to Interface:Classical propositional calculus and am toying with moving on to one or more of the following projects: (2) Prove that Principia axioms imply Nicod's (probably not too hard, going via Classical propositional logic), (3) Add the Lukasiewicz (Margaris/metamath/Hamilton) propositional logic axioms and prove they are equivalent to the Principia ones, (4) move on to first order logic, since it would be nice to be able to do some real math like number theory or graph theory, and first order logic seems like the next stop towards either Peano or any of the various set theories.
As for the definitions, thanks for the notice; I had just run into dummy variables when my naive attempt to prove Tautology blew up. I think I know how to solve that (I'll know after another hour or so of work). Whatever you decide probably does have implications for ⊤ and ⊥, at least the way they are currently implemented, but the vast majority of the propositional logic module would be untouched. Kingdon 23:51, 11 February 2010 (UTC)
Well, you seem to have a lot of great plans. And congratulations for making classical propositional logic exportable with Principia Mathematica! As for improvements to Interface:Classical propositional calculus, I'll be glad for any suggestions. This will be crucial interface for a large part of mathematics, so it's important it's well thought through by more than just one person. Just be bold. BTW, what do you think about featuring your fine work on Principia Mathematica propositional logic on the main page, maybe after your improvements have been implemented?--GrafZahl (talk) 14:37, 13 February 2010 (UTC)
Featuring our work sounds great (I won't take full credit given how much of it was already there when I started). I've done a cleanup pass. I see that you did at least one copy-edit pass; thanks. If you want to wait on the featuring until after the Interface:Classical propositional calculus ideas, that's fine, as some of them will get used a lot in Principia Mathematica propositional logic if we decide we like them.
My suggestions are at Interface talk:Classical propositional calculus; I'd rather be slightly less bold on these ones, partly because every substantive edit requires editing two pages. Kingdon 05:18, 14 February 2010 (UTC)

Dummies, definitions and all that

Thanks for your dummies example (normal dummies in this case) and your continued work in general. You've probably realised that there are efforts under way to change the dummy/definition mechanism of JHilbert/Ghilbert in fundamental ways, and your work is slowly approaching realms where this stuff starts to really matter. Now, until the changes are actually implemented, I expect one or two months to pass at the very least. That's probably an insanely optimistic estimate. The thing is that once the new version goes online, some modules might require non-trivial changes (added proof steps) in order to still verify. That's very unfortunate, but obviously you don't want functionality which leads to unsoundness in your proof verifier, and right now I don't see a way to salvage the current very convenient definition mechanism.--GrafZahl (talk) 18:22, 25 February 2010 (UTC)

This example won't change with any of the new proposals, I don't think. In fact the error message is more confusing if you have been following the discussions than if you haven't, which was the main reason for adding it to the manual. Every time I get confused by an error message, even momentarily, I try to use that as my cue to add it to the manual. As for needing to update the proofs, part of why I want to push forward on some of these pages is so that you have real-life examples which can help inform your decisions, and I'm not too scared about fixing them when JHilbert changes. I have no strong opinion about automatic definitions; at times they make a proof really hard to follow but on the flip side making a proof shorter is usually a good thing. Kingdon 23:20, 25 February 2010 (UTC)

New featured page

Hi, I've started the blurb for the next featured page at Template:Featured/Draft. Maybe you can edit it a little… Feel free to choose a better image if you find one. Be careful with EU copyright restrictions, however (70 years pma vs. the US "pre-1923" rule). In particular, photographs of Whitehead or Russell are probably still copyrighted.--GrafZahl (talk) 18:54, 25 February 2010 (UTC)

Well, I made a stab at a blurb, although feel free to revise if you can think of anything more interesting or otherwise better to say. Kingdon 01:58, 26 February 2010 (UTC)
I've made some additions. I think it's OK to bring it out now, unless you want to add more stuff.--GrafZahl (talk) 16:58, 5 March 2010 (UTC)
Looks ready to me. Kingdon 17:03, 5 March 2010 (UTC)
'Tis done.--GrafZahl (talk) 17:17, 5 March 2010 (UTC)

Peano arithmetic theorems

(moved from User:Kingdon, next to the list of theorems to prove in Peano arithmetic).

Many (but not all) of these are proved in (new) Ghilbert. See [1] for the source, but keep in mind I haven't yet pushed the batch or interactive verifier that will accept these. Right now, params to interfaces don't work, so I've had to hand-hack the interface files.
So, my questions are: Is there some way to gateway these Ghilbert proofs so that they can be imported here? (Or vice versa, for that matter). Is there some place I can jump in and contribute a theorem or two to get started (maybe first-order predicate logic)? Raph 02:56, 26 February 2010 (UTC)
Definitely would love to have you jump in and give it a whirl. First-order logic is what I've been working on lately, and you can see what we have so far in Category:Classical_first-order_logic. Feel free to be bold; my own personal list of what seems most important is at User:Kingdon but your ideas of what might be useful are probably as good as mine. My current focus is: (1) getting a few more subst theorems (my experiments, for example User interface:Kingdon/Sandbox and User module:Kingdon/Sandbox have led me to think that subst-style induction might work out nicer than finds-style, although I'm not completely convinced on the point), and probably (2) start proving some of the Peano theorems (for one thing this is a way of finding out what is missing in the first-order logic). Kingdon 03:44, 26 February 2010 (UTC)


I'd like to ask you if you'd be interested in administrator access to this wiki. Your prolific work occasionally requires changes to protected pages (most notably Mediawiki:Edittools) and you obviously have enough experience with the MediaWiki software for reasonable use of the admin tools. On the other hand, if you feel uncomfortable being an admin, I see no problem in continuing our current practise of change on request.--GrafZahl (talk) 16:34, 5 March 2010 (UTC)

Fine with me. At our current size, or likely size any time soon, I don't think it will be too much of a burden/distraction. Kingdon 16:38, 5 March 2010 (UTC)
OK, you are now an admin.--GrafZahl (talk) 17:01, 5 March 2010 (UTC)

Thank you

Hi Kingdon. Thank you so much for all your content contributions, your talk page posts and the occasional vandal block. Right now I'm pretty much occupied elsewhere (my Ph.D. thesis is finally reaching critical mass), so I don't have any significant time to spare for Wikiproofs, JHilbert and all that. I hope I'll come back in the not too distant future.--GrafZahl (talk) 09:31, 27 July 2010 (UTC)

Thanks for letting me know (I had guessed as much, but it is nice to hear an update from time to time). I do appreciate whatever small amount of time you may have, and hope that your PhD goes well. I too am certainly hoping that you'll find some time at some point, as a lot of the stuff you have been interested in would benefit my efforts too. Kingdon 23:08, 27 July 2010 (UTC)

Server crash

Hi Kingdon, in case you were wondering, the server crashed at about 1:32 UTC this night with what I believe was an out of memory problem. I rebooted and it seems to work fine again. Hopefully, it won't happen again too soon.--GrafZahl (talk) 08:27, 26 August 2010 (UTC)

Thanks for keeping me informed. Doesn't sound like there is anything worth doing about it unless perhaps if it starts happening often. 21:52, 28 August 2010 (UTC)
Hi Kingdon, once again the server crashed this night at about 5:30 UTC, again due to lack of memory. It seems to be in working order again.--GrafZahl (talk) 09:34, 12 November 2010 (UTC)
I was getting 500 errors (probably about 01:00 UTC 12 Nov, over a period of an hour or a few). Glad to see it is back up. Kingdon 01:32, 13 November 2010 (UTC)
Now the site is up but fairly slow and I'm also getting "Feed failure: I/O error" on both First-order logic and Basic geometry. I wonder if it has anything to do with all the editing I was doing on Basic geometry - that's a big file (which I'm not sure I'd prefer to break up on stylistic grounds although if the software requires smaller files I could figure out a way). But I'm speculating here... Kingdon 03:31, 13 November 2010 (UTC)
It seems to be back to regular speed and I was able to clear the I/O error. Kingdon 01:44, 14 November 2010 (UTC)

Hi, today I registered the domain in addition to The .org domain seems more appropriate for an international non-profit project. My provider tells me that it may take up to 48 hours until the new domain correctly resolves to the Wikiproofs host everywhere in the world. I'd have registered the .org domain earlier but there used to be another site sitting on it (possibly intended as a non-formal proof wiki, but it always looked kinda defunct to me). I'll try to switch MediaWiki and the web server over to use .org by default when the 48 hours have passed.--GrafZahl (talk) 16:35, 1 September 2010 (UTC)

Hmm. The .org is probably a bit easier to confuse with which as far as I can tell is non-defunct. But use your best judgement. Kingdon 17:52, 1 September 2010 (UTC)

New java runtime

The wikiproofs server has experienced several OOM failures during the last 3 days or so. It seems my hosting provider measures memory usage by allocated virtual address space, of which Sun's JRE takes several hundred megs regardless of actual heap size. I've switched to OpenJDK now, but since that's also from sun, I don't expect much improvement. I also tried GIJ, but it's classpath-based and lacks several Java 1.6 features. I'll try and fiddle around with GIJ a little more, but it seems like in the long run I simply need more memory for the server.--GrafZahl (talk) 14:31, 18 November 2010 (UTC)

OK, I've "downgraded" JHilbert to hopefully use Java 1.5 features only and installed GIJ as JVM. At least for now, it appears to have a much smaller memory footprint than the Sun stuff. First access to pages will be a bit slower because the entire module cache has to be rebuilt. Also, the "downgraded" version contains some extra DV stuff I had started to code before we all realized that DV has to be done differently. Hopefully, it doesn't break anything. Please let me know if something weird happens.--GrafZahl (talk) 15:04, 18 November 2010 (UTC)
You also might look at some of the server settings. I've noticed that one thing which seems capable of bringing the server to its knees is loading more than one page simultaneously (for example, in two tabs of the browser). This may indicate that you are allowing too many worker processses relative to how much memory is available. See for example MaxClients (and some of the other settings) at . I think I've seen this behavior even on non-JHilbert page loads (but I'm not sure of that part - I didn't do enough testing to be sure of when it is hitting JHilbert and when it is serving it from cache). Kingdon 02:45, 19 November 2010 (UTC)
Thanks, but wikiproofs is running lighttpd. My guess is that lighttpd's PHP-FCGI backend is the bottleneck. It has two configuration parameters I don't seem to quite understand. One is "max-procs", the other is "PHP_FCGI_CHILDREN". As far as I understand it, lighttpd starts max-procs FCGI servers, each of which will spawn PHP_FCGI_CHILDREN children, so that the number of CGI processes is max-proxs * (1 + PHP_FCGI_CHILDREN). When PHP performs a JHilbert request, JHilbert itself will direct a query to the webserver for each interface not already in the cache, recursively causing more CGI processes to be tied up. What I'm unsure about is how to best distribute numbers over max-procs and PHP_FCGI_CHILDREN. Previously, I had max-procs=2 and PHP_FCGI_CHILDREN=4. Experimentally, I've changed it to max-procs=5 and PHP_FCGI_CHILDREN=1. Let's see if there is any improvement.--GrafZahl (talk) 13:59, 19 November 2010 (UTC)
Bad idea, it seems. Now trying max-procs=1, PHP_FCGI_CHILDREN=6 and feeling like a Voodoo master.-- 00:55, 20 November 2010 (UTC)
Well, nothing seems to work satisfactorily. Also GIJ appears to be significantly slower than Sun's JRE; at least some large pages constantly produce feed failures, indicating processing timeouts. I'll have to negotiate with my hosting provider about RAM extension options. I'll keep you informed.--GrafZahl (talk) 23:37, 20 November 2010 (UTC)
Sounds like you found the right settings to tweak. The rough calculation should be similar for lighttpd or other servers: (number of processes times memory for each process) + whatever is used by everything else = total memory. The part about JHilbert calling back to load interfaces is a twist I hadn't thought of. Thanks for looking into this and hope you can get it fixed. I have some proofs on my github mirror which I'm ready to upload - the site's reliability is the biggest limiting factor at the moment. Kingdon 01:47, 21 November 2010 (UTC)
I'm going to migrate the site to a new server with 1G RAM (current server has 384M). This will involve some lock time (during which the wiki becomes immutable) and maybe even some downtime. I'll try to keep the migration as smooth as possible. I think the effort should be worth it.--GrafZahl (talk) 18:16, 22 November 2010 (UTC)
In an ideal world, 384M would be up to the task, but given how much memory is taken up by java plus however many PHP processes, I think you made the right choice. Keep me posted as I'm kind of stalling the College Mathematics Journal guy until we can get the site at least serving the home page reliably. Kingdon 01:28, 23 November 2010 (UTC)
The new server is up and running. Everything seems to work fine. Please inform me if something appears broken. Thanks again for preparing the journal article. I'm running PHP processes now. Hopefully that is enough for some visitor influx caused by the publication. Memory usage is at about 600-700M now (running Sun's VM again).--GrafZahl (talk) 10:58, 23 November 2010 (UTC)

The server seems snappy enough that I couldn't do a manual load test (by the time I went to click on a second page in a second tab, the first one had loaded), which is a good sign. I did think of one more thing if java is using up a lot of memory, which is the -Xmx and -Xms options to java (at least, that's what they are called for the JDK; I suspect the other javas you tried have something similar). Set those too low and java will spend all its time garbage collecting, but set them too high and it will tend to chew up memory unnecessarily. Unless they changed something, the defaults are pretty high and may depend on the memory size (as in, don't really assume there is much else running on the box). As for the publication, still no guarantee it will happen, but sounds like the server is probably ready if it does. Kingdon 13:03, 24 November 2010 (UTC)

Oh, and I'm changing to in the thing I'm planning to send them. Kingdon 13:21, 24 November 2010 (UTC)
The new server is back to Sun java. It seems to be the fastest alternative (probably due to the HotSpot thing). On the old server, java was started with -Xmx64m. On the new server, I increased that to -Xmx128m. Total memory usage on the server is currently 717M. If that remains relatively stable during the next few days, I'll feel save to increase the java heap to -Xmx256m. One other thing I wrote above was slightly inaccurate: while JHilbert does callback the server to retrieve interfaces, it does so using the MediaWiki API, completely loading the interface text before doing any parsing. So in terms of PHP process utilisation, the recursion depth is never greater than 2, which is also a good thing (though it could be reduced to no recursion at all by direct database access).
As for .org vs. .de, I figure the international TLD is more apt for a project like Wikiproofs, but since the .de domain comes free with the server package, I'll keep it around. My hosting provider will have it point to the new server within the next few days.
Regarding the publication, from my own experience I'm quite aware that stuff you intend to publish may not end up in the journal you expected it to (if it ends up anywhere at all), nor within the intended time frame, which is all the more reason for me to thank you for your effort.
Oh, and I guess I can remove the site notice now.
--GrafZahl (talk) 16:43, 24 November 2010 (UTC)
Dot org is fine with me, so I'll follow your lead on that. As for the site notice, yeah, it is kind of intrusive to leave it there for long (unless/until we implement a "close" button like they have on wikipedia, and I haven't looked into how they do that over there). Kingdon 02:49, 26 November 2010 (UTC)
Apparently they do it with Javascript/Cookies, see Extension:DismissableSiteNotice. I've created such a site notice as a test. It can be controlled with MediaWiki:Sitenotice and MediaWiki:Sitenotice id.--GrafZahl (talk) 10:35, 26 November 2010 (UTC)

Happy holidays!

Hi Kingdon, I'd like to wish you a happy holiday season! I'd also like to congratulate you on your steady progress in geometry formalisation. Without you, Wikiproofs would be a much emptier place.

My boss now has the almost-final draft of my Ph.D. thesis and he won't be due back until 10 January. So I'm hoping to be able to dedicate some time for some JHilbert/Wikiproofs developing in the first week of January.

Enjoy your holidays!--GrafZahl (talk) 12:34, 24 December 2010 (UTC)

Thanks for the kind words. The geometry is fun because it is a little off the beaten path (and also has the potential to tie into the part of the math curriculum where students learn about proofs, although I haven't yet read the papers - from some Coq people - about how they are using formal proof systems in education). As for the possibility that you'll have some more time in the next few weeks for JHilbert/wikiproofs, that is great news. It has been a pretty lonely place sometimes and there's certainly no shortage of things to do. Happy holidays to you as well. Kingdon 13:19, 24 December 2010 (UTC)

Breakage, repair, hyperlinks

Hi Kingdon, and Happy New Year to you! I did an OS upgrade, and the JHilbert extension broke, so I had to rewrite it. Doing that, I also hacked some kind of hyperlink support into JHilbert. That is, all module locators and statement/theorem names should now be either anchored (with id="statBlah") or a hyperlink. The module locators simply link to the respective module pages. As for the statement/theorem names, if they appear in a proof, they are hyperlinks. You can hover over them: if they are from a different module, the module name appears. In all cases, clicking on them should transport you directly to its stmt/thm command. To make this work on all pages, you might have to purge the parser cache. If you find bugs, please notify me on my talk page or via e-Mail.--GrafZahl (talk) 02:06, 5 January 2012 (UTC)

Holy cow! If this is the result, I hope the extension breaks more often :-). The hyperlinks are fantastic. I had been working around the lack of them for import/export by putting a link in the text prior to the JHilbert import/export, and have at least occasionally pondered doing something similar for theorems/statements. But having it built into the JHilbert extension is better, as it avoids the clutter of a separate link. At least so far, haven't noticed any problems, although I have had to purge the cache on most of the pages I looked at. Kingdon 05:37, 5 January 2012 (UTC)
There seems to be no simple way to mass purge the pages. There is a maintencance script, but it expects a list of page names. I've manually wiped the objectcache table in the database. Hope that helped.--GrafZahl (talk) 22:33, 7 January 2012 (UTC)

Pull request

Thanks for your pull request. I'm very busy, so I cannot review it right now. Sorry for the inconvenience.--GrafZahl (talk) 21:00, 4 April 2012 (UTC)

Nothing urgent in it, I don't think. I just figured it would be easier to send one now before the number of changes got even bigger, that's all. Thanks for keeping me posted. Kingdon 06:42, 6 April 2012 (UTC)


Hi, I have done some proofs with Metamath's in the past (many of my shortened proofs are there). I was wondering: does wikiproofs have any advantages over Metamath and friends, besides the fact that it is easily accessible and editable by anyone? Also, more specifically, let's say I had a set and operations that satisfied the axioms for complex numbers. Would I be able to use the complex number module directly, or would I have to create an isomorphism? Asalmon14 (talk) 07:02, 16 May 2012 (UTC)

Wikiproofs uses JHilbert, which is like ghilbert in that it aims to solve some of the problems of metamath, while preserving its basic spirit. If you have a module built on set theory which defines +, ·, ℂ, etc, and proves the axioms, you could then export Interface:Complex number axioms which would then justify an immediate import of Interface:Complex numbers. An isomorphism would not be necessary or helpful, as far as I can see, because in Interface:Complex number axioms, ℂ is not a particular set; it is either posited to exist (if you take those axioms as axioms), or proven to exist in a module which exports the interface (not in the interface itself). Kingdon (talk) 03:21, 17 May 2012 (UTC)