3 ms·

yeah I'm aware that I'm trying to build a platform that proves arbitrary theorems. I think where we're butting heads is that I'm wanting to approach such a plat

yeah I'm aware that I'm trying to build a platform that proves arbitrary theorems. I think where we're butting heads is that I'm wanting to approach such a platform from a constructive angle - starting with simple axioms and building up from there. The initial system may only be capable of interpreting natural number equality and addition. My original question was around what theoretical approach best matches that goal - whether it's an axiomatic system based on Peano arithmetic, or a natural deductive system, or something based on type theory. From a non-academic perspective these fields all seem very similar and there seems to be a lot of crossover so I didn't know what best suited the problem I'm trying to solve. Of course even when the system is complete some functions will remain undecidable, but I'm totally OK with that. It may even be that something like a deductive classifier better suits the problem than a mathematical representation.

lisper 8y ago
> I'm aware that I'm trying to build a platform that proves arbitrary theorems. OK, well, that was far from clear. Here's your original question: > the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into some interesting implications when I incorporate dependent typing, but it feels like there must be something theoretical that's already out there. You're right, there is "something theoretical that's already out there", and that "something theoretical" is Turing-equivalence (and a vast literature on automated theorem proving). > My original question was around what theoretical approach best matches that goal - whether it's an axiomatic system based on Peano arithmetic, or a natural deductive system, or something based on type theory. From a non-academic perspective these fields all seem very similar and there seems to be a lot of crossover so I didn't know what best suited the problem I'm trying to solve. You're right. All of those fields are very similar. In fact, they are equivalent because they are all Turing-complete. It is really hard to avoid Turing-completeness, and even there all of the possible options are well understood. The bottom line is that you (AFAICT) are at the very beginning of an extremely well-worn path. Actually, not just one path, but many, many paths, all of which lead to the same place: undecidability (and meta-undecidability and meta-meta-undecidability...) No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found (though of course that can't be proved because undecidability!) The best you can hope for is to make reasonable engineering tradeoffs that work for some domain of interest. But at the end of the day, you're just doing math, and math is hard. Nowadays it's really, really hard because all the low-lying fruit was picked a long, long time ago. But if you're really serious about this, the first step is to get a stack of textbooks on computability theory and automated theorem proving and read them.
- beaconstudios 8y ago
  > OK, well, that was far from clear. Here's your original question: Yeah, sorry about that - not being an academic myself makes it hard to put it across in the correct way. > No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found That's absolutely fine by me - I'm not looking to break through the undecidability barrier, only to implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories). The numerous branching and totally equivalent fields is the thing I'm wary of - I don't want to have to invest 6 months learning category theory, only to find out that what I want to do is better expressed by type theory or second order logic or something else entirely. I guess in my mind it's similar to building a complex application in one programming language just to discover certain patterns can't be idiomatically expressed in that language, so you have to write horrible hacks to compensate for that lacking where you could have chosen a different language in the first place. From my own research I'm leaning towards axiom systems, perhaps utilising Zermelo-Fraenkel set theory as a basis. I don't know, it's early days yet. I'll keep reading and get a rough grasp on the principal fields before I make a definitive decision.
  - lisper 8y ago
    > I'm not looking to break through the undecidability barrier That, too, was far from clear. You said you were tackling this problem: > what is the property of a program that makes it undecidable? and I told you: > That is itself an undecidable question! and explained why (at least three times). And AFAICT you still don't get it because you still say you want to: > implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories) and that is the problem of automated theorem proving, which is an open research issue, and (provably) always will be. If you want to get a small taste of what you're up against, try proving that this program always halts: f(x:int, y:int) = ( x+y == y+x ? halt : loop ) In other words, try proving the commutative law of addition. If you get that, try to prove that this lambda-calculus expression (λ (n f) (n (λ (c i) (i (c (λ (f x) (i f (f x))))))(λ x f) (λ x x))) computes a factorial expressed as a Church numeral. (See http://www.flownet.com/ron/lambda-calculus.html http://www.flownet.com/ron/lambda-calculus.html for some hints.) And that's just what you get from elementary arithmetic. If you really want to blow your mind, look at: http://www.mrob.com/pub/math/largenum.html http://www.mrob.com/pub/math/largenum.html and the associated software: http://www.mrob.com/pub/perl/hypercalc.html http://www.mrob.com/pub/perl/hypercalc.html Once you get to infinity you are only just getting started: https://johncarlosbaez.wordpress.com/2016/06/29/large-countable-ordinals-part-1/ https://johncarlosbaez.wordpress.com/2016/06/29/large-counta... And even all that is just what you get from discrete math! Then there's calculus, topology, algebraic varieties (of which elliptic curves are one example, and even that is a whole field of study). And even here we've not even begun to scratch the surface of what is possible. The world of math is (provably!) richer than you -- or anyone -- can possibly imagine! That's what "undecidable" means. Your only reasonable hope of making any kind of non-trivial progress is to focus on one domain, and then use the constraints imposed by the properties of that domain to shrink the problem down to something potentially manageable.

