Actually, the trope is the second of four topics I wish to address

I recently exchanged opinions with Michael Jackson on the use of mathematics and logic in software development (his main interest) and system safety engineering (mine). If I understand him right, Michael believes that a story must be told about how mathematics and logic applies to clarification of things expressed in natural language, and about how mathematics and logic applies to the world. I have what I believe is a simple, direct story, which comes first.

I believe that people working in system safety engineering often form opinions about use of mathematics and logic which are wrong. These opinions propagate amongst sympathetic hearers, and thereby become tropes. I want to address here one such trope. This comes second.

Third, I comment further about the Hazan I discussed earlier in Progress in Hazard Analysis.

Finally, I say a word about the justification for model-theoretic semantics for first-order logic, as proposed by Alfred Tarski some 75 years ago.

First, the story about applying mathematics and logic. There is some story about how natural language works. I don’t want to suggest here what that story is; just that there is one. Whatever that story may be, I hope it is compatible with some sort of Austinian naive realism, as follows. When I assert “the sky is blue now“, I am referring to a real object, the sky, ascribing to it an objective property, that of being blue, and what I say is true or false, or indeterminate if it approaches a color boundary uniformly (say blue-grey), or it is disproportionately covered with cloud and so on. The story will explain how I refer (to a real object in «the world»), how properties are ascribed, and what counts as success for such an ascription («true») and what as failure («false») with some middle group («indeterminate»).

Exactly the same story, whatever it may be, holds for a formal language. Whatever the story is about how reference works for designatory terms, how property ascription works, how truth and falsity is determined, works the same way for a formal language as it does in natural language. Whatever I can say, and however I can say it, I can also say it formally in just the same way. The only ability I need to be able to say something formally which others might have expressed in natural language is the ability to parse.

Mathematics in its function of applying to the world, and logic similarly, extend the naive view of language expressed by the sky example in that they are schematic ways of doing things. That is, they generalise over concrete instances and demonstrate to us inferences we may perform that lead from true things we know to true things we were not necessarily sure about but now may be sure, after the inference has been performed. I may derive an answer to 456 + 7491 = ??. I may accept A and accept B, and want to know what I can assert about both in one assertion: for example, (A && B), or (A OR B). Alternatively, attempted inferences we wish to make do not go through, for example we know (A OR B) and want to know what this tells us about A (answer: nothing), and we are thereby induced to discover additional truths which may make them go through, or conclude indeed that our wished-for conclusion might be wrong.

Whatever the story is about how all this works, it works with other things also. I know the law forbids me to drive my car immediately after the “30” sign at 50 kmh, and I do not have to tell myself a complicated story about abstractions and symbols in order to explain the summons that comes in the post after I do so. Few of our fellow citizens who had problems with math and other abstractions in school have difficulty understanding why that summons arrived. So some story of how general schemes work is available to them, without it having to rely on those difficult topics which they could not master in school. Naive realism works for them. For the story about how engineering mathematics works, or business book-keeping for that matter, I am also inclined towards some kind of explanation along the naive-realistic lines proposed by Penelope Maddy some while ago (Realism in Mathematics, Oxford University Press, 1992).

If one doesn’t go for some such account, then it seems to me that the only available alternative is to explain the success of business book-keeping in terms of some sort of tacit convention, as John Searle explained concerning the use of money (The Construction of Social Reality, Penguin, 1995). We somehow “agree” to use arithmetic to come to agreement on transactions. But then the question arises why we use Peano arithmetic (PA), that is, the calculations that are theorems of PA, rather than some other calculations which are not. One can show certain advantages. For example, if I agree with the merchant that I may buy two items and pay him the Peano-sum of the prices, we can merge transactions rather than having to make two separate consecutive ones. But then, a story still has to be told of how PA correctly predicts what change I have in my pocket after either form of transaction, and that this turns out to be the same whether I make the one transaction with the sum, or the two transactions consecutively. PA is obviously more useful than other alternative calculations and a purely-conventional account must explain how this comes to be. A Maddy-type realism account gives a straight answer.

Logic is the science of inference. It says what conclusions follow from what premises because of their form (and how), and provides some methods of determining conclusions that may validly be drawn and those that may not be. It is a science of the use of language. We may and do put it in mathematical terms nowadays for the same reason, I suggest, that Newton was able so to formulate his natural philosophy, and merchants, much earlier, were able to do so for their transactions, and invented 0 to help them. There are certain generalities we discover that may be put in a much more perspicuous and manipulable form by such techniques than if we continue to use our everyday words to work with them. But the principles remain the same. Naive realism suggests that no new story must be told to explain how this works than must be told to explain how language works in general (whatever that might be).

There are some people who want to say “formal logic is not very useful in engineering“. Formal logic is one way of putting the science of inference in manageable terms, and inference is especially useful in engineering, indeed it is one of the main two or three activities in engineering, the others being bending metal and talking to liability lawyers :-).

