Natural Deduction Calculus for First-Order Logic

TL;DR

This paper provides an accessible, step-by-step explanation of natural deduction for first-order logic, covering inference rules, soundness, completeness, and practical examples to facilitate understanding of this proof system.

Contribution

It offers a clear, comprehensive introduction to natural deduction in first-order logic, including formal properties and illustrative problem-solving examples.

Findings

Natural deduction extends propositional logic to first-order logic with quantifiers.

The paper demonstrates the soundness and completeness of the proof system.

Examples range from simple to complex applications of natural deduction.

Abstract

The purpose of this paper is to give an easy to understand with step-by-step explanation to allow interested people to fully appreciate the power of natural deduction for first-order logic. Natural deduction as a proof system can be used to prove various statements in propositional logic, but we will see its extension to cover quantifiers which gives it more power over propositional logic in solving more complex, real-world problems. We started by going over logical connectives and quantifiers to agree on the symbols that will be used throughout the paper, as some authors use different symbols to refer to the same thing. Besides, we showed the inference rules that are used the most. Furthermore, we presented the soundness and completeness of natural deduction for first-order logic. Finally, we solved examples ranging from easy to complex to give you different circumstances in which you can apply the proof system to solve problems you may encounter. Hopefully, this paper will be helpful makes the subject easy to understand.