I don’t think I want to make it fully general. I want to contrast between two schools of thinking, both of which are hard to get out of with only the tools of that school.
At what point do you put down the formal proof tools? You might prove that a statement is unprovable, but you may not do it may just hang around like P vs NP forever. Or you might prove a statement is unprovable within a system and then just switch to a different system (adding oracles and what not). What is your stopping condition?
Same with Empiricism. You will never show that empircism isn’t a useful method of gaining knowledge for a specific goal using just experiments, just that a single line of experimentation is unfruitful.
You can prove that certain lines of empiricism are likely to be unfruitful (things like trying to create infinite free energy) based on other axioms that hold up empirically. Similarly if an empirical approach is being productive you can use that to constrain the formal proofs you attempt.
This is something I would like to have said a long time ago. I’m not sure how relevant it is to current MIRI research. How much of it is actually writing programs?
I don’t think I want to make it fully general. I want to contrast between two schools of thinking, both of which are hard to get out of with only the tools of that school.
At what point do you put down the formal proof tools? You might prove that a statement is unprovable, but you may not do it may just hang around like P vs NP forever. Or you might prove a statement is unprovable within a system and then just switch to a different system (adding oracles and what not). What is your stopping condition?
Same with Empiricism. You will never show that empircism isn’t a useful method of gaining knowledge for a specific goal using just experiments, just that a single line of experimentation is unfruitful.
You can prove that certain lines of empiricism are likely to be unfruitful (things like trying to create infinite free energy) based on other axioms that hold up empirically. Similarly if an empirical approach is being productive you can use that to constrain the formal proofs you attempt.
This is something I would like to have said a long time ago. I’m not sure how relevant it is to current MIRI research. How much of it is actually writing programs?