Metablog

I’m thinking about getting electro-convulsive therapy. Apparently it’s quite an ordeal, what with the full anesthesia every two days for a month. On the other hand, it’s only done once, and then you’re done with it, pretty much. And if it works, well great. And it’s a month away from work. (Work that I can barely handle right now.) If my new psychiatrist doesn’t have some really compelling medication options on the table, I’ll probably be getting it soon.

Welcome to my online world! You know, I’ve thought a lot about building my own world. Like, you know, a personal vision of a fantasy world of some sort that’s immersive and expansive and provides an extended analogy to my psyche and whatnot. I guess I haven’t gotten crazy enough and single-minded enough to pursue such a vision yet. I’ve thought about doing such a world in a text-based environment, like a MUD, and in a graphical environment. The latter would require more tools (like a 3d modeler) and more time per unit of world, but be more immersive. (And more primitive, considering my lack of artisticalish skilz.)

I’ve found the main limitation in pursuing such a dream is the lack of inspiration. I don’t really have many ideas for worlds that are much different than our own, dull, dreary, miserable, dissatisfying world to draw upon. I’m not creative in that way. If I were, I would definitely have been creating such a world and wouldn’t be here now posting. I’m a very practical person. More interested in science than art. More interested in programming languages than programs.

Continue reading »

Hello, world. I’m learning Scala. It’s a pretty neat language, despite my initial negative reaction based on the name, logo, and color scheme of the site. I think I’ve finally gotten over liking Lisp especially. F# doesn’t seem especially impressive to me compared to Scala. Or even SML, to be honest.

Still single, and miserable. There’s no one out there like me. Well, close enough to no one that I haven’t been able to find them after three years of looking, off and on, through dating sites. Only a couple people that even come close, and those ones don’t respond.

They say that suicide is a disease in itself. Aside from depression, it takes a life of its own, and eats away at you even when you’d otherwise be happy. I’m not quite happy, but I’m close to it. Closer than I was a year ago. I still have plenty to justify suicide. I just wonder if I will ever run out of things to justify it. I clearly have a will to live. Just not a very strong one.

