Comment

You’re just covering my third paragraph. Yes, everybody is a philosopher because we don’t have the tools to do away with philosophical arguments entirely yet.

source

Sort:hotnew top

lemonwood@lemmy.ml ⁨13⁩ ⁨hours⁩ ago
I explicitly refer to your second paragraph.

I covered those other arguments in another top level comment in this same thread. Yes, you absolutely can argue computer verified proofs. They are very likely to be true (same as truth in biology or sociology: a social construct), but to be certain, you would need to solve the halting problem to proof the program and it’s compiler, which is impossible. Proofing incompleteness with computers isn’t relevant, because it wasn’t in question and it doesn’t do away with it’s epistemological implications.

source
- pfried@reddthat.com ⁨13⁩ ⁨hours⁩ ago
  It is not necessary to solve the halting problem to show that a particular proof is correct.
  
  source
  - lemonwood@lemmy.ml ⁨13⁩ ⁨hours⁩ ago
    Lean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.
    
    source
    pfried@reddthat.com ⁨13⁩ ⁨hours⁩ ago
    The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that Lean is Turing complete does not prevent it from verifying the proofs that it has verified.
    
    source