Navigation – Plan du site
Logic and Philosophy of Science in Nancy (I)

Proofs as Spatio-Temporal Processes

Petros Stefaneas et Ioannis M. Vandoulakis
p. 111-125

Résumés

Le concept de preuve peut être étudié selon différentes perspectives. Beaucoup de types de preuves ont été développées à travers l’histoire, comme les preuves apodictiques, dialectiques, formelles, constructives et non-constructives, les preuves par la visualisation, les preuves basées sur des hypothèses, les preuves générées par ordinateur, etc. Dans cet article nous développons le concept général des preuves-événements de Goguen et la méthodologie de la sémiotique algébrique, afin de définir le concept de style mathématique, qui caractérise les preuves produites par des cultures, écoles ou chercheurs différents. D’après nous, le style peut être défini comme un méta-code sémiotique qui dépend du mode sous-jacent de signification (semiosis), du code choisi et de l’espace sémiotique sous-jacent, et il détermine le mode individuel d’intégration (sélection, combinaison, mélange) dans une structure narrative (preuve). Pour conclure, nous examinons certains types historiques de styles de preuves mathématiques, afin de clarifier notre point de vue.

Haut de page

Texte intégral

1 Introduction

1The Greek concept of apodictic proof, as exemplified by geometrical demonstration in Euclid’s Elements, and refined during the 17th-18th centuries in the form of analytic proof, became the major characteristic of the European mainstream mathematical culture. Gödel’s investigations in meta-mathematics, after the 20th-century foundational crisis, shook down the established belief in the identification of truth with proof. During the subsequent years, mathematical logicians developed powerful methods for the formal representation of proofs in different formal languages. Nevertheless, many mathematicians were not willing to accept the new ideal of formalistic proof. Mac Lane, for instance, emphasized that

Real proof is not simply a formalized document, but a sequence of ideas and insights. [Mac Lane 1997, 152]

2The appearance of computer-generated proofs in 1976, by Kenneth Ira Appel (1932-) and Wolfgang Haken (1928-) for the solution of the famous four-color problem, and the Web-based proof that was initiated by Joseph A. Goguen’s Kumo proof assistant and Tatami project in the 1990s and Timothy Gowers’ Polymath and the Tricki Project in 2009, posed new challenges to the traditional concept of proof, as it concerns the role of new technologies in the process of proof and its understanding by a human [Stefaneas & Vandoulakis 2012].

3Thus, Joseph Goguen (1941-2006), proposed a new approach to proof, designed to cover apodictic, dialectical, constructive, non-constructive proof, as well as proof steps and computer proofs, essentially relying on concepts and methods from cognitive science, semiotics, ethnomethodology and modern philosophy of science.

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...). 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. [Goguen 2001]

4Accordingly, the concept of proof-event has the following components:

51. Social component. A proof-event is a social event, that takes place at a given place and time involving a public presentation; thus it is characteristic of particular persons forming groups of experts, who have particular skills as members of an appropriate mathematical community.

62. Communication medium. Certain communication media are used: written text (manuscripts, printed or electronic texts, letters, shorthand notes, etc.) in (ordinary or formal) language or any other semiotic code of communication (signs, formulae, etc.), including oral communication (speeches, interviews, etc.), visual (non-verbal) communication (diagrams, movies, Java applets, etc.), as well as communication through practices.

73. Provers and interpreters. Proof-events presuppose two agents: a prover, which can be a human or a machine, and an interpreter, who must be only human (person or group of experts). The prover and the interpreter may be separated by space and time, but they are in communication: the prover produces the item to be proved in the course of the proof-event process, and the interpreter perceives and reacts to it.

84. Interpretation process. This is the determination of the definition or meaning of the signs, which are fixed by the language or communication code used for the presentation of a proof or what is thought of to be a proof. The communication code contains symbols and rules for the combination (syntax), interpretation (semantics) and application (pragmatics) of those symbols that have been agreed upon to use or have to be decoded. Thus, interpretation is an active process, during which the interpreter may alter the initial proof by adding new concepts (definitions) and filling possible gaps in the proof. Interpreters, who share different communication codes, may fail or have difficulties in communication.

