On the Role of Argumentation in Discovery Proof-Events

Abstract

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, 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. Since argumentation is inseparable from the process of searching for mathematical proof, we suggest a modified model of the proof-events calculus, based on certain versions of argumentation theories. 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 in this modified model.

Keywords

• Discovery Proof-Events
• Argumentation
• Proof-Events Calculus

-

The concept of mathematical proof has undergone significant changes in the 20th century. Proof, particularly formalized proof, was initially identified with truth in traditional philosophy of mathematics. However, many mathematicians dealing with real proofs did not accept the paradigm of formalized proof. Joseph Goguen [ 10 ] suggested the broader concept of proof-event, which is actually a social event that takes place in specific place and time and involves public communication. The concept of proof-event is designed to embrace any proving activity, including incomplete proofs or attempts to verify a conjecture. Vandoulakis and Stefaneas [ 31 ] described proof-events as activity of a multi-agent system incorporating their history, insofar as they form sequences of proof-events evolving in time. Thus, they modelled certain temporal aspects of proof-events, using the language of the calculus of events developed in Kowalski’s calculus of events [ 19 ].

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 using arguments and counterarguments. Hence, we extend the calculus of proof-events by integrating argumentation theory to represent 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 dialogue of agents that use arguments and counterarguments or counterexamples in their attempt to clarify the validity of a purported proof.

Many researchers have highlighted the role of argumentation in mathematics. Mathematicians do much more, than simply prove theorems. Most of their proving activity might be understood as varieties of argumentation [ 2 ]. Lakatos’ Proofs and Refutations [ 20 ] is an enduring classic that highlights the role of dialogue between agents (a teacher and some students) by attempts at proofs and critiques of these attempts1. The comparison between argumentation supporting an assumption or a purported proof and its proof is based on the fact that proof can be regarded as a specific kind of argumentation in mathematics [ 22 ].

