3 ms·

Doesn't Goedel's Theorem forbid building a logic checker?

• drdeca 2y ago
  No. Gödel’s theorem forbids something that in general tells you whether a statement is true or not. (As in, a method which would work for every possible statement within a system.) It certainly doesn’t preclude something that checks if a proof is correct, any more than it precludes checking whether some calculation is done correctly (I.e. it doesn’t preclude it at all) . It says that there are statements which the proof system doesn’t have a proof of the statement being true nor of it being false. It doesn’t mean you can’t have a proof system.
• bubblyworld 2y ago
  Not Gödel's theorem, but inference for first-order logic is undecidable in general for other reasons. You can still get pretty far with heuristics though. Don't let perfect be the enemy of good =P
  • dpierce9 2y ago
    First order logics can be provably sound and complete when they do not express certain arithmetic operations.
    • bubblyworld 2y ago
      First-order logic is sound and complete in general (via Gödel's lesser known completeness theorem, for instance). That doesn't contradict what I wrote =)