Generalization in first-order logic.
Hugues Leblanc · Notre Dame Journal of Formal Logic · 1979
Dealing initially with QC,, the standard quantificational calculus of order one, I shall comment on a shortcoming, reported in 1956 by Montague and Henkin [18], in Church's 1944 account [2] of a proof from hypotheses, and sketch three ways of righting things.*The third, which exploits a trick of Fitch's and for this reason will be called Fitch's account, is the simplest of the three.I shall investigate it some, supplying fresh proof of UGT, the Universal Generalization Theorem.The proof holds good, it will turn out, as one passes from QC to QC* ; the presupposition-free variant of QC.Turning next to QC = , the standard quantificational calculus of order one with identity, and to the presupposition-free variant QC2 of QC = , I shall establish the lemmas needed there to obtain UGT.That given Fitch's account of a proof from hypotheses UGT holds for QCί was argued in my recent Truth-Value Semantics [14], but the argument is circular, as Robert J. Cosgrove found out to my dismay.The results submitted here are elementary, to be sure; but the difficulty that Montague and Henkin reported was quite a serious one, and ways of meeting it accordingly deserve attention.The results, by the way, are readily adapted to suit most (if not all) logics with quantifiers.1.1 In most treatments of the calculus, QC has as its primitive signs:(a) for each d from 0 on, aleph-zero predicate variables of degree d (to be referred to by means of 'F**') 1 (b) aleph-zero individual variables, say, 'x', 'y', ( z', V, ζ y", ( z", etc. (to be referred to by means of X and Y) (c) the three logical operators: '~', '!)', and 'V (d) '(', <)', and ','.1.2 It has as its formulas all finite sequences of primitive signs of QC * Thanks are due to Robert J. Cosgrove, Michael J. Duffy, and Nyles McNally for reading and spotting errors in an earlier draft of the paper.