Gödel’s first incompleteness theorem – an interactive tutorial

Re:Gödel’s first incompleteness theorem – an interactive tut... by perryizgr8 on Monday October 17, 2022 @02:17PM (#33237577)

> 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?

[ Parent | on HN ]

Re:Gödel’s first incompleteness theorem – an interactive tut... by plus on Monday October 17, 2022 @02:33PM (#33237766)

If 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.

[ Parent | on HN ]

Re:Gödel’s first incompleteness theorem – an interactive tut... by miga on Monday October 17, 2022 @04:02PM (#33238815)

Trying 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

[ Parent | on HN ]

Re:Gödel’s first incompleteness theorem – an interactive tut... by aristofun on Wednesday October 19, 2022 @04:15PM (#33267401)

> 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?

[ Parent | on HN ]

Re:Gödel’s first incompleteness theorem – an interactive tut... by caiquelira on Monday October 17, 2022 @02:57PM (#33238039)

It 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

[ Parent | on HN ]

Re:Gödel’s first incompleteness theorem – an interactive tut... by aristofun on Wednesday October 19, 2022 @04:13PM (#33267390)

How and why does a specific contradiction "coll_conj and ¬coll_conj" apply to all possible conjectures?

[ Parent | on HN ]