You are quite right that Gödel's (first) incompleteness theorem attracts all kinds of bizarre "interpretations". Various examples are discussed and dissected in Torkel Franzen's very nice short book, Gödel's Theorem: An Incomplete Guide to its Use and Abuse, which I warmly recommend.

My guess is that a main source for the whacky interpretations is the claim that has repeatedly been made that the theorem shows that we can't be "machines", and so -- supposedly -- we must be something more than complex biological mechanisms. You can see why that conclusion might in some quarters be found welcome (and other technical results in logic generally don't seem to have such an implication). But as Franzen explains very clearly, it doesn't follow from the theorem.

No.

But that's no limitation on such a god's power. We're not saying that there is some possible task that this god fails to be able to pull off. We're saying that there isn't any task that is coherently describable as "making a square triangle".

For consider: what could possibly count as making a square triangle? To be a square requires having four sides. To be a triangle requires not having four sides but only three. So nothing can possibly count as being both a square and a triangle. Hence whatever the god (or anyone else) does, it couldn't correctly be described as "making a square triangle" for that isn't a coherent description of anything.

Take a mundane case. I pass you the cookies. You can take one. Or you can take none. Both are within your power. But you can't simultaneously both take one and not take one. But saying that plainly isn't to say that there is some limitation on your powers of choice vis-a-vis cookies! The point is that nothing could count as simultaneously both taking one and not taking one -- it's just not a coherent description of a possible action. Likewise to say that some god can't make a square triangle isn't to limit his creative powers: the point is that nothing could count as succeeding at that.

