@20:35 or so, he says that it’s obvious that equality for natural numbers is decidable. I haven’t seen how he defines what a natural number is, so I’m not sure why he says this is clear. If the traditional definition were accepted, using the axioms of first order Peano Arithmetic, then sure. In propositional logic? I’m not convinced. I never considered that question. Something to think about?
![เปิดใจ "อาจารย์เบียร์ คนตื่นธรรม" อดีตเคยสุดทุกทาง ถ้าใช้หนี้หมดไปบวชแน่ l [Nickynachat]](http://i.ytimg.com/vi/IxeE0xVhy08/mqdefault.jpg)
@20:35 or so, he says that it’s obvious that equality for natural numbers is decidable. I haven’t seen how he defines what a natural number is, so I’m not sure why he says this is clear. If the traditional definition were accepted, using the axioms of first order Peano Arithmetic, then sure. In propositional logic? I’m not convinced. I never considered that question. Something to think about?
THERE IS A WHOEP
foo : ¬ (¬ (A ⊎ ¬ A))
foo ¬A⊎¬A = ¬A⊎¬A (inj₂ λ A → ¬A⊎¬A (inj₁ A))
-- I still think its a sorcery ._.