95. Understanding and validation. A proof is complete when the persons involved in a proof-event conclude that they have understood the proof and agree that a proof has actually been given, i.e., that the proof is a fact. Thus, a proof-event is a process, the conclusion of which means that the proof is validated and, further, is considered infallible by the appropriate group of the mathematical community. Only proofs that have been understood are considered valid and integrated into mathematical culture.

106. Historical component. Insofar as proof-events take place in time, they are themselves, as well as the communication codes they use to be transmitted, embedded in history; thus they also include the history of the texts and records, by which the transmission of proofs as well as the information about proofs are realized.

117. Styles. Proof-events generate proofs in different styles. Styles characterize different cultures, schools or scholars that may differ in their perception of rigor and other views of meta-theoretical character.

2 Hermeneutics

12The two-agent communication model highlights the social component of proving and leads to the idea of the community as ultimate collective interpreter of proof-events; the mathematical community ought to “understand” (interpret), and “confirm” the proof, so that a proof could be accepted as “valid”. The communication process takes place between a prover and an interpreter (or, at least, an intended interpreter) that both take part in a proof-event. The prover and the interpreter may belong to different mathematical worlds, formed by their different experiences, expertise, concepts, ideas, etc. Thus, they perceive and interpret a proof differently. However, it is assumed that there is some kind of common or shared interpersonal space, so that communication was made possible.

  • 1 In L.E.J. Brouwer’s (1881-1966) intuitionistic mathematics, these insights [Anschauung] are restric (...)

13The prover experiences an insight (intention) that something in mathematics is true.1 He formulates his experience in linguistic terms, i.e., in the form of a meaningful proposition, or, generally, in some semiotic code. In this way, the prover chooses a code in order to communicate his experience (his intention). The item transmitted may not be a complete proof. In general, it is a sequence of thoughts or arguments designed to convince a sound mind. However, it may also be just an outline of a proof, a flawed proof, a visual argument or even a conjecture, i.e., just the formulation of an intention that has to be proven or refuted. Consequently, the prover conveys an encoded (finite) mental construction to a potential interpreter across distance and time in the shared space, pretending that it is convincing enough to be perceived as a proof.

  • 2 Thus, there is an ethical aspect in provers activity, which is not shared by an interpreter. This a (...)

14Having conveyed the item, the prover is confident that he will succeed in persuading the potential interpreter that the item transmitted is actually a proof. This confidence of the prover may stem from his formed idea of consistency of the strategy adopted to handle the problem (intention), the logical arrangement of the particular steps (sub-proofs), the beauty and transparency of his mental construction and his personal firm belief that he is not betrayed by his own intuition.2 Provers generally expect interpreters to be persuaded easily to understand (decode) the item, as the prover understands it. However, this does not always take place in reality. The item produced by a prover may lead to different communication outcomes. Some interpreters may admit that this is probably a proof or others may deny it. As Goguen notes:

A proof event can have many different outcomes. For a mathematician engaged in proving, the most satisfactory outcome is that all participants agree that “a proof has been given”. Other possible outcomes are that most are more or less convinced, but want to see some further details; or they may agree that the result is probably true, but that there are significant gaps in the proof event; or they may agree the result is false; and of course, some participants may be lost or confused. [Goguen 2001]

  • 3 Hans Georg Gadamer (1900-2002) considers understanding as an active process, notably as reconstruct (...)

15Hence, the item transmitted by a prover is not necessarily perceived in the manner that the prover advocates. Based on what the interpreter perceives, on the grounds of his own understanding of the item input, he will form an idea of whether the item will be considered a proof or not. In any case, the prover’s item will mean something to the interpreter. It might or might not mean what was intended by the prover, i.e., that the item has the status of proof. In the case of successful communication, the interpreter can retrace all the steps of a proof conveyed by the prover, and is convinced that the item is actually a proof. Any item which is presented as a proof can be analyzed into parts (proof steps), which are evident and convincing. If a part of the item (a proof step) is not transparent, then this part needs further reduction to evident and convincing subparts. During the process of retracing a proof, the interpreter may alter the initial item by introducing new concepts or refining the existing ones, by filling possible gaps, or by making it shorter or more explicate. Thus, understanding a proof is an active process.3 To a certain extent, an interpreter may reconstruct the suggested item, so that he could understand it and became convinced that it is actually a proof. The prover will know that the interpreter has understood the transmitted item, only if he receives a message back that is congruent with what he had in mind.

