Ariel Roffé is a member of the BA-Logic group (which meets periodically at the IIF-Sadaf) and the ANFIBIO group. He has a scholarship from Conicet to pursue his doctoral studies. His research subjects lie at the intersection between logic, philosophy of science and computer science. The reason for this interview is the recent publication of an article by him in the Journal of Applied Non-Classical Logics, about one of the computer programs he designed, called Reconstructor.
Mariela Rubin: What is Reconstructor? What is it for?
Ariel Roffé: Reconstructor is a computer program that has as its main goal to allow researchers to test formal reconstructions of empirical theories.
There is quite a long tradition in the philosophy of science of trying to formally reconstruct or represent the content of scientific theories, using the tools of logic. This tradition began with the logical empiricists and, after its disappearance, continued (although as a less dominant task) in various schools. One of those is metatheoretical structuralism, in which we work at the Centro de Filosofía e Historia de las Ciencias, at the National University of Quilmes.
But independently of the school in which one works, there is something common to all these formal metatheories: none counted with systematic methods to test their products, until now at least. In other words, if one worked within one of these schools, then one would typically make a reconstruction, and then check by eye if it was adequate, that is, if it expressed the same thing than the target theory being reconstructed.
What I do in the paper is to delineate a methodology for testing reconstructions, and to provide a computer program capable of reasoning semantically in order to carry out that methodology.
MR: What does this methodology consist in?
AR: It consists of various things. An example would be the following. In the structuralist metatheory applications of theories (either successful or unsuccessful) are represented by models (in the logical sense of the term). Thus, one the things that I propose is that models that represent paradigmatically successful applications of the target theory must satisfy the formalization of the laws. The reverse must also happen with paradigmatically unsuccessful applications (the models that represent them must not satisfy the formalization of the laws). In that way, one can see that the reconstruction “behaves” in the same way than the target theory.
This is similar to what we teach students in an initial logic course, when we given them as a criterion of adequacy of a formalization of a natural language sentence the requisite that it must have the same truth conditions as that sentence. The idea here is similar, but what functions as the “empirical basis” of a reconstruction is not so much the intuitive understanding that we assume that our students have as competent language speakers, but rather the paradigmatic examples that the relevant scientific community accepts as successful or failed applications of the theory.
MR: And why is it important to test a formal reconstruction in this way?
AR: The answer I’d give has to do with the particular way in which I view the philosophy of science (or at least this part of the philosophy of science), as forming part of the science of science. In particular, I would say that structuralism (and other formal metatheories) are scientific theories, which have the peculiarity that their subject are scientific theories themselves.
In any other field of science, having a theory that one cannot rigorously test would be considered highly problematic. I do not see why us metascientists should feel exempt from testing the theories that we propose to account for the phenomena we wish to explain. Of course, theories (including theories about theories) are never tested in the abstract, but rather they are always testes through their applications. In this case, the applications of the metatheory are the particular reconstructions of theories. Thus, testing a reconstruction is an indirect way of testing the metatheory itself, and of making it more fully scientific.
MR: How did it occur to you to do this through a computer program?
AR: It came up because it is not enough to just propose a methodology to do the above. It must be possible to carry out this methodology. And although the one I proposed can be carried out with pen and paper, it would be extremely tedious to do it that way. A formalization of a real scientific law usually involves many nested quantifiers, presupposes a lot of mathematics, etc. The software I introduce allows one to see the internal reasoning processes it uses to check if a model satisfies a sentence. In the cases of the real theories I tried, checking if an application satisfies the laws requires (recursively) calculating thousands and thousands of valuations.
At a more personal level, this came up because in the begging of last year I was learning to program, and for that I was trying to design functions that did logic stuff (as examples to learn programming concepts). Once I had various functions designed, it occurred to me that I could apply them to do this.
MR: What is the target audience of Reconstructor?
AR: It is aimed at different audiences. On the one hand, at people who are working in doing formal reconstructions (and more particularly, but not exclusively, for the structuralists). The idea is that they be able to check if the results of that reconstructive work are adequate or not.
On the other hand, I believe it can also be of use to logicians, because the program automatizes calculations in model theory, which is one of the approaches from which the logical consequence relation is usually defined. Also, because the software works with a non-classical semantics, with three truth values, and because it contains quite a rich base language (which includes arithmetic and set theory), so one can even codify and automatize parts of the metalogic.
MR: Reconstructor utilizes a non-classical logic?
AR: Yes, in particular it uses a paracomplete semantic apparatus. The idea si that one can load incomplete models, that contain denotation failures. In the case of empirical science, these would represent applications of the theory where the values or extensions of some concepts are not known in advance, for example before making a prediction. To evaluate sentences in these incomplete models, the K3 matrices of Kleene are used. These matrices have a third truth value that can be used to represent situations of indetermination or lack of knowledge of the truth value.
The program also includes the possibility of filling out the incomplete denotations in a model through algorithms provided by the end-user. This is what the structuralists call “determination methods”, which are systematic procedures for finding out the extension of a concept (or, more precisely, this would be a new way of explicating the notion of a determination method). That is, once a reconstruction has been loaded into the software, it can be used to make automatized predictions.
MR: Do you think the program also has educational uses?
AR: Yes, of course, this is another objective that I always had in mind. Within the philosophy of science it can have educational uses because the former is a multidisciplinary field, where people with very different backgrounds converge. For example, it is just as usual to pursue an undergraduate career in the sciences and then specialize in philosophy as the reverse. This diversity of backgrounds and skills can cause some people to enter the field with less knowledge of formal logic, and they can have a harder time attempting to do a formal reconstruction. I think the program can help especially those people who are learning to do formal reconstructions.
In the case of logic students, the educational applications are even more obvious: the program can be used to teach formal semantics and model theory. For logic teaching more specifically I have also designed another software, called TAUT, which actually reuses part of the code that I had originally developed for Reconstructor. TAUT also does some things in proof theory and works with other logic systems. We are already using TAUT in the logic courses at the University of Buenos Aires. (Editor’s note: another interview regarding TAUT can be found here).
MR: What’s next for the development of Reconstructor?
AR: I’ve lately been working on adding some new features. One of the most interesting ones is the possibility of having automatic determination methods. This means that you give the software an incomplete model and a law (an axiom), and the program automatically infers the missing denotations by enforcing the law on the model (when this is possible). For that, what I did was to generalize the Kripkean fixed-point apparatus, in order to allow it to complete the extension and anti-extension of any language item (not just the truth predicate), and to computationally implement this generalization. I think that the result is something like the semantic equivalent of an automated theorem prover.
MR: Lastly, how can we get the software?
AR: It can be freely downloaded from my website. It works with every operating system. The version 2.0, that has the functionalities that I was just mentioning, will come out shortly.
MR: Thank you
AR: Thank you as well.