In *TTP* 11, I emphasized that Weir’s position interweaves two separable strands. One strand I called “formalism about arithmetical correctness”: at a first approximation, what makes an arithmetical claim correct is something about what can be done in some formal game(s) played with uninterpreted tokens. The other strand proposes, as I put it, that the content of arithmetical claims is not “transparently representational”. So far, in these blog posts, I’ve been talking mostly about the way the second strand gets developed. It has been Hamlet with only brief appearances of the Prince of Denmark.

Weir’s story about content is intended to serve as a kind of protective wrapping around the formalist core (so he can say e.g. that although arithmetical claims have formalist correctness conditions we aren’t actually talking about synactic whatnots when we make common-or-garden arithmetical claims — thus avoiding at least some incredulous stares). But there is no getting away from it: when the wraps are off, the story about those correctness conditions is indeed very starkly formalistic. What makes arithmetical claims correct, when they are correct, is facts about plays with concrete tokens in some rule-governed practice of token-shuffling (actual plays, or practically possible ones).

Well, here I am, making arithmetical claims. These are supposedly made true by facts about concrete moves in some formal practice. *Which formal practice?* Look again at the toy models I offered in *TTP* 10. There was a (1) a game with an abacus, with facts about this making true tokens like ‘68 + 57 = 125’ (whose content is tied to such facts, but non-representationally). Then there was (2) something like school-room practice where we write down “long additions” etc. on our slates, with facts about what can be written down in this practice making true equiform tokens ‘68 + 57 = 125’ (which therefore have a different content from before). Then there was (3) a formal proof-system for quantifier-free arithmetic, and tokens such as ‘68 + 57 = 125’ are now tied to facts about what can be derived inside the formal system. So when *I* say ‘68 + 57 = 125’ which formal game is *my* utterance tied to (one of these or another)? What content does my utterance have? What’s to choose?

Weir’s response is: don’t choose.

The neo-formalist position is

pluralistrather than relativist. The truth-value of ‘68 + 57 = 125’ is not relative to a formal system. Rather there is a plurality of systems, and the sentence expresses different senses in each, whilst it is made true (or false) in the context of a given one iff it is provable therein. (p. 108)

Which is the line he has to take (irrespective of the details of his story about non-representational content). Take the child brought up “bilingually” to play the abacus game and comment on that, and play the school-room game and comment on that. By mishap the child could come to believe 68 + 57 = 125 in the comment mode in one context and disbelieve in the other: so the contents had better be different.

OK: two children taught two different games and two different commenting practices will mean something by equiform comments. Yet it would be mighty odd, wouldn’t it, to say that two real children taught real *arithmetic* by different methods mean something different by ‘68 + 57 = 125’? The natural thing to say, most of us will think, is that if the kids end up as practical arithmeticians counting the world in the same ways, using addition when they want to put together the counts of two different piles to give a count of their combination, then whether they get to ‘68 + 57 = 125’ by abacus, school-room sum, doing a formal proof (heaven help us!) or using a calculator, they mean the same. For the sense of what they say is essentially grounded in their applied practice, in how they *use* arithmetic in the world.

From this natural perspective, Weir’s story begins to look upside down. He first talks of unapplied formal games (as it might be with an abacus, or writing down sums as in the school room, or operating with an uninterpreted proof system); assigns various contents to ’68 + 57 = 125′ treated as comments on moves in those various as-yet-unapplied games. And only afterwards, with the various informational contents fixed by the liaisons to the uninterpreted formal games, does Weir talk about applying the ‘arithmetic’ to the world. But at least as far as *arithmetic* is concerned, this looks topsy turvy: it’s the embedding in the applied practice of counting and adding and multiplying that gives sense to arithmetic; claims, properly so called. (Cf. Wittgenstein in the *Big Typescript* discussing what makes arithmetic different from a game.)

Later (p. 218) Weir modifies his pluralism. He says two speaker S and S* using e.g. ‘68 + 57 = 125’ “express the same sense” if there is an “admissible mapping” between theie linguistic practices L and L*. The details don’t matter (which is good, because they are not clear). The trouble is that I don’t see what entitles Weir to play fast and loose with the notion of sense like this. He’s spent chapters earlier on the in book trying to give us a story about sense or “informational content” that allows him to distingish the thin sense of ‘68 + 57 = 125’ from the rich sense of a statement of the correctness conditions of the claim in terms of moves in a formal game. He can do this because he cuts sense fine. And his criterion of difference in sense is that you can believe 68 + 57 = 125 (as a comment on the game) without being able to frame the concepts necessary to state the metaphysical correctness conditions. But then, by the same Fregean criterion of difference, the bilingual L/L* speaker like the abacus user who also does sums on paper could still express two different senses by different uses of ‘68 + 57 = 125’. Weir seems, later, just to be changing the sense of “sense”.

So I think Weir is landed with the radical pluralism he cheerily embraced earier, and his later attempt to soften it is a mis-step by his own lights. Many will count this as a strike against neo-formalism.

*To be continued*

Alan WeirDear Jeff,

Thanks for the link to the Dorr, Arntzenius piece, looks really interesting.

‘But you don’t think that there are fields, functions, fibre bundles, gauge groups, the fine structure constant, etc., so this is surely nominalism.’ Well, I do and I don’t, so I am and am not a nominalist in your sense. Sounds evasive but I claim it isn’t!

Speaking in formal mode I think there are functions, manifolds, divergence operators etc, but in representational mode, hoping to describe mind-independent reality, I do indeed deny such things exist. But like Field, I don’t deny that physical reality can be isomorphic to mathematical structures, in fact as I said, I think I’ve an easier time than him because I believe (physical) properties and relations exist, so we can specify the function mapping the mathematical structure in order-preserving way onto the physical entities, regions of spacetime and properties and relations thereof.

