4 ms·
"Strong" and "weak" have well-understood meanings in mathematical logic and model theory. For example, imagine there's a true and "important" statement S about
by jfarmer 13y ago
"Strong" and "weak" have well-understood meanings in mathematical logic and model theory.
For example, imagine there's a true and "important" statement S about Turing machines for which we could prove "it is impossible to prove S using provability logic." In that sense PL would be "too weak" to do computer science.
- EGreg 13y agoOkay, but what is "very weak"? Also, I remember you - you did adonomics back in the day for facebook apps :)
- jfarmer 13y agoHe's just speaking colloquially and I don't know anything about the system of logic he's describing. He means something like "weak relative to all the other ones we'd consider on a day-to-day basis" or "so weak we'd never seriously consider it except as a specialized tool." That's not really the point, though. The point is that "strong" and "weak" are well-defined terms in mathematical logic and he was almost certainly using them in that sense. :)
- EGreg 13y agoI think he was saying that their math-fu was weak, too weak for comp sci :)
- deleted 13y ago[deleted]
- jfarmer 13y agoNo, he's almost certainly not. Keep in mind, I know nothing about PL. I'm solely relying on my background as a mathematician to think of the most reasonable interpretation for what he's saying. He's saying something like, "You can axiomatize Peano Arithmetic in PL and explore the idea of provability therein because that's what PL was invented for. At first glance we might try to use something like PL to do what we're setting out to do, but it's so specialized that it winds up not being worthwhile." This makes more sense in the context of his paper, anyhow. Gödel's Incompleteness Theorem basically says that Peano Arithmetic can't prove its own consistency within PA unless it's inconsistent So, we could model PA inside another logical system (e.g., PL) which has notation for certain meta-mathematical statements like "P(X): it is provable that X". You'd then need to demonstrate that a version of PA axiomatized with this logic is both complete and sound WRT PA, etc. etc.