[FOM] Teneant, Avron, Constants, and Variables

[A.P. Hazen]

    Neil Tennant points out that in the system of his book "Natural 
Logic" (this is a natural deduction system virtually the same as 
those studied by Prawitz in "Natural Deduction," and so to the 
N-systems of Gentzen's "Invenstigations  into logical deduction") the 
only formulas occurring in derivations are sentences (= closed 
formulas).  The rule of Universal Generalization (U. Quant. 
Introduction) is that you can infer Ax(...x...) from (...a...), where 
a is a NAME (= constant).  Of course, there's a restriction: you have 
to make sure that the constant, a, does not occur in the  premisses 
and  hypotheses from which (...a...) has been derived.  This is not 
an uncommon feature of textbook formulations of natural deduction.
    Two comments:
    Terminological: the constant a will (typically) be a constant that 
is otherwise not used: it won't be (if we think of the derivation as 
representing a proof expressed in an INTERPRETED language) a constant 
that we are using as the name of an interesting member of the domain. 
As Arnon Avron puts it, it is not a DECLARED constant.  This 
distinction is often noted; constants used as in the manner of a (and 
similarly thosed use as instantial terms in tableaux-calculi) are 
often called DUMMY CONSTANTS (or "dummy names").
    Historical: the idea that in proving a universal statement we 
prove a particular instance of it, and note that our proof has made 
no special assumptions about the particular object we have 
considered, is one with very old philosophical resonances.  Berkeley, 
for example, wrote that the triangle ("triangle ABC", as they say) 
you prove a theorem about in the course of proving a theorem about 
triangles in general is NOT an "abstract" triangle-- it is, rather, a 
perfectly ordinary, particular, triangle (most likely the one we have 
drawn in the diagram illustrating our proof, or perhaps our mental 
image of that drawing), and that we reach our general conclusion by 
reflecting that we have not, in our proof, made use of any special 
information distinguishing this triangle from others.  (Cf. paragraph 
16 in the Introduction to his "Principles of Human Knowledge"; the 
connection between Berkeley's doctrine and the rules of formal 
quantification theory was commented on by Beth (among others).)

     Arnon Avron comments that Tennant's use of "undeclared" constants 
seems to differ at most verbally from, e.g., Takeuti's use of "free 
variables" in his "Proof Theory".  (Takeuti, following Gentzen, 
formulates First-Order Logic with separate alphabets of free 
(a,b,c...) and bound (x,y,z...) variables, and takes the terms "free 
variable" and "bound variable" to signify the two classes of 
expressions-- this leads to such odd-sounding, but perfectly clearly 
defined, terminology as "quasi-formula": an expression which is like 
a formula except for containing unbound occurrences of bound 
variables.)  Tennant's (and similar) systems, therfore, don't REALLY 
avoid the "assertion" of open formulas... or, putting it in less 
beligerent words, don't avoid it in the same sense that systems like 
Quine's axiomatic system in "Mathematical Logic" do.
    Another bit of literature: Richmond Thomason's "Symbolic Logic: an 
introduction" (Macmillan, 1970: a very rigorous presentation of FOL 
and its metatheory (through Completeness and the equivalence of 
natural deduction and Hilbert-style formulations)) emphasizes this by 
using THREE alphabets of individual signs: what he calls VARIABLES 
(corresponding to Takeuti's bound variables), CONSTANTS 
(corresponding to Avron's declared constants, and used to "translate" 
natural-language names), and PARAMETERS (which are used, in the 
fashion of Tennant's constants, in formulating quantifier rules).

--

Allen Hazen
Philosophy Department
University of Melbourne