Of course this function, and its domain, do not exist in mind-independent reality but the theory specifying the isomorphism is a theory from applied mathematics (and so in a mixed mode according to my account of applied maths) and such theories can be true for me by contrast with (at least in his official earlier theory) Field. So if the Arnztenius/Dorr accounts work, then we can fillet out the physical content of classical vector field theories and quantify in representational mode over entities which combine in the same fashion as the uncountably many components of vector fields do. Like Field, I have no hang-ups about size, well not of that form anyway, no problems with physical reality being infinite. On the other hand, perhaps physical reality is just a giant, but finite, matrix of spacetime regions and finitely many properties and relations thereof but of such complexity that we can’t get any kind of predictive or explanatory handle on it except by imposing a more fine grained structure of continuous manifolds or the like on it. Since I’m a bit of a sceptic (a big sceptic in fact) in epistemology, I don’t think we’ll ever know the truth of the matter here.

Another thing I disagree with the fictionalists on though: I think maths isn’t just useful as an inference-shortening device. I think it is *conceptually* indispensable. That is to say, we’d never be able even to think about the very small or the very large, we’d never be able to pick out the properties, relations and spacetime structures delineated in classical field theories, in general relativity, in quantum physics (supposing the Field/Arnztenius/Dorr nominalisation can go through) without going through the mode of presentation, as it were, of mathematical concepts, without going through applied mathematical physics. And we can’t grasp the mathematical concepts unless we grasp the distinction between correct and incorrect application; and if you think it is incorrect mathematically to say there are infinitely many primes or uncountably many reals, you’ve made big mistakes. From which I think all but the ardent non-deflationist should conclude those claims are true. But, (the harder part) we don’t need to conclude that what makes them true is that they represent a domain of abstract entities the way that in representational mode theories are rendered true or false by dint of the right kind of entities existing independently of the mind.

Jeffrey KetlandHi Alan, sorry about the delay. Dealing with crap at Edinburgh.

(I need a device to contain a highly mobile 2-year old, some sort of Star Trek force field …!)

But you don’t think that there are fields, functions, fibre bundles, gauge groups, the fine structure constant, etc., so this is surely nominalism. If there are no such things, our best physics is radically false. So, a realist should accept them! Still, a Field-style program conducive to this kind of nominalism has just recently appeared in new work “Calculus as Geometry” by Cian Dorr and Frank Arntzenius, which they aim to nominalize theories in curved spacetime, with gauge fields. That’s here,

http://users.ox.ac.uk/~sfop0257/papers/CalculusAsGeometry.pdf

Yes, I read some of your work on deflationism and naive set theory, including your nice paper “Naive truth and sophisticated logic”. Like Field and Beall, we are to keep the unrestricted T-scheme, and avoid explosion by adopting a non-classical logic. I don’t really have a good enough detailed knowledge of that kind of thing to be sure of what I think.

Cheers,

Jeff

Alan WeirI suspect my advice on being a dad is even less to be relied on than my advice on interpreting maths or physics!

I also suspect I’m not a nominalist in your sense. I’m all for physicists (and the rest of us) quantifying over manifolds, gauge groups and the like, I’m happy to say (outside the Small Caps Metaphysics Room) these things exist. If we can’t find a representation theorem for a theory in mathematical physics mapping it into a structure we can reasonably take as non-mathematical and empirically real, causally active etc. (that seems to be the case for quantum physics: infinite dimensional Hilbert spaces don’t look to be empirically real in fact even for classical theories phase spaces might be a problem) then that means we lack a realist interpretation of the theory as yet. It doesn’t mean we shouldn’t use the theory, indeed for me it doesn’t even mean the theory, as a theory of mathematical physics, is not true.

I’m a rampant deflationist about ‘true’ (thereby leading to more heresy in the form of espousal of the naive notion of truth) but not for ‘make-true’, the latter linked with ‘metaphysical content’ the former ‘informational content’. Best Alan

Jeffrey KetlandHi Alan, thanks again!

(Well, we went to the shop to try and buy a netbook. Sam ran round the shop for 20 minutes. We failed in our objective. You and Peter are both dads – you should give us some advice.)

I have your book on order now!

The main reason I reject nominalism is because it’s inconsistent with science. As you say above, you think that physics can be “nominalized”. But there is only a little evidence for this, but a lot against it; physicists continue to quantify over numbers, functions, sets, manifolds, gauge groups, etc. Even, more recently, a very abstract hierarchy of n-categories.

Putting aside the negative doctrine of neo-formalism (nominalism), it seems to me that the real sticking points on the positive doctrines are:

(1) the identification of truth relative to a proof game with the existence of a concrete proof token.

(2) the identification of the content of a string in a proof game with the existence of concrete proof token.

But I think both involves a radical revision in what we mean by “true” and “content”.

Cheers,

Jeff

Alan WeirJeff: hope the park trip went well.

On ‘5+7 = 7+5’ doesn’t mean something different in Q than in Q + commutativity. Well each instance is provable in Q, surely, by simplifying numerical terms using the recursive equations until we just get zero prefaced by the same number of ‘S’s on either side. It’s just the generalisation which fails no? So the difficult case is your

“AxAy(x + y = y + x)” expresses different propositions in Q and Q*.

Mmm good point. The reason it seems such a strong claim is it’s very difficult to think of the commutativity thesis as a thesis in the system of Q or some still rather restricted extension. It’s hard not to think of it as we usually do, as a thesis of *arithmetic* the theory which emerges from our practices, rather than one crystallized in a text book. And ‘folk arithmetic’ is a much stronger theory, including perhaps commutativity itself as a constitutive truth. But anyway since I think the logic of arithmeticincludes the omega rule, commutativity is provable. I have a section II.4 Chapter Four pp. 109ff. on the ‘inadequacy objection’- how can the formalist say that Q is an inadequate theory, too weak to capture ‘the numbers’ if there are no such things in reality? If all Q is ‘about’ are the Q-truths and these are just the Q-theorems then it will be a complete account. The above might indicate the way the reply goes.

On your other points I’m in danger of repeating myself and am tempted to say that it’s all in the book. E.g. your conjecture as to the ‘content of a string’. A crucial point to the whole book is differentiating two notions of content, informational and metaphysical and Peter and I have already had a few rounds on that in this blog.