A methodological tool that has been widely used to examine argumentation is Toulmin’s model [ 28 ], in which argument consists of “claim”, “data”, and “warrant” that are considered the essential elements of applied arguments. The procedure by which mathematicians evaluate reasoning resembles to argumentation, as various researchers have showed ([ 6 ], [ 1 ], [ 22, 23 ], [ 4 ], by adjusting Toulmin’s model to mathematical examples. We propose to integrate argumentation theory into the calculus of proofevents. By doing so, we can represent all the relevant stages that we go through when proving, from the statement of a problem until its validation or rejection by the relevant community that uses arguments and counterarguments or counterexamples in checking the validity of a purported proof.

To combine the proof-event calculus with argumentation theory, we use the basic structure of Toulmin’s model for the representation of arguments and Pollock’s logicbased argumentation theory. We rely on Pollock’s view of defeasible reasoning that has non-monotonic character. Pollock represents argument in the form ,c , where Φ is a set of data and c is a claim [ 25 ]. He separated the rebutting and undercutting defeat and presented one of the first monotonic logics with concepts of argument and defeat, even though he did not explicitly distinguish between them [ 24 ].

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 in terms of the levels of argumentation. In the last section, Fermat’s

Last Theorem is investigated as a case study illustrating the concepts introduced.

2

Proof-events vs. arguments

Comparison of the basic elements of proof-events and argumentation theory shows similarities in structure, the sequence of events, the agents, the layers of communication, and the levels of argumentation. 1 Lakatos uses Euler’s theorem for star-polyhedra to conclude that no proof is ultimately certain.

However, in our view, Lakatos’ counterexamples can be removed by reinterpretation (by another agent) of the initial definitions, so that the community involved in a proof event could reach an agreement concerning the validity of a purported proof. Accordingly, the mathematical community is the ultimate truthmaker of mathematical intuitions, the validity of which is decided within a finite, although possibly too long time-period of evolution of sequences of proof-events.

Arguments and proof-events have three common characteristics: a set of premises for a task or problem, a method of reasoning and a conclusion. Moreover, each proofevent 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 earlier proof-events (sequences of proof-events or sequences of arguments and counterarguments) [ 31 ]. A sequence of proof-events is complete when the community involved in it concludes that they have understood the suggested proof and agree that it is actually a proof or that is invalid, based on advocated counterargument (or counterexample).

Proof-events presuppose the existence of at least two agents enacting the roles of prover or interpreter [ 31 ]. Similarly, argumentation involves (at least two) agents enacting the roles of supporter or opponent [ 17 ]. The layers of communication, understanding, interpretation, and validation that agents use to disseminate their knowledge, are common in both approaches. An agent is a proactive and intelligent system that enacts a specific role. We may consider some software systems as agents, provided that they possess these characteristics. The main concept advanced in agent-based approaches is that of autonomy: agents operate as independent individual entities trying often to collaborate and coordinate with others [ 13 ]. However, the steps that an individual agent strives to perform in order to accomplish a mathematical task may intersect with the steps attempted or undertaken by other agents. A number of important questions arise out of this inter-agent debate, such as the systematization of agents’ contribution as phases in a goal-directed plan (such as proving) and the review in the formalization of logic-based languages in terms of both syntactic and semantic aspects [ 16 ]. 3

Argumentation models

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 formalize proof-events based on argumentation theory, using a list of structures, which represent arguments and counterarguments. Our approach presupposes a multi-agent system, where the agents enact the roles of provers and interpreters. An argument has premises, sentences, and conclusion. Arguments considered in this section involve grounds and claims, which are formulae in classical logic and methods of inference by which a claim follows from a set of formulae, which are taken to be deductive inferences, denoted by ⊢. A proof-event е can be understood as a communicated argument ,c [ 26 ] concerning a stated (fixed) problem specified by certain conditions (predicates) and be designated by the pair e ,c , i.e. e ,c

e communicate(Problem,t) ,(communicate ,c ),w where Φ is the Data of the argument, c is the Claim that refers to a stated (fixed) problem (proposition), specified by certain conditions (predicates) and w are the (possibly implicit) inference rules (Warrant) which allow Φ to be logically associated with c, such that: (i) (ii) c (iii) There is no , such that c .

A counterargument to a proof-event e ,c represents a new proof-event that can be

designated by the pair e , , where Ψ is the Data (generally different from those of Φ) on which is based the Claim (Counterargument) β that refers to the same fixed problem (proposition) stated at time t, specified by the same conditions (predicates).

Argumentation may require chains (or trees) of reasoning, where claims are used in the assumptions for obtaining further claims [ 8 ], so that a proof-event could be an atomic argument or a sequence of arguments (fluent). Fluents f are sequences of proof-events (proving instances) evolving in time that refer to a fixed problem, specified by certain conditions [ 30 ]. Let R be a set of rules of inference. A fluent f is a formula of the form e1,e2,e3 e where e1 1,c1 , e2 2,c2 , e3 3,c3

is a finite, possibly empty, sequence of arguments, such that the conclusion of proof-event ei is the claim ci , i.e.

conc(e1) c1, conc(e2 ) c2, conc(e3) c3 for some rule c1,c2,c3 c

R [33]. Accordingly, the meaning of the three essential

components of argument based on Toulmin’s model [ 28 ], which abbreviated by corresponding prefixes, are defined as follows for the concept of fluent:

Data:

Claim: prem(e) prem(e1) prem(e2) prem(e3) 1 2 3 conc(e) c c1 c2 c3 Warrant: sent(e) sent(e1) sent(e2) sent(e3) w1 w2 w3 where c (Claim) is the statement communicated by the agent, Φ (Data) are facts that serve as the ground of the claim, and w (Warrant) are the inference rules, which allow data to be logically associated with the claim. The aforementioned elements are frequently used to define a consequence relation between the arguments and/or the counter-arguments. (1) (2) (3) 3.1

Argument moves

In the course of a proof-event, 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. When a chain of reasoning ( x0x1, x2, xn , where the argument xi attacks the argument xi 1 for i

0 ) is explicitly constructed, 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 [ 11 ] refers to “argument moves” as analogues of three roles for legal cases2. We reserve the term argument moves for specific, active tactics or strategy that a prover can choose to support his claim. We present four fundamental relations that indicate links and conflicts at the sequence of proof-events. The possible argument moves could provide support or attack the claim.

Given a claim c and an argument communicated during the proof-event e, possible

argument moves, which provide support for c [ 12 ] include:

Equivalence: an argument for a claim, which is equivalent to (or is) c;

Elaboration: an argument that is elaboration of c, and

whereas 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.

Argument moves that support a claim. A proof-event e1 is equivalent with proofevent e2 , if , c c , although it might be w w , i.e., whenever they have the same data and the same conclusion (although possibly different warrants), i.e.

Equivalence(e,e ) e( ,c) e ( ,c ) .

Therefore, equivalent proof-events can have different ways of proving3.

If e ,c is a proof-event, a set of sentences S is called that elaborates or embellishes

upon e, if the following relation holds Elaboration(e,S) sent(e) sent(S) concl(e) iff

S c

These moves are used for backing our claim and supporting our proof, so that

Support(e,t)

Equivalent(e,e )

Elaboration(e,S) (4) (5) (6) (7) Counterargument moves that attack a claim. A counterargument communicated during the proof-event e ,

attacks or rebuts the conclusion of an argument communicated during the proof-event e ,c , if the following relation holds Rebutting(e ,e) rebut(e ,e) concl(e) iff c A counterargument communicated during the proof-event e , is called that undercuts or attacks some of the premises (defeasible inference) of the argument communicated during the proof-event e ,c , if the following relation holds 2 This term was also previously used by Rissland [ 27 ], Asley and Aleven [ 7 ], Pease et al [ 21 ]. 3 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.

Undercutting(e ,e) undercut(e ,e) prem(e) iff i i (8) for { 1, 2, , n }

Given an argument communicated during the proof-event e ,c , a counterargu

ment 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. In symbols, Attack(e ,t) rebut(e ,e) undercut(e ,e) (9) 3.2

Temporal Predicates

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 [ 19 ]. Reasoning about actions and change (RAC) [ 16 ] is concerned with the study of how fluents change when new information is acquired and how this view of the problem is affected by the observation of some events remaining active or terminated at a particular time. The language in RAC uses causal propositions (c-propositions), of the form “A initiates F when C” or “A terminates F when C”, which in this paper are represented in more detailed and specific form with the arguments’ and counterarguments’ moves that initiate or terminate a fluent. In most cases, we will take into consideration only the starting point of a proof-event, with the exception of those proofevents that terminate, or when duration plays a significant role. In these cases, we mention both the starting and termination points.

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) . In particular,

