Formal Philosophy Tutorial

Philosophical, mathematical and computational logic, linguistics, formal argument, game theory, fallacies, paradoxes, puzzles and other related issues.

Formal Philosophy Tutorial

Postby xcthulhu on February 24th, 2009, 11:09 am 

What is Formal Philosophy?

Formal philosophy is the practice of employing mechanized, logical reasoning for settling philosophical disputes and aid in inquiry. The idea dates back to a quote due Leibniz:

Gottfried Wilhelm Leibniz wrote:If controversies were to arise, there would be no more need of disputation between two philosophers than between two accountants (Computistas). For it would suffice to take their pencils in their hands, to sit down to their slates (abacos), and to say to each other…: Let us calculate (Calculemus).
[taken from]

Historically, only a handful of logicians and theoretical computer scientists were aware of how to do this. However, I recently have been inspired by the work of Ed Zalta, and I believe anyone with basic knowledge of philosophical reasoning may do this.

This FAQ shall be centered around prover9/mace. This is a computer system for automated deduction and model construction, available for Windows/Linux/MacOSX. Specifically, prover9 is capable of providing proofs and counter models. Thus, it is suitable for the investigation of whether a proposition or equation follows from a set of assumptions or not. As will be demonstrated, one may also use it to illustrate that a set of assumptions is consistent; that is, that they will not deduce a contradiction.

I urge that essentially anyone can use prover9 to aid in thinking about philosophy, if they so desire. It is safe for a casual user to employ without knowing any of the theory behind it. If you can reason argumentatively, and know how to typeset HTML or program in some computer language, then you learn how to use prover9.

Throughout this tutorial, I shall demonstrate how to investigate arguments in philosophy using prover9. I shall illustrate how to translate them into the language of prover9, and how to check whether this translation is valid or not. I shall on occasion introduce a few key ideas from formal logic, but I assume no prior background.
Last edited by xcthulhu on February 24th, 2009, 7:11 pm, edited 2 times in total.

The Barbara and Celerant Syllogisms

Postby xcthulhu on February 24th, 2009, 4:49 pm 

The Barbara and Celerant Syllogisms

The very first syllogism we shall investigate in this tutorial is the Barbara syllogism. Barbara is the medieval mnemonic for the following inference pattern:

Wikipedia - Barbara Syllogism - wrote:All men are animals
All animals are mortal
All men are mortal

Just about everyone can recognize this as logically valid. Note that I am following the wikipedia entry on syllogisms, which are elementary logical reasoning patterns. This is to give a common point of reference. Furthermore, I shall employ the symbol "" stand for "Therefore", introducing a conclusion to an argument.

We now turn to verifying that this syllogism is true in prover9; we assume the reader has installed the program, following the link above. In the "Assumptions" box, input:

Code: Select all
all x (man(x) -> animal(x)).
all x (animal(x) -> mortal(x)).

This input reads "Forall x, if x is a man, then x is an animal" and "Forall x, if x is an animal, then x is mortal". Note the placement of parentheses. This is important, since otherwise "forall x" binds to "man(x)" and this reads "If all x are men, then every x is mortal", which is actually weaker than what we are reasoning.

We now input the "Goals":

Code: Select all
all x (man(x) -> mortal(x)).

This reads "Forall x, if x is a man, then x is mortal", exactly as in the syllogism.

Now hit "Prove" in the proof search box. In less than a second, a window should appear. It will have a lot of text, and some output:

Code: Select all
1 (all x (man(x) -> animal(x))) # label(non_clause).  [assumption].
2 (all x (animal(x) -> mortal(x))) # label(non_clause).  [assumption].
3 (all x (man(x) -> mortal(x))) # label(non_clause) # label(goal).  [goal].
4 man(c1).  [deny(3)].
5 -man(x) | animal(x).  [clausify(1)].
6 animal(c1).  [resolve(4,a,5,a)].
7 -animal(x) | mortal(x).  [clausify(2)].
8 mortal(c1).  [resolve(6,a,7,a)].
9 -mortal(c1).  [deny(3)].
10 $F.  [resolve(8,a,9,a)].

