The language(s) of first-order logic #2
One theme touched on the last post is whether the language for our preferred natural deduction system syntactically distinguishes symbols used as parameters in (UI) and/or (EE) proofs. Of the nine books I mentioned, two use distinct symbols for parameters, as against names (individual constants) and variables. And another book (Teller’s) syntactically marks the use of names as parameters in subproofs leading to an application of (UI).
‘Distinguishers’ are perhaps over-represented in our sample: in Pelletier and Hazen’s table of 50 texts, only 11 are reported as syntactically distinguishing “arbitrary names”. In a way, this low proportion of distinguishers is a bit surprising, for two reasons. First, there’s the weight of authority: Gentzen himself gives distinguished symbols for bound variables and variables occurring free in the role of parameters. (True, Gentzen was not the only begetter of natural deduction, and Jaśkowski does not distinguish real variables from symbols used as parameters.) But second, and much more importantly, Gentzen’s symbolic distinction marks a real difference in the role of symbols: and we should surely follow (as I put it before) the Fregean precept that important differences in semantic role should be perspicuously marked in our symbolism.
True, we can recycle ordinary names or ordinary variables to play the new role of parameters (or ‘temporary names’ or whatever you want to call them). This gives us economy of notation. But Frege would insist that the desire for economy in one’s primitive symbolism should be trumped by the desire for perspicuity (on marking another distinction, he talks of “[his] endeavour to have every objective distinction reflected in symbolism”). I think we should aim, within reason, to be with Frege here.
An oddity to remark on. There are some who mark only one of the special use of symbols in (UI) inferences and in (EE) inferences. Thus Teller, we noted, puts hats on what he calls ‘arbitrary occurrences’ of a name in the course of a (UI) proof; but he doesn’t syntactically distinguish the use of a name as a temporary name instantiating an existential quantifier in the course of a (EE) proof. Suppes in his much used Introduction to Logic (1957) does things the other way about. The same variables that appear bound appear free in his (UI) inferences; but instantiations of existential quantifiers are done using special symbols as what he calls ‘ambiguous names’. Of course, both proof systems work fine! – but I’m not sure why you would want to leave it to context to mark one distinction in the use of symbols and syntactically mark the other. (Lemmon, whose Beginning Logic (1965) taught generations of UK students natural deduction in a Suppes-style layout, uses distinguished symbols as what he calls ‘arbitrary names’ in both (UI) and (EE) inferences.)
To be continued.
