In this paper, we demonstrate how argumentation theory can be used to explore certain aspects of the development of discovery proof-events in time. The concept of proof-event was introduced by Joseph Goguen, [10], who understood mathematical proof, not as a purely syntactic object, but as a social event, that takes place in specific place and time and involving agents or communities of agents. Proof-events are sufficiently general concepts that can be used to study besides the “traditional” formal proofs, other proving activities, such as incomplete proofs, purported proofs or attempts to verify a conjecture. Since argumentation is inseparable from the process of searching for a mathematical proof, we suggest a modified model of the proof-events calculus, initially suggested by Vandoulakis and Stefaneas [32], based on the versions of argumentation theories advanced by Pollock [26], Toulmin [28] and Kakas and Loizos [14]. We claim that the exchange of arguments and counterarguments set forward to clarify eventual gaps or implicit assumptions occurring in the course of a proof-event can be formalized by appealing to argumentation theories. Additionally, we highlight the connection between proving, human reasoning, cognitive processes and creativity.
The concept of mathematical proof has undergone significant changes in the
20th century. Proof, particularly formalized proof, was initially identified in
philosophy of mathematics with truth. However, many mathematicians dealing with real
proofs did not accept the paradigm of formalized proof. Goguen [
Our approach combines proof-events with logic-based argumentation to study in a more adequate way the categories of purported, faulty or incomplete proofs, setting forward the concept of dialogue between agents with the use of arguments and counterarguments. Hence, we extend the calculus of proof-events through argumentation theory by depicting the relevant stages of a discovery proof-event (incomplete or even false proofs, ideas, valid or invalid inference steps, comments, etc.) in a form of a dialogue of agents that use arguments and counterarguments or counterexamples in their attempt to clarify the validity of a purported proof.
Many researchers claim that the role of argumentation is central in
mathematics. Mathematicians do much more, than simply prove theorems. Most of their
proving activity might be understood as kinds of argumentation [
A methodological tool that has been widely used to examine argumentation
is Toulmin’s model [28], in which argument is constituted by “claim”, “data”, and
“warrant” that are considered the substantial elements of applied arguments. The
procedure by which mathematicians evaluate reasoning resembles to argumentation, as
various researchers, such as Alcolea [
To combine the proof-event calculus with argumentation theory, we use the
basic structure of Toulmin’s model for the representation of an argument and
Pollock’s logic-based argumentation theory. We rely on Pollock’s view of defeasible
reasoning and we associate the procedure of human reasoning with proving.
Defeasible reasoning has a non-monotonic character. Pollock presented in his work the
concept of an argument in the form <Φ,α>, where Φ is a set of data and α is a claim [
In this paper, we proceed from a comparison of proof-events and argumentation. Then, we suggest a formalization of proof-events involving argumentation theory. We model the argument moves and the calculus of the temporal predicates. The aforementioned calculus is analyzed through the levels of argumentation. In the last section, Fermat’s Last Theorem as a proof-event is investigated as a case study illustrating the concepts introduced.
Comparison of the basic elements of proof-events and argumentation theory shows similarities in the structure, the sequence of events, the agents, the layers of communication, and the levels of argumentation.
Arguments and proof-events have three common fundamental components: a set of premises for a task or problem, a method of reasoning and a conclusion. Moreover, each proof-event has temporal extension and, thereby history: it has a starting point and a termination point and what is posed to be proved, emerges often out of the history of provings (sequences of proof-events or sequences of arguments and counterarguments) [31]. A sequence of a proof-event is complete when the community involved in it concludes that they have understood the proof and agree that a proof has actually been given or that a proof is invalid, based on a suggested counterargument (or counterexample).
Proof-events presuppose the existence of at least two agents: a prover and an
interpreter [31]. Similarly, argumentation involves agents or group of agents, enacting
the roles of supporter and opponent of an argument [
Argumentation models generally contain the following main elements: an underlying logical language with the definition of the concepts of argument, conflict between arguments and counterarguments, and status of argument. We will outline formalizations of proof-events based on argumentation theory, using a list of structures, which represent arguments and counterarguments. Our approach suggests a multiagent system, enacting the roles of provers and interpreters. An argument has premises, sentences, and conclusion. In the definition of an argument given in this section, the knowledge grounds and claims are formulae in classical logic and the method of inference by which a claim follows from a set of formulae is deductive inference and is denoted by ⊢. A proof-event е can be represented as a communicated argument 〈 〉 [26] designated by the pair 〈 〉: , where Φ is the Data of the argument, c is the Claim that refers to a fixed problem (proposition), specified by certain conditions (predicates) and w are the inference rules (Warrant) which allow Φ to be connected with c, so that: • • ⊢ • ⊢ c.
Counterarguments are represented by the corresponding pair , where Ψ is the data that the claim β (that refers to the same fixed problem (proposition), specified by the same conditions (predicates)) of the counterargument is based.
Argumentation may require chains (or trees) of reasoning, where claims are
used in the assumptions for obtaining further claims [
The aforementioned elements are frequently used to define a consequence relation between the arguments and/or the counter-arguments.
In the course of a proving procedure, we pass through various inference
stages, such as attempts, impasses, confirmed or unconfirmed steps, false suggestions
or implicit assumptions, intuitive ideas, intentions, etc. Arguments can then be
specified as chains of reasoning leading to a conclusion with consideration of possible
counterarguments at each step. With the explicit construction of the chain of
reasoning (a chain x0, x1,.. , xn where the argument xi attacks the argument xi−1 for i > 0),
distinct concepts of defeat can be conceptualized. When an agent has gained control
of an argument, he must select which argument-move to apply. Gordon [
Given a claim c and and an argument communicated during the proof-event
e, possible argument moves, which provide support for c [
Argument moves, which oppose c [26] include: Rebutting: an argument for a claim which disagrees with c; Undercutting: an argument for a claim which disagrees with a premise of c. 2.1.1. Argument moves that support the claim: when Φ=Φ΄, c=c΄ (although it might be w≠w ), where the proof-event e1 is equivalent with the proof-event e2, whenever it has the same data and the same conclusion (although different warrants). Thus, equivalent proof-events can have different ways of proving. For instance, the Pythagorean Theorem has been proved in numerous ways, such as by Euclid’s geometrical proving or by James Abram Garfield algebraic proving. , (5) where 〈 〉, is a proof-event and S is a set of sentences which elaborate or embellish upon e, iff ⊢ .
These moves are used for backing our claim and supporting our proving, so that 2.1.2. Counterargument moves that attack the claim: where a counterargument communicated during the proof-event e*<Ψ,β> attacks (rebuts) the conclusion of an argument communicated during the proof-event e<Φ,c>, iff ⊢β ↔ ¬c, where a counterargument communicated during the proof-event e*〈 〉 undercuts (attacks) some of the premises (defeasible inference) of the argument communicated during the proof-event 〈 〉, iff ⊢ ↔ { }
Given an argument communicated during the proof-event e<Φ,c>, a counterargument communicated during the proof-event e* 〈 〉 attacks the argument communicated during the proof-event e, at time t, iff e* rebuts e or e* undercuts e. Therefore:
Even though proof-events can be regarded as taking place instantaneously, the
Event Calculus is actually neutral with respect to whether events have duration or are
instantaneous [
We apply the abovementioned operators combined with the basic temporal predicates from [32]: Happens(e,t),Initiates(e,f,t), Terminates(e,f,t), ActiveAt(f,t), Clipped(t1,f,t2.) (11) which means that if a proof-event e occurs at time t, then there are no counterarguments that attack the validity of the outcome of the proof-event and there is adequate support for our claim at the specific time t1.
( which means that a fluent terminates when there is a counterargument attacking our sequence and there is no proof-event e2 that Happens in time t2, with t1<t2, to defend our claim. The termination of a sequence of proof-events may be caused by the proof of the falsity of the problem (there are counter-arguments that attack the conclusion of the proof-event), or the undecidability of the problem (there is a lack of adequate warrants to prove the desideratum). → which means that a fluent is active, if there is an argument to support our claim for every counterargument attacking our claim,. This means that for every counterargument e*<Ψi,βi>, i= 1,…,n, nϵ , there is a proof-event en+1(Φn+1, cn+1), which Happens(en+1,tn+1) and defeats the attack of the counterargument en*<Ψn,βn>, for tn+1>tn.
From the above-mentioned, we can conclude that: which means that a fluent remains active at time t2, if a proof-event e has taken place at time t1, with t1<t2 and has not been terminated at a time between t1 and t2.
[ ] which means that a fluent could consider valid at time tn, if it is active and there is no counter-arguments to terminate it at time ti for every i=1,…,n, nϵ . → → (14) (15) (16)
In order to define the warranted premises that are justified by a set of arguments
in the sequence, we need a mechanism, which by recursion could examine the
representation of the arguments. Pollock introduces defeasible reasoning where arguments
are chains of reasoning that may lead to a conclusion, whereas additional information
may destroy the chain of reasoning. Kakkas and Moraitis [
We can apply the same levels in mathematical proving, in order to understand the history of proof-events, starting from the statement of a problem until its validation or rejection, including attempts or failures [32]. The data and the claim of the initial proof-events constitute the object-level arguments. Proof-events constitute the first-level priority arguments, in which we have preferences and justifications in the object-level arguments. The proof-events that have fulfilled their purpose terminate, while the rest of them continues to the higher-order priority arguments. As proof-events continue from lower levels to higher, they constitute fluents. In the example below, we describe the possible steps and conflicts for the justification of a proof-event e through the levels of argumentation.
[ →
] → for i=1,….,m, mϵ , ti≤tm<t.
In the object level arguments, we have our claim and the initial representations of arguments. The proof-events that are not attacked constitute the fluent fo and continue to the first level priority arguments.
First-level priority arguments for every iϵ that we have: → → [ → [ ] t, ] (17) (18) (19) (20) and continues to the second-level priority arguments.
The same pattern continues for n-level priority arguments and for n fluents fn, that deal with potential conflicts between priority arguments of the previous level until all conflicts are resolved or our claim proved invalid. In the final level we have:
If the proof-events fail to resolve all the conflicts, our claim cannot be proved and it clips:
If the proof –events manage to deal with all the attacks and:
[ ( ) then our claim is proved valid. ,
We use the famous Fermat’s Last Theorem to illustrate our approach. Fermat's Last Theorem was formulated in 1637 by Pierre de Fermat, who stated that there are no three distinct positive integers a, b, and c, other than zero, that can satisfy the equation an+bn=cn , whenever n is an integer greater than two (n> 2). The statement of the problem marks the starting-point of a proof-event. Even though Fermat claimed to have proved this theorem, it actually took 358 years and numerous attempts undertaken by many famous mathematicians and amateurs to prove it until its final proof by Andrew Wiles in 1995. Thus, Fermat’s alleged proof cannot be included in the initial proof-event, since it was never communicated. Fermat communicates the Theorem only for the cases n=3 and n=4 in his letters and gives a solution for the latter case. The statement of the problem marks the beginning of a sequence of proof-events that evolved in time for 358 years. This sequence of proof-events was evolving in time, since many famous mathematicians and amateurs (agents) were involved in various distinct proof-events that took place in different places and times in their attempt to solve the problem posed.
We cannot expose here the whole sequence of such proof-events. We confine ourselves to select some of these historical attempts (proof-events) until the proofevent that includes the communication and validation of the final proof of the theorem and demonstrate how argumentation is involved in the process of search for proof.
The first attempts to prove the Theorem were proofs for specific exponents. The case n = 3 was first explored by Abu-Mahmud Khojandi (c. 940 - 1000), but his attempt has not survived (and thereby cannot be considered as a proof-event) and it is conjectured that it was incorrect. Leonhard Euler gave a proof for n = 3 in 1755 and for n=4 in 1747, but his proof of the former case contained a basic fallacy [9, p.3940]. Many other mathematicians proved the theorem for n=3 using various methods. Gabriel Lamé (1795 –1870) proved it for the case n = 7. In 1847, he communicated a proof of the Theorem, but it was flawed. Gabriel Lame’s proof failed because it was claimed incorrectly that complex numbers could be factored into primes uniquely. This gap was indicated instantly by Joseph Liouville [9, p.76-77]. In 1984, Gerhard Frey pointed out a connection between the modularity theorem and Fermat’s equation, but Fermat’s Last Theorem remained to be a conjecture. The TaniyamaShimura-Weil conjecture, which was proposed in 1955, was the method that led to a successful proof of Fermat’s Last Theorem, when Andrew Wiles accomplished a partial proof of this conjecture in 1994 [29].
Wiles, after spending six years applying various methods that were proved unsuccessful, he approached the problem in a new way. He decided to present his work in June 1993 at the Isaac Newton Institute for Mathematical Sciences [29].
However, during the peer review, it became evident that there was an
incorrect critical point in the proof. Wiles tried almost a year to resolve this point, firstly by
himself and then in collaboration with Richard Taylor, but without success [
This example illustrates the contribution of the agents in the process of proving. Firstly, the central aim of the proving itself is to convince the rest of the community about the justification and the validity of your approach. Moreover, the other agents also contribute significantly in the procedure. So many people had to participate in order to reach the initial goal, which was the proving of the Fermat’s Last Theorem. This participation is depicted with two ways, either with the rejection of someone else’s attempt by pointing out a fault and/or inaccuracy (ex. Liouville indicated Lame’s gap concerning complex numbers) or with the dialogue between cooperators in order to detect and resolve weak or deficiently supported areas in the proving (ex. Wiles asked other colleagues’ help, like Richard Taylor, whenever he found a dead-end or fault in his attempt). Argumentation is more efficient in more interactive contexts, as they let counterarguments to be addressed and stronger arguments to surface. An audience with mainly common beliefs will generate less differentiated counterarguments, making them easier to address. Thus, a mathematician is in a favored position if he wants to ask the assistance of a few colleagues in order to point out most of the possible counterarguments and resolve them in the final proof. By doing this, the proving could be more convincing not only to these few colleagues, but probably to the whole community.
The arguments and the counterarguments also play an essential role in the process of proving, contributed equally in the building and the justification of the proving. The warranted parts of the initial provings acted as a groundwork for the next provings, while the counterarguments that signalize the faults in those unsuccessful provings open the way for better justified provings and in some cases turn the interest of the mathematical community in new unexplored areas. Those incomplete provings may add more or less to the proof of Fermat’s Last Theorem, but the methods that were created with them lead to major discoveries and creation of new fields in the era of Mathematics like the foundation of modern algebra. Discoveries that are even more significant than the proving of the theorem itself and might have not been found if it weren’t for the warranted proof-events and the counterarguments emerged from the previous attempts of proving.
In the next part we present a brief representation of this example through the levels of argumentation1.
In the object level arguments, we have Fermat’s conjecture as the initial proof-event and his claim that he has a proving for this conjecture, without any claim-counterargument clearly opposes this conjecture. →
In the first-level priority arguments, we have proofs for specific exponent n of the Fermat’s Last theorem from various mathematicians in different time points.
For the exponent n=3 (en=3), Leonhard Euler ( have: . ) gave a proof in 1755, so we Many other well-known mathematicians followed with equivalent proofs that support the validity of the proof for n=3. Each prover used a different way (warrant) for proving the conclusion, so their provings are equivalent. i=1:(eEuler,t1707), i=2:(eKausler,t1802), i=3:(eLegendre,t1823), i=4:(eCalzolari,t1855), i=5:(eLame,t1865), i=6:(eTait,t1872), i=7:(eGunther,t1878).
] → Fermat’s Last Theorem was also proved for the exponents n = 5, 6,7, 10, and 14.
In 1847, Gabriel Lame’s proving (eLame) failed because it claimed incorrectly that complex numbers can be factored into primes uniquely. This gap was indicated instantly by Joseph Liouville (eLiouville*).
[ → ]
Andrew Wiles presented his work in June 1993, but it became evident that there was an incorrect critical point (eWiles*) in the proving. Wiles tried almost a year to 1 Names of provers and dates are taken from Wikipedia «Fermat’s Last Theorem». Retrieved from: https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem] resolve this point, firstly by himself and then with the contribution of Richard Taylor, but without success. .
→
Finally, in 1994, Wiles submitted two papers that combined Kolyvagin–Flach approach and Iwasawa theory which was the last step in proving Fermat's Last Theorem. ),
The proof–event managed to deal with all the attacks and we have: at the time t1994.
Thus, Fermat’s Last Theorem is proved valid by Wiles, with the contribution of the other agents that opened the way before him in this ages-long sequence of proof-events.
We have developed a model of the proof-events calculus [32] based on Pollock’s [26], Toulmin’s [28] and Kakas’ argumentation theories, extending the proofevents calculus with the integration of arguments and counterarguments. The combination of Vandoulakis’s and Stefaneas’s proof-events-based theory and logic-based argumentation has the advantage of highlighting weak areas in a proof. Proof-events are not considered as infallible facts before their ultimate validation, thus enabling the exploration of flawed approaches and proofs to be found and resolved. We focused on the connection between proving, human reasoning, cognitive processes and creativity. We presented a calculus for the proof-event argument, argument moves, and temporal predicates and we analyzed them in terms of levels of argumentation. The calculus adds an additional dimension and performs a significant role in making these connections sufficiently detailed and specific. In our future work, we can apply this model to express the proof-events sequence and history in specific examples of mathematical proving, as in the example of Fermat’s Last 26. Pollock J. L. (1992), “How to reason defeasibly”. Artif. Intell., 57(1):1–42. 27. Rissland E.L., (1985), “Argument moves and Hypotheticals” In C. Walter (Ed.), Computing Power and Legal Reasoning, St. Paul, MN: West Publishing Co. 28. Toulmin S. E. (1993). The use of arguments. Cambridge, Cambridge University Press. 29. Singh Simon, (1997), Fermat’s Last Theorem, Fourth Estate Ltd. 30. Stefaneas, P. & Vandoulakis, I. (2015), “On Mathematical Proving”. Computational Creativity, Concept Invention, and General Intelligence Issue. Journal of General AI, 6(1): 130-149. 31. Vandoulakis Ioannis M., Stefaneas Petros, (2015), “Mathematical Style as Expression of the Art of Proving”, Handbook of the 5th World Congress and School on Universal Logic, Istanbul, Turkey, UniLog 2015. 32. Vandoulakis Ioannis M., Stefaneas Petros, (2016), “Mathematical Proving as Multi-Agent Activity Spatio-Temporal”. 23rd World Congress of Philosophy, Methodology of Mathematical Modelling and of Applications of Logical Systems in Scientific Knowledge. 33. Vreeswijk Gerard A.W. (1997), “Abstract argumentation systems” AI, 90: 225-279.