 However, Metamath provides no direct support for natural deduction systems.As noted earlier, the database "nat.mm" formalizes natural deduction.The Metamath Proof Explorer (with its database "set.mm") instead use a set of conventions that allow the use of natural deduction approaches within a Hilbert-style logic.