3 ms·
> Gödel showed that some theorems are unprovable in a consistent formal axiomatic system... ...of sufficient power, eg. that can model arithmetic with both add
by naasking 1y ago
> Gödel showed that some theorems are unprovable in a consistent formal axiomatic system...
...of sufficient power, eg. that can model arithmetic with both addition and multiplication. I think the caveats are important because systems that can't fully model arithmetic are often still quite useful!
- gf000 1y agoIndeed! But I am afraid general purpose programming languages almost always need that kind of power (though being Turing complete is not necessary)
- naasking 1y agoThey need it operationally for calculations and such, but those calculations don't necessarily need to be statically validated beyond simple things like type and unit checking.