On deriving the standard inductive clauses for truth etc. As before, I do all that in formal semantics and proof theory not concretist theory, the latter being a pretty thin thing. Perhaps I can try to get the gist of the idea over this way. Imagine that though I don’t convince you to abandon your belief in abstract objects I somehow or other convert you to the view that, in maths, truth is at least extensionally equivalent to provability (with proofs for you still abstract objects). This might cause you to make radical revisions of some areas of mathematical practice if I don’t convince you that there should be no size limitation on proofs but e.g. for Delta-0 arithmetic there won’t be a problem.

Then one Saturday night on returning from your devotions at the Church of Platonism (Reformed, Non-subscribing) you suddenly lose your faith in abstract objects. (Or perhaps it happens on a bike ride, like Russell falling out of love with his first wife, so he claimed.)

Initially you are inconsolable but after a while I get you to consider the idea that although there are no abstract objects there are concrete proof tokens (and with a bit of mereology or similar, perhaps proof tipes in my sense). In particular concrete proofs of results of formal semantics and proof theory. These are enough, I suggest to you, to ground the truths of formal semantics and proof theory you and I hold dear:- unique readability, inductive clauses of truth definitions or theories, inductive clauses of proof definitions, proofs that for Delta-zero arithmetic at least, truth and provability coincide or at least are necessarily conjoined and so on. So once you had accepted the truth-proof link, you didn’t need abstract objects at all, I say, concrete proof gives you everything you need. Show me a mathematical statement you want to uphold but which you do not believe ever could have a concrete proof (or disproof) in its ‘proper system’, even in the relaxed sense I outlined last time, and I’ll just say that’s a statement you should be agnostic on.

But, you say, you believe concrete proofs which tell you every Delta-zero sentence is provable or refutable, hence every instance of LEM over such sentences is provable hence true. Adding all such instances of LEMs as axioms is redundant but a useful shortcut. And you believe the concrete demonstration that truth distributes over disjunction and negation in the usual way, hence each such disjunct of a true instance of LEM is true or false. But you do not believe of every such disjunct that it has a concrete proof or disproof. Concrete truth and concrete proof come apart, we can see for theoretical reasons, even if we can’t come up with a particular instance of something we believe is true but lacks a concrete proof.

My reply is that we are indeed engaged in a debate which only makes sense inside rather sophisticated theorising and that the notions of formula, truth, proof and so on we use here are idealisations, legitimate idealisations (partly because we have concrete proofs of the key theorems of the theories which in essence are the idealisations, in formal syntax and semantics); idealisations we compare to the concrete notions and to the corpus of our utterances but inescapable idealisations all the same. The concrete notions of wff and proof which figure in theories which tell us what exists in mind-independent reality are not susceptible to theoretical generalisations of the type we need in deciding e.g. which logic to adopt (or in showing that concrete truth and proof will come apart because of theoretical arguments setting lower bounds on proof size as a function of conclusion length). In asking whether truth equates to proof we need to look at our formal notions of truth and proof in our (legitimate) idealisations.

The thesis that truth for a concrete mathematical utterance amounts to existence of a concrete proof is not refuted by a concrete thesis which we know will lack concrete proofs or disproofs, if the formalised idealisations link up appropriately (not a trivial matter at all as we see in the case of Godelian incompleteness). No more than our grammatical claim that for any sentences you like there is a conjunction which conjoins them all is falsified by the existence of concrete tokens so large that no conjunction of them all exists (perhaps even could exist). To be sure the Moderator of the Church of Platonism told you that the only reason that the grammatical claim is correct is because the tokens are all tokens of abstract types which exist outside space and time and you have sure and certain knowledge that there is one such abstract type which is the (or a) conjunction of all the types the tokens realise. Anyone lacking faith in the existence of this abstract type is an unjustified sinner, the Moderator intoned, if he or she nonetheless promulgates the grammatical principle that languages are closed under conjunction. Bollocks I say.

Alan WeirThanks Jeff apologies for the delay, I’ve been away for a few days out of email contact. And thanks to Peter for letting us hijack his blog for this exchange!

I won’t repeat your questions Jeff, just refer to the numbered points

1) I claimed that I’m a pluralist not a relativist. There is a trivial sense in which the truth of all sentences is relative: relative to the meaning of the sentence. As regards the truth of the propositions expressed, in the book I declare my view of mathematics to be pluralist but not relativist. If two calculi are derivationally equivalent, then a string means the same thing (in both my two aspects of meaning) relative to one as to the other. But in that case, it has the same truth value in each. If they are non-equivalent calculi (cf. my example in these posts of ordinary arithmetic and the various modular arithmetics) then the string means something different so it is not the same proposition which has different truth values. Of course one might wish to indicate which calculus is determining truth value (via determining provability) by some such notation as indexing sentences (or the conclusion or some such) by a designation of the calculus, and if that counts as relativisation then in this innocent sense I’m a relativist.

2) PA is a formal system, thus an infinite mathematical structure, like the set of natural numbers. Both structures exist, I hold, the claim that they exist is literally true. I also hold that neither exists (in the metaphysics room, as critics of this type of view might say):- it is also literally false that they exist. I’m not a dialetheist, so I think there is an ambiguity here, but not in ‘exist’ rather in the sentences as whole. They mean something different, in the two aspects of meaning, informational and metaphysical which I distinguish, in their mathematical usages versus their ‘metaphysical uses’. What makes them true in one ‘formal mode’ context (a concrete proof) is very different from what makes them false in the other representational mode (non-existence in the mind-independent world of abstract objects). (I used small caps in the book to indicate when an existential claim was in representational mode.) This kind of ‘have your cake and eat it’ position rightly attracts suspicion and a demand for substantive justification, at least book-length I’d say; so pretty much the whole book is devoted to a defence.

3) Applied mathematics I deal with in chapter five in a fairly standard way. A theory which consists of sentences of pure maths plus bridge principles plus empirical sentences can also be treated in its totality as a formal theory, and thus its theorems can be made true in what I call formal not representational mode- made true because a concrete proof exists- just as much as a pure theory. In that mode, they aren’t ‘limning’ physical reality. We have a practical interest in truth in an applied theory where we believe the empirical axioms are all true and we can prove a conservative extension theorem, for then we have grounds for believing the empirical consequences are made true in representational mode by the actual world. Conservative extension theorems for me are true (when concrete proofs exist) just like other bits of applied maths.

