5 ms·

On a related note, does anyone know where I would look to understand reducibility of formal systems to one another? I'm really interested by questions like: W

by haliax 14y ago

On a related note, does anyone know where I would look to understand reducibility of formal systems to one another? I'm really interested by questions like: Why is second order logic irreducible to first order logic if I could use first order logic to reason about the behavior of a turing machine running a second order logic theorem prover with whatever inputs I like? How do I get something that can do what I can do, which is to say take any formal system and prove theorems with it? How do you determine what formal systems are "valid" logics? (Leading to sensible conclusions rather than nonsense like A & ~A)

Rickasaurus 14y ago
Godel Escher Bach is a great book (it's entertaining and informative) for learning about formal systems. There are general rules (rules of inference) for their construction from axioms that will keep you from going wrong.
- haliax 14y ago
  I've read it, but clearly didn't digest enough (a common problem I'm told :P). I will take another look, thanks!
  - JamesLeonis 14y ago
    If you didn't already know about it, there's a Reddit group that's doing a weekly readthrough and discussion. They're on chapter 13 currently. http://reddit.com/r/GEB http://reddit.com/r/GEB
    - Rickasaurus 14y ago
      Oh man, wish I had seen this sooner. It's been a quite a few years and I'd love to give it another read with a group.
    - haliax 14y ago
      Awesome, thanks!
  - nodemaker 14y ago
    My intelligence fails me whenever I try!
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 haliax 14y ago

Rickasaurus 14y ago

Godel Escher Bach is a great book (it's entertaining and informative) for learning about formal systems. There are general rules (rules of inference) for their construction from axioms that will keep you from going wrong.

haliax 14y ago
I've read it, but clearly didn't digest enough (a common problem I'm told :P). I will take another look, thanks!
- JamesLeonis 14y ago
  If you didn't already know about it, there's a Reddit group that's doing a weekly readthrough and discussion. They're on chapter 13 currently. http://reddit.com/r/GEB http://reddit.com/r/GEB
  - Rickasaurus 14y ago
    Oh man, wish I had seen this sooner. It's been a quite a few years and I'd love to give it another read with a group.
  - haliax 14y ago
    Awesome, thanks!
- nodemaker 14y ago
  My intelligence fails me whenever I try!

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.)