May 28, 2009

Mathematical Intuitionism and the project

I don't really know what im talking about, but ...

It occurred to me that my project does not use negation as failure, and also doesn't use the law of excluded middle. Its not like Im purposely trying to go against what would be normal, I only did what I thought made sense when writing. This just goes to show how much creatively there is in ignorance.

Im not trying to view this projects as something mathematically concrete. I don't really refer to anything as a "Model". My reasoning for the ternary model was that any proposition exists in one of THREE states with respect to a body of knowledge, that it either is confirmed, denied, or bears no relation. It looks like ive somehow stumbled into being a mathematical intuitionist though.

Funny how the wikipedia article, which is my only source of info on this area, doesn't mention anything about ternary logic, or modal logic (my ternary logic is really just a cheap substitute for modal logic after all).

At any rate this intuitionism appeals to me on some really sort of zen level. Maybe God can separate out all logical statements into True, and False. We however can't and it leads me to be very unsettled. I don't think ive ever written a nonconstructive proof in college. Now I don't feel safe in saying that anything thats not false is true.

Open Source Board Games

Earlier I talked about making Monopoly "open sourced" and how such an important piece of American culture should be owned by the culture. Now Im wondering how to do this for Settlers of Catan, a really fun and unique board game I just learned about. This game too, seems a bit overdone, but nowhere nearly as bad as monopoly. Making a game free from its manufactured nature often requires reducing the complexity of the game in several ways and just trusting the natural shape of the game to produce interesting situations. Ive been having some luck with a version Im trying with a deck of cards as the board.

May 11, 2009

Logic Unification in Trinary Logic

Im still workin on making the logic programming language of my dreams. Right now I have to get some sort of unification working, but Im using trinary logic so its been a bit of an adventure. Prolog doesn't have real negation so it really manages to sidestep alot of actual work. Informally in my logic system, called Llull, a statement has three possible truth states: 0 = No, 1 =Iono, 2 = Yes.

Yes and No are basically like True or False. Iono is much different. Since negation is allowed in Llull, determining wether a model implies something is an NP Hard problem. My unification isn't an exhaustive search, therefore, for hard problems, Llull will just throw its hands up in the air and say "iono and i don't care to actually figure it out". Iono means that either theres no data about the thing you asked about, or that it just can't find it.

Anyway, traditionally And, Or, and Not have been defined for trinary as:

  • And(s1,s2) = min(s1,s2)
  • Or(s1,s2) = max(s1,s2)
  • Not(1) = 1
  • Not(0) = 2
  • Not(2) = 0

If you check, these definitions make tons of sense. But to see why they really arent sufficent for my purposes maybe I should cover my unification algorithm. My unification algorithm works by breaking up statements in this manner (where s1, s2, s3 are all Llull statements) :
  • s1 -> And(s2, s3) if And(s1->s3, s2 ->s3)
  • s1 -> Or(s2, s3) if Or( s1->s3, s2->s3)
  • s1 -> Not(s3) if Not(s1->s3)

Rough Example:

Sean is a CS/Math Major -> Sean Studies CS And Sean Studies Math
iff
Sean is a CS/MathMajor -> Sean Studies CS And Sean is a CS/Math Major -> Sean Studies Math


Seeing this, it would be tempting to believe in rules such as:
  • And(s1, s2) -> s3 if Or(s1->s3, s1->s3)
This would be the case if we didnt' have Not, which is the source of all our No/0 values. But If we consider this case:

  • Suppose s1->s3 = 1. That is, Statement 1 doesn't tell us wether Statement 2 is True. Suppose s2 -> s3 = 0. That is, Statement 2 tells us that Statement 3 is False.
  • Our algorithm gives us the wrong answer. It gives 1 when it should give 0.
Clearly what is needed is a function like Or and one thats like And. I figured out what they should be and named the Or substitute Kind, the And substitute Cruel. I really don't know how the names came up in my head, they just did. They names just seem to fit well somehow.