Hence, any proof checker will have statements it can’t handle.
There are many things wrong with many of your statements here, but this one is particularly simple. You simply misunderstand what a proof checker does.
A proof checker does not deal with statements, it deals with formal proofs. Proof checking is roughly as complicated as parsing a context free language. That is, it is almost a trivial task.
Proof finding is another matter. A proof finder (aka a “theorem prover”) takes a statement as input and attempts to produce a proof as output. Godel shows that there are statements that a proof finder can’t handle.
You have repeatedly made claims which only make sense if you have the two kinds of programs confused. Fix that confusion, please.
There are many things wrong with many of your statements here, but this one is particularly simple. You simply misunderstand what a proof checker does.
A proof checker does not deal with statements, it deals with formal proofs. Proof checking is roughly as complicated as parsing a context free language. That is, it is almost a trivial task.
Proof finding is another matter. A proof finder (aka a “theorem prover”) takes a statement as input and attempts to produce a proof as output. Godel shows that there are statements that a proof finder can’t handle.
You have repeatedly made claims which only make sense if you have the two kinds of programs confused. Fix that confusion, please.