Home Philosophy Advances in Proof-Theoretic Semantics
When we describe the meaning of an expression, we always do it in some format: maybe a picture, or a diagram, or a formal definition in words, or a physical demonstration, or an abstract set, or . . . In other words, the information about the expression always has to be packaged up as an object—I will call the object the semantic value of the expression—in some form of representation. This places on us the burden on making sure that both we and the people we are speaking to can read the representation, i.e. that we can understand what information the semantic value is supposed to convey.
There is a great temptation for logicians just to throw symbols on the page and hope that they are self-explanatory. For example we might write, as a partial explanation
(φ and ψ )
But what does this diagram mean? Does it mean for example one of the following?
(a) If we are entitled to assert (φ and ψ) then this fact entitles us to assert φ.
(b) If we have already asserted (φ and ψ) then we are entitled to assert φ.
(c) If we are committed to defending (φ and ψ) then we are committed to defending
(d) If (φ ∧ ψ) is true then so is φ.
(e) In any situation S, if (φ ∧ ψ) is true in S then φ is true in S.
Some of these statements are deducible from others by general principles. Let me straight away generalise the notion of transfer arguments to include the arguments that justify these deductions. These arguments generalise not from one context of use to another, but from one kind of statement about use to another kind of statement about use.
Note that if we use reading (e), then there is a very plausible argument to show that the natural deduction rules for ∧ and the standard truth table for ∧ give exactly the same information about ∧, so that in this case the difference between a proof-
theoretic semantics and a model-theoretic one becomes purely one of notation. But in any case a person who wants to compare model-theoretic semantics with prooftheoretic semantics for logical operators will need to answer the question above for (6), and similar ones for the other natural deduction diagrams and for truth tables. This applies to intuitionist logical operators just as much as to classical ones.
There seem to be more ways of reading a formal derivation than there are of reading a truth table. Derivations, particularly in Hilbert-style or natural deduction formalisms, look a bit like formalised natural language arguments. But usually they are missing the explanatory tags that we put all over the place in natural language arguments: 'Then', 'But', 'Suppose', 'I grant that', 'I think I can show that', 'I claim that' etc. etc.
To illustrate the possibilities, let me sketch how Ibn S¯ına¯ thought we should read arguments in which an assumption is made and then discharged . He observed
that when we introduce an assumption φ by saying 'If φ', we don't always repeat the 'If φ' whenever we state a proposition that depends on the assumption. (That's certainly so if φ is introduced with 'Let' or 'Suppose'. But Ibn S¯ına¯ is right; one can find enough examples where it's true with 'If' too.) So, he argued, we must intend that 'If φ then' should be understood at the beginning of all relevant propositions down to the point where the assumption is discharged. So we should understand
(φ χ ) as meaning (φ → φ ) Ψ
(φ χ )
In the 'understood but not stated' derivation on the right, the formula (φ → φ) at the top is an axiom, and the discharging step that derives (φ → χ) from χ falls away. A general metarule asserts that for every step .6., α f β we have a step
.6., (φ → α) f(φ → β). (This analysis is extraordinarily close to Frege's explanation
of making and discharging assumptions, though it was given over 800 years before
Frege. But as Peter noted at the meeting, Ibn S¯ına¯ and Frege had different motivations. In fact Ibn S¯ına¯ wanted to understand the real intentions of the person giving the proof, whereas Frege aimed through Begriffsschrift to display the true 'logical weaving' of informal proofs that begin 'Let . . .' [6, pp. 379ff].)
Ibn S¯ına¯'s position is in effect a claim about what kind of contentful argument is expressed by the natural deduction rules. So it's directly relevant to how we can read
the proof rule of →-introduction as carrying information about the meaning of →.
The discussion so far has used only natural deduction proof rules. It would be possible to give a semantics using fas a primitive notion, so that for example we define ∧ by
(φ ∧ ψ) fφ, (φ ∧ ψ) fψ, φ, ψ f(φ ∧ ψ). (8)
(There are well-known variants of this definition.) The difficulty with taking fas primitive is that until we have a definition of f-, there is going to be no purchase
for transfer arguments. In particular we won't be able even to raise the question whether (8) gives the same information as a truth table for ∧, frankly because until fis explained, we don't know what information (8) is giving us.
One last point: some kinds of semantics refer to the semantic value of an expression as the 'denotation' of the expression. This is just a name, no more. It certainly doesn't entail that the semantics treats expressions as proper names of their semantic values. To single out some kinds of semantics as 'denotational' is like singling out the semantics that are written in Turkish; the classification is pointless.