> It's better to say that some functions like "does this program halt?" simply don't exist.
Let f : (p: String) -> Boolean equal the function that returns True if p is a halting program, and False otherwise
> It's better to say that some functions like "does this program halt?" simply don't exist.
Let f : (p: String) -> Boolean equal the function that returns True if p is a halting program, and False otherwise
This is really just the constructive/classical argument but I want to be specific.
You just named a function and specified a property you want it to have. However no function with this property meaningfully exists. We can manipulate the symbol just fine, but we can never look inside it because it’s not real. Classical mathematics was developed before computation was relevant and the question of decidability arose fairly late, it makes more sense to consider it an early attempt at what is now called intuitionistic mathematics. The halting problem disproved excluded middle.
> The halting problem disproved excluded middle.
That's a weird category error.