(A nice question arises though if we can prove in theory T that some maths plus bridge principles conservatively extends purely empirical theory E and prove it doesn’t in T*. Following the line in (1), I have to say ‘conservative extension’ means something different in T* than T. What if it makes a difference to building bridges, planes, spaceships? Scary- but I don’t think the platonist is any better off here. Compare how, e.g. pure 2nd order formulations of CH are read as logical truths in first order ZFC+CH semantics but not in semantics done in ZFC+¬CH. To say the mind-independent abstract world determines that exactly one is right and the 2nd order sentence is logically true or not depending on which one doesn’t help us epistemically).

Don’t I need Field’s ‘filleting’ out of non-mathematical content from empirical science for the above tactic? Well, I’m not a platonist so not a heavy-duty platonist. So I don’t think, when thinking representationally about the mind-independent world, that vector spaces exist, never mind have causal effects. But Field at the time of Science without Numbers attempted to get by with an ontology which was nominalist in the medieval sense: no properties, relations, attributes, universals, states- nothing like that. But I think this ontology, even though not logically incoherent, is hopeless and that it’s much easier to ‘nominalise’ in Field’s sense if you aren’t nominalist in the old sense. Roughly, you posit isomorphic non-mathematical structures in reality. But that doesn’t always work or make empirical sense, no realist interpretation may be forthcoming. In which case, I say: be an instrumentalist *for that particular empirical theory*. Such a view is perfectly compatible with a general metaphysical realism: it’s the Nagelian idea that the very concepts needed even to think about, never mind know about, a particular domain, may be forever beyond us. M, then, is formally true in mathematical physics as a formal theory, false as a representation of reality. There may or may not be a realist nominalisation a la Field which works, I don’t take a stance on that.

4) ‘consistency’ in these contexts is a notion from proof theory, I’m not going to be tempted to try to say anything interesting about it in concretist terms, indeed I spend some time attacking the idea, which perhaps is a form of strict finitism, that one can translate formal syntax, or any mathematical theory, into a concrete theory. And being rather Quinean about modality, I don’t like talk of possible tipes, or possible anythings at all.

Perhaps this will help. I’m not sure how to superscript in the markup language for this blog so I’ll write e.g. 2 to the power k as 2[k]. Suppose I am working in a fairly standard formal language, say it is propositional logic, and introduce the abbreviation ¬{n}p for p prefaced by k negations, where n is a numeral in some formal notation and k its referent (here I speak in formal, non-representational mode). Then I know that (¬{2[10000]}p & ¬p) is inconsistent and that there are (not small caps) formal proofs of a contradiction of the form (A & ¬A) or (¬¬B & ¬B) from it (say using 2[10000-1] applications of double negation introduction or double negation elimination)). But I might well also know there is (small caps IS) no concrete such derivation in the unabbreviated formalism. Nonetheless I’d say that if one adds some such abbreviatory conventions both for formulae but also for derived rules, one could write quite a small concrete structure down which should count as a concrete proof (not just a proof sketch) of contradiction in propositional logic. Even though epistemically, in order to grasp that the concrete proof is a propositional proof, one would need some arithmetic. (pp. 202-3, 214-5 of the book)

All that raises big and interesting questions about proof sketches versus proofs, the role of abbreviation and derived rules. I know a little of the work by Cook and Reckhow on proof length bounds, extended systems, abbreviation and the like but this sort of topic can pass from stuff I can work on to material which can only be adjudicated by people who work further along from me on the spectrum I set out in my preface: with generalist philosophers interested in maths at one end, philosophers with mathematical training in the middle, philosophically minded mathematicians at the other. My conjecture is my ‘neo-formalist’ position is robust enough to be compatible with whatever results come out of the technical stuff but of course that might prove to have been over-optimistic, that’s a risk you have to take if you are a philosopher rather than a specialist scientist.

In the book I try to take a very liberal attitude to proof, both as to what can concretely realise it; to what the architecture can be like, diagrammatic, natural language, formal, computerised; to how long they can be (no restriction at all) and to whether abbreviation, derived rules, redundancy can be allowed (definitely yes). But clearly I don’t want ‘aye, p seems right to me’ to count as a proof of p. A proof system should have fairly definite rules (allowing axioms as a special case). Another system can be equivalent, in terms of what strings are provable from what, but have a different axiomatisation, or take as primitive rules which are derived in the first. But if I just affirm p, which happens to be a theorem and so an axiom on a different ‘proof architecture’ well that doesn’t count as a proof, likewise affirming say Boolos’ inference as a derived rule. On the other hand, to do that but in addition give a compelling proof, even in a different system, that the formula is a theorem, or the inference is a derived rule, that should count as a proof I think: ‘proof’ is a pretty contextual notion.

On the problem that the maths, metamathematics in fact, used in proving that formal derivations exist itself might be inconsistent, that’s true, there is no Cartesian certainty. Moreover, as noted above, different maths might yield different answers to whether a derivation exists or not, whether a system is inconsistent or not (particularly when one moves to infinitary logic, where e.g. different strengths of choice principle, or lack of it, can make a difference).

Jeffrey KetlandThanks, Alan – that’s all much clearer. (Thanks to Peter too.)

On (1), yes, I agree entirely – the truth value of strings is relative to an interpretation I, so it’s the language-independent meaning that matters. It does seem you’ll have a bit of problem again though, since propositions are abstract entities, but let that pass. On the relativity/pluralism issue, yes, I get your point:

“If they are non-equivalent calculi (cf. my example in these posts of ordinary arithmetic and the various modular arithmetics) then the string means something different so it is not the same proposition which has different truth values.”

Right. I think Peter was articulating an objection to this also. Here’s my version.

Suppose T’ is just a proper extension of T in the same language L. For example

T is Q and T’ is Q plus the axiom “addition is commutative” (i.e., “AxAy(x+y = y + x)”). (Call this deductive system Q*.) Then this means that the string “5 + 7 = 7 + 5” expresses a different proposition in Q and Q*. Or, if you like, “AxAy(x + y = y + x)” expresses different propositions in Q and Q*.

