Comment by unexpectedtrap
3 days ago
Correctness of the kernel and consistency of the theory implemented in it are different things. Gödel’s theorems prevent you from proving the latter, but not the former.
3 days ago
Correctness of the kernel and consistency of the theory implemented in it are different things. Gödel’s theorems prevent you from proving the latter, but not the former.
Interesting - what is correctness of the kernel here? That it faithfully implements the model?