lisper 8y ago

> I'm aware that I'm trying to build a platform that proves arbitrary theorems. OK, well, that was far from clear. Here's your original question: > the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into some interesting implications when I incorporate dependent typing, but it feels like there must be something theoretical that's already out there. You're right, there is "something theoretical that's already out there", and that "something theoretical" is Turing-equivalence (and a vast literature on automated theorem proving). > My original question was around what theoretical approach best matches that goal - whether it's an axiomatic system based on Peano arithmetic, or a natural deductive system, or something based on type theory. From a non-academic perspective these fields all seem very similar and there seems to be a lot of crossover so I didn't know what best suited the problem I'm trying to solve. You're right. All of those fields are very similar. In fact, they are equivalent because they are all Turing-complete. It is really hard to avoid Turing-completeness, and even there all of the possible options are well understood. The bottom line is that you (AFAICT) are at the very beginning of an extremely well-worn path. Actually, not just one path, but many, many paths, all of which lead to the same place: undecidability (and meta-undecidability and meta-meta-undecidability...) No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found (though of course that can't be proved because undecidability!) The best you can hope for is to make reasonable engineering tradeoffs that work for some domain of interest. But at the end of the day, you're just doing math, and math is hard. Nowadays it's really, really hard because all the low-lying fruit was picked a long, long time ago. But if you're really serious about this, the first step is to get a stack of textbooks on computability theory and automated theorem proving and read them.

beaconstudios 8y ago
> OK, well, that was far from clear. Here's your original question: Yeah, sorry about that - not being an academic myself makes it hard to put it across in the correct way. > No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found That's absolutely fine by me - I'm not looking to break through the undecidability barrier, only to implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories). The numerous branching and totally equivalent fields is the thing I'm wary of - I don't want to have to invest 6 months learning category theory, only to find out that what I want to do is better expressed by type theory or second order logic or something else entirely. I guess in my mind it's similar to building a complex application in one programming language just to discover certain patterns can't be idiomatically expressed in that language, so you have to write horrible hacks to compensate for that lacking where you could have chosen a different language in the first place. From my own research I'm leaning towards axiom systems, perhaps utilising Zermelo-Fraenkel set theory as a basis. I don't know, it's early days yet. I'll keep reading and get a rough grasp on the principal fields before I make a definitive decision.
- lisper 8y ago
  > I'm not looking to break through the undecidability barrier That, too, was far from clear. You said you were tackling this problem: > what is the property of a program that makes it undecidable? and I told you: > That is itself an undecidable question! and explained why (at least three times). And AFAICT you still don't get it because you still say you want to: > implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories) and that is the problem of automated theorem proving, which is an open research issue, and (provably) always will be. If you want to get a small taste of what you're up against, try proving that this program always halts: f(x:int, y:int) = ( x+y == y+x ? halt : loop ) In other words, try proving the commutative law of addition. If you get that, try to prove that this lambda-calculus expression (λ (n f) (n (λ (c i) (i (c (λ (f x) (i f (f x))))))(λ x f) (λ x x))) computes a factorial expressed as a Church numeral. (See http://www.flownet.com/ron/lambda-calculus.html http://www.flownet.com/ron/lambda-calculus.html for some hints.) And that's just what you get from elementary arithmetic. If you really want to blow your mind, look at: http://www.mrob.com/pub/math/largenum.html http://www.mrob.com/pub/math/largenum.html and the associated software: http://www.mrob.com/pub/perl/hypercalc.html http://www.mrob.com/pub/perl/hypercalc.html Once you get to infinity you are only just getting started: https://johncarlosbaez.wordpress.com/2016/06/29/large-countable-ordinals-part-1/ https://johncarlosbaez.wordpress.com/2016/06/29/large-counta... And even all that is just what you get from discrete math! Then there's calculus, topology, algebraic varieties (of which elliptic curves are one example, and even that is a whole field of study). And even here we've not even begun to scratch the surface of what is possible. The world of math is (provably!) richer than you -- or anyone -- can possibly imagine! That's what "undecidable" means. Your only reasonable hope of making any kind of non-trivial progress is to focus on one domain, and then use the constraints imposed by the properties of that domain to shrink the problem down to something potentially manageable.