← Back to context

Comment by Smaug123

16 hours ago

Not necessarily. For example, perhaps my ZFC first-order-logic theorem checker implicitly accidentally contains the continuum hypothesis as an axiom. This isn't inconsistent but it is a correctness bug.

(For that matter, another correctness bug is "the checker rejects all proofs". You can't prove false if you can't prove anything.)