16What is transmitted across the communication channel are neither all the concepts that the prover possesses in his own mathematical world, nor the meanings and intentions he had experienced, but only symbols. In other words, the item is represented in a semiotic code, which generally may consist of signs of the natural language (words), special signs of some mathematical language and other notation, such as diagrams, charts, icons, abbreviations, etc. These kinds of signs may have different meanings for the prover (the intended meaning) and the interpreter (perceived meaning), depending on the difference of their mathematical worlds. Understanding is achieved when the perceived meaning is congruent to the intended meaning of the prover.

17When a proof has been understood, that is when every proof step has been retraced and reduced to trivial evidence, then a certain community of mathematicians recognizes that the item transmitted was actually a proof. This declaration expresses the inter-subjective conviction of the community that the suggested item is true and infallible.

18The final validation of the prover’s item is not necessarily achieved by means of its formalization. In practice, mathematicians do not think in formal systems. In view of a proposed proof, their immediate response is not an attempt to formalize it. Instead, they try to find out and refine an ill-defined concept or fill a possible gap in deductive reasoning, or to make rigorous a flawed argument, or even try to find an alternative proof to increase evidence that the proposed item is actually a proof. On the contrary, in case they suspect that the item is wrong, they try to devise a counter-example. Formal systems are used as a means of meta-mathematical investigation. They aid in the rigorous operation with abstract concepts and facilitate communication, thus ensuring validity and objectivity of mathematical proofs. However, they are not used as a means to understand a proof. Formalization is secondary in comparison to the content: a formalization of an informal (contentual) proof is accepted as adequate only when it is considered that it captures the “(real) content” of proof.

19The process of validation is always finite in time. In all cases, the mathematical community within a finite (although, possibly very long) time interval will consider an item suggested by a prover and conclude either a positive or a negative assessment of it. In case of a negative evaluation, that is, when the item cannot be corrected so that to become a proof, this would mean that the initial intention of the prover was illusory or misleading, that is, the prover might have been betrayed by his intuition. There is a long history of mistaken intuitions and blind attempts of proof in mathematics. This usually is clarified in the light of subsequent in time mathematical results. In this sense, the mathematical community’s collective mind that acts as an interpreter of a proof-event is the absolute criterion of reliability of a prover’s suggested proof.

20Each proving has a history. What is posed to be proved (the intentions) emerge often out of history, during the unfolding of sequences of proof-events. Thus, the initial intention of a proof bears a historical meaning that can also determine the significance of a proof. Moreover, the semiotic code chosen by the prover to communicate his intention is also embedded in history. One code can be more suitable for the communication of an intention, while another can be proved less suitable. Thus, there are different ways to communicate intentions and different proofs can be devised for some reason by different mathematicians, belonging to different cultures and times. This is a sign that the intentions and the items that are proposed as proofs of these intentions have inter-subjective character.

3 On the organisation of mathematical discourse

21The structure of proofs in mathematics is a particular kind of narrative structure. This enables us to appeal to the means of semiotic discourse analysis to study proof-events. This structure is organized in a complex hierarchical order.

  • 4 We use here some examples suggested by Goguen [Goguen s.d.].

22At the first level, expressions, such as “definition”, “hypothesis”, “theorem”, “property”, “conclusion”, etc., are used to introduce objects. These expressions connote, using the means and conventions of natural language, the contents (intentions) of mathematical thinking that direct the prover’s mind toward certain objects or states of affairs. The objects thus introduced express the provers’ (tacit) epistemic values and their belief in the degree of existence of the considered objects. For instance,4 expressions of the form:

