> 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.
> 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.
> 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)))
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.
See, I'm not an academic - proving that addition is commutative is not in scope for what I'm wanting to do. It is not a big leap for me to make that an axiom in my system, I'm almost entirely disinterested in trying to innovate in the pure theory of foundational mathematics. I find the theory itself extremely interesting but that's just not my path. I thought I was clear about what I was wanting to build - a practical system for categorising functions that can be shown to halt or not always halt, lumping everything else into a third category. Academia and pure maths just isn't for me, this is so I can build a language with minimal bugs.
Yes, you were very clear. But saying "I want to build a practical system for categorising functions that can be shown to halt or not always halt, but I'm not interested in theory" is kind of like saying, "I want to build a practical warp drive, but I'm not interested in physics."
I'm not interested in trying to encode a proof that addition is commutative. I'm interested in the theory to the point where I'll enjoy (and have been enjoying) learning about the math, but in terms of implementation I just don't want or need to start that low.
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.