Wednesday, April 17, 2013

Necessity is not provability

A plausible account of necessity is that p is necessary provided that p can be proved in the correct logical system K and p is possible provided that its negation cannot be proved. Assuming K is axiomatizable and proves enough of the axioms of arithmetic, this account can be shown to be incorrect.

Fix any sentence s in K. It follows from Goedel's Second Incompleteness theorem that there is no K-proof of s's being K-unprovable (for if there were such a proof, then it would follow that there is a K-proof of K's consistency, since if K is inconsistent, then every sentence, including s, can be proved in K). But on the account of modality under consideration, this means that it is possible that s is K-provable, i.e., it is possible that s is necessary.

In other words, this account of modality implies that every sentence is possibly necessary. But it is absurd to think that 0=1 is possibly necessary!

I think much the same reasoning can be used to disprove Swinburne's account of necessity, since where we are not dealing with directly referential rigid designators, Swinburne's account agrees with the provability account.

I am skirting over distinctions between s and its Goedel number, but I think that's a mere technicality to work out in greater precision.

This makes for a nice way to see a relationship between the two incompleteness theorems. The first one tells us that not everything true is provable. From the second we learn that not even everything necessary is provable.


Michael Gonzalez said...

On this account would "impossibility" be identified as "negation is provable"?

Alexander R Pruss said...

Right, but the more usual (though equivalent) way to put that is that p is impossible iff a contradiction can be proved from p.

Richard Davis said...

Basic question about Godel's incompleteness theorems:

Does it prove that in any system of the relevant type, there are truths for which no proof exists; or does it prove that in any system of the relevant type, there are truths for which no proof-writing algorithm will ever write a proof? (Or even that for each proof-writing algorithm, there is some truth for which it will not write a proof?)

If it was only the second or third of these three, then I don't see why there'd be a problem for the necessity = provability thesis.

Alexander R Pruss said...

The first two. And they are actually equivalent. Suppose p has a proof. Then there is an algorithm that will generate a proof for p. The algorithm loops through all finite strings of symbols (first all the strings of one symbol, then all the strings of two, and so on) and for each one checks if it's a proof of p. If it is, it's done.

Richard Davis said...

Thanks, Alex. (Sorry --- should it be: thanks, Dr. Pruss?)

Do the incompleteness theorems work for second-order logical systems? How about systems with plural quantifiers?

Do the proofs assume that the natural numbers are not themselves statements in the system? I'm thinking about a certain system in which not only each mathematical object (including the natural numbers) but also each set and each mereological sum of mathematical objects is a statement in the system. For example, 1 is (literally is) the statement that something exists; 2 is the statement that two things exist; and so forth.

Alexander R Pruss said...

I think you can apply this to any sufficiently formal system that has sufficient expressive power.

I actually prefer to do Goedel stuff in terms of strings of characters rather than numbers, but the two approaches are equivalent.

By "sufficiently formal", I mean that there is an algorithmic procedure for checking whether a string of characters is a proof, and by "sufficient expressive power", I mean that there is enough expressive power to express that procedure in the language as well as to express some basic facts about strings of characters, like "c is the string formed by taking a and then putting b after it" and "c is the string formed by taking string a and replacing it with a quotation of itself".

Given the above, one can express in the language "There is a proof of s", and one can then come up with a sentence that says of itself that there is no proof of it (basically, you need a self-recognizing sentence). This sentence can't be false, on pain of self-contradiction, so it is true and hence unprovable. That's Goedel's first theorem. Then to get the second theorem, you basically run the proof of Goedel's first theorem within the language.

As far as I can tell--but I am not really a logician--none of this depends on the details of the proof procedures, the ontology of numbers, or the order involved, as long as proofs are algorithmically recognizable and the algorithms can be expressed in the language.

Richard Davis said...

Thanks greatly, Alexander. A concern about your argument:

Suppose that for every Cantorian cardinality C, there are at least C primitive predicates in K. I'm concerned that K isn't the sort of system that Goedel's Incompleteness Theorems have anything to say about. There are so many primitive predicates in K that there aren't enough strings of characters or enough Goedel numbers to pair them one for one with the primitive predicates in K.

So mightn't necessity = K-provability for some system K with as many primitive predicates as I've suggested?

Alexander R Pruss said...