A quantum analogue of the classical first-order logic (FO) was discussed lately in [CiE 2024, LNCS 14773, pp. 311–323] from a semantic viewpoint in order to characterize logarithmic-time/space quantum computability. From a syntactic perspective, we further study this new, intriguing quantum logic by introducing a quantum analogue of Gentzen’s tree-like proof system of classical natural deduction and further analyzing the expressing power of this new quantum natural deduction system. In particular, we prove the fundamental features of the soundness and completeness of this quantum proof system and, as a consequence of them, we further show the compactness of the system. Quantum natural deduction is expected to pave a road to automated theorem proving in a quantum-mechanical fashion.