So there you have it. Hundreds of pages and more than 3000 diagrams later, we've told you (pretty much) everything we know about quantum theory and diagrammatic reasoning. So, where to now? Is it time for everyone to start covering blackboards and filling papers with diagrams? Of course!

But even better, what if someone else did all the diagrammatic proving for you while you sit back, relax, and have a beer? That's even better! The fact that the diagrams we use are essentially made up of a finite number of ingredients (namely, spiders) means they are particularly well suited to automated reasoning. In this subfield of artificial intelligence, one develops software that allows a computer to do a whole range of things often associated with human mathematicians: from simply checking mathematical proofs for correctness to automatically searching for new proofs or even new and interesting conjectures to then try and prove automatically.

In the past, automated reasoning has typically concerned traditional, formula-based mathematics built on formal logics and set-based algebraic structures, and there it has been very successful. It has provided us with tools called proof assistants, which allow us to automatically construct proofs of mind-bending results, such as Gödel's incompleteness theorems, and rigorously check proofs that are way too big for a human mathematician to get totally correct, like Kepler's conjecture, the four-colour theorem, and the Feit– Thompson theorem (famously massive proofs in geometry, graph theory, and group theory, respectively).

In addition to serving essentially as ‘robot teaching assistants’, which tirelessly check the work of human mathematicians, techniques from automated reasoning can actually tell us something new, via conjecture synthesis. Much as a human mathematician would discover features and behaviours of an unfamiliar mathematical creature by ‘poking at it’ (i.e. making educated guesses about how it will behave and trying to prove them), there exist automated techniques that do this at high speed. When it succeeds in a proof, the result is a freshly minted theorem that no human has ever seen or even thought to ask about.

The 1996 European Summer Meeting of the Association of Symbolic Logic was held held the University of the Basque Country, at Donostia (San Sebastián) Spain, on July 9-15, 1996. It was organised by the Institute for Logic, Cognition, Language and Information (ILCLI) and the Department of Logic and Philosophy of Sciences of the University of the Basque Country. It was supported by: the University of Pais Vasco/Euskal Herriko Unibertsitatea, the Ministerio de Educatiόn y Ciencia (DGCYT), Hezkuntza Saila (Eusko Jaurlaritza), Gipuzkoako Foru Aldundia, and Kuxta Fundazioa.

The main topics of the meeting were Model Theory, Proof Theory, Recursion and Complexity Theory, Models of Arithmetic, Logic for Artificial Intelligence, Formal Semantics of Natural Language and Philosophy of Contemporary Logic.

The Program Committee consisted of K. Ambos Spies (Heidelberg), J.L. Balcázar (Barcelona), J.E. Fenstad (Oslo), D. Israel (Stanford), H. Kamp (Stuttgart), R. Kaye (Birmingham), J.M. Larrazabal (San Sebastián), D. Lascar (Paris, chairman), A. Marcja (Firenze), G. Mints (Stanford), M. Otero (Madrid), S. Ronchi della Rocca (Torino), K. Segerberg (Uppsala) and L. Vega (Madrid).

The organizing Committee consisted of X. Arrazola (San Sebastián), A. Arrieta (San Sebastián), R. Beneyeto (Valencia), B. Carrascal (San Sebastián), K. Korta (San Sebastián), J.M. Larrazabal (San Sebastián, chairman), J.C. Martínez (Barcelona), J.M. Méndez (Salamanca), F. Migura (Victoria) and J. Pérez (Victoria).

Twenty-three one hour lectures were given at the meeting by: N. Asher (University of Texas), M.L. Bonet (Universidad Politécnica de Cataluña), J. Etchmendy (Stanford University), D. Evans (University of East Anglia), L. Gordeev (Tuebingen), M. Hyland (University of Cambridge), V. Kanovei (Moscow TEI), U. Kohlenbach (Frankfurt University), R. Kossak (City University of New York), M. Kummer (Universität Karlsruhe), S. Lempp (University of Wisconsin), B. Nebel (University of Ulm), A. Nesin (Tehran), H.J. Ohlbach (Imperial College, London), M. Pentus (Moscow State University), M. Pinkal (Universität des Saarlandes), G. Priest (University of Queensland), M. Reynolds (King's College, London), E. Sandewall (Linkoping University), J. Schmerl (University of Connecticut), S. Starchenko (Vanderbilt University), G. Takeuti (University of Illinois) and L. Torentliev (University of Amsterdam).

In this paper I attempt to convey an idea of Hao Wang's style as a philosopher and to identify some of his contributions to philosophy. Wang was a prolific writer, and the body of text that should be considered in such a task is rather large, even if one separates off his work in mathematical logic, much of which had a philosophical motivation and some of which, such as his work on predicativity, contributed to the philosophy of mathematics. In a short paper one has to be selective. I will concentrate on his book From Mathematics to Philosophy [1974], since he considered it his principal statement, at least in the philosophy of mathematics. It also has the advantage of reflecting his remarkable relationship with Kurt Gödel (which began with correspondence in 1967) while belonging to a project that was well under way when his extended conversations with Gödel took place. Although Gödel's infiuence is visible, and in some places he is documenting Gödel's views by arrangement with their author, the main purpose of the book is to expound Wang's philosophy. Although I will comment on the Wang-Gödel relation, a discussion of Wang's work as source for and interpretation of Gödel, work which included two books written after Gödel's death ([1987] and [199?]) will have to be deferred until another occasion.

Style, convictions, and method

Wang's writings pose difficulties for someone who wishes to sort out his philosophical views and contributions, because there is something in his style that makes them elusive. FMP, like other writings of Wang, devotes a lot of space to’ exposition of relevant logic and sometimes mathematics, and of the work and views of others. Sometimes the purpose of the latter is to set the views in question against some of his own (as with Carnap, 381-384); in other cases the view presented seems to be just an exhibit of a view on problems of the general sort considered (as with Aristotle on logic, 131-142). The presence of expository sections might just make Wang's own philosophizing a little harder to find, but it is not the most serious difficulty his reader faces. That comes from a typical way Wang adopts of discussing a philosophical issue: to raise questions and to mention a number of considerations and views but with a certain distance from all of them.