Variable declarations in natural deduction (Q861825)

The version of natural deduction for the first-order logic without equality proposed here (call it D) seems to be very similar to the ordinary (Gentzen-Prawitz) version of natural deduction (call it G) except for Fitch format. Every deduction in D is a deduction in G; every deduction in G becomes a deduction in D after inserting ``declare \(v\)'' before the first (uppermost) occurrence of the variable \(v\) in every branch. Most part of the paper consists of comments addressed mainly to readers having little experience with the use of variables in mathematics or programming.