Investigating Logical Arguments with somerby.net/mack/logic

I created a web application that evaluates logical arguments.  To provide an example of how it might be used, I'm going to use it to help me do a brief investigation of two modal arguments about the existence of God.  The first is Alvin Plantinga's modal argument for the existence of God.  The second is Juan Manuel Correa's counter-argument against the existence of God (or at least against the soundness of Plantinga's argument).  Statements of both arguments can be found on Wikipedia at http://en.wikipedia.org/wiki/Ontological_argument#Alvin_Plantinga.

First off, I'm going to strip the arguments down to what I think is the essential logic that makes both arguments work.  I don't suppose this will be agreeable to everyone, at least not without some persuasion, but I'll just go with it for now and try to defend myself later if I have to.  So, for Plantinga's argument I will use:

<>G->[]G
<>G
->
G

Which is saying,

• If God exists in some possible world, God exists in every possible world.
• There is a possible world in which God exists.
• Therefore, God exists.

For Correa's counterargument, I will use:

<>G->[]G
<>~G
->
~G

Which is saying,

• If God exists in some possible world, God exists in every possible world.
• There is a possible world in which God does not exist.
• Therefore, God does not exist.

 The web application, which, in this post, I will call "the decider", decides that both arguments are valid.  So what's going on?  There are three premises between the two arguments, and each seems plausible.  I suspect the fact that both arguments are valid in spite of their contradictory conclusions means that the three premises are logically inconsistent with each other.  So I try them out in the decider:

<>G->[]G
<>G
<>~G

It tells me they are impossible, i.e. logically inconsistent with each other.  So we can't believe all of them at once.  Which one should I doubt?

Before I try to answer that question, I want to check that neither argument is trivially valid.  I mean, I want to be sure that neither conclusion follows from its premises simply because those premises contain a contradiction and anything follows from a contradiction.  So I test the premises by themselves in the decider.

<>G->[]G
<>G

Then

<>G->[]G
<>~G

The decider says both pairs are contingent.  So no problem there.   What about the two differing premises?  The decider says

<>G & <>~G

is possible, which it just what I expect, so I could believe both.  Which is what I'm inclined to do.  I can imagine a world with God, and I can imagine a world without God.  Of course, just because I can imagine them doesn't mean that there is not some contradiction hiding in either conception.  But I'm still most inclined to drop Premise #1.  It's obvious that []G and <>~G are incompatible, and it's not clear to me that there ever could be such a thing as a necessary being.  Some logics entail that at least one being must exist; See Proposition 24.52 in Principia Mathematica for one.  Even so, just because you can prove that at least one object exists doesn't mean you can prove that it has any nontrivial properties, like divinity.  And I'm not enamoured of the idea that God has every possible perfection; necessary being being one of those perfections.  Clearly, if a being has every possible perfection, it must smell like freshly-baked chocolate chip cookies at least some of the time.  And play a face-melting guitar solo every time it picks up a guitar.  Unless someone is taking a nap within earshot.  But I'm a Christian, and I'm sure both of these perfections are irrelevant to the Gospel, so I don't care.

So, to conclude, I will assert 1. that God exists in some possible world.  2. There is a possible world where God doesn't exist.  Therefore, Premise #1 is false.  

To summarize my reasoning in symbolic form:

<>G
<>~G
[]( (<>G&P) ->  C )
[]( (<>~G&P) -> ~C )
->
~P

Where  P is premise #1, C is the conclusion of  Plantinga's argument, and G is as defined above.

The decider confirms that this argument is valid.

One more thing I'd like to point out: when considering modal arguments for the existence of God, one should be careful about the statement "It is possible that God exists."  It might be interpreted two different ways.  First, as "there is a possible world in which God exists".  The second, as "I don't know anything that precludes the existence of God."  The first is easy to represent in terms of modal logic, but the second is the more natural interpretation.  In my analysis, I assumed the first.  If I were to choose the second interpretation, my analysis of these two arguments would have to be different.

Linking Ada, C and Haskell Together Statically

So, you want to statically link object code from C, Ada and Haskell into one executable? Probably not. But how could that be done, anyway? Many programming languages provide a means both of exporting subroutines to make them callable from C code and importing C functions so they can call them. You can easily find documentation on how to statically link C to one other language. But what if you want link C with two different languages in the same project? Just compile all of the code separately and link the object files, right? Haha. Not so fast! Programming languages have different run-time systems; they have their own libraries and they may use more than just a stack and a heap and a space for global variables. So if you want to include object code from several languages in a single executable, you'll often have to build run-time code for each application and link it in to the executable as well. In this post, I'm going to demonstrate how you can accomplish this in a project that uses C, Ada and Haskell.

Click here.

somerby.net/mack/logic

Here's a web application that decides simple statements in a fragment of first-order symbolic logic: somerby.net/mack/logic. It's based on that .NET console application I was calling "Monadic Predicate Logic".

Perl Poetry

