Very fun. It turns out that it is easy to implement a natural deduction system using a system based on Hilbert's approach. A discussion on this for metamath's

Very fun. It turns out that it is easy to implement a natural deduction system using a system based on Hilbert's approach. A discussion on this for metamath's set.mm is here: http://us.metamath.org/mpeuni/mmnatded.html#natural-deduction-metamath http://us.metamath.org/mpeuni/mmnatded.html#natural-deductio... Many steps are an implication phi → ..., and the antecedent mimics the context (Γ) of most ND systems.