Monadic Predicate Logic

Suppose we restricted our thoughts to the concepts of  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.
Man is mortal.
Therefore, Socrates is mortal.

Which can be restated in a way that makes its logic more obvious:

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.
x,Hx->Mx
// Socrates is a man.
Hs
// Therefore,
->
// Socrates is mortal.
Ms

I would test it through the command prompt like this:

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.

Basically, mpl.exe expects an input file to contain a single statement.  The contents of a file might look like this:

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

This is the basic categorical syllogism.  You can add comments by adding "//"  and text behind it:

((x,Hx->Mx)&Hs)->Ms //the basic categorical syllogism

mpl.exe will ignore anything behind  "//" .  If a line only contains a comment, mpl.exe will ignore it completely:

// the basic categorical syllogism
((x,Hx->Mx)&Hs)->Ms

A statement can be spread across multiple lines.  mpl.exe treats separate lines as if they were separate operand in a logical conjunction, so

Ax|Bx

Bx->Cx

Cx

means the same as

(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->Mx
Hs
->
Ms

means the same as

((x,Hx->Mx)&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:

// 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.