在直覺邏輯下證明 |x| < 1/n -> x = 0 ?

[xcycl (XOO)]

在古典邏輯下，我們有 (﹁p →﹁q) → (q → p) 這件事情，
也用這論述來證明當某個實數 x ，若對所有自然數 n 有 |x| < 1/n  則 |x| = 0
而證明就是假設 x 非零，則可以找到 1/n 比 x 還小矛盾。

但這在直覺主義邏輯下並不成立，那要怎麼在這系統下證明這件事情呢？
在 Bishop 的 Constructive Analysis 前面有用到這件事情，
卻想不通是依據什麼成立的 ...

--
※ 發信站: 批踢踢實業坊(ptt.cc) 
◆ From: 123.193.218.153
推 aletheia:這要有請數龜大師