postulate
¬¬-elim : ∀ {A} → ¬ ¬ A → A
lem : ∀ {A} → A ⊎ ¬ A
lem = ¬¬-elim ( λ f → f ( inj₂ ( λ x → f ( inj₁ x))))
postulate
em : ∀ {A : Set} → A ⊎ ¬ A
dne : ∀ {A : Set} → ¬ ¬ A → A
dne ¬x = case-⊎ (λ x → x) (λ x → (exFalso (¬x x))) em
A: 这上面是表达什么意思
B: 是说排中律和双重否定律等价。但无法构造出其中一个。
A: 用人的语言说呢？
B: 我不是不爱国就说我爱国，等价于， 我除了爱国就是不爱国了。但是却无法构造或证明我爱国和不爱国。
A: 我挥舞着国旗，高唱着国歌，不能说明我爱国？你冷嘲热讽，甚至蒙面侮辱国旗，不能说明你不爱国？
B: 表演需要有观众，成为演员就放弃了表现和他真实的一致性。所以只能说他表演的很爱国，很不爱国，但精神灵魂的拷问，无法说出所以然来。
A: 可是每个人都要接触其他人，必然是演员了啊。
B: 所以说才会谈论演技的好坏，有的人演不出自己本性，就会让人觉得浮夸。有的人本色出演，但总让人觉得有点过，觉得入戏太深。
A: 为了表现反抗的反抗，和为了表现的认同的认同就差不多一样，不用认真对待？
B: 你真是蠢，别人打你一下表现反抗，和给你 100 元，表示认同能一样吗？既然都是表演，当然是为了最大利益。
A: 可是短期的利益和长期利益总是不容易分清，打我一下可能是为了让我记住教训，给我 100 元，可能是为了腐蚀我。
B: 所以身为演员的我们，需要识别其他演员真实的表演性，并能清楚的认知自己的表演性。比如这两个演员，司马迁和刘彻你记住了谁？你更愿意记住谁呢？
A: 我不知道，可是我们都是被迫参演。我到底是不是演员呢？难不成有人的时候是演员，没有人的时候就是自己了？
B: 就像 "死火" 一样，没有燃烧起来叫死，燃烧起来叫火，燃烧完的刹那，就是死火。所以死火是活的，还是死的呢？
A: 在有人和无人的边界上做自己?
B: 所以 ‘我思故我在’ 你现在懂了吗？
(至于我对话的表演性的自指是不言而喻的)