3 ms·

'Reducibility' in general is an informal notion, and as such there are many different technically precise ways of capturing aspects of it. Mutual interpretabili

by ionfish 14y ago

'Reducibility' in general is an informal notion, and as such there are many different technically precise ways of capturing aspects of it. Mutual interpretability and bi-interpretability are two of these, but they apply to formal systems with the same underlying logic (that is, the same semantics and proof theory). There are also many other notions of translation between different logics like Gödel–Gentzen negative translation between classical logic and intuitionistic logic. I'm not sure if there is a good introduction to all of these different ways of capturing reducibility, but you could try asking on math.stackexchange.com, there are usually helpful responses to reference requests there. Second order logic does not have a complete proof theory, so your Turing machine will not be able to compute the consequences of a theory formulated in second order logic. This can be avoided by employing Henkin semantics, but then you're not working with full second order logic anymore. Stewart Shapiro's 2000 book, Foundations without Foundationalism: A Case for Second-Order Logic has the technical details should you be interested.

haliax 14y ago
> Second order logic does not have a complete proof theory Is this different from saying that second order logic contains unprovable true statements / that the incompleteness theorem applies? Also thanks for the really well informed response!
- ionfish 14y ago
  One of the features of first order logic is that the provability relation is recursively enumerable: given any recursive first order theory, there is a Turing machine that can list every theorem of that theory (although of course it will run forever). Additionally, first order logic is complete: for every statement true in all models of a theory, there is a proof of the statement from the theory. These two constraints cannot both be satisfied in a sound deductive system for second order logic. To see that this is so, consider that in second order logic we can prove Dedekind's categoricity theorem: there is only one model (up to isomorphism) of the second order Peano axioms (PA2). Let's assume that the provability relation for second order logic is recursively enumerable. We know from Gödel's incompleteness theorem that the set of first order sentences true of the natural numbers is not recursively enumerable. So take a sentence of the form "If PA2 then _" for some sentence _ which is in that set but not in the extension of the provability relation (this is a legitimate statement since the PA2 axioms are finite so we can just take their conjunction). This should be a logical truth of second order logic, but it's not provable (by the argument just given), so second order logic is incomplete: there are statements which are logical consequences yet are unprovable. So in other words, yes, the incompleteness theorem is very much at play in this limitation of second order logic. For the technical details I very much recommend chapters 3 and 4 of Shapiro's book; it's not terribly expensive, and any decent university library should have a copy. (A small footnote to my earlier post: Shapiro's book originally came out in 1991, not 2000—that's just the date of the paperback edition, and I'm unsure as to whether there are any substantial differences between the two.)

by ionfish 14y ago

haliax 14y ago

> Second order logic does not have a complete proof theory Is this different from saying that second order logic contains unprovable true statements / that the incompleteness theorem applies? Also thanks for the really well informed response!

ionfish 14y ago
One of the features of first order logic is that the provability relation is recursively enumerable: given any recursive first order theory, there is a Turing machine that can list every theorem of that theory (although of course it will run forever). Additionally, first order logic is complete: for every statement true in all models of a theory, there is a proof of the statement from the theory. These two constraints cannot both be satisfied in a sound deductive system for second order logic. To see that this is so, consider that in second order logic we can prove Dedekind's categoricity theorem: there is only one model (up to isomorphism) of the second order Peano axioms (PA2). Let's assume that the provability relation for second order logic is recursively enumerable. We know from Gödel's incompleteness theorem that the set of first order sentences true of the natural numbers is not recursively enumerable. So take a sentence of the form "If PA2 then _" for some sentence _ which is in that set but not in the extension of the provability relation (this is a legitimate statement since the PA2 axioms are finite so we can just take their conjunction). This should be a logical truth of second order logic, but it's not provable (by the argument just given), so second order logic is incomplete: there are statements which are logical consequences yet are unprovable. So in other words, yes, the incompleteness theorem is very much at play in this limitation of second order logic. For the technical details I very much recommend chapters 3 and 4 of Shapiro's book; it's not terribly expensive, and any decent university library should have a copy. (A small footnote to my earlier post: Shapiro's book originally came out in 1991, not 2000—that's just the date of the paperback edition, and I'm unsure as to whether there are any substantial differences between the two.)