5

In software engineering one often starts with defining principles, standards and guidelines that programmers should stick to and apply in their products. There comes a moment when one has to evaluate whether these rules were obeyed. It was suggested to me that Tarski's Convention T would be useful here.

I understand this partly, it's purpose apparently is to define the conditions in which a given statement is true, right? But why would I care?

"Snow is white" is true iff snow is white. That is the kind of statement that would cause my teenage daughter to say "duhh!". I'm trying to find the practical use of Convention T in a situation where a standard says, for example: "All data exchange between two systems is done in XML". When I want to verify that a certain system does indeed exchange its data through XML, what good would Tarski be to me?

  • 2
    Just to point out, you're missing the use of Truth in your biconditional. "Snow is white" is just a sentence, and it's a category mistake to say that it is iff anything! This is an example of a "use/mention" confusion. – Paul Ross Nov 7 '13 at 22:09
  • Edited the statement. – Lisosia Nov 8 '13 at 7:58
8

Tarski's Convention T is not strictly speaking a definition principle for truth - it is an evaluation condition on whether a given axiomatically theorised predicate is a "Materially Adequate" definition to count as a Truth predicate.

The work that Tarski did in showing how a truth predicate could be defined was not in presenting the T-Schema. That "snow is white" ought to be true if and only if snow is white is just something that Tarski reckoned anything that might be called "Truth" ought to satisfy, in the same kind of common-sense way that might meet your children's exacting standards.

Tarski's work was presenting a way in which we might take our formulae of first order logic and understand what mathematical sense we might make of them. Tarski started by presenting the idea of a Model, as being an algebraic characterisation of a domain of objects, relations over and between those objects, for a class of names, constants and relation/property terms in our logical language, and a notion of an interpretation function that connects the various terms in our language to either objects or relations in our model.

A model deems an atomic sentence P(a) (or is_White(snow)) true (or sometimes we say "value 1" to distinguish it from the question of the Truth predicate) if the interpretation of a is an object in the domain that is a member of the relation interpreted by P (that snow, being the interpretation of snow, is a member of the set of white things, being the interpretation of the predicate is_White(x)).

Then, the interesting aspect of Tarski's notion of a model is it matches the compositional structure of logical language, so we can add connectives like "and", "or", and quantifications like "every", "some" as part of how we mathematically model the domain of objects we're interested in, and build up more complex sentences from the basic cases. So thanks to using the maths of model theory, we can make sense of something Not being white, of what it would mean for everything to be white, or (given that there are other colours) how we might test whether something is "white and not some other colour" etc.

By making mathematical sense of a logic in a model, Tarski showed that we could in principle define a Truth predicate over an interpreted language as a way of considering well-formed value 1 logical sentences as a class of "True sentences". He did this through a notion of what it takes for an object to satisfy an open formula. This is interesting, because it shows that there is not only a sensible and useful algebra for logical languages, but also a sensible and useful algebra for modelling logics and reasoning about how evaluated sentences might relate to one another. So if we want to be able to comparatively evaluate different logics or theories, we can use a Tarski-style definition to build mathematical models of their sentences and use mathematical tools to analyze them. As an example of how you might use this definition, suppose we might ask a sequence of logical questions, and want to test whether the resulting answers are all true. If Truth is well defined, there exists in principle a way of testing all of our sentences to show that they are all members of that class.

Fortunately, for standard models, Tarski's construction satisfies the principle of the T-schema - a given sentence is a member of the class of True sentences just in case the sentence interpreted in the base model is given the value 1 through the model-theoretic semantics. So there is a fairly simple algorithm for evaluating all of some set of sentences for truth - namely, interpret them in the base model and evaluate them, continuing on if they get value 1 and returning if any gets value 0. This isn't going to be true of all sentences in all models (consider - the Liar sentence "this sentence is not true"), but the construction shows how we can characterise a truth predicate over some base model and thus treat it as itself an object for comparative evaluation.

You can have a look at the SEP Article on Tarski's definitions for a more worked-through explanation of the mathematical project he was trying to build. A concrete instance of how this kind of reasoning sheds light on practical problems in mathematical logic is in the idea of reducing quantified logical sentences to a Skolem Normal Form, which massively simplifies the problem of automated theorem proving. We can do this because Skolemized sentences are "equisatisfiable" with their quantified counterparts.

What we might say is that software specification and verification ought to be suitably founded in a semantics in just the same way that first order logic is founded in the model-theoretic programme following on from Tarski's initial discoveries. In formal computer science, this is studied in the field of Denotational Semantics and other related programmes, and some of the ideas about what kind of axiomatizations there are for correct software (and also hardware) behaviour are considered in Formal Specification and Verification logics such as Floyd-Hoare logic.

  • Your answer is elaborate and points to at least one source I found myself, but regrettably I fail to grab what you mean. I'm trying to apply this in a situation where an acquirer of software just wants to know whether or not the developer followed all requirements. It was suggested to me by a mathematician that Convention T might be helpful, but I do not have access to him anymore. This stuff intrigues me, but in school I was a total loser in math, even though I now work in the software business. – Lisosia Nov 8 '13 at 8:05
  • @Lisosia, I'll see if I can tidy things up a bit, but if you're going to look into formal verification processes, you're going to need to get a bit mathematically stuck in! – Paul Ross Nov 10 '13 at 17:33
  • 1
    @Lisosia, I've tried to tweak and expand the answer to make it a little more practically applicable, but I'm still not sure if it matches what you're looking for. I definitely recommend looking into the Floyd-Hoare material, which might really be closer to the kind of thing you want to know - namely, given some process with outputs and inputs, is there some logical analysis of what we might expect a given program implementation to do? – Paul Ross Nov 10 '13 at 18:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.