Happens(e,t) means that a proof-event e occurs at time t.

Initiates(e, f ,t)

Happens(e,t1)

attack(e ,t1) support(e,t1) , at time t1 , (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 .

Clipped(t1, f ,t2 ) [ e2,t2(Happens(e2,t2 ) e1,e1 ,t1,t[Happens(e,t1),(t1

t t2 ) attack(e1 ,t)] attack(e1 ,t))], for t1 t t2 which means that a proof-event clips when there is no proof-event e2 that attacks the counterargument e1 attacking the proof-event e1 between t1 and t2 . (10) (12) Terminates(e1, f ,e1) e,e ,t1([attack(e ,t1) 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).

ActiveAt(e, f ,tn 1)

Happens(t,en 1,tn 1)

attack(en,tn ) support(en ,tn ), for every n , tn 1 tn 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 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 aforementioned, we can conclude that

Happens(e,t1) Initiates(e, f ,t1) (t1 t2) attack(e ,t2) ActiveAt(e, f ,t2 ) 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 . (13) (14) i , i , (15) (16) i n[ActiveAt(e, f ,ti ) (ti tn )

Valid(e,tn ), at time tn, i

Terminates(e, f ,ti )] 1, ,n, n which means that a fluent could consider valid at time tn , if it is active and there is no counterarguments to terminate it at time ti , for every i 1, ,n, n . 4

Levels of argumentation

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 [ 17 ] presented three levels of arguments: object level arguments, which represent the possible decisions or actions in a specific domain. First-level priority arguments, which express justifications on the object-level arguments in order to resolve possible conflicts. Then, higher-order priority arguments are used to deal with potential conflicts between priority arguments of the previous level until all conflicts are resolved.

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 proofevents 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 continue 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. 4.1

Object level arguments

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 f0 and continue to the first level priority arguments.

Happens(ei,ti ), i 1, ,m, m , ti tm t ei[Happens(ei,ti ) attack(ei ,ti ) (ti tm )]

Initiates(ei, f0,tm ) for i 1, ,m, m , ti tm

t . 4.2

First-level priority arguments for every i that we have (17) (18) (19) (20) Initiates(em 1, f1,tm 1), attacks(em 1, f1,tm 1), i 1, ,m1, m1 , tm 1 tm m1 t em i ,em i ,tm i [attack(em i ,tm i ) conc(em i )

prem(em i )] (tm i tm m1 t) [ em i 1,tm i 1(Happens(em i 1,tm i 1)

prem(em i )] attack(em i ,tm i )]

Terminates(em i , f1,tm m1 )] so that the proof-events that have been attacked and could not resolve the conflict, terminate in this fluent. The rest of them remain active, so we have:

ActiveAt(em j , f1,tm m1 ) for every j i, j 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 preceding level until all conflicts are resolved or our claim proved invalid. In the final level, we have 4.3

Higher-order priority arguments

If proof-events fail to resolve all the conflicts, our claim cannot be proved and it clips: (21) (22) (23) Clipped(ti,e,tn ) at the time tn tm(n 1) mn ti

If the proof –events manage to deal with all the attacks and

j, j [ActiveAt(em(n 1) j , fn,tn ) Valid(e,tn ), at the time tn Terminates(e, fn,tn )] tm(n 1) mn ti then our claim is proved valid. 5

A Case Study: Fermat’s Last Theorem

We illustrate our approach by the examination of Fermat’s Last Theorem (FLT). It 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 satisfy the equation an bn cn , whenever n is an integer greater than 2. The statement of the problem marks the startingpoint of a sequence of proof-events that evolved in time. Even though Fermat claimed to have proved this theorem, it actually took 358 years and numerous attempts undertaken by eminent mathematicians (agents) to prove it until its final proof by Andrew Wiles in 1995. Fermat’s alleged proof cannot be included in the initial proof-event, since it was never communicated. In his letters, Fermat communicates the Theorem for the cases n 3 and n 4 and gives a solution only for the latter case.

We cannot expose here the whole sequence of such proof-events. We confine our

selves to select some of these historical attempts (proof-events) until the proof-event, during which the communication and validation of the final proof of the theorem took place and demonstrate how argumentation is involved in the process of search for proof.

The first attempts to prove FLT concerned 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, 39-40 ]. Many other mathematicians proved the theorem for n 3 using various methods. In 1825, Legendre (1752–1833) and Peter Gustav Lejeune Dirichlet (1805-1859) proved independently FLT for the case n 5 . Several novel approaches were developed by Sophie Germain in 19th century [ 9, 59 ]. In 1839, Gabriel Lamé (1795 –1870) proved FLT for the case n 7 . In 1847, he communicated a proof of FLT, but it was flawed, because it was assumed incorrectly that complex numbers could be factored into primes uniquely. This gap was indicated by Joseph Liouville [ 9, 7677 ]. Kummer proved the conjecture for regular prime numbers, but not for irregular primes. Further, the Theorem was proved for the exponents n 6,10,14 . In 1984, Gerhard Frey pointed out a connection between the modularity theorem and Fermat’s equation, but FLT remained unproved. The Taniyama-Shimura-Weil conjecture, which was proposed in 1955, was the method that led to a successful proof of FLT, when Andrew Wiles accomplished a partial proof of this conjecture in 1994 [ 29 ].