I think this is pretty a strong claim! I take this string to express a single proposition in the interpreted language of arithmetic. And Q doesn’t prove it, but Q* does. It seems as if you’ll get a huge proliferation of propositions (solely on the basis of their derivability status), which are normally identified. On the neo-formalist view, can we say what the proposition expressed (relative to Q) by “AxAy(x + y = y + x)” is? For example, is it different from “AxAy(x times y = y times x)”?

Another question on the truth side. Your basic notion is “t is a concrete proof tipe of concrete string tipe S in deductive system D”. (This predicate applies to triples of concreta.) And then, this is equivalent to “making S true”.

So, we have a predicate written “t makes S true relative to D”. But how does one show this is a truth predicate? I.e., if one replaces “S is made true …” by “S has a concrete proof in D”, how does one get the standard inductive clauses,

(a) an atomic formula s = u is true iff the denotations of s and u are identical.

(b) a negation not-F is true iff F is not true.

(c) a conjunction F&G is true iff F is true and G is true.

(d) a quantification Ax F is true iff, for all n, F(x/n) is true.

It seems like “has a concrete proof in D” is not a truth predicate!

Relating the previous two point, here’s a guess as to what content of a string, relative to system D is, on the neo-formalist view: the content of a formula string S relative to D is the proposition that there is a concrete proof token t of S in D.

This would account for why the content of “AxAy(x + y = y + x)” in Q is different from its content in Q*. But if that is right, it seems a highly non-compositional view of content?

(Must dash – my son, Sam, is in dire need of a visit to the park!)

Cheers,

Jeff

Jeffrey KetlandHi Alan – thanks, lots to take in!

Hopefully this quick summary isn’t a travesty of your view!

Tipe theory is an empirical theory (itself fomulated using tipes); the entities it quantifies over are tipes (squiggles of ink or spurts of sound); and certain kinds of tipes (wff-tipes) are made true by other kinds of tipes (proof-tipes). So, the semantics seems like:

Here goes four more questions/objections:

1.

Relativity of truthSuppose that F is a Q-tipe and F’ is a Q(exp)-tipe. Then there is a tipe t true in F’ but not true in F. So, truth is relativie?

2.

Status of syntactical entities (cont.!)What is a formal system? Say, PA? Is this (the physical aggregation of) six tipes and all tipes gotten by substitution into a certain tipe-scheme? Is there a canonical PA-tipe? Presumably there are many? Each one of these tipes is a finite concretum. This means that, strictly speaking, you think PA doesn’t exist (for PA is not finitely axiomatizable).

3.

Applied mathematics/physicsConsider a mixed statement, say,

What is the semantics for this? This isn’t derivable in pure mathematics, as it’s both mixed and contingent. (We could use Schrödinger’s equation, or the Dirac equation, etc. It’s just that (M), usually written “div B = 0”, is a standard field equation from real physics, and I don’t know any nominalist who can make sense of it.)

Since B is a function on spacetime to a vector space isomorphic to R^3, and your underlying view is that there are no functions, then literally (M) is surely false?

4.

Modal status of consistency of tipesSuppose t is a tipe of the negation of one of my pigeonhole formulas (or Boolos’s using the Ackermann function). Then (I’m guessing here!) presumably: t is consistent iff there is no tipe (logical) derivation t’ of a contradiction-tipe from t. But whether there is, or isn’t such a tipe in a world is a contingent matter. If there is (contingently) no such tipe, then t is consistent! But we have used ordinary mathematics to prove it inconsistent. The solution seems to be to introduce “possible tipes”, and define consistency to mean “there is no possible tipe …”.

(I think there’s an important subtlety here: the difference between “t is inconsistent” as an ordinary claim, true (in English) iff t is inconsistent, and “t is inconsistent” as a mathematical claim, true-in-F and not-true-in-F’, etc. Roughly, it seems to me that your truth definition doesn’t let you disquote the latter if you have merely generated a F-derivation tipe of “t is inconsistent”. After all, F might itself be inconsistent! So, you can’t conclude from this that t actually is inconsistent, unless you have soundness expressed, in the metatheory (i.e., about F), in some standard form – e.g., as a reflection principle for F.)

I’ll stop there!

Cheers,

Jeff

(I just take science as is, with its quantities, fields, symmetry groups, spacetime tensors, Fock spaces, etc.; since science has a significant epistemic status, and is inconsistent with nominalism, I tend to reject such things. But this is just Quine-Putnam, so I won’t dwell on it!)

Alan WeirNo woops, I take this bit back:

‘If there exists no concrete feasible structure which we could interpret as a proof that in the formal idealisation of a given concrete body of utterances, the mathematical correlate of tipe A is formally derivable, then A is not true.’

It should be:

‘If there exists no concrete feasible structure which we could interpret as a proof that in the formal idealisation of a given concrete body of utterances, the mathematical correlate of tipe A is formally provable or else refutable, then A lacks a determinate truth value’.

Alan WeirJeff: ‘the claim that there is a tipe of some sort is a claim of empirical science?’ Well ‘science’ is maybe a bit too grand but yes it’s an empirical fact in each case. No I don’t reject the Completeness theorem (for systems which are complete!) You say

‘For derivations are finite sequences of finite sequences of symbols, and you don’t have a tipe for each derivation.’

I agree there aren’t derivation tipes for lots of theorems- even in finitary logic and remember I accept infinitary logics. But the completeness theorem is not a claim about concrete tokens and tipes, it’s a mathematical theorem relating formal semantics and formal syntax. You can prove only a limited amount of things about concrete tokens and tipes directly. You can’t prove every wff tipe is an immediate constituent of a negation, some will exist which never get negated. You can’t prove every wff tipe of a given corpus has an even number of left and right brackets- you need induction or similar to prove that and concrete bodies of utterances aren’t amenable to that because, for one thing, abbreviation ‘induces’ gaps further down the structure of a tipe formed using abbreviation. (Moreover you’d likely come across a token which didn’t have the even brackets property and would write it off as an ill-formed mistake. But you are guided by formal syntax here. We can demonstrate non-trivial generalities about our concrete practice but only by going via meaningful, true, standard maths and the haphazard embedding of the concrete system in the formal. Strict finitism is hopeless.)