a. “Let n be an integer”,

b. “Assume that n is an integer”,

c. “Suppose n is an integer”,

d. “Let an integer n be given”,

are, from a formal point of view, indiscernible, i.e., they are just declarations about a variable n ranging over the domain N of integers. However, in natural language, the tenor of the words “let”, “assume” and “suppose” is different: they express different values of belief in the existence of the objects introduced, i.e., concerning the ontological status of the objects. The “let” form is stronger (expresses greater certainty) than the “assume” form, which in turn is stronger than the “suppose” form. The last form is the weakest one.

  • 5 Ludwig J.J. Wittgenstein (1889–1951) [Wittgenstein 1921, 4.26] argued that only elementary proposit (...)

23At second level, assertions (positive statements) and proofs are introduced in mathematical texts in a similar fashion. They are abstract representations of states of affairs and have a “truth status”, in contradistinction to the ontological status that objects possess.5 For instance, assertions of the form

e. “We will prove that...”

f. “We observe that...”

g. “It can be shown that...”

have not the same truth status. They introduce a state that is in the process of being established or foreseen that can be (hopefully, easily) established. Further, expressions of the form

h. “Obviously...”

i. “It is clear/evident that...”

j. “The reader can easily prove/verify that...”

are expressions with hidden or implicit truth status. An extreme case is assertions used in reasoning ad absurdum, in which it is assumed the existence of an object, but it is finally shown that it does not really exist. For instance,

k. “Let a be an integer, such that a2=2

l. “Therefore, there is no number a possessing the given property”.

24Although the phrases (a) and (k) look similar, the truth status of (k) is very low, because the ontological status of object a is undermined.

25Mathematical discourse includes also expressions that do not refer to objects, but to linguistic entities used within this discourse. For instance,

m. “using formula...”

n. “applying the Pythagorean theorem...”

26Such expressions have mediated truth status, since they refer to assertions that in turn refer to states of affair (i.e., they belong to the meta-linguistic level).

27The combination of propositions into a proof step is made by using basic connectives, such as “then” (or its variations, such as “thus”, “so”, “therefore”, “since”, “follows”, etc.) that have the standard meaning of logical implication. Further, proof steps are combined together to build up a proof. Proof usually requires more than one proof step; it may require a “tree” of proof steps (which nevertheless is represented as a linear sequence of steps, i.e., as narrative). This is attained in the following ways, which ensure the sequential organization of discourse:

  1. The conclusions of preceding steps are repeated in the next step; however, their (truth) status has changed: it has been transformed from target point (conclusion) into starting point (hypothesis).

  2. Some of the statements that have been used in preceding steps can be disregarded or play no role in subsequent steps.

28In this way, formal processes of mathematical proofs, phrased by a prover in ordinary language, are deeply affected by the communicational conventions of ordinary discourse, which presume concrete objects as referents of the linguistic units and nuanced assignments of values to objects that are related to their ontological or truth status.

4 Semiotic morphisms

29The narrative structure outlined above serves to support the existence/construction of a reality for mathematical objects or ideal entities, in virtue of the communicational conventions of ordinary language used.

30The basic connective “then” (or its variations, such as “thus”, “so”, “therefore”, “since”, “follows”, etc., or even “and”, in some contexts) with the standard meaning of logical implication serves as conceptual metaphor. By conceptual metaphor is understood a mapping from a source conceptual space (objects and relations among them) or image schema (families of metaphors sharing a common name) to a target conceptual space [Fauconnier & Turner 2002]. The connective “then” maps the original temporal meaning of the connective “then” (used in ordinary language) into the more abstract meaning of implication in the domain of logic [Goguen 2003], [Lakoff & Núñez 2000].

31The use of conceptual metaphors supports the idea of reality of mathematical objects and facilitates the communication and understanding of an idea of a conceptual space in terms of another one in a different, more perceptible, conceptual space. For instance, the representation of real numbers as points on a line is a common mathematical metaphor that maps the conceptual space (image schema) of points on a line to a conceptual space for the real numbers. However, in mathematics, where the structure of a proof is essential, the more general concepts of semiotic space and semiotic morphism are more adequate.

