*something*,

*everything*,

*nothing*, logical connectives like

*and*,

*or*,

*if...then*or

*not*, and monadic predicates, which are attributions of a property to an individual object, like "the sky is blue" or "tomorrow is Tuesday". (In the first statement,

*the sky*is the object and

*blueness*is its property. In the second statement,

*tomorrow*is the object and

*being a Tuesday*is its property. That's pretty restrictive, but it's enough to capture the logic behind such truths as the argument:

Socrates is a man.Which can be restated in a way that makes its logic more obvious:

Man is mortal.

Therefore, Socrates is mortal.

If Socrates is a man and if something is a man then it is mortal, then Socrates is mortal.The validity of any proposition that can be constructed from only the above-mentioned concepts is decidable. By "validity" I mean the proposition is true independent of anything else. "If something is both large and round, then it is large" is true whether or not anything large and/or round actually exists. The above-mentioned proof of Socrates' mortality is valid, too. By "proposition" I mean the meaning of a declarative, true-or-false statement. By "decidable" I mean someone could write a computer program that would the determine any one of these proposition's validity, and it would work for any proposition.

So why have I been explaining all this? Because I wrote a computer program that does just that. It's not the first to do so, and it only works for propositions that contain five or fewer predicates, but I spend a fair amount working on it, so I'm going to share it, anyway.

**The Application**

The application runs from the command line. It takes one or more text files as command-line arguments. When you execute it, it will read each file and try to interpret it as a statement of monadic predicate logic. If it can, it will decide whether the contents are necessarily true (valid), possibly true (valid only if additional premises were added), or self-contradictory (necessarily false).

So, if I had an input file that contains the following text:

// All men are mortal.I would test it through the command prompt like this:

x,Hx->Mx

// Socrates is a man.

Hs

// Therefore,

->

// Socrates is mortal.

Ms

**The Language**

mpl.exe recognizes a particular language of symbolic logic. The language uses only ASCII characters available on American English keyboard. Its elements resemble either elements of ordinary symbolic logic or C-style bitwise operators. My intent is for the language to be unoriginal enough for someone who knows symbolic logic to be able to use it without much trouble. I'm too lazy to give a precise definition of the language, so I'll give a brief synopsis. If anyone has questions, I'll be happy to answer them.

The elements of the language are as follows:

- Ax - a predicate, A, predicated on one variable x. Predicates can be any character from A to Z. Variables can be any character from a to z. These are what represents attributions of a property to an object. mpl.exe will handle statements with an unlimited number of these, so long as they use no more than five different predicates.
- (,) - grouping by parentheses, just like in algebra.
- .,:,:., etc. - old school grouping, like in
*Mathematical Logic*. - x,... - universal quantification, i.e. "for all x, ... is true". The generalization extends to the end of the group it is in, e.g. "x,Ax&y,By->Cx" means the same as "(x,Ax&(y,By->Cx))", but not the same as "(x,Ax)&(y,By->Cx)".
- 3x,... - existential quantification, i.e. "there is an x such that ... is true". It also extends to the end of the group it is in.
- ~... - negation.
- ...&.. - logical AND.
- ...|... - logical OR.
- ...->... - material conditional, i.e. IF...THEN...
- ...<=>... - logical equivalence. &,|,-> and <=> all have the same precedence and are left-associative.
- // ... - comments; anything after them is ignored by mpl.exe.

((x,Hx->Mx)&Hs)->MsThis is the basic categorical syllogism. You can add comments by adding "//" and text behind it:

((x,Hx->Mx)&Hs)->Ms //the basic categorical syllogismmpl.exe will ignore anything behind "//" . If a line only contains a comment, mpl.exe will ignore it completely:

// the basic categorical syllogismA statement can be spread across multiple lines. mpl.exe treats separate lines as if they were separate operand in a logical conjunction, so

((x,Hx->Mx)&Hs)->Ms

means the same asAx|BxBx->CxCx

(Ax|Bx)&(Bx->Cx)&(Cx)If a binary operator is on a line by itself, every line before it is conjoined and treated as its left operand; everything after it is conjoined and treated as its right operand. So

x,H->Mxmeans the same as

Hs

->

Ms

This allows us to symbolize logical arguments and test their validity. Think of the first two lines in the text above as the premises of an argument and the last line as the conclusion. As with computer programs, comments can be helpful:((x,Hx->Mx)&Hs)->Ms

// All men are mortal.

x,Hx->Mx

// Socrates is a man.

Hs

// Therefore,

->

// Socrates is mortal.

Ms

**The Algorithm**

I won't say much about the algorithm right now, but I will say it is based on "possible worlds" semantics for logic. I will also say that it runs in O(2^

*n*^

*n*) time, where

*n*is the number of predicates mentioned in a statement; it does not scale well. On my computer, mpl.exe finishes instantaneously for statements with three or fewer predicates and finishes in about a second for a statement with four predicates. I haven't tried it, but I estimate it would take about a day to finish evaluating a statement with five predicates. I didn't bother to implement mpl.exe in such a way that it would support more than five predicates, considering how long it would take to do that.

**The Download**

Click here to download the application.

**The Future**

I plan on extending mpl.exe to handle identity and modal operators for possibility and necessity. Maybe soon.

## 2 comments:

Wow. What's binary for "parlez vous anglais?"

"1110000 1100001 1110010 1101100 1100101 1111010 100000 1110110 1101111 1110101 1110011 100000 1100001 1101110 1100111 1101100 1100001 1101001 1110011 111111". Foo!

Post a Comment