Throughout this tutorial, I shall be ignoring this output. What prover9 is doing is insanely technical - we are seeing the output of the machine reasoning technique that prover9 employs. Specifically, it employs resolution based theorem proving, combined with unification including modulation and paramodulation, as well as Skolemization for handling existential operations. This method is extremely fast but does not produce proofs suitable for a person to follow. For those curious about how prover9 works, I shall defer them to the documentation.

The output is not what we are interested in; the point is
prover9 managed to prove the deduction!

If you have followed this tutorial so far, then you have verified your very first result in formal philosophy.

Another syllogism we might like to look at is the Celerant syllogism (perhaps the most widely known syllogism):

Wikipedia - Celerant Syllogism - wrote:All men are mortal
Socrates is a man
Socrates is mortal

We can now turn to inputting this into prover9:

Code: Select all
all x (man(x) -> mortal(x)).


...and sure enough, when we hit "Prove", prover9 gives us a proof.

Hopefully if you have been following, you have managed to verify these very simple arguments, too. Next, I'll go over Mace, which is a tool for constructing counter-examples.

Consistency Checking

Postby xcthulhu on March 21st, 2009, 7:28 pm 

Consistency Checking and Countermodels

In formal logic, we define consistency to mean that something has a model; see the wikipedia entry on this. This is the common definition employed by most modern logicians. So under this definition, if a sentence is consistent it must have a model. In this entry in the Formal Philosophy tutorial, I'll show you how to have a computer automatically generate a model of a consistent theory.

In another thread, another author wrote:

Hardstreet wrote:Previously I've used the example of time and color: "I leave for work at 9AM and my favorite color is green." The two parts of that statement are true (for the purposes of example), and they are perfectly consistent...

We shall now formally verify that they are consistent. The easiest way to check is to formalize "I leave for work at 9AM and my favorite color is green." There's always a variety of ways to do this, so proper formalization is occasionally something people argue about. But in a computer system you are of course free to play around with a variety of formalizations at your leisure. I'll do a simple one. Fire up prover9 and input the following into Assumptions:
Code: Select all