Wiles, after spending six years applying various methods that were proved unsuc

cessful, he approached the problem in a new way. He discovered an Euler system developed by Victor Kolyvagin and Matthias Flach, which, with his own extension, seemed to work successfully. He asked his colleague, Nick Katz, to help him in checking his line of reasoning for eventual flaws. 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 crit

ical 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 [ 18 ]. When Wiles was on the verge to quit his attempt, he experienced an insight that the Kolyvagin– Flach approach and Iwasawa theory were each insufficient on their own, but in combination they could be strong enough to overcome this final obstacle. In 1994, Wiles submitted two papers that establish the modularity theorem for the case of semistable elliptic curves, which was the last step in proving FLT [ 29 ].

This example illustrates the contribution of different agents (mathematicians) that take part in the sequence of proof-events. Firstly, the main objective for a prover is to convince the community about the soundness of his reasoning and the validity of his purported proof. Moreover, other agents involved also in the proof-event contribute significantly by enacting sometimes as provers or supporters (by suggesting additional supporting arguments) and other times as interpreters or opponents (by suggesting counterarguments that identify eventual gaps or inaccuracies). Thus, many agents participated in the considered sequence of proof-events in order to fulfil the initial task, which was the proof of FLT. This participation has the following manifestations: a. By suggesting partial proofs (for specific cases) of the Theorem. b. By the rejection of someone else’s attempt, pointing out a fault and/or inaccuracy. c. Through a dialogue between provers in order to detect and resolve weak or insufficiently supported arguments in proving (for instance, Wiles asked his colleagues’ contribution, notably Nick Katz and Richard Taylor, when he faced a dead-end in his attempt).

