What is a Proof?
http://www.cse.ucsd.edu/users/goguen/papers/proof.html
Mathematicians talk of "proofs" as real things. But the only things that can actually happen in the real world are proof events, or provings, which are actual experiences, each occurring at a particular time and place, and involving particular people, who have particular skills as members of an appropriate mathematical community.
A proof event minimally involves a person having the relevant background and interest, and some mediating physical objects, such as spoken words, gestures, hand written formulae, 3D models, printed words, diagrams, or formulae (we exclude private, purely mental proof events, for reasons discussed below. None of these mediating signs can be a "proof" in itself, because it must be interpreted in order to come alive as a proof event; we will call them proof objects. Proof interpretation often requires constructing intermediate proof objects and/or clarifying or correcting existing proof objects. The minimal case of a single prover is perhaps the most common, but it is difficult to study, and moreover, groups of two or more provers discussing proofs are surprisingly common (surprising at least to those who are not familiar with the rich social life of mathematicians -- for example, there is research showing that mathematicians travel more than most other academics.)
References
The references below include not only further details on the Kumo system, but also some prior work by the author on the sociology of mathematics and information technology. A more formal version of the above material would of course include citations to relevant work in ethnomethdology and the sociology of mathematics, especially work of Harvey Sacks, Eric Livingston, and Donald MacKenzie.
The first reference below was written three years after (the first draft of) the present essay, and goes considerably deeper into certain issues that are only hinted at here, including the structure of natural proofs, and the value system of professional mathematicians.
Slides for The Reality of Mathematical Objects, lecture by Joseph Goguen for the UCSD Science Studies Colloquium, 20 November 2000; summarizes recent work applying discourse analysis, cognitive linguistics, ethnomethodology and semiotics to mathematical discourse and its natural ethics. There is also a pure postscript version. Warning: You may have to change the orientation of the pages from landscape to seascape; also, this is just a sketch of an unwritten paper, with many details missing.
Notes on Narrative. This is a brief overview of some techniques for the analysis of stories, including summaries of the structural theory of narrative, and techniques for the extraction of value systems from stories.
An evolving collection of proof displays generated by the latest Kumo proof assistant and website generator (version 4). This is part of the Tatami project, one goal of which is to make machine proofs much more readable than usual; the project has some emphasis on behavioral proofs for distributed concurrent systems.
Web-based Support for Cooperative Software Engineering, by Joseph Goguen and Kai Lin, in Annals of Software Engineering, volume 12, 2001, a special issue on multimedia software engineering edited by Jeffrey Tsai. An uncompressed postscript version is also available. This is an overview of the Tatami project and version 4 of the Kumo proof assistant and website generator, focusing on its design decisions, its use of multimedia web capabilities, and its integration of formal and informal methods for software development in a distributed cooperative environment. The paper is a revised and expanded version of the paper Web-based Multimedia Support for Distributed Cooperative Software Engineering, by Joseph Goguen and Kai Lin, which appeared in Proceedings, International Symposium on Multimedia Software Engineering, edited by Jeffrey Tsai and Po-Jen Chuang, IEEE Press, pages 25-32; this meeting was held in Taipai, Taiwan, December 2000.
Towards a Social, Ethical Theory of Information, in Social Science Research, Technical Systems and Cooperative Work, edited by Geoffrey Bowker, Les Gasser, Leigh Star and William Turner (Erlbaum, 1997) pages 27-56. A pdf version is also available. Presents a theory of information based on social interaction, and shows how values arise naturally in such a theory.
Brief text of keynote address Towards a Design Theory for Virtual Worlds: Algebraic Semiotics, with information visualization as a case study, by Joseph Goguen, given at the Virtual Worlds and Simulation Conference, Phoenix AZ, 10 January 2001. A sketch of algebraic semiotics and its applications, especially to scientific visualization and user interface design; the slides for the talk are also available. Warnings: Some figures shown in the lecture are not included; also, you may have to change the orientation of the slides from landscape to seascape. This talk is an update of the "distinguished" lecture Algebraic Semiotics and User Interface Design, given at the Institute for Software Research, University of Irvine, 20 October 2000, with some additional material on virtual worlds.
Are Agents an Answer or a Question? by Joseph Goguen. Position paper on agent technology, in Proceedings, JSAI-Synsophy International Workshop on Social Intelligence Design, 21-22 May 2001, Matsue, Japan. A pure postscript version is also available.
These notes were in part inspired by remarks of Eric Livingston, whom I wish to thank, though he is not to blame for any lapses from pure ethnomethodology that I may have committed. The remarks on narrative draw on detailed studies by the sociolinguists William Labov and Charlotte Linde.
To the Tatami project homepage.
To the CSE 271 homepage: User Interface Design: Social and Technical Issues.
To my homepage..............OR.............
Defactualization of Analysis - Nodwell
2007-07-30 03:35:35
·
answer #8
·
answered by Anonymous
·
0⤊
0⤋