Perhaps part of the problem is the word "prove", which also tends to get used when talking about such things as the existence of God. (No-one can prove that God exists, we're often told.) As our erstwhile leader, Alex George, has often pointed out, however, outside mathematics, one can rarely "prove" anything. So to be told in that sense that no-one can "prove" a negative is unhelpful. One can't "prove" a positive in that sense, either.

As Peter said, more or less.

I'm reminded of the exasperated Bertrand Russell faced with the young Wittgenstein: "He thinks that nothing empirical is knowable. I asked him to admit that there was not a rhinoceros in the room, but he wouldn't. I looked under all the desks without finding one but Wittgenstein remained unconvinced." It is Wittgenstein here who is being obtuse and in the grip of a silly theory. Of course we can establish empirical propositions both positive and negative – for example, that there are five desks in the room and no rhinoceroses.

By any sane standard, it is just plain false that you can't prove a negative, and that supposed "discussion-killer" should itself be promptly killed off.

Same as they are if God does exist. The idea that God (if such there be) has control over truths of math and logic is one that a few philosophers have argued for (Descartes, for instance, if I'm not mistaken) but even staunch believers in omnipotence typically understand omnipotence in a way that doesn't call for the puzzling idea that God could change the laws of logic. Briefly, the view of many theists would that God can perform any logically possible task.

One reason for saying that is that logical "constraints" help us make sense of what omnipotence might mean.Why anyone would want more is hard to fathom. Suppose someone asked God to light up a set of pixels on an infintely high-resolution screen so that these pixels made a figure that was perfectly round and perfectly square. What would count? Is there actually a genuine task to be done here? If not, then it hardly seems to be a limitation on God's power (or anyone else's) that s/he can't complete the task.

The number of victims is not the only consideration entering into the judgments of whether a genocide is taking place. Other relevant factors are the nature and size of the victim group and the motivations and intentions of the perpetrators. Still, we can hold these other factors fixed and ask your question again, for example: hypothetically lowering the number of people killed, maimed, raped, and otherwise brutalized in the Rwanda genocide, when do we reach the point at which the genocide label would no longer be applicable? Or: at what time, in those horrible months of early 1994, did the daily decision of the world's leading governments not to intervene become a decision to ignore a genocide?

You're right that there is some vagueness here. But this does not render the term meaningless. As Wittgenstein writes, there may be some unclarity about where exactly the boundary lies between two countries -- say between China and Russia -- but this does not entail that it's unclear on which side Beijing or Moscow fall. Similarly, for many terms widely used in the criminal law, terms like "negligent," "reckless," "due diligence," "reasonable person," and so on. Even the word "kill," which you seem to find unobjectionable, is subject to a Sorites problem. Suppose you hurt someone and, as a result, she dies earlier than she would otherwise have done. Have you killed her? Surely yes, if she dies within seconds of your action. Presumably no, if she lives another 80 years rather than 81. So how long exactly must she survive for you to escape the killer label?

We confront and resolve such questions all the time in legislation and jurisprudence, and the borderlines are surely arbitrary to some extent. Here "genocide" is basically in the same boat with lots of other terms and, if we tossed all those terms overboard, we'd have very little language left.

Peter always gets to these before I do. I agree with what he says, but will add a couple points.

First, modern logic emerges in the work of Gottlob Frege, one of whose contributions was the first formal system of logic. Frege is explicit about his motivations. Here's a passage from his paper "On Mr Peano's Conceptual Notation and My Own", from 1897:

"I became aware of the need for a concpetual notation [formal language] when I was looking for the fundamental principles upon which the whole of mathematics rests. ...For an investigation such as I have in mind here, it is not sufficient just for us to convince ourselves of the truth of a conclusion, as we are usually content to do in mathematics; on the contrary, we must also be made aware of what it is that justifies our conviction, and upon what primitive laws it is based. For this are required fixed guiding-lines, along which the deductions are to run; and in verbal languages these are not provided. If we try to list all the laws governing the inferences which occur when arguments are conducted in the usual way, we find an almost unsurveyable multitude which apparently has no precise limits. The reason for this, obviously, is that these inferences are composed of simpler ones. And hence it is easy for something to intrude which is not of a logical nature and which consequently ought to be specified as an axiom. This is where the difficulty of discerning the axioms lies: for this the inferences have to be resolved into their simple components."

So Frege's motivation was this: We want to know on exactly which assumptions a given theorem rests. But, even if we specify our assumptions clearly in advance, how we be sure some other, as yet unspecified assumption has not tacitly been made somewhere along the way? Answer: We can be sure, if we carry out our argument in a formal language and clearly specify the forms of inference we are going to use in such a way that it is always possible to tell, on purely formal grounds, whether we have indeed reasoned in accordance with those rules.

Nowadays, people rarely carry out arguments in formal systems---except for students in logic classes. But that does not mean that formal argument has become any less important. It is, rather, that we have a developed a good sense for what such reasoning is like, and we can usually tell pretty well when an informal argument could or could not be carried out in such a system. But when things become unclear, then people who are interested in the sort of question in which Frege was interested---logicians---do start formalizing things, if not to the same degree Frege did, then at least to some degree. I've recently had to do just that sort of thing myself in a study of the question what sorts of principles are involved in "semantic" consistency proofs.

One other point. Both in Peter's remarks and in my preceding remarks, the focus is primarily on what logicians call "soundness": Formal arguments can be used to establish the validity of inferences, because what is formally derivable really does follow. There are other things to be said about the significance of completeness: the fact that all valid first-order inferences can be derived using an appropriate set of formal rules. This is extremely important to the study of the notion of computation as it relates to formal theories. Peter's other book, An Introduction to Gödel's Theorems, is a nice introduction to that material.

Logic is about what follows from what. But what follows from what isn't always obvious (or else, e.g., pure maths would be a lot easier than it is). So we need ways of demonstrating unobvious entailments.

And a standard way of doing this is to show how we can get from the given premisses to the intended conclusion by a sequence of small steps, each of which is guaranteed to be truth-preserving. If we can break down the big inferential leap from premisses to conclusion into smaller inferential moves, each one of which is evidently valid, that shows the big leap is valid too.

Now all this applies equally to informal reasoning -- e.g. derivations or proofs in informal mathematics -- and to formally tidied-up reasoning alike. There's nothing mysterious then about derivations in formal logic. They just do in a regimented way, in some tightly constrained formal language, the sort of thing we usually do in a less regimented way. And given a formal version of a proof, we can read back an informal, ordinary-language version of the proof (at the risk of prolixity and getting tangled with quirks of the vernacular).

For more about the notion of a proof or derivation, and about the relation between informal and formalized versions, see any introductory logic text. E.g. my An Introduction to Formal Logic (Ch. 5 on proofs, Ch. 7 on why we might want to go formal).

Note, desiring something isn't needing it. I may desire a villa in Tuscany, but I don't need one. And, whatever is the case with needs, plainly it isn't the case that for every human desire there is a way of fulfilling it (especially given other people's desires). Maybe lots of us would love a villa in Tuscany; but we can't all get one. And in fact we often desire flatly impossible things. Lots of humans would love to time-travel: but of course that desire doesn't make it possible. And maybe lots of us would love to live for ever: but there's no reason to suppose that merely having the desire makes eternal life possible either.

I'm really glad you enjoyed the Gödel book!

I don't know if anyone has actually tried to prove that establishing Goldbach Conjecture needs additional axioms added to "regular arithmetic". But if someone had succeeded we would certainly have heard a lot about it!

Why so? Well, suppose T is your favourite theory of "regular arithmetic" (and we can assume T contains at least Robinson Arithmetic, Q). And suppose we can show that GC can't be proved by T as it stands. Then, trivially, T + not-GC is consistent. So, since GC is a Pi₁ sentence, it follows from Theorem 9.3 of my book that GC is true! In other words, proving GC can't be proved by T in fact proves Goldbach's Conjecture.

So we can put it this way: if it does need new axioms to establish GC, then proving that is so is at least as hard as proving Goldbach's Conjecture itself. Which, the evidence suggests, is very hard!

As to the "odds": my hunch is that GC is true, and can be proved in PA -- but I wouldn't bet even a decent meal out on it!!