During all these years, thousands of unsuccessful proofs have been undertaken, most of which remain unknown, but some of them have been proposed by eminent mathematicians, such as Euler, Cauchy, Lamé, Kummer, and others. Argumentation is evident in interactive contexts, as they let counterarguments to be set forth and stronger arguments to survive. Both arguments and counterarguments play essential role in the process of proving, contributing equally in the construction and justification of the proof. The warranted parts of the proofs act as groundwork for the subsequent proofs, while the counterarguments that identify faults in unsuccessful proofs open the way for better-justified proofs and, in some cases, turn the interest of the mathematical community on new unexplored areas. In the next section, we present a model of this example in terms of the levels of argumentation. 5.1

Object level arguments – Fermat’s Conjecture

In the object level arguments, we have Fermat’s conjecture as the initial proof-event eFermat and his claim that he has a proving for this conjecture, without any claim-counterargument eFermat clearly opposes this conjecture.

Happens(eFermat ,t1637 ) attack(eFermat ,t1637 )

Initiates(eFermat , f0,t1637 ) 5.2

First-level priority arguments - Proofs for specific exponents

In the first-level priority arguments, we have proofs for specific exponents n of the FLT from various mathematicians in different time points.

For the exponent n 3 , the proof-event en 3 happened when Leonhard Euler gave a proof in 1755. Therefore, we have Happens(eEuler ,t1755 ) .

Many other well-known mathematicians followed with equivalent proofs that sup

port the validity of the proof for n 3 . Each prover used a different way (warrant) for proving the conclusion. Thus, their provings are equivalent.

Support(en 3,ti ) Equivallent(en 3,ei ) for i 1, ,14 , with i i i i 1 : (eEuler ,t1707 ) , i 2 : (eKausler ,t1802 ) , i

3 : (eLegendre,t1823 ) , 4 : (eCalzolari,t1855 ) , i 7 : (eGunther ,t1878 ) , i 10 : (eRycklik ,t1910 ) , i 5 : (eLamé,t1865 ) , i

6 : (eKausler ,t1802 ) , 8 : (eGambioli ,t1901) , i

9 : (eKrey ,t1909) , 11 : (eStockhaus ,t1910 ) , i 12 : (eCarmichael ,t1915) , i 13 : (eThue,t1917 ) , i

From the aforementioned, we have

14 : (eDuarte,t1944 ) .

Happens(eEuler ,t1755 ) Initiates(en 3, f1,t1755 ) [ attack(en 3,ti ) support(en 3,ti )] (t1755

ActiveAt(en 3, f1,ti ), for t1755 ti ti )

Similarly, we have proofs for n ticians (provers). The first proof for n 5 (en 5 ) and n

7 (en 7 ) by various mathema5 belongs to Legendre (1825). Accordingly, we have Happens(eLegendre,t1825 ) . Equivalent proofs were also proposed.

Equivalent(en 5,ej ) for i 1, ,10 , with 1 : (eLegendre ,t1825 ) , j 4 : (eLebergue ,t1843 ) , j 7 : (eWerebrusow ,t1905 ) , j 10 : (eTerjanian ,t1987 ) .

2 : (eDirichlet ,t1825 ) , j

3 : (eGauss ,t1875 ) , 5 : (eLamé ,t1847 ) , j

6 : (eGambioli ,t1901) , 8 : (eRychlik ,t1901) , j 9 : (eCorput ,t1159 ) 1 : (eLamé ,t1839 ) , k 4 : (eMaillet ,t1897 ) .

7 , the first proof was provided by Lamé in 1839; therefore, we have

Happens(eLamé,t1839 ) and the equivalent supporting provings Support(en 7,tk )

Equivalent(en 7,ek ) for k 1, ,10 , with 2 : (eLeberguet ,t1840 ) , k 3 : (eGenocchi ,t1876 ) ,

Therefore, we have

Happens(eLamé ,t1839 ) Initiates(en 7, f1,t1839 )

FLT was also proved for the exponents n

) tried unsuccessfully to prove FLT for all even exponents (en 2p ) , which was proved by Guy Terjanian (eTerjanian ) in 1977. Germain’s attempt was incomplete; thus, it clipped

Clipped(t1776,en 2p ,t1831) (t1776 t1 t1831) [ e2,t2(Happens(e2,t2 ) eGermain ,eGermain ,t1[Happens(eGermain ,t1) attack(eGermain ,t)] attack(eGermain ,t1))], for t1776 t1 t1831. and became active again after the successful proving of Terjanian in 1977.

