4 ms·

Of course. That falls under "understanding why the proof is a proof".

• throwaway290 2y ago
  Now we only need to find that human that never makes mistakes and we're golden...
  • deleted 2y ago
    [deleted]
  • auggierose 2y ago
    Luckily, that is not necessary. You can make many mistakes, until you arrive at a logic you are happy with. Then you talk with other humans about it, and eventually you will all agree, that to the best of your knowledge, there is no mistake in the logic. If you pick first-order logic, that has already been done for you. Then you need to implement that logic in software, and again, you can and will mistakes here. You will use the first version of that software, or another logic software, to verify that your informal thoughts why your logic implementation is correct, can be formalised and checked. You will find mistakes, and fix them, and check that your correctness proof still goes through. It is very unlikely that it won't, but if it doesn't, you fix your correctness proof. If you can indeed fix it, you are done, no mistakes remain. If you cannot, something must be wrong with your implementation, so rinse and repeat. At the end of this, you have a logic, and a logic implementation, which doesn't contain any mistakes. Guaranteed.