I accept the completeness theorem as true- I’m not a fictionalist, I think mathematical theorems are true. I’ve seen concrete proof sketches of it, I believe it is prov*able*. The modality here I take to be very weak. Perhaps best taken as: there actually exist concrete structures which we, with our actual powers, could interpret as proofs, could (with our actual powers, in an everyday sense of ‘could’) check any part of, even if we couldn’t take it all in. Or perhaps that we could design machines whose general operation we understand which could help us do this.

Appeal to machines won’t alter the fact, though, that as I accepted in the previous post, there are short feasible theorems (or entailment claims) with no feasible proof. I downloaded your Analysis article, excellent stuff. I discuss Boolos’ curious inference which you start from in a few places in the book, most fully pp. 178-80 (and make the point, very informally I didn’t know how to calculate the length, that the formal version of ‘there are 125’ would be pretty long (p. 129 fn3)). Your examples highlight further the problem for we formalists by showing how such homely examples can quickly become unfeasible.

I, of course, think the formula you sketch above is logically true, after all you’ve given a concrete proof (or at least proof sketch- I’m inclined to think the proof sketch/proof distinction isn’t all the philosophically important even for a ‘concretist’ like me but maybe I’m being complacent). Now sometimes if we alter the rules of inference, we change the derivability relation over the language in question and then we change meanings. If we now prove some string we couldn’t feasibly prove in the old system then we haven’t necessarily proved the same proposition. The arithmetic to modular arithmetic case I discuss above is of that sort. But as I said in my discussion with Peter, a different proof system which generates the same theorems doesn’t change meaning for me. So if you give a short proof in a more powerful system, set theory, higher-order logic, which is conservative over the ‘lower’ language, I’d count that as a proof, thus something which makes the sentence true.

This still doesn’t alter the fact that the equation of truth with proof central to my formalism is bound to break down in places at the concrete level, specifically with concrete wff tipes that lack concrete proof (or disproof) tipes in any proof system which yields the derivability relation that characterises our system (e.g. by being equivalent to the one we use to introduce the system). For such a tipe A how can I hold A v ¬A? Well, I might not, perhaps not in higher set theory; but I certainly want to in Delta-zero arithmetic. (I used angled brackets to put the zero in, in my previous post, but discovered that wipes it from the blog HTML!)

Why is LEM a problem for me? Because I reject supervaluationism (and set inferentialism aside too, p. 78 fn 14) and say that a disjunction is only true if one disjunct is true, and that truth = proof. But no one can prove that claim about disjunction over concrete tipes, one could only go through a few of them one by one asserting it. We have to take the concrete system to be a fragment of a formal system, give the (non-supervaluational) clause for disjunction, and prove inductively unique readability results establishing that every disjunction has a unique truth value which is only true if one disjunct is. We work with a formal notion of truth in other words. And to establish whether truth equates with proof we look at derivability in the formal system and see if we can equate formal truth with formal proof. For some systems (but not all, only prime ones, including negation complete ones), we do have truth equating with proof and only those are genuinely coherent for me. That a given concrete tipe in the body of practice we idealise in the formal system has no concrete proof nor disproof doesn’t falsify formalism, for me. Similarly the fact, as it might be, that a million distinct concrete wff tipes exist but their million-fold conjunction tipe does not, that does not show that the language is not closed under formation of conjunctions.

It is crucial, though, that the mathematical theorems which generate our idealisation, which for me is just the formal system not anything modal, are ‘concretely true’, have concrete proofs. If there exists no concrete feasible structure which we could interpret as a proof that in the formal idealisation of a given concrete body of utterances, the mathematical correlate of tipe A is formally derivable, then A is not true. (Of course what makes a formal system a legitimate idealisation is an important question; and interesting questions would arise if different coherent mathematical theories made conflicting claims about what is or is not a wff, or is or is not provable, in what we take to be one and the same formal idealisation.)

I agree with what you say about modality if that goes beyond very quotidian uses such as ‘I could walk the West Highland Way’ (not sure that is true right enough!) or ‘I could write out a 1,000 symbol formula’. Stronger notions of modality, certainly those to be found in modal realism, raise equally bad epistemological and metaphysical problems as abstracta (I hold forth on such lines at pp. 139, 167-8, 181-91).

But you should worry about all your realism regarding this stuff, Jeff! At least if you are any type of naturalist. How can you rest happy with entities even weirder than Cartesian souls- outside space as well as time? How can you hope to give a naturalistic explanation of how you can even conceive of particular examples of such things, never mind know things about them??

Jeffrey KetlandHi Alan,

Great – thanks for that. (I was going to mention Quine/Goodman 1947.)

But then it looks like your syntax is a part of physics – i.e., the claim that there is a tipe of some sort is a claim of empirical science? Does this means that you reject, e.g., the Completeness theorem: if A is valid, there is a derivation of A. For derivations are finite sequences of finite sequences of symbols, and you don’t have a tipe for each derivation.

Maybe this might focus that objection. Consider the kind of pigeonhole example I gave in a 2005 paper, “Some more curious inferences” (Analysis). One can express “If there are 101 dalmatians, and 100 food bowls, and each dalmatian uses exactly one food bowl, then at least two dalmatians share the same bowl” as a sentence of first-order logic (quite long). It is valid, but its validity requires a derivation with about 10^7 symbols. Suppose I give a formula of this kind (say with just 1000 symbols) and prove (using ordinary mathematics) that it is valid, and that it has no derivation with less than 10^{100} symbols – and therefore using mathematics I prove that it has no concrete proof. Is the formula valid?

I guess that the idealization approach is a form of “going modal”. Is it ok for someone who rejects abstracta to go modal? When Quine later reminisced about Q&G1947 and nominalism, he said in connection with going modal that “the cure is worse than the disease”! For example, the epistemological problem (how do we gain epistemic access to these abstract/modal facts) seems about the same, and the metaphysical problem (abstract/merely possible entities are spooky) seems marginally worse.