ActiveAt(en 2p, f2,t1977 ) Happens(eTerjanian ,t1977 )

5.4 Third-level priority arguments - Ernst Kummer and the theory of ideals

The sequence of proof events continues in the third-level with further attempts for proving FLT. In 1847, Lamé’s proof (eLamé ) failed, because it incorrectly assumes that complex numbers can be factored into primes uniquely, a gap that was revealed by Liouville (eLiouville ) . Thus the counterargument generated by Liouville indicated the fault in

Kummer (eKummer ) proved the conjecture for regular prime numbers (eregular ) , although not for irregular primes (eirregular ) . Therefore, we have

ActiveAt(eregular , f3,t1893 )

Happens(eKummer ,t1893 ) attack(eKummer ,t1893) , but Happens(eFrey ,t1984 ). 5.6

Fifth-level priority arguments – Andrew Wiles

In the fifth-level priority arguments, the procedure and history in the Andrew Wile’s attempts is represented. Wiles (eWiles ) discovered and extended an Euler system. He also asked his colleague, Nick Katz, to help him in checking his reasoning for eventual faults.

Initiates(eWiles , f5,t1993 )

Happens(eWiles ,t1993 ) attack(eWiles ,t1993 ) support(eKatz ,t1993 ).

He presented his work in June 1993, but it soon became evident that there was an

incorrect critical point (eWiles ) in the proof. Wiles tried for almost a year to resolve this point, firstly by himself and then in collaboration with Richard Taylor (eTaylor ) , but in vain. Thus, his attempted is clipped on the time period from 1993 until 1994.

Clipped(t1993,eWiles ,t1994 ) (t1993 t1 t1994 ) [ e2,t2(Happens(eTaylor ,t2 ) eWiles,eWiles ,t1[Happens(eWiles,t1) attack(eWiles 1 ,t )]

In 1994, Wiles managed to overcome this gap by combining Kolyvagin–Flach approach

[Elaboration(eWiles,SKolyvagin Flach )] and Iwasawa theory [Elaboration(eWiles,SIwasawa )] and he submitted his final paper which was the last step in proving FLT.

ActiveAt(eWiles , f5,t1994 )

Happens(eWiles ,t1994 )

attack(eWiles ,t1994 ) Elaboration(eWiles ,SKolyvagin Flach )

Elaboration(eWiles ,SIwasawa ) 5.7

Higher-order priority arguments-Fermat’s Last Theorem

The proof–event managed to deal with all the attacks and we have

[ActiveAt(eWiles, fn,t1994 ) Terminates(eFermat , fn,t1994 )] Valid(eFermat,t1994 ) at the time t1994 .

Thus, FLT 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.

attack(eWiles,t1))], for t1993 t2 t1993. 6

Conclusion

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 proof-events calculus by integrating argumentation theories. The combination of Vandoulakis-Stefaneas 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 outlined a calculus for proof-event argument, argument moves, and temporal predicates and analyzed them in terms of levels of argumentation.

References

1. Aberdein Andrew , ( 2005 ), “ The Uses of Argument in Mathematics” . Argumentation 19 : 287 - 301 .

2. Aberdein Andrew , ( 2008 ), Mathematics and argumentation . Netherlands , Kluwer Academic Publishers.

3. Aberdein Andrew , ( 2009 ), “Mathematics and argumentation”. Foundations of Science 14 ( 1-2 ): 1 - 8 .

4. Aberdein Andrew , Dove Ian J. (Eds.). ( 2013 ). The argument of mathematics . Dordrecht: Springer.

5. Aczel Amir D. ( 1996 ) Fermat's Last Theorem: Unlocking the Secret of an Ancient Mathematical Problem . New York: Dell Publishing.

6. Alcolea Banegas , J. ( 1998 ), “L' Argumentació en Matemàtiques” . E. Casaban i Moya (ed.), XIIè Congrés Valencià de Filosofia. Valencià, 135 - 147 . Translation online at http://my.fit.edu/~aberdein/ArgMathIntro.pdf

7. Ashley K.D. , Aleven V. , ( 1991 ), “A Computational Approach to Explaining CaseBased Concepts of Relevance in a tutorial Contect” . Proc. Case-Based Reasoning workshop , Washington, 257 - 168

