Comment by corethree
2 years ago
>A theory makes only sense with respect to some logic. So first, you need to define what logic you are using. This logic is your theory with the lowest amount of primitives and axiomatic concepts.
Logic as I know it can't be made up. It's already well defined and the basis for all other formal theories.
The lowest amount of primitives and axiomatic concepts is largely a design choice for developing a theory. Makes it easier to deal with the theory rather than a theory that starts out with extremely complicated axioms.
>But don't pretend that this is so that you can reason about computer programs better. Sure, learning more about functions is useful, but numbers are also very important for computer programs. So are trees. And graphs. Expressing all of these just in terms of functions can be a fun exercise (pun intended, Church numerals anyone?). But instead of trying to express the important concepts of your program as functions, and then studying them, maybe your time is better spent studying the concepts themselves directly.
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.
> 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.
1 reply →