32A semiotic space is an algebraic many-sorted structure—organized in layers—with an arbitrary number of domains; the sorts play the role of names that signify objects for the different domains. Signs of a certain sort are represented by terms of that sort. They are not, necessarily atomic (“indivisible”) entities, such as the letters of an alphabet; they may be whole words, sentences or paragraphs in natural language, as well as complex entities of an arbitrary nature (figures, graphs, etc.) that are treated as single objects. In a mathematical text, as sorts may serve headlines, paragraphs, name or propositional forms, formulas, figures, graphs, fragments of computer programs, Web pages, blogs or applets (in the case of Web-based mathematical proving).

33There is a partial ordering on sorts by level (that has a “top” element) expressing the whole-part hierarchy of complex signs. There is also a partial priority ordering expressing the relative importance of the constituents at each level. These orderings are specified by social qualities.

34Moreover, for each level, there is a set of constructors (functions) used to build complex signs out of signs from the same or lower levels. Finally, there may also be relations and predicates defined on signs (e.g., a “location” function or a “highlight” predicate) and a set of axioms, i.e., logical formulas built up from constructors, functions and predicates, that govern the behavior of the possible signs.

35Thus, a semiotic space serves as the “context” of the signs, which, in this way, may include conventional meanings of the signs and symbols, information on the importance and use of different signs, etc., which determine their meaning and their possible communicational functions. Signs and semiotic space constitute the code in which mathematical information is encoded by a prover.

36Mappings between semiotic spaces, called semiotic morphisms (or “translations”), are uniform representations for signs in a source space by signs in a target space. Besides structure, semiotic morphisms also partially preserve sorts and priorities of the source space. This kind of representation or “translation” allows meaning related in the target semiotic space to be related to signs in the source semiotic space. The more structure is preserved under a “translation”, the more the target semiotic space can be viewed as a faithful translation of the source semiotic space.

