Comment by auggierose
2 years ago
> Logic as I know it can't be made up. It's already well defined and the basis for all other formal theories.
Of course logic can be made up, and in fact, all logics are. First-order logic, simply-typed higher order logic, dependent type theory, all made up.
My favourite made up logic is Abstraction Logic (http://abstractionlogic.com).
But I guess what you mean is that you are a mathematical realist. That's good! I am too.
> Yeah but I would want to prune all that other stuff away and focus on a theory on the best way to organize and abstract programs. The primitive most important for that is the function because that's basically at it's core all a computer does, just calculate stuff.
If that's what you want to do, then that's what you want to do!
>Of course logic can be made up, and in fact, all logics are. First-order logic, simply-typed higher order logic, dependent type theory, all made up.
That's like saying math is made up. Is it made up or is it discovered?
You're just being pedantic.
>If that's what you want to do, then that's what you want to do!
Yeah and if you want some theory of program design that encompasses every damn concept under the sun as an axiom go for it as well! Genius!
> That's like saying math is made up. Is it made up or is it discovered?
Personally, I think it is discovered, although the concrete incarnations are made up, of course. That's pretty much what it means to be a mathematical realist.
> You're just being pedantic.
I just know more about these things than you seem to do. People disagree on what the "right" logic is (personally, I think the right logic is Abstraction Logic), and the choice of your logic influences your axioms. First-order logic for example has no built-in functions as mathematical objects, so you need to come up with axioms for functions. Simply-typed higher-order logic, on the other hand, comes fully equipped with functions, so no need for additional function axioms. And also no need for additional axioms for other things, you can create numbers, trees, graphs etc. without introducing new axioms (except an axiom for an infinite type of individuals) for these things.
When I look at the book you cited, it's just full of really simple stuff made really complicated. Pointless, indeed. Personally, I am more interested in the opposite direction. But that's just my personal opinion.
>I just know more about these things than you seem to do.
No you're being pedantic. I don't think you know more.
Think about it. We both agree math is discovered. So why the hell are we diving into this tangent? It's because you decided to say that logic is made up and then subsequently agree it's not. The nuance of whether and what part of logic is made up is pedantic.
>When I look at the book you cited, it's just full of really simple stuff made really complicated. Pointless, indeed. Personally, I am more interested in the opposite direction. But that's just my personal opinion.
Sure tbh I never fully read the book. Skimmed. Seems to be a good resource for beginners. But I also don't think you're an expert.
Your interested in the opposite? You mean the philosophy of programming? Well good on you. You go study that then. Again I can't understand your genius.