8. Besnard Philippe and Hunter Anthony, ( 2008 ), “Elements of Argumentation”. The MIT Press Cambridge, Massachusetts London, England.

9. Edwards Harold M. ( 1977 ) Fermat's Last Theorem . Springer.

10. Goguen , Joseph, ( 2001 ), “ What is a proof” , http://cseweb.ucsd.edu/~goguen/papers/proof.html

11. Gordon T. F. , ( 1991 ), “ An abductive theory of legal issues” , International Journal of Man-Machine Studies , 35 ( 1 ): 95 - 118 .

12. Haggith , M. ( 1996 ), “A meta-level argumentation framework for representing and reasoning about disagreement” . Ph.D. thesis , Dept. of Artificial Intelligence, University of Edinburgh.

13. Kakas A.C. , Kowalski R.A. , Toni F. , ( 1992 ), “ Abductive logic programming” , J. Logic Comput . 2 ( 6 ): 719 - 770 .

14. Kakas Antonis , Loizos Michael , ( 2016 ), “Cognitive Systems: Argument and Cognition” . IEEE Intelligent Informatics Bulletin , 17 ( 1 ): 15 - 16

15. Kakas Antonis , Loizos Michael, Toni Francesca , ( 2016 ), “Argumentation: Reconciling Human and Automated Reasoning” . Proceedings of the Workshop on Bridging the Gap between Human and Automated Reasoning , New York, USA.

16. Prendinger Helmut , Schurz Gerhard ( 1996 ) “Reasoning about actions and change” . Journal of Logic, Language and Information . Volume 5 , Issue 2 , 209 - 245 .

17. Kakas A. , & Miller R. ( 1997 ). “A simple declarative language for describing narratives with actions” . Journal of Logic and Algebraic Programming , 31 , 157 - 200 .

18. Kakas Antonis C. , Moraitis Pavlos , ( 2003 ), “ Argumentation based decision making for autonomous agents” . In: Proc. Second International Joint Conference on Autonomous Agents & Multiagent Systems, AAMAS 2003 , Melbourne, Australia, 883 - 890 .

19. Kolata Gina , ( 1994 ), A Year Later , Snag Persists in Math Proof, Published: June 28, 1994 , http://www.nytimes.com/ 1994 /06/28/science/a -year-later-snag-persistsin-math-proof .html

20. Kowalski Robert , ( 1992 ), “ Database updates in the event calculus” . The Journal Of Logic Programming , Elsevier Science Publishing Co., Inc., 12 : 121 - 146 .

21. Lakatos , I. ( 1976 ), Proofs and Refutations . Cambridge, Cambridge University Press.

22. Pease Alison , Smaill Alan, Colton Simon, Lee John , ( 2008 ). Bridging the gap between argumentation theory and the philosophy of mathematics , Kluwer Academic Publishers.

23. Pedemonte , B. ( 2007 ). “How can the relationship between argumentation and proof be analyzed?” Educational Studies in Mathematics , 66 : 23 - 41 .

24. Pedemonte B. ( 2008 ), “Argumentation and algebraic proof” . ZDM Mathematics Education, FIZ Karlsruhe , 40 : 385 - 400 .

25. Prakken Henry , Horty John , ( 2012 ), “ An appreciation of John Pollock's work on the computational study of argument” , Argument & Computation . 3: 1 - 19 .

26. Pollock J. L. ( 1987 ), “ Defeasible reasoning” . Cognitive Science , 11 : 481 - 518 .

27. Pollock J. L. ( 1992 ), “ How to reason defeasibly” . Artif. Intell., 57 ( 1 ): 1 - 42 .

28. Rissland E.L. , ( 1985 ), “ Argument moves and Hypotheticals” In C. Walter (Ed.), Computing Power and Legal Reasoning , St. Paul, MN: West Publishing Co.

29. Toulmin S. E. ( 1993 ). The use of arguments . Cambridge: Cambridge University Press.

30. Singh Simon , ( 1997 ), Fermat's Last Theorem , Fourth Estate Ltd.

31. Stefaneas , P. & Vandoulakis , I. ( 2015 ), “On Mathematical Proving”. Computational Creativity , Concept Invention, and General Intelligence Issue . Journal of General AI , 6 ( 1 ): 130 - 149 .

32. 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 .

33. 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.

34. Vreeswijk Gerard A.W. ( 1997 ), “Abstract argumentation systems” AI , 90 : 225 - 279 .