I’m learning Isabelle. I want to write a new user interface for it. Something awesome. I have a good idea of how to make it awesome, but I haven’t yet decided how to approach it. Or how to spend my free time working on it. Or how to deal with the stress of my job. Or the lack of a desire to live. Anyway, I’ve thought that I might take a bottom-up approach, reading the source code in order of how the compiler compiles it, which is guaranteed to be the most linear bottom-up approach available. (Unlike in languages like C# where source files can have circular dependencies up to the assembly (dll) level, which makes bottom-up reading potentially impossible.) But I’m not sure I’ll do that.

Due to an unfortunate incident, I’m required to attend AA meetings. It’s a shame, since I’m not an alcoholic, that I’m being forced to intrude on these meetings, but seeing the camaraderie between these people makes me want to attend something more appropriate for me. A bipolar meeting, perhaps? I don’t see anything in my city. Shame. I should call some hotlines that have better resources than google on this issue.

No real progress on lucid dreaming, despite the post title. I remember bits of dreams every few days. That’s about it. I promise not to subject you to any of my dreams. I may post here of some revelation I’ve had as a result of some dream. But that’ll be it. So far, the most significance any dream has had is that I needed to pee while I slept.

You know, I’m not even sure why I do this type of post. It’s not like there’s anyone who enjoys them. Now, my last post. That was one with popular appeal.

As an exercise, to get some experience with Metamath’s formal system, I’ve been working on a formalization of the Lambda Calculus. (That article should provide more than enough background for this post.) I’ve run into a little issue, though. When defining combinators (certain fixed expressions with special meaning), one needs to use dummy variables. For instance, the S combinator is λxyz.xy(xz), where “x”, “y”, and “z” could be any three letters. You could choose them as needed not to collide with any other variables you’re using. However, when expanding these definitions in Metamath, it becomes impossible to avoid having to prove things like “x is not free in M”, even though of course it’s not free. For example, through beta reduction, we have

As the next step, we’d like to substitute y for N, yielding (MN(Mz))[z := L]. But we can’t do this without also proving that y is not free in M, because, expanding the steps in more detail, we have

There is no way to eliminate the [y := N] after the M without proving that doing so would not change the meaning of the term. Of course, I could eliminate that requirement from the axiom, but I fear the system would become unsound. Now, we know that this is a fine step to do, because we know that in the definition of the S combinator the variables x, y, and z are postulated not to match any of the other variables in the terms you’re substituting for them. The problem, however, is representing this notion in the formal system.

The paper I’m working on, available here, provides a fairly thorough and rigorous introduction to the subject, and so is pretty much ideal for what I’m using it for. However, it deal with the problem presented here by postulating that bound variables and free variables are drawn from two distinct sets. I don’t believe this approach is practical for Metamath.

Also published at Less Wrong.

So, you wanna be a rationalist, huh? Then it’s more than likely that at some point you’ve had the thought: “I should be completely honest with everyone. I shouldn’t hide any truth.” And it’s likely you’re a bit more honest than the average human. (Robin Hanson might take issue here.) And it’s likely you’re nothing like completely honest with everyone. So where, and why, do these ideals fall short?

First, strict honesty is a form of vulnerability. You’re bound to say a particular thing in any given situation, regardless of how it may work to your advantage or disadvantage. You pass up opportunities to manipulate or obfuscate that could work to your advantage. In the game of life, you’re conceding ground. Now, this is made up for, to some extent, by the reputational advantages of honesty. Is the balance positive? Not hardly, in my opinion. (And we haven’t even considered the “telling it like it is” problem yet.)

Second, it takes a lot of active effort to stay honest with someone. And that effort needs to pay off for honesty to be worthwhile. Strict honesty can only pay off with particular people. You say you want honesty. No, what you want is honesty from someone who thinks rather highly of you and is committed to your well-being. Someone who doesn’t have much negative to say about you at all, compared to the positive.*

Really, I think what people are searching for with these honesty impulses is reciprocal honesty. Reciprocal honesty is much more practicable than strict honesty. You can be reciprocally honest in limited ways, with specific people on certain topics. You can pick and choose. (Do you feel an obligation to tell the truth to those who lie to you?)

Continue reading »

Great name for a song. (I wouldn’t drink it that way myself, obviously. I take it neat. (I wouldn’t drink it that way, obviously. I take it intravenously.))

Thanks to drinking a tiny bit of Everclear in my PowerCitrus! soda and listening to Katamari On The Rocks, the a capella version of the main Katamari Damacy theme in the Moon level (the last level).

Isabelle is a program that checks your math. You tell it, in a very technical computer language, how to prove that some line of mathematical reasoning is correct, and it verifies that you’ve told it right. It’s also a great help in searching for proofs to begin with, because it has powerful techniques to simplify and transform mathematical statements into simpler or just different versions that help you understand the statements.

Isar is a language built on top of Isabelle. Unlike most computer proof languages, It allows steps in a proof to be done without mentioning the theorem being used by name in certain circumstances, allows explicit naming and reference of statements, and allows backwards and forwards proof to be mixed together arbitrarily. (In these respects it’s similar to the difference between assembly language and higher-level programming languages.) You can state subgoals explicitly on your way to proving the main goal if you like (similar to subroutines). A key strength of Isar is its flexibility—you can state a given proof in many different ways, which means that you can usually find a way that’s fairly easy to read.

What’s more, the ideas behind Isar don’t have a whole lot to do with the underlying logical or even metalogical framework. In other words, Isar is to a large extent orthogonal to Isabelle. Isabelle/Isar uses unification and resolution in an intuitionistic metalogic as its principles, but they could be substantially different while keeping Isar useful.

Metamath is a system that’s quite similar to Isabelle at heart, but much, much, much simpler. It’s correspondingly less powerful (practically speaking, not formally) and harder to use. Its main advantage is that its proofs, while longer, are very explicit and thus possible to follow with a minimum of prior knowledge. (And, as far as I’m concerned, the simplicity is also quite nice in that I can easily use Metamath ideas to design my own math system and have a lot more confidence in the results than I would with a system of my own design or a system that imitated the design of a more complex system like Isabelle.)

Continue reading »

I’ve been doing a lot of mathy things recently, and one of them has been playing with Metamath, which is step by step formalizing a whole bunch of mathematics. You can see what real numbers really are, how recursion and induction can be defined using only basic set theory, what a function really is, and a million other neat things. It has proofs for all of its theorems that can be verified by a very simple program, or by hand if you like. It’s just a whole bunch of substituting A for B and matching.

The only problem with it is that it’s kind of low-level. It’s hard to follow the proofs and even sometimes the definitions. Now, on the one hand, it’s probably good to become more fluent in formal mathematical language if you want to learn a lot of math. But on the other hand, part of the difficulty I was encountering was entirely avoidable, due to not including enough information about the proof when it’s displayed. In particular, to know what substitution is being made at any given point, you have to open the theorem being used at that step, and then go back to the proof. If the theorem is quite large, you might have to go back and forth quite a bit to get it in your head enough to understand what’s going on. And further, for very long equations, it can be completely impossible to do this in your head.

So I made it all happen on the screen, right there in front of you. Proofs still aren’t easy to follow, but they’re quite a bit easier than they were. Perhaps as easy as they’re going to get with Metamath. We’ll see if I get any better at reading them now. (By the way, this is done along with shrinking the site quite a bit by having it all done in javascript.)

Unfortunately, I don’t currently replicate all of the features of the Metamath site, since that would be hard and kind of boring. So you need to really start here, and then type in http://pdf23ds.net/projects/Metamath/theory-name.htm when you have a theorem whose proof you want to follow.

I invite your comments.

Hi, google!

And hi, searcher! If you’re looking for a .NET or C# or VB version (really, just the output part) of the Rats! PEG parser, I can probably help! I have written such a thing, and could be persuaded to assist with its use. It isn’t in the main distribution of Rats!, for various reasons, though could be in the future if there’s any demand for it. There is a Bazaar repository with my changes here (though this might not be the latest–check with me).

UPDATE: Someone just notified either 911 or the police about this post, and they came out to check on me. (No problems.) Whoever it is, knock it off. You sort of missed the point.

Have you ever thought about committing suicide? Well, if so, maybe you should actually go through with it. I know, I know, you don’t really hear that anywhere. But it needs to be said. Sometimes, suicide is the answer. I believe suicide is the answer for me. And it very well could be for you.

But not likely. Most people who commit suicide are not thinking terribly rationally. If you’re having really hard times right now, things do get better. (On average.) If you’ve just broken up with someone and are feeling extremely depressed, suicide is almost certainly a bad idea. If you’ve just suffered a large or huge financial loss, it’s very likely that if you just hang in there you’ll be just as happy in a couple years as you were before (even if poorer). People’s happiness is sticky like that. It tends not to change over large time periods. Fluctuate, yes, but not change permanently. (There are some exceptions to this. If you’re friendless, making friends will make you happier. If you get into an accident and become disabled, your happiness does go down some, but not as much as you would think.)

This essay is really aimed towards people like me: people with treatment-resistant depression. I have bipolar II disorder, and it has not responded well at all to many different medication combinations. My suicidal thoughts have never really gone away. I have no support structure, and no chance of forming one—I have rather severe avoidance issues. No friends, unsupportive family. I hate people, deeply. Mostly people I’m not close to. I don’t hate humanity, though. If I did I wouldn’t be writing this. I do hate the world—the system as a whole, in which people play the part of small cogs. The world screws people over. (I understand this isn’t an especially unhealthy feeling.) I feel sorry for those people as people, even as I hate them as individuals.

In other words, I am, emotionally, severely fucked up. This isn’t going to get better. I’ve spent the last 8 years trying to make it better. I made some progress, in easing my social anxiety and in increasing how well I understand social cues and such. I’m not autistic or anything, just a late bloomer. (I do have non-verbal learning disorder, which involves social awkwardness.) But I’ve stopped making progress. There is no more progress to make on this front.

My life right now is not worth living. It hasn’t been for two years. And I can’t foresee that changing for at least five years. Five years of probably pointless therapy and stupid self-reflection and even more medication changes and dealing with idiotic insurance and bills and the other stuff I can’t stand to deal with. Before I start to get better. In the best case. And by then, I won’t even be young anymore.

It’s not worth the terrible anxiety and lack of purpose* and continued isolation and the ups and downs. I’m even starting to think that, maybe, there is no way out of the emotional corner I’m in. That my hate of people has such a great amount of real support in people’s behavior that I won’t be able to change the attitude and still be able to be intellectually consistent. That’s a rather new belief, though, and I’m not sure it’ll stick.

* Anhedonia, really. I think happy people are able to feel plenty purposeful without trying too hard. I believe people make their own purpose; they don’t get it handed to them. But you can’t find a purpose if you can’t feel anything.

Why write all this? Because it makes me really fucking angry that so many people out there would read this and think that I’m crazy. Out of my mind. Not rational. Not able to validly come to this decision. I feel that it is my right to decide to end my life, and that I’ve been plenty rational. There’s a little trick that they pull in this argument, you see. They define rational partly based on the person’s feelings, rather than solely based on their processing of those feelings. If I’m having suicidal thoughts, that means, ipso facto, that I’m being irrational. The more naunced position is that if I feel that my life is not worth living in its current state, that I’m being irrational. Because every rational person has a will to live. And that is such complete bullshit.

If you want to commit suicide, for the right reasons, having thought through everything you can be expected to, then you should be able to go to the hospital and get put down.

Now, I myself don’t have any dependents, but suicide for those who do does raise some moral questions that I’m not sure how to answer. On the other hand, it is a person’s right to commit suicide regardless of the pain that they might inflict on friends or family. I think in many cases it might be wrong to do so, but that doesn’t impinge on the right. Again, I’m speaking abstractly here because these considerations don’t apply to me. My parents would be the most upset by my suicide, but besides them, I don’t think anyone would really be too disturbed. And they helped put me in this huge clusterfuck in the first place, so I’m not shedding any tears for them.

And as for society? Do I have any sort of obligation to society to remain alive? FUCK NO. Society can fuck itself in the ass with a poison-tipped mace as far as I care. “Society” doesn’t care one bit about its people. Some of its more altruistic members have been trying to change that, since, like, forever, but so far their overall effect has been negligible. And believe it or not, I’m actually mildly optimistic about the future. But that doesn’t change my condition, right now. Society is not yet worth being a member of.

These judgments are very contentious, of course, and legitimately so. But regardless of whether there’s a consensus on these issues, I have a right to, motivated by these judgments, end my own life. I can’t be put into the crazy-house because I think society isn’t worth living in.

Any comments arguing from the suicidal person’s sense of obligation to family, friends, or society will be deleted with prejudice. It’s a legitimate issue, but banned from this thread.

I have no immediate plans to commit suicide. I have a good chance of trying several more treatments before I commit suicide, if it comes to that. Any comments urging me not to commit suicide will be deleted if uninteresting. Also, I’m not terribly interested in sympathy, but advice is not entirely unwelcome.