6 ms·
> So, even though 1+1=3 is surely false, we could prove it in Lean like so: “Let’s assume that ¬(1+1=3). But this leads to a contradiction: coll_conj and ¬coll_
by perryizgr8 4y ago
> So, even though 1+1=3 is surely false, we could prove it in Lean like so: “Let’s assume that ¬(1+1=3). But this leads to a contradiction: coll_conj and ¬coll_conj. We can therefore deduce that our assumption must be false, so 1+1=3.”
I was following along with the logic, but got completely lost here. Can anyone explain how does the assumption "1 plus 1 is equal to three is false" lead to a contradiction? What is the contradiction here exactly?
- caiquelira 4y agoIt doesn't lead to a contradiction, the contradiction was already there. If you have a contradiction on your system you can prove everything: 1- Assume ¬X 2- Point out the contradiction 3- Therefore X is true
- aristofun 4y agoHow and why does a specific contradiction "coll_conj and ¬coll_conj" apply to all possible conjectures?
- plus 4y agoIf your system of logic contains a contradiction, then it can be said that any statement in that system "leads to" a contradiction. Thus "proof by contradiction" can prove any statement in that system.
- miga 4y agoTrying to find a formal system that encodes unbounded infinitary mathematical objects including most of maths, but yet to require that all statements are decidable within a finite number of steps... Is it contradiction in the proof, or rather a contradiction in assumptions? More on logic that permits all that *Bounded* Turing Machine does: https://arxiv.org/abs/2106.13309 https://arxiv.org/abs/2106.13309
- aristofun 4y ago> then it can be said that any statement in that system "leads to" a contradiction Why exactly it "leads to"? I don't get it. Why system can't have a contradiciton for one set of inputs, and not have it for others?