37It may happen that one could know the target semiotic space and seek to infer properties of signs in the source semiotic space from their images in the target space. This is the case when an interpreter tries to understand a mathematical text, an equation or anything else. On the contrary, a prover, who uses the source semiotic space, may seek for a target semiotic space to provide a more eligible explanation or interpretation or visualization of objects from the source semiotic space (a concept, a theorem, a proof, etc.). An example of this case is the geometrical (visual) or kinematic meaning of the first derivative of a function.

  • 6 A precise mathematical definition is given in [Goguen & Malcolm 1996].
  • 7 A computation approach to blending in mathematics was lately developed in [Guhe, Pease, et al. 2011 (...)

38A blend can be built out of two or more semiotic morphisms that have a common source semiotic space (called the generic space) with targets (called the input spaces), by providing two or more semiotic morphisms from the input spaces to a blend (semiotic) space, subject to certain optimality conditions (blending principles) that determine the “good” blends [Goguen & Harrell 2004; 2005].6 In case structural blending can be defined algorithmically, then a structural blending algorithm can be programmed to compute the “good” blends.7

5 Styles of proofs

39Proof-events generate proofs presented in different styles. Styles characterize different cultures, schools or scholars that may differ in their perception of rigor and other views of meta-theoretical character. It is viewed often as the personal “seal” of the author, or of a copyist who mimics the style of the original author.

40The analysis of literary style goes back to classical rhetoric, but modern analysis of style has its roots in the school of Russian Formalism and the Prague School in the early twentieth century. Roman Jakobson, an active member of these schools, is often credited with the first coherent formulation of style, in his famous Closing Statement: Linguistics and Poetics at a conference in 1958 [Jakobson 1960], where he exposed his theory of communicative functions of language.

41Goguen & Harell [Goguen & Harrell 2004; 2005] have proposed a new approach to the concept of style, originating from algebraic semiotics [Goguen 1999], which is suitable to describe styles in mathematics, because it takes into consideration structural and syntactic characteristics, as well as metaphors. They define style in terms of the blending principles used for the construction of a blend (semiotic) space.

42In the case of mathematics, insights (intentions) allow formulation in different semiotic codes and, thereby a multiplicity of choices of semiotic spaces and metaphors are possible to be constructed. Hence, the particular mode of signification [semiosis], the domains, sorts, constructors, axioms, etc., i.e., the underlying semiotic space (algebraic, geometric, probabilistic, λ-calculus, etc.), which are chosen in order to formulate mathematical meanings and convey information, have already a stylistic dimension. Further, style depends on the metaphors used in the narrative (semiotic) space as well as the communicational functions of the codes and metaphors chosen. Finally, style depends on the choice of the blending principles used to create blend spaces.

43Consequently, style, in our view, can be defined as a meta-code that determines:

  • a. The selection of a particular code, among a multitude of possible alternatives;

  • b. The combination of blending principles to produce an integral narrative mathematical structure (proof-event).

  • 8 Nicomachus, Introductionis Arithmeticae, [Hoche 1866, I.vii, section 1, line 1].
  • 9 Theon Expositio rerum mathematicarum ad legendum Platonem utilium [Hiller 1878, I-iii, 1-5].
  • 10 Euclid Elements [Heiberg 1883-1916, VII, Def. 2].

44The choice of a segment by Euclid to designate a number (instead of the alternative Pythagorean designation of numbers by pebbles) is decisive for the Euclidean style of arithmetic. This leads to the construction of a geometric semiotic space. Thus, operations over numbers are defined using the metaphor of concatenation of segments; naturally, division of numbers is not defined, since division of segment by a segment cannot be defined in a geometric semiotic space. Moreover, the successor operation is not crucial in this geometric semiotic space; instead, it is essential in the semiotic space of the Pythagorean arithmetic, in which it serves as generating procedure for all kinds of numbers introduced. Thus, the semiotic spaces associated with these versions of ancient arithmetic are distinctively different and produce mathematical texts in clearly different styles. The metaphors used are also different. Numbers are characterized by the metaphor of “flaw of quantity made up of units”8 or “progression of multitude beginning from a unit”9 in the Neo-Pythagorean tradition; in the Euclidean tradition, numbers are introduced by the metaphor of “multitude composed of units”.10 The underlying semiotic space can be described by the metaphor of an evolving universe (expanding in the direction of increase), in the first case, whereas, in the second case, it has the structure of (algebraic) module [Vandoulakis 1998; 2009; 2010].

45The style of the Bourbaki (or the authors who mimic their style—the “bourbakists”) is characterized by a careful selection of the code, i.e., symbolism and vocabulary, which has determined even current usage. The narrative space is strictly structured and principally lacks expressions of the form (e)-(g), that have hidden or implicit truth status, or pictures that could motivate geometrical intuitive metaphors. Assertions follow a descending order, from the abstract and general to the special ones. Proof expositions are complaint to the outmost rigorous standards.

46However, communicational matters play a dominant role in the style of other mathematicians of the 20th century, for instance, in the expositions of Michael Spivak (1940-) and Aleksandr Gennadievich Kurosh (Aleksandr Gennadievich Kurosh, 1908-1971). Both authors are characterized by their tendency to embrace prose (thus avoiding dry and terse writing) and display an “artistic” practice of mathematical narratives. They also pay attention to history and the human element. Kurosh’s concise historical introductions to his books Higher Algebra [Kurosh 1946] and Theory of Groups [Kurosh 1940] sets forward the background ideas to support understanding of the mathematical ideas exposed in the books. Spivak’s sporadic historical notes are dispersed throughout his books Calculus [Spivak 1967] and A Comprehensive Introduction to Differential Geometry [Spivak 1969]. The second volume of the later book begins with the classical theory of curves and surfaces, followed by a discussion of Gauss’s Disquisitiones and Spivak’s commentary. In a similar fashion, the part on classical Riemannian geometry begins with Riemann’s seminal paper “Über die Hypothesen, welche der Geometrie zur Grunde liegen” followed by Spivak’s commentary “What Riemann said”. In this way, history/time environment is incorporated in the channel of transmission of mathematical information.

47These kinds of mathematical style require the choice of various, more complex parameters of communication models as driving blending principles, such as the conative function (the forms of appellation to the addressee that aim to stimulate certain response), the aesthetic (poetic) function (the art of discourse), the temporal dimension in the information conveyance, or others.

6 Conclusion

48Proof-events are presented in different styles. The definition of style as a meta-code that determines the individual mode of integration of concepts into a narrative structure, enrich the study of mathematical proof. Hence, our approach may enable us to study the concept of mathematical activity from a novel standpoint since the prover-interpreter interaction and the interpretation process can be studied using tools from semiotics and theories of communication. Critical processes of structural changes in the systems of mathematical knowledge can be elaborated further when a change of mathematical practice takes place, that calls for validation by an appropriate interpreter.

Haut de page

Bibliographie

azhanov, Valentin A. [2011], Mathematical proof as a form of appeal to a scientific community, Russian Studies in Philosophy, 50(4), 52–72, doi: 10.2753/RSP1061-1967500404.

Fauconnier, Gilles & Turner, Mark [2002], The Way We Think, New York: Basic Books.

Gadamer, Hans-Georg [1979], The problem of historical consciousness, in: Interpretative Social Science: A reader, edited by P. Rabinow & W. M. Sullivan, Berkeley: University of California Press, 103–160.

Goguen, Joseph A. [1999], An introduction to algebraic semiotics, with application to user interface design, in: Computation for Metaphors, Analogy, and Agents, edited by C. L. Nehaniv, Berlin; Heidelberg: Springer, Lecture Notes in Computer Science, vol. 1562, 242–291, doi: 10.1007/3-540-48834-0_15.

—— [2001], What is a proof?, URL https://cseweb.ucsd.edu/~goguen/papers/proof.html.

—— [2003], Semiotic morphisms, representations, and blending for interface design, in: Proceedings, AMAST Workshop on Algebraic Methods in Language Processing, AMAST Press, 1–15, Conference held in Verona, Italy, 25–27 August.

—— [s. d.], Reality and human values in mathematics, URL http://cseweb.ucsd.edu/users/goguen/pps/real.ps.

Goguen, Joseph A. & Harrell, Fox D. [2004], Style as a choice of blending principles, in: Style and Meaning in Language, Art, Music, and Design, edited by S. Argamon, S. Dubnov, & J. Jupp, Menlo Park: AAAI Press, 49–56.

—— [2005], Information visualisation and semiotic morphisms, in: Multidisciplinary Approaches to Visual Representations and Interpretations, edited by G. Malcolm, Elsevier, Studies in Multidisciplinarity, vol. 2, 83–97, doi: 10.1016/S1571-0831(04)80035-2.

Goguen, Joseph A. & Malcolm, Grant [1996], Algebraic Semantics of Imperative Programs, Cambridge, MA: MIT Press.

Guhe, Markus et al. [2011], A computational account of conceptual blending in basic mathematics, Cognitive Systems Research, 12(3–4), 249–265, doi: 10.1016/j.cogsys.2011.01.004, special Issue on Complex Cognition.

Heelan, Patrick A. [1998], The scope of hermeneutics in natural science, Studies in History and Philosophy of Science Part A, 29(2), 273–298, doi: 10.1016/S0039-3681(98)00002-8.

Heiberg, Johan Ludvig (ed.) [1883-1916], Euclides opera omnia, Leipzig: Teubner.

Hiller, Edward (ed.) [1878], Theonis Smyrnaei Philosophi Platonici Expositio rerum mathematicarum ad legendum Platonem utilium, Leipzig: Teubner.

Hoche, Richard (ed.) [1866], Nicomachi Geraseni Pythagorei Introductionis Arithmeticae Libri II, Leipzig: Teubner.

Jakobson, Roman [1960], Closing statement: Linguistics and poetics, in: Style in Language, edited by T. Sebeok, Cambridge, MA: MIT Press, 350–377.

Kurosh, Aleksander [1940], Теориыа Грыпп, Moscow: Наука, English translation by K.A. Hirsch: Theory of Groups. Vols. 1–2, New York: Chelsea Publishing Company, 1955.

—— [1946], Курс высшей алгебры, Moscow: Наука, English translation by G. Yankovsky, Moscow: Mir Publishers, 1972.

Lakoff, George & Núñez, Rafael E. [2000], Where Mathematics Comes from: How the Embodied Mind Brings Mathematics into Being, New York: Basic Books.

Mac Lane, Saunders [1997], Despite physicists, proof is essential in mathematics, Synthese, 111(2), 147–154, doi: 10.1023/A:1004918402670.

Spivak, Michael [1967], Calculus, New York: W. A. Benjamin.

—— [1969], A Comprehensive Introduction to Differential Geometry, Waltham: Brandeis University.

Stefaneas, Petros & Vandoulakis, Ioannis M. [2012], The Web as a tool for proving, Metaphilosophy, 43(4), 480–498, doi:10.1111/j.1467-9973.2012.01758.x, reprinted in Halpin, H. and Monnin, A. (eds.) Philosophical Engineering: Toward a Philosophy of the Web, Chichester: Wiley-Blackwell 2014, 149–167.

Vandoulakis, Ioannis M. [1998], Was Euclid’s approach to arithmetic axiomatic?, Oriens–Occidens, 2, 141–181.

—— [2009], Styles of Greek arithmetic reasoning, Study of the History of Mathematics RIMS – Kôkyûroku, 1625, 12–22.

—— [2010], A genetic interpretation of neo-Pythagorean arithmetic, Oriens–Occidens, 7, 113–154.

Wittgenstein, Ludwig [1921], Tractatus Logico-Philosophicus, London: Routledge, Trans. by D. Pears and B. McGuinness.

Haut de page

Notes

1 In L.E.J. Brouwer’s (1881-1966) intuitionistic mathematics, these insights [Anschauung] are restricted to constructive truths, that is, he excludes the possibility for a mathematical finite mind to comprehend completed infinite objects; such objects are non-experienceable.

2 Thus, there is an ethical aspect in provers activity, which is not shared by an interpreter. This aspect is highlighted by Bazhanov [Bazhanov 2011].

3 Hans Georg Gadamer (1900-2002) considers understanding as an active process, notably as reconstruction of meaning [Gadamer 1979].
Further, M.M. Bakhtin (
Михаил Михайлович Бахтин, 1895-1975) considers that meaning comes into being, not by its utterance, but as a result of its being understood by somebody else. Thus, according to Bakhtin, interpretation is not only a way of understanding a meaning, but also mode of existence of meaning. See also [Heelan 1998].

4 We use here some examples suggested by Goguen [Goguen s.d.].

5 Ludwig J.J. Wittgenstein (1889–1951) [Wittgenstein 1921, 4.26] argued that only elementary propositions are designators of states of affairs and represent a picture of a state of affairs.

6 A precise mathematical definition is given in [Goguen & Malcolm 1996].

7 A computation approach to blending in mathematics was lately developed in [Guhe, Pease, et al. 2011].

8 Nicomachus, Introductionis Arithmeticae, [Hoche 1866, I.vii, section 1, line 1].

9 Theon Expositio rerum mathematicarum ad legendum Platonem utilium [Hiller 1878, I-iii, 1-5].

10 Euclid Elements [Heiberg 1883-1916, VII, Def. 2].

Haut de page

Pour citer cet article

Référence électronique

Petros Stefaneas et Ioannis M. Vandoulakis, « Proofs as Spatio-Temporal Processes », Philosophia Scientiæ [En ligne], 18-3 | 2014, mis en ligne le 19 janvier 2015, consulté le 17 janvier 2018. URL : http://journals.openedition.org/philosophiascientiae/1010 ; DOI : 10.4000/philosophiascientiae.1010

Haut de page

Auteurs

Petros Stefaneas

National Technical University of Athens (Greece)

Ioannis M. Vandoulakis

The Hellenic Open University, School of Humanities (Greece)

Articles du même auteur

Haut de page

Droits d’auteur

Tous droits réservés

Haut de page