Second, the trope. There are some people who want to say “formal logic, say first-order logic, has Tarskian model-theoretic semantics, so one needs to have a model of anything expressed in first-order logic, and this model is mathematical, and mathematical abstractions cannot be a perfect guide to reality; there’s always some misfit“. I see that kind of argument a few times a year and I think it is balderdash (to use another word starting with “b”). Since I see it a few times a year, I conclude it’s a trope. Since it’s balderdash, I conclude it is misleading.

First point: I use first-order logic (FOL) to talk about inferences in language. No one can force a Tarskian semantics on me purely through that use. (I might still want to use one, though, and the final portion of this note explains why.) When I talk about the sky, I have in my FOL-language a term “the-sky” that designates that (here is interpolated the usual story about reference, identical for my NL talk and for my FOL-talk, whatever that story might be). So, in the trope, that step to model-theory fails.

Second point: it is demonstrably not true that there is always some misfit between mathematical “abstractions” and reality. Peano arithmetic tells me exactly what the reality is about monetary transactions. There is no misfit. If one might be worried about Wittgenstein’s point (actually, Kripke’s point which he attributes to Wittgenstein in Wittgenstein On Rules And Private Language, Harvard University Press, 1982) about how one can tell if one is applying a rule, let’s restrict talk about Peano arithmetic and reality to all combinations of transactions in £ and ¢ which lie under £1.

There are a few logical Luddites in system safety, but I don’t know any who go as far as to argue that you always have to remain wary of your demonstrably-correct arithmetical calculations in case the world just doesn’t fit arithmetic exactly. That formalising one’s inferences should be somehow metaphysically suspicious while formalising one’s arithmetic is not seems to me to be plainly inconsistent. If you asked a civil engineer to design a bridge, and heshe gave you a design, and you asked for the engineering calculations, and heshe said “well, we don’t have any, because statics relies on calculus and arithmetic, and calculus relies on arithmetic also, and, well, we are suspicious that arithmetic may not be a helpful guide to the way the world really is“, what would you think? I know what I’d think, and I may be tempted to put it in writing and send it off to the engineering institution that chartered that engineer.

Third, progress (unfortunately not so much) on the Hazan example. The reason I addressed the trope above is that it arose during discussion on the York list of the Hazan example which I treated a couple of notes back in Progress In Hazard Analysis. Here is where we seem to be (to be stuck?) on the example today.

Recall that Daniel Jackson formalised the analysis in Alloy, and found that the initialisation conditions were not addressed in the STPA analysis. Nancy Leveson says in a reply that these conditions are handled later in the book, but does not provide a citation.

Daniel included his analysis in a set of slides he produced for How To Prevent Disasters, his Keynote talk at SIREN//NL in Veldhoven on 2 November 2010. A “more polished” version of the Alloy model is at this associated URL.

I had another question of the STPA analysis, posed in this note: how does one show completeness of the high-level safety requirement? What this meant was not apparent to everyone; for example see Andrew Rae’s response. Translated, using the terms introduced in Formal Definition of the Notion of Safety Requirement, the question means: how do you show that you have captured all the necessary safety properties expressible in the limited vocabulary that you are using at this stage, and not captured more than you need?

If the answer is to be “this is impossible” (the original answer, but possibly misunderstanding the meaning of the question, from this note) then the answer is simply wrong. If the answer is to be “this is not possible in [XYZ proposed Hazan method]” then I would observe that [XYZ proposed Hazan method] forgoes an objective test of its quality, which other methods (such as OHA) have shown how effectively to incorporate.

To date, I have seen no technical answer to the question, despite subsequent discussion about the matter on the York list.

To summarise, (1) Daniel Jackson’s analysis using Alloy showed a weakness of the specific analysis of the example. I am not familiar enough with STPA to know whether it requires a check for initialisations. Since the example evidently did not include one, I would imagine not. If this is so, it seems to be a weakness. (2) It appears that STPA does not explicitly require a check that all necessary safety properties expressible in the vocabulary at a certain development stage have been captured; and no more than necessary. This is possible within certain limitations (indeed OHA shows how to go about it). A method which does not do this foregoes an objective test of its relative success.

Fourth, and finally, the model theory of FOL and its foundations. It was invented by Alfred Tarski in the 1930’s. I met Tarski in the 1970’s (I did my Ph.D. in “his group”, the Group in Logic and the Methodology of Science at U.C. Berkeley). Tarski was very clear that everything he did was science. He treated the subject matter of mathematics as no different from trees or galaxies. As far as he was concerned, he was discovering things about the world. He would have had no patience with people who argued “it’s a model, and models cannot reflect reality perfectly“. I think he would have said “models are reality; just bits of it, not the whole thing“. He thought the encapsulation into models was a form of closed-world assumption in the same way as, when we talk about the vagaries of chess, we do not need to invoke quantum mechanics or the make-up of distant galaxies. I imagine he would have said: in the same way in which if we are talking about the hazards to an A380 aircraft taking off from London Heathrow airport, we do not need to invoke the weather in Beijing. The language of a model is a restriction to what is relevant, no more and no less. And to determine what is relevant we have criteria which are outside the model itself, but which are no less clear for that. So people invoking the trope considered above are also, in my view, being unfaithful to the justification with which model-theoretic semantics for FOL was proposed.