[FOM] Teneant, Avron, Constants, and Variables
A.P. Hazen
a.hazen at philosophy.unimelb.edu.au
Sat Sep 11 01:47:38 EDT 2004
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
More information about the FOM
mailing list