I think Perl poetry is pretty cool. I should write some sometime. I've made one or two attempts, but being the lazy programmer I am, instead of actually finishing any Perl poems, I wrote a Perl module that facilitates the writing of Perl poetry. The module is based on one observation: plain English text, especially the kind you would find in a poem or a novel, is often very close to being syntactically valid Perl. In fact, were you to declare a Perl operator (that is, a subroutine whose arguments don't need to be wrapped in parentheses) for each word that is not already a Perl keyword in some English text, the text would only need small changes to become a syntactically valid Perl script that executes without warnings or errors. The Perl module I wrote does just that: if you use it in a Perl script, it pre-reads the script and declares operators for each bareword that is not a keyword.

• Download: perlify.pm

To show how it works, here's an example. This is not a valid Perl script:

As I walked through the wilderness of this world, I lighted on a certain place where was a den, and laid me down in that place to sleep; and as I slept, I dreamed a dream. I dreamed, and behold, I saw a man clothed with rags, standing in a certain place, with his face from his own house, a book in his hand, and a great burden upon his back.  I looked and saw him open the book, and read therein; and as he read, he wept and trembled; and not being able longer to contain, he brake out with a lamentable cry, saying, "What shall I do?" 

This is a valid Perl script:

use perlify;

As I walked through the wilderness of this world, I lighted on a certain place where was a den, and laid me down in that place to_sleep; and_as I slept, I dreamed a dream. I dreamed, and behold, I saw a man clothed with rags, standing in a certain place, with his face from his own house, a book in his hand, and a great burden upon his back.  I looked and saw him open_the book, and read_therein; and_as he_read, he wept and trembled; and_not being able longer to contain, he brake out with a lamentable cry, saying, "What shall I do?"

 They are not very different. To convert the text to a working Perl script, I just used perlify.pm and changed some spaces to underscores to prevent the text from calling certain Perl operators without the correct number of arguments. The default action for a word in this text is to print itself and then return 1. The output of the script is

world den a was where place certain a on lighted I this of wilderness the through walked I As to_sleep place that in down me laid slept dream dreamed I a dreamed I I and_as behold rags place house hand his in book a own his from face his with certain a in standing with clothed man a saw I back looked I his upon burden great a book open_the him saw read_therein he_read wept he and_as trembled contain cry saying lamentable a with out brake he to longer able being and_not

 This example isn't especially creative, but there are ways to embellish it to make it more interesting.

One more thing: if you read perlify.pm, notice a variable named "our $callback".  If you care enough to use the module, I probably don't need to tell you what to do with it.

Drum Machine Joy!

I made a drum machine.  Actually, a web page that's a drum machine.  It's all in the browser, HTML5 and Javascript.  It works in Firefox, Chrome and Safari, but not Internet Explorer.  It's fully functional, but it could use some more features.

Monadic Predicate Logic with Some Modal Operators

I have a new version of the monadic predicate logic program that I posted a while ago.  It has operators for possibility and necessity (<> and [], respectively).  They bind to sub-expressions the same way negation (~) does; they bind to the nearest existential or universal quantifier to the right, or, failing that, the nearest predication to the right, so <>Px&Py is equivalent to (<>Px)&(Py) but not <>(Px&Py).  <>x,Px&Py is equivalent to <>(x,Px&Py) but not (<>x,Px)&Py.  I'm posting it and its source code, now that I have written a parser that I'm not ashamed of.  The one downside is that it no longer supports the "old school" dot grouping.  If any one wants to use it, tell me and I'll add it back in.  If anyone uses this program at all, tell me!

• Download mpl.exe and some example logic files.
• Download the source code.

Setting Local Variables in Visual Studio

Have you ever wanted to change the value of a local variable inside of a method?  Without changing its code or pausing it in the debugger, that is?  Maybe not, but I did, while writing a unit test this week.  I figured out how to do it in Visual Studio, using Visual Studio's DTE object.  The DTE object provides a programmatic interface to Visual Studio's debugger.  With it, breakpoints can be set and deleted programmatically.  But what about changing the variable?  Breakpoints can have conditions, so...

using EnvDTE;
using System.Runtime.InteropServices;

...

// Get the DTE object.
DTE lDTE =
  Marshal.GetActiveObject( "VisualStudio.DTE" ) as DTE;

// Set a conditional breakpoint.  In this example, the
// break is in file.cs, line 422.
lDTE.Debugger.Breakpoints.Add(
  null,
  "file.cs", 
  422,
  1,
  // Use the break condition to set the local variable
  // you want changed.  Note that the expression always
  // returns false; the debugger will assign 1 to
  // lVariable every time the condition is evaluated,
  // but never pause the unit test.
  "(lVariable = 1.0f).ToString() == null",
  dbgBreakpointConditionType
    .dbgBreakpointConditionTypeWhenTrue,
  null,
  null,
  0,
  null,
  0,
  dbgHitCountType.dbgHitCountTypeNone );

// Call that method...
...

// Delete the breakpoint if you don't want it
// to affect later code.
lDTE.Debugger.Breakpoints.Item( 1 ).Delete();