Now go to "Model/Countermodel Search" and hit "Start". In a second, prover9 will come up with a model, probably like this one:
Code: Select all
interpretation( 2, [number = 1,seconds = 0], [
    function(green, [0]),
    function(me, [0]),
    relation(Leaves_for_work_at_9AM(_), [1,0]),
    relation(Favorite_color_is(_,_), [

Obviously, the output is a bit technical. Many computer scientists think of first order models like computer databases, which is how I am going to think about what we are seeing. You can use the "Reformat" button to change this into other forms which make it clearer what is going on. I shall interpret this output for you, however.

Essentially what mace did was make a model with two two mathematical objects, 0 and 1. It declared two constants, me and green, to denote the number 0. As a peculiarity of prover9's design, it denotes constants as nullary functions, ie functions that take no argument.

Anyway, mace also invented a predicate and a relation, Leaves_for_work_at_9AM(x) and Favorite_color_is(x,y). In this case Leaves_for_work_at_9AM(x) takes one argument and Favorite_color_is(x,y) takes two arguments. In both cases, the argument is suppose to be a term, like me or green. Mace says that in the model it made, Leaves_for_work_at_9AM(x) is true when it's input is 0, and false when it is 1. It also says that that Favorite_color_is(x,y) is only true when both x and y are 0.

We could jot this down and verify that this model makes true the assumptions we said, but in this case, we can make prover9 verify it for us. Go to the reformat button and hit "Cooked", it should give the following output:

Code: Select all
green = 0.

me = 0.

- Leaves_for_work_at_9AM(1).

- Favorite_color_is(0,1).
- Favorite_color_is(1,0).
- Favorite_color_is(1,1).

Copy this, and go back to the "Assumptions" and "Goals" window in prover9. Clear the assumptions, and paste this output into assumptions. Now paste our original assumptions in goals, ie, copy this and past it into goals:

Code: Select all

We are going to have prover9 logically derive our premises, from it's own logical specification of the model of our premises it made. Go over to "Proof Search" and hit start. In a second it will have a proof (it also gives me a weird error, I don't know what that's about).

You are probably thinking "This is crazy! I'm not a number, I'm a free man! And neither is green! And even if we were numbers, we wouldn't be identical!" Mace, and like a typical logician, doesn't really care if the models it generates are sensible. They are just intended to be little databases that make true all of the assumptions. There's nothing, logically, that says that you, 0, and green can't be identical.

A better way to understand what is going on is to understand that while Mace makes models, which are good for proving your assumptions are consistent, but it also makes countermodels. A countermodel in this program is something that makes all of the premises true and the goal false.

Here's an example. Suppose I put in the old premises about going to work at 9AM and favorite colors, and put in my goal
Code: Select all

Now, suppose I sat down to prove that if I go to work at 9AM and my favorite color is green, then I rock out to Iron Maiden. I'd be at the task until my grave, and the logicians would write "Idiot" on my tombstone. 'Cause you can't prove if this conclusion from it's premises. Why can't you? I certainly rock out to Iron Maiden in real life. But the reason you can't deduce it from the premises because there is a counter example. How do I know there is a counter-example? ...I just made MACE make me one. You can too! Go over to "Model/Counterexample search" and hit start, and in a second it will come up with a counter-example. You can interpret its output yourself.

Hardstreet wrote:Or think of a physical model. I want to build a model of a vehicle, and the pieces I've got so far are a wheel, a carburetor, and the Statue of Liberty. What are you going to do with that?

Well, in mathematical modeling like I just described, our universe consists of integers (that is to say, we have an infinite number of objects to build with). Mace rarely has a dearth of mathematical objects to work with; it only has trouble when my premises state I have an infinite number of objects. This is a real technical limitation for Mace; I shall write on it sometime.

That's all for now!

Re: Formal Philosophy Tutorial

Postby HappyMan on June 10th, 2009, 10:51 pm 

You are not all that I am.
I am not all that you are.
I am a man.
.'. You are not me.

You are not what I am.
I am a man.
.'. You are not a man.

Can you explain the difference in these two?

Re: Formal Philosophy Tutorial

Postby nameless on May 28th, 2017, 3:19 am 

xcthulhu » Tue Feb 24, 2009 8:09 am wrote:What is Formal Philosophy?

Formal philosophy is the practice of employing mechanized, logical reasoning for settling philosophical disputes and aid in inquiry.

And thus is it's failure to encompass Reality.
Once, a true philosophical mind was a path into the Light, like any such 'path'; Jnana yoga is the yoga of the philosophers.
In this age, where 'thought' is so degraded and on it's deathbed/insane that it is no longer recommended yoga.
Any 'philosophy' relegated to the mechanized formal logic, will always fall short!
Philosophy entails original critical thought, 'logic' and experience and intuition and any and all human means of Knowing!

Charles Sanders Peirce required that the first and primary obligation of any philosopher or scientist is to do nothing that would block inquiry...
(Such as reducing it to some formalized robotic equations)

Speaking of 'logic', are you aware that quantum mechanics has refuted every single one of Aristotle's 'Laws' of Logic!?
For example;
A=A AND A=/=A AND A sometimes = A AND ... AND all this "at the same moment"!
It is still a bit pragmatic for 'thoughts' (ego), but throwing rocks was pragmatic... until bullets!
So using some form of 'logic' as one's total philosophical system, discarding others, is an error.

Holy crap, I keep answering years old threads.
Seems that things could be simplified with newer posts and years old posts right next to them.
Oh well, there are no accidents...
Banned User
Posts: 145
Joined: 01 Dec 2007
Location: Here! Now!

Re: Formal Philosophy Tutorial

Postby wolfhnd on May 28th, 2017, 2:01 pm 

At it least has substance and avoids ideological digression.

Return to Logic

Who is online

Users browsing this forum: No registered users and 4 guests