First order logic (+ peano arithmetic etc)

Yesterday, I mentioned that proving a theorem in first-order logic is "semi-decidable" in that if the theorem is true then your program will halt in finite time, and if it is 

false, it may never halt. 

This probably didn't make much sense to you as none of you seemed to recognize the phrase "first order logic". Let me explain what it is (you all actually probably know about it without that particular name).

Suppose you have the statements:   All mortals will die. All men are mortal.  Socrates is a man. 

From this, you can conclude "logically" that Socrates will die.  First order logic supports doing this inference. Specifically, in the syntax of first order logic, the statements above are written as

FORALL_x  mortal(x) => dies(x)     

FORALL_y  man(x) => mortal(x)

man(SOCRATES)

The "theorem" you want to prove is

dies(SOCRATES)

==It is the proof of theorems like these that is semi-decidable (an informal technical reason is that that FORALL quanitification can be over infinite number of objects)==

Now, normal first order logic doesn't subsume arithmetic, and in particular, doesn't support mathematical induction (the rule that you may have used to prove the truth of statments such as  Sum of 1..n = n*(n+1)/2      You would have done this by showing that the formula holds for n = 1 (the base case); and showing that *if* it holds for n=k then it will hold for n=k+1, and thus by induction it holds for all numbers).  If you strengthen first order logic with mathematical induction, then for the resulting logic, Godel's incompleteness theorem holds--i.e., there may be theorems that are true given what you know, but you cannot prove that).

regards

Rao

ps: Boolean logic is also called propositional logic, and is a *weaker* logic than first-order one. Where as first-order logic assumes that the world is made up for objects and relations "predicates" between them, boolean logic believes that the world is made up just of atomic statements that are either true or false. 

So, P & Q => R is a boolean logic formula

M(a,b) & N(a) & L(b) => R(a,b) is a predicate logic formula