Of course, as you probably know, I’m a realist about all this stuff, and never worry about it!

Cheers, Jeff

Alan WeirHail Jeff! There’s somebody else out there listening, which is great!

The main problem you raise I take to be a fundamental, probably *the* fundamental, problem for formalists (pp. 8, 72). This is, very briefly, that formalists take mathematics to be grounded in formal systems (not necessarily orthodox first-order predicate logic ones but that’s irrelevant) and formal systems have effectively the same expressive and ontological powers as arithmetic. So no escape from platonism.

A main aim of the book, then, is to answer this objection. So to your question

‘Can I ask about your syntactical metatheory? Does it quantify over types or tokens?’

my answer is definitely not types, as abstract entities, that would spell defeat (if used in the metatheory which explains what makes mathematical utterances true). But something a bit more general than tokens. In ch. 6 ‘Proof Set in Concrete’ I attempt a sort of dusting down and revamping of Quine and Goodman’s ‘Steps towards a constructive nominalism’ reconstruing ‘types’ as concrete entities in an attempt at a purely physical concretist syntax. The most obvious idea is to drop abstract types in favour of mereological fusions of concrete tokens. I have some discussion of whether mereology is nominalistically suspect, put forward a few alternative candidates. But since the mereology I need is very weak, in particular all the entities of the syntax are small finite things we can digest and work with, mereological fusions probably can do the job. So the mereological fusion of all tokens equiform (not a simple notion I admit) with this token: ‘Quine’- I call the *tipe* of that token. (I had a bit of a proof-setting hiccup when the proof-reader changed all occurrences of ‘tipe’ back to ‘type’ and I had to change some, but not all, tokens of ‘type’ back!)

This has the consequence, a bullet I bite, that there are only finitely many, and rather small at that, sentences and proofs, construed as tipes. What about all the missing mathematical propositions? A formalist might try shrugging them off: you can’t produce any tokens of them why should I worry? But we can’t shrug off the following problem with proofs which exercises me quite a bit in the book. Many small comprehensible token theses: a simple example from Neil Tennant is certain primality claims applied to a numeral which includes an exponential tower string- we know will have no concrete proof or disproof. Any such proof/disproof would not only not be small and comprehensible but require more tokens than neutrinos in the observable universe etc.

So we need to idealise. I set my face completely against idealisation via appeal to supernatural beings, superheroes who can carry out any algorithm or perhaps supertasks etc; appeal to such beings is no more legitimate here than in biology, (the phrase ‘in principle possible’ is the last refuge of the philosophical scoundrel!). Chapter seven tackles the strict finitist, someone I, with the above concretist goals, have to take seriously (there do seem to be some about anyway, dotted around the shores of New Jersey and the like). The concrete tokens and tipes which constitute the actual reality of syntax, according to me, form a relatively small and in particular *patchy* universe; the all-pervasive use of abbreviation means we can have comprehensible tokens which lack nearly all of their constituents- no one could attempt to write them out in full. This, I argue in that chapter, blocks any attempt to prove anything systematic about concrete syntax, your example of unique readability is one I give, also the definition of wff, proof. We can’t do any systematic theorising about our concrete language without formal syntax, essentially arithmetic; when we move on to semantics, we need likewise set theory or something similar.

So I agree with you on all that. But my version of formalism holds that the theorems of all these theories are true. A little more carefully, if there exists, or could in a practical sense exist, a concrete proof of a token of formal syntax: saying that every wff of a given formal system is uniquely readable, or that Delta arithmetic is negation-complete or whatever, then these are truths about those formal systems. And we can see our corpus of actual tokens and tipes as a fragmentary, patchy, small finite, realisation of that formal idealisation. But the formal theory feedbacks back into actual concrete practice helping us set norms. If we want to know whether a particular area is bivalent, so for me this means negation-complete, we don’t ask whether for every token there is a token proof or disproof, we ask if there is a concrete proof of a formal negation-completeness result for the idealised theory. If so, we are allowed to lay down all instances of LEM for that sub-language as axioms (excluded middle does not hold in the logic I use), even if that means that some concretely provable theorems (or axioms, one line proofs): t is prime or t is not prime say- have disjuncts which are neither concretely provable nor refutable. I suspect this get out of jail manoeuvre will prove one of the biggest sticking points in the reception of the book, but I’m still confident about its legitimacy!

As to Gödel sentences, the Gödel sentences for extensions of Q which are true in the standard model (a notion from formal syntax/semantics of course) are themselves true I hold, true because provable in omega logic. The last chapter develops a non-classical infinitary logic (going way beyond omega logic) whilst prior to it chapter seven argues against the notion, which took root in the 1930s with Gödel, that the legitimate idealisation of concrete derivability should be constrained by recursive enumerability, nothing closer to actual practice (like derivable in polynomially-bounded logic) and nothing infinitary. Infinitary model theory is ok as an idealisation, orthodoxy has it, but not proof theory. I have never seen any rational justification for this prejudice whatsoever. But I suspect that will be another sticking point!

So to the abacuses and actual smart phones, computers:- yes, like us they are finite, bounded, patchy realisations of larger structures, infinite structures in fact, even for finitary systems where each element is finite. The structures don’t exist, we should say in the metaphysics room, but theorems which proof the existence of e.g. Turing machines as abstract devices, are concretely provable.

And Jeff: get the library at Edinburgh to buy the book otherwise I’ll send some neds out from Glasgow to ‘interview’ the subject librarian!

Jeffrey KetlandHi Peter, hi Alan

Thanks for these detailed discussions, Peter – really interesting!

Alan, I haven’t got your book, I’m afraid, but it sounds like fun.

Can I ask about your syntactical metatheory? Does it quantify over types or tokens? If types, does it assume at least 2 types (presumably you assume a symbol for “0” and a symbol for “S”, and presumably even some primitive variable, say “x” and some way of getting new ones – e.g., by suffixing with a prime symbol, “x’ “, ” x’ ‘ “, etc.)? If so, does it assume unique readability? And that the set of terms is the smallest set containing variables, constants and closed under applying function symbols?

If so, then your syntactical metatheory interprets PA. If you have all the correct atomic sentences, then the term model for your syntactical metatheory is isomorphic to N. So, is this formalism – when you’re assuming a metatheory at least as strong as PA?

Also, since your syntactical metatheory (if it’s about types, finite sequences of symbols, etc.) seems to be sufficiently strong to interpret PA, it is incomplete. Consider an undecidable sentence about the syntax (e.g., “The syntax metatheory assumed by Weir in his book is consistent”). Does this have a truth value?

I have another quick question about the abacus here – I think it’s meant to be a real physical abacus. A finite computational device (like the innards of an iPhone with its calculator app) will only compute successor, addition, etc., partially, because of finite memory constraints (I guess it’s a Turing machine with a finite tape). But when we use such devices, we generally see how to idealize, and consider what the physical device would compute if memory resources were increased. Is that how you’re thinking of the abacus?

Cheers,

Jeff

Alan WeirThanks Peter; I think I can avoid the strike against neo-formalism you outline, let’s see if I can convince you.

Yes I am a pluralist- not quite that ‘The truth-value of ‘68 + 57 = 125’ is not relative to a formal system’ but certainly, as you go on to indicate, the proposition it expresses is not thus relative. My staple example is modular arithmetic. The proposition that string expresses when the underlying game is arithmetic is a true one, when it is arithmetic modulo 50 it expresses a different, false proposition.

I also agree that it would be very odd to say that the children whose affirmations or denials of ‘68 + 57 = 125’ are sometimes keyed to the abacus, sometimes the calculations on the slate, sometimes their calculator, are expressing propositions with different senses. So I don’t say it, for example, on p. 218 I say:

But my children carry out long multiplication and division by a slightly different algorithm from the one I was taught all too many years ago at school. Do we then understand 56 x 843 = 47208 differently? Surely not.

and accept that utterances prompted by calculators which arrive at the same results express the same sense even if the algorithms used are different.

Am I entitled to do this, though, on my account of sense? On that page I suggest that a necessary condition on sameness of informational content for mathematical utterances is that the underlying derivability relation is the same. If my kids (in full command of their senses, after the application of any correctional dispositions which apply etc.) derive, when playing a particular game, B from A just when I do, we mean the same. So we do in that arithmetical case, but not if I am doing modular arithmetic and they are not.

This is more complex if the tokens are even more different than their Belfast speech versus my Glaswegian: if we are comparing Fermat’s seventeenth century Latin arithmetic to mine, for example (p. 219). So yes the sense in which there is an ‘admissible’ mapping between his language and mine is not clear, but I’m not sure that anyone has made it clear. That’s a big, big project in philosophy of language and I don’t pretend to have done anything much towards it in this book.

So although I think sense is more fine-grained that even necessary co-extensionality, it is not fruitful to make the notion maximally fine-grained. Many will hold that in some sense language-understanding is constituted by linguistic practices. Some, like me in chapter Two §II, distinguish between (roughly speaking) meaning-constitutive practices and others. But that does mean one cannot try to find an (approximate) equivalence relation across such practices which encompasses different practices as different ways of grasping the same sense. In a trivial sense that is inevitable where the token utterances are not homophonic and we will not get a concept of sense which corresponds at all closely to the one we use unless one tries to do so. I’ve suggested that sameness of the derivability relation should form a component of the account in the mathematical case and different routes, as it were, for getting to B from A don’t matter, if speakers (correcting for errors) agree on what can be derived from what.

Does that answer the crucial objection: ‘By mishap the child could come to believe 68 + 57 = 125 in the comment mode in one context and disbelieve in the other: so the contents had better be different.’ Well in my Fregean account of informational content on pp. 26-7 I gave a sufficient condition for sameness of such content but qualified it by the rider ‘holding context fixed’. It’s an interesting example though. I’d ask, would the child who disbelieves, when using the abacus say, retract when taken through the abacus operations more carefully? If not, then she does express a different sense (or perhaps no determinate sense at all) when utterances are keyed to the abacus than to the slate. If so, if the corrected derivational practice is the same then there is no difference of sense.

Compare somewhat different examples from different theoretical frameworks. Direct reference theorists, insofar as they have a notion of notion of sense, might agree that someone who says ‘Jim is middle-aged’ to Alice, and ‘Jim isn’t middle-aged’ to Bob- believing wrongly that the two ‘Jims’s she’s picked up from those two people refer to different individuals- nonetheless means the same by ‘Jim is middle-aged’ in both cases. Or take a rather verificationist view which associates two distinct criteria with F, both, let us say, reliably linked to the same property in the world when applied properly. Jim might be more prone to mistakes using one not the other and might affirm t is F and then in essentially the same context deny it when applying the other procedure. If when corrected he’d come to agree regardless of the criterion used, I’d say he expressed the same sense in both cases, and is mistaken in one. And I think I can say something similar about my fine-grained, but not maximally fine-grained notion of sense. Different practices at the very fine-grained level can ‘realise’ the same sense.

I’ve appealed, of course, to derivability relations. Aren’t they abstract relations relating abstract objects? Well, no because no such things exist according to me. Nonetheless formal proof theory, and certain applications of it to mesh with the theory of understanding generate true theorems, I say, because they too get made true by concrete proof tokens. But I suspect my claim to be able to invoke such talk whilst not compromising my uncompromising anti-platonism will not be accepted lightly!

Finally I think my view of the relation of pure maths to practice is, if not quite ‘topsy-turvy’, certainly anti-Wittgensteinian as you say; that’s important to my account of applications in chapter five. I’d try to soften any implausibility here by saying that the emphasis is on the independence of the meaning of pure mathematics from arithmetical practice. But this isn’t a temporal matter. Pure and applied usages might develop at the same time. In a certain restricted sense, the applied could even come first. The child might learn ‘the number of apples in the bowl is 5’ as tied to a perhaps rather primitive understanding of numerical quantification, ‘there are five apples in the bowl’ before learning the algorithms for adding. But once the latter are learnt they give the pure sentences their entire meaning- that is indeed my view.