Abstract
It is often said that in a purely formal perspective, intuitionistic
logic has no obvious advantage to deal with the liar-type paradoxes. In this
paper, we will argue that the standard intuitionistic natural deduction systems
are vulnerable to the liar-type paradoxes in the sense that the acceptance of
the liar-type sentences results in inference to absurdity (⊥). The result shows
that the restriction of the Double Negation Elimination (DNE) fails to block
the inference to ⊥. It is, however, not the problem of the intuitionistic
approaches to the liar-type paradoxes but the lack of expressive power of the
standard intuitionistic natural deduction system.
We introduce a meta-level negation for a given system and a
meta-level absurdity, ⋏, to the intuitionistic system. We shall show that in the
system, the inference to ⊥ is not given without the assumption that the
system is complete. Moreover, we consider the Double Meta-Level Negation
Elimination rules (DMNE) which implicitly assume the completeness of the
system. Then, the restriction of DMNE can rule out the inference to ⊥.