 # Discrete mathematics, computer science, logic, proof, and their relationships

Faïza Chellougui, Viviane Durand-Guerrier and Antoine Meyer

This chapter relies on original contributions to the first two INDRUM conferences, summarizing their research lines, the theoretical and methodological issues raised, their results and perspectives. It aims at providing a synthesis of the research field as it appeared through the presentations and discussions at INDRUM. It presents some of the challenges faced by university students when dealing with discrete mathematics, computer science, logic, and proof and proving in their mathematical activity.

The chapter is structured into three main parts, all concerned with university levels. The first part describes the issues of teaching and learning discrete mathematics, combinatorics and their interactions with computer science. The second part presents the place and role of logic in defining, reasoning, proof and proving. The third part is devoted to the need for logic in mathematics and computer science.

Discrete mathematics and links with computer science

In this part, we first present reasons for teaching discrete mathematics at university level. Then we provide three examples of situations for teaching discrete mathematics, two of which stand at the interface with computer science.

Reasons for teaching discrete mathematics at university level

As pointed out by Ouvrier-Buffet, Meyer and Modeste (2018), discrete mathematics is a recent field linked to computer science. The authors underline the fact that teaching and learning discrete mathematics involves mathematical skills and heuristics (e.g. different kinds of proof and reasoning techniques, several ways of modelling etc.) and also develops objects, concepts, methods and tools that are relevant for computer science. This, in turn, raises new types of questions for mathematics. More generally, several aspects of discrete mathematics are at the interface between mathematics and computer science. An important example is the concept of algorithm (Modeste, 2012, 2016). Durand-Guerrier, Meyer and Modeste (2019) elaborate on the links between algorithms, proofs, and programs, and argue that the question of proof in mathematics and computer science is a central didactical issue, in particular at undergraduate levels. Considering that several topics are often gathered under the term discrete mathematics, Ouvrier-Buffet et al. (2018) claim that a way to characterize this field is to emphasize the specific modes of reasoning and the discrete nature of the structures that are involved. Knuth (1974, p.329) pointed out that many parts of mathematics use methods referring to discrete mathematics (e.g. group theory, number theory, geometry, algebraic combinatorics, graph theory', or cryptography) and wondered whether the traditional curriculum — calculus courses, etc. - should be revised to include more of these discrete aspects. The crucial role of discrete mathematics for developing heuristics and reasoning skills is pointed out by Abdallah (2018). She notes that in the debates around proof and proving, many examples in discrete mathematics are provided. Grenier and Payan (1998) provide evidence that discrete mathematics is relevant for changing the students’ view on proof: discrete objects and situations are in general easily accessible and favour the devolution of problems; it is relevant in that context to explore particular simple cases, to solve them and then to move on to more sophisticated ones, and further to generalization. Alcock (2009) considers that such examples enhance the semantic development of mathematical concepts and proving skills. Nowadays, in some countries, such as France, the place of discrete mathematics in curricula is still not well established (Ouvrier-Buffet et al., 2018), contrary to other countries with a strong tradition such as Hungary, or the USA where it is part of curricular recommendations (Epp 2016). Ouvrier-Buffet et al. (2018) advocate that “discrete mathematics courses are relevant to a wide variety of majors at university level, including mathematics, number theory, computer science, and engineering” (ibid, p. 256). They claim that for countries such as France where the teaching of discrete mathematics is not well established, a key research question is "How to design curricula and didactical engineering2 for the first university years?” (ibid, p. 258). In the next section, we present examples of situations for teaching discrete mathematics that were presented and discussed during the conferences, as a first step for dealing with this question.

Examples of situations for teaching discrete mathematics at university level

The brief overview presented in the previous section provides evidence that the crucial contribution of discrete mathematics to foster proof and proving skills in mathematics and in computer science is acknowledged by a number of researchers. This was defended and discussed during the two INDRUM conferences, relying on concrete examples of activities both in mathematics and in computer science. In this section, we present some of these examples and activities, trying to make clear the dialectic between proof and conceptualization, in the sense that working on proofs fosters conceptualization (Durand-Guerrier & Tanguay, 2018), and conversely deepening the appropriation of concepts enhances the capability to engage in proof.

Generalization is a key aspect of mathematics that fresh university students are expected to be able to grasp. Indeed, an important part of university courses (e.g. Calculus) consists in conjecturing and proving universal statements (theorems), most often using proofs by generic element, that are then used in proofs through inferences. In addition, students are expected to be able to engage by themselves in a proving process. However, there is research-based evidence that university students face strong difficulties regarding this aspect of mathematical activity. One can hypothesize that even in Calculus, the mathematical objects at stake are too complex to allow fresh university students to explore them in a fruitful way. In other words, students will be more inclined to look for a relevant theorem in order to solve a general problem in one step, than to explore the properties of objects by examining particular cases or small examples of a given class in order to make conjectures on a possible generalization and then try to prove it. Lockwood and Reed (2018) support the idea that combinatorial enumeration problems are relevant to develop rich mathematical thinking. In their paper, they focus on the role of generalization in students’ counting, relying on a model developed in Lockwood (2013) in a set-oriented perspective, with three main components: formulae/ expressions; counting processes; sets of outcomes, and their interrelation. They report on two experiments with students following a Calculus course, aiming to shed light on the following research question:

In what ways can specific examples, concrete outcomes, and particular contexts be leveraged to foster generalizing activity in a combinatorial setting? (ibid, p. 244).

In the first experiment, four volunteer students having not yet followed a course on discrete mathematics were involved. They were invited to solve tasks aiming to shed light on the fundamental role of “concrete examples, concrete outcomes and particular contexts in combinatorial reasoning and of its relevance for generalization”. Lockwood and Reed (2018) report on the resolution by a student named Carlson of the “horse race problem”: There are 10 horses in a race. In how many different ways can the horses finish in first, second, and third place? They noticed that Carlson had solved the problem in a non-standard way, by dividing the total number of outcomes (namely 10!) by the number of outcomes for the 7 horses that were not ranked (namely 7!). During the experiment, when confronted with various other arrangement problems that he explicitly recognized as similar to the horse race problem, Carlson repeatedly resorted to this resolution, using the same mode of reasoning (related to the counting process of arranging all objects and then dividing by the number of ways to arrange the leftover objects). Finally, he refers once more to this problem in order to provide the general formula for arranging a certain number of objects from a finite set of distinct objects. Thus, the horse race problem served for Carlson as a generic example (in the sense of Mason & Pimm, 1984) of this kind of combinatorial problem. In addition, this exemplifies the model developed by the author in Lockwood (2013), by shedding light on the interrelation between its three components.

In the second experiment, a Calculus student, Tyler, was interviewed by the author, while working on a password activity:

In the interview Tyler was counting two kinds of passwords - those involving either upper case As and/or Bs, and those involving As, Bs, and the number 1 (with repetition allowed). Tyler had initially engaged in systematic listing activity to count the number of possible 4-character AB passwords.

(ibid, p. 25 i)

Later in the interview, the student showed that he recognized, in a more complex password problem, the opportunity to reduce it to the prior problem, and engaged in generalization. Lockwood and Reed (2018) argue that: “reasoning carefully about the concrete examples and actually engaging in concrete listing activity' may have helped to solidify a broader combinatorial process.” (ibid, p. 252).

These two examples are developed more in depth in Lockwood and Reed (2018). The short synthesis above stresses the role of concrete examples and concrete outcomes for leveraging generalization in combinatorial setting. This is consonant with several aspects of the work developed by Gardes (2013) in the frame of number theory', in particular with the concepts of gesture adapted from the philosophy of mathematics (Cavailles, 1981; Chatelet, 1993; Longo, 2005). The main features of this perspective are summarized in the second part of this chapter.

Two examples at the interface with computer science

In this section, we briefly present two situations in discrete mathematics developed in Ouvrier-Buffet et al. (2018), designed as examples

to illustrate the potentialities of discrete mathematics to engage students in learning modelling, proving, and mathematical reasoning and also to underscore the validity and the interest of keeping in mind the algorithmic point of view and the connections with computer science.

(ibid, p. 259).

The first example is a research situation for the classroom in the sense of Grenier and Payan (1998). The object at stake is the discrete straight line (the colouring of squares, or “pixels”, on a regular rectangular grid, in order to give the best possible visual impression of a straight line). Ouvrier-Buffet (2006) had previously analysed the evolution potential of zero-definitions3 of the concept of “discrete straight line”. Professional researchers in discrete geometry (both mathematicians and computer scientists) use several definitions, but the proof of their equivalence remains worth considering. From a mathematical point of view, discrete geometrical objects, and more specifically discrete straight lines, can be approached in several ways, such as discrete differential analysis, algorithms involving combinatorial analysis, or through an arithmetic definition. The author underlines the fact that approaching the discretization of a real straight line by checking linearity conditions is directly related to number-theoretical issues in the approximation of real numbers by rational numbers. From a didactical point of view, discrete straight lines are accessible through their representations (e.g. perceptive and analytical aspects of geometry) and the (real) straight line can act as a referent. Their definitions and properties are not institutionalized (a concept is institutionalized if it has a place in an official curriculum). Ouvrier-Buffet (2006) reports on an experiment implemented with fresh university students, who were invited to elaborate a definition of a discrete straight line. She underlines several approaches dealing with this concept, which she refers to as “real straight line” (What is the “nearest” pixel to a real line? What kind of modelling should be used?), “regularity” (What are the properties of the sequence of stages -called the chaincode string?), and “axiomatization” (What about the existence of the intersection of two discrete straight lines? Is a discrete straight line unique?). Each point of view brings about several zero-definitions. To engage into an axiomatic perspective carries great difficulty, requiring to deal with both the perceptive aspect of a straight line and the axiomatic perspective, the latter requiring some implicit skills and knowledge in students (e.g. building a theory and choosing among competing definitions). The main results of this experiment underscore the ability of students to engage in a defining activity with this concept. Although students did not choose an axiomatic perspective, they were able to engage in reasoning involving methods of approximation close to those used for real straight lines (e.g. statistical linear approximation, op. cit. p.277) and also recursive arguments in order to characterize the sequence of stages of pixels (how can we modify a sequence to obtain a better regularity?). Ouvrier-Buffet et al. (2018) conclude that

The ongoing mathematical problems in discrete geometry are intimately related to questions in other fields of mathematics and computer science. The construction and the manipulation of algorithms are important for this purpose.

(ibid, p. 260).

This example supports the relevance of the introduction of research problems in discrete geometry in mathematics education (Grenier & Payan, 1998).

The second situation presented in Ouvrier-Buffet et al. (2018) deals with a classical “divide and conquer”-type algorithm computing the nth power (for some natural number n) of some floating-point number (or integer) a. This situation is formulated as a typical algorithmic problem: given a and n, compute a". As usual in this kind of setting, one expects an algorithm as an answer, and not simply the mathematical definition of the nth power of a, which is considered known or given. The algorithm provided for computing a" is called “exponentiation by squaring”. It relies on the observation that for all n, a" = (a2)"72 when n is even, and a" = (h2/"'1)/2 otherwise. It is presented as a recursive function power (ti) written in the Python programming language. The main motivation for this particular way of computing a" is of course that it performs far fewer operations than a more naive algorithm (such as multiplying a by itself n — 1 times). This activity includes considerations regarding its analysis. In particular, the typical questions of termination, correctness and algorithmic complexity are discussed, which mobilizes competencies related to infinite-descent arguments, proofs by contradiction, by recurrence or by induction, logic, recurrent sequences, counting, etc.

The authors’ point of view is that tackling these questions mobilises specific mathematical objects and concepts, notably from the above-mentioned fields of arithmetic, discrete mathematics, combinatorics, etc., and provides an opportunity to illustrate, on a simple example, the types of reasoning and proofs which are involved in the analysis of simple algorithms and programs. The article only presents the case of a recursive function, but similar tools can also be used when working with iterative algorithms and programs.

Conclusion of the first part

There is evidence that some mathematical knowledge and skills are required in order to become proficient in computer science. Conversely one may postulate that reasoning about algorithms may provide an incentive towards mathematical activity. The authors therefore advocate the need for continued cooperation between mathematics and computer science teachers and between researchers on mathematics and computer science education in order to better understand the interactions between these disciplines when teaching and learning them.

Logic, defining, proof and proving at university level

In this second part, we consider the place and role of logic in defining, reasoning, proof and proving at university level in the teaching and learning of mathematics, relying mainly of the papers presented during the two INDRUM conferences. Here Logic refers to the domain dealing with reference and with validity of inference. As is generally the case in Mathematics education, we restrict ourselves to first-order logic, which encompasses the interplay between syntax and semantics that is crucial for mathematical activity (Durand-Guerrier & Dawkins, 2018). One hypothesis is that the role of logic in the teaching and learning of mathematics at university is often underestimated by university teachers. This could be a consequence of a rather common assumption that practising mathematics in higher secondary school should guarantee that the logical competences required for advanced mathematics are available to students entering university. However, there is research-based evidence that this is not the case. During the two INDRUM conferences, in line with Durand-Guerrier, Boero, Douek, Epp and Tanguay (2012), several contributions supported the relevance of teaching logic for undergraduates. In the first section, we report on two pieces of research presented in Chellougui (2016) and Brown (2018). The first aims to shed light on the logical complexity of the concept of supremum that is likely to hinder its appropriation by students, and hence advocates the need for addressing the logical aspects of its definition and of its use at university level; the second emphasizes the logical complexity of proof by contradiction. In the second section, we present two case studies aiming to analyse the links between logical skills and students’ activity in proof and proving processes.

Logical complexity in mathematical activity at university level

In this section, we examine the relevance of and interest in taking into consideration the logical complexity of the definition of advanced mathematical concepts at university level. In several countries, university and college faculty teachers commonly complain that many students lack the logical competences, such as the use and interpretation of quantifiers (Dubinsky & Yiparaki, 2000; Selden & Selden, 1995), or access to indirect modes of reasoning (Antonini & Mariotti, 2008), to learn advanced mathematics. This contradicts the view that the knowledge and practice of mathematics gained during secondary education sufficiently develops the required logical abilities. In a didactical perspective, recurrent, resistant and widespread difficulties question both the mathematics at stake and the teaching choices. This means that didactic research on logical issues in the teaching and learning of mathematics and computer science at university should not focus only on students’ difficulties, but also on intrinsic mathematical difficulties and on teachers’ practices, in order to design activities focused on these difficulties. The first point is addressed in the first subsection, which relies on Chellougui (2016). The second point is partially addressed in the second subsection, which relies mainly on Brown (2018).

Logical complexity of the concept of supremum and related students' difficulties

Chellougui (2016) reported on empirical research experiments aiming to investigate the impact of the logical complexity of the concept of supremum on its appropriation by undergraduates. She first acknowledged the logical complexity of the definition by providing a logical analysis of the classical definition of the supremum given in natural language.

“Given a set E endowed with a generic order relation <, an element a € E is called a least upper bound (or supremum) of a non-empty bounded above set A £ E if and only if a is an upper bound for A and a is the smallest upper bound for A.” (translated from Chellougui 2016, p. 269)

In this definition, many components are interwoven: objects (elements of a set); two structures (the initial ordered set E; the set of upper hounds of a given subset A of E); implicitly two relations between objects (to he greater than; to be smaller than);

explicitly two properties of structure (to be bounded above; to have a minimum), linked with two binary relations between an object and a structure (to be an upper bound of; to be the smallest element of).

As usual, the definition is an open sentence that could be satisfied or not by a given element of E. In the case where it is possible to find an element satisfying the definition, it is unique. It is noticeable that in this definition in natural language, there are no explicit quantifiers, while formalizing it in Predicate calculus shows the presence of three quantifiers, including an AE4 alternative:

Given E an ordered set and A a subset of E,

• • An element a of E is the supremum of A if and only if “a is an upper bound for A” and “for all element у of E less than a, у isn’t an upper bound for A (i.e. no number less than a is an upper bound for A)”.
• • An element a of E is the supremum of A if and only if (Vx Є A x < а) Л (Vy < a zl.v Є A у < x).

As underscored by Chellougui (2016) the logical formalization in predicate calculus reveals the logical complexity of the definition. She hypothesizes that giving the definition in natural language without unpacking (Selden & Selden 1995) with students the logical underlying structure (which was the case in her institution, a Faculty of Sciences in Tunisia) might prevent an adequate appropriation of this concept by students. To test this hypothesis, she conducted six interviews of pairs of first year university students, asking them to provide a definition of the supremum and questioning them to tiy to identify their understanding of the logical structure and of the links with the meaning of the concept. During the interviews, it appeared that for all pairs, there was a confusion between the definitions of the relation “to be an upper-bound of’ between an object and a subset of an ordered set, and the property “to be bounded above” for such a subset. The effort of the interviewer to help students clarify the logical aspect at stake (open versus closed sentence, type of objects, importance of the order of quantifiers in a sentence involving an alternation of quantifiers) was not successful. More precisely, the interviews underline the difficulties met by students in acknowledging the logical structure of the definitions of the different components intertwined in the definition of the supremum, when trying to formalize this definition. The analysis of the students’ arguments shows that:

• • Definitions do not seem to be identified as providing properties or relationships to be satisfied. For example, when asked to give the definition of an upper bound of a given subset A of E, many students provide a closed sentence, instead of the expected open sentence. Chellougui (2016) hypothesizes that this is related to the lack of explicit work with students on open sentences that model predicates, properties, and relationships.
• • Nearly all the interviewed students failed to recognize that the order of the two quantifiers in an alternation of the universal and existential quantifiers has an impact on the meaning of the sentence. This is consonant with the results of Dubinsky and Yiparaki (2000) and Durand-Guerrier and Arsac (2005) who underlined the difference between an expert and a novice: experts widely use semantic controls to check the correctness of what they are doing, while a student, as a novice in the field, needs to be able to consider both semantic and syntactic controls to check the validity of their inferences in the process of proof and proving.

The results of this experiment show difficulties both in the appropriation of the meaning of the concept and in the understanding of the links between the syntax of a statement and its semantics (i.e. how to interpret it in terms of objects, properties, relationships). It should be clear for the reader that we do not claim that developing syntactic abilities will be sufficient in itself to improve conceptualization. We rather consider the importance of addressing, with undergraduates, the interplay between syntax and semantics as a crucial tool for contributing to conceptualization and to the development of proof and proving competences (Weber & Alcock, 2004; Alcock 2009; Durand-Guerrier et al., 2012).

Logical complexity in proof by contradiction: the case of "there exist no".

In Brown (2018), the author reports on findings from two analyses of students’ engagement in meta-theoretical tasks drawn from a model of the reasoning requirements in a proof by contradiction. The studies aimed to explore students’ engagement in the tasks, the extent to which they were successful, and the similarities and/or differences between students’ and mathematicians’ approaches.

Following Antonini and Mariotti (2008), the author identifies two meta-theoretical requirements (i.e. the use of logical theorems) in a proof by contradiction of a universal conditional statement. The first is at the beginning, when one must produce the negation of the statement to prove, asserting the existence of a counterexample. The second, when one must recognize that having proved that there exists no counterexample (conclusion following the identification of a contradiction) provides a proof of the initial statement. She recalls that Antonini and Mariotti (2008) have pointed out that both points might be difficult to accept for some university students: the first one because it is difficult to accept the idea of starting a valid argument from a supposedly false statement; the second because the equivalence between the fact that there is no counterexample to the initial statement and the initial statement itself might not be easily recognized. These authors also point out that difficulties with indirect proofs may occur either in mathematical theory or in logical theory. Brown (2018) focuses on the second point. She first conducted a survey addressed to 46 students in a university in the United States on the first day of a Basic Set Theory and Logic course that served as the university’s first course on logic and their “Introduction to Proof’ course. In the survey, two tasks concern the identification of the logical equivalence between a universal conditional statement and the assertion that there exists no counter-example: given the statement “For every integer n, if 11 is a perfect square, then n has an even number of factors”, students were asked if this statement could be proved by proving 1. “There exists no integer n such that n has an even number of factors and n is not a perfect square” (the correct answer is no); 2. “There exists no integer n such that n is a perfect square and n has an odd number of factors” (the correct answer is yes). Only 24% of the students answered correctly to both tasks. This low rate of success called forth a further research question on the persistence of these difficulties after instruction. This was explored by the author in a second study addressed to 21 students (among the 46 surveyed) having completed the Basic Set Theory and Logic course, and to 6 mathematicians. The author briefly presents the contents of the course as follows:

As the course focused on set theory and logic in the service of proof writing, the instruction on set theory and logic was limited to basic properties, terms, and definitions, as well as symbolizing practices, and then on specific proof techniques and/or strategies. (Brown, 2018, p.217)

The participants took part in video-recorded interviews during which the task was presented on a large piece of paper. The participants were given as much time as required, and were then asked to explain their answer to the following question:

TABLE 7.1 The interview task (Brown, 2018, p. 217)

Question: Can you prove Theorem 5 by proving Statement A?

Theorem 5. For all positive integers », if » mod(3) = 2 then » is not a perfect square.

Statement A. There exists no positive integer » such that n mod(3) = 2 and n is a perfect square.

The analysis focused on: 1. the correctness of the answer (the correct answer is yes) with or without hesitation; 2. the theory (mathematical or logical) the participant worked in and how they engaged in that theory; 3. the use of syntactic (rule-based) reasoning and/or semantic reasoning (relying on meanings). Responses were considered as mathematical theory approaches if the participant was observed: 1. explicitly exploring mathematical statements, definitions and/or ternis; and/or 2. constructing a proof of either statement. Responses were considered as logical theory approaches if the participant was observed: 1. posing explicit questions of equivalence; 2. constructing truth-tables and/or working with symbolic logic; and/or 3. citing logical theorems or practices. In addition, the use of syntactic and/or semantic reasoning was noted.

Specifically, coding noted participants’ use of syntactic and/or semantic reasoning, with semantic referring to reasoning that employs meanings and multiple representational systems and syntactic referring to rule-based reasoning within a representational system, (op. cit. pp. 217—218)

Findings indicate students tend towards syntactic, logical theory approaches while mathematicians gravitate towards semantic, mathematical theory approaches. Drawing on interview data, it is shown that students may use symbols to avoid employing fragile content knowledge, yet encounter further difficulties by viewing quantifiers as additional symbols rather than as variable-binding operators that act on open sentences. The author concludes that instruction had little impact on the students’ success with the metatheoretical requirements of a proof by contradiction; indeed the data demonstrate that post-instruction, novices continued to struggle with the metatheoretical requirements of proof by contradiction. As for mathematicians, as expected, they express no doubt about their answer, but three of them show hesitation on their reasoning. To conclude, the author claims that:

The study contributes to the literature by highlighting the logical complexities novices may encounter when producing or comprehending proofs by contradiction, given the approaches they gravitate towards (op. cit. p. 222).

This is in line with previous results in the literature already mentioned in this section concerning: indirect reasoning; quantifications issues; and the role of the interplay between syntax and semantics, echoing the paper of Chellougui presented above.

In the concluding remarks, the author wonders why the students did not progress after the course. She claims that “the lack of progress may be due to an insufficient curricular treatment, or to the cognitive demand of the tasks”. Ttiming to the curricular material supports the former, while the hesitation showed by some mathematicians in their reasoning supports the latter. She finally questions the relevance of inferring instructional recommendations from mathematicians’ practises, her data showing that they might generate inference automatically, preventing proper rationalization. This issue was already raised in Durand-Guerrier et al. (2012) in the section entitled “Contexts that may require understanding logic at a syntactic level”, which concluded:

From an educational perspective these examples [given in the section] suggest that syntactic control is not only particularly important for novices but also necessary for more advanced students facing concepts about which their semantic control is still shaky. [...] In such context, a lessening of rigour, considered by experts as an innocuous shortcut, can results in serious misunderstandings by students, (op. cit. p.383)

Analysing proof and proving process at university: case studies.

In this section, we consider two case studies that were presented during the two INDRUM conferences. Both consider means to analyse the links between logical skills and students’ activity in proof and proving processes.

Designation at the core of the dialectic between experimentation and proving

It is well known in mathematics education that students experience strong difficulties with elaborating mathematical proofs by themselves, even when they are involved in meaningful research and problem-solving activities. There is researchbased evidence that even in settings where the milieu for validation seems rich enough to support the proving process, some students fail to enter it appropriately.

An important aspect for entering a proving process is the designation of objects that, according to Tarski (1933), is one of the main characteristics of a semantic approach. In their paper, Gardes and Durand-Guerrier (2016) acknowledge this crucial role of designation, i.e. the representation of a mathematical object by means of a natural language expression or of a symbol (e.g. “Q” designates “the set of rational numbers”) and provide some empirical results supporting the following hypothesis. Although the designation of objects plays an important role in the heuristic phases, it might not be sufficient to enrol students in elaborating proofs in cases where the properties of these objects and their mutual relationships are not made explicit. The empirical results come from a didactical engineering developed by Gardes (2013), whose main goal was to study the conditions and constraints pertaining to the transposition of professional mathematicians’ research activity in the mathematics classroom. The didactical engineering was elaborated from an unsolved problem in Number Theory, the Erdos-Straus conjecture:

“The equation „ = | can be solved in positive integers x, у and z for

any integer n > 1”.

To analyse her data, Gardes (2013) adapted the concept of gesture from Cavailles (1981) and Chatelet (1993):

A gesture is an action connecting mathematical objects and which is carried out with intentionality. It is an operation that is accomplished through a combination of signs with respect to the usage rules of these signs. Because they open on possibilities, gestures have the power to enhance mathematical creativity.

(translation by Gardes and Durand-Guerrier (2016) of Gardes (2013), p. 155)

Among the seven gestures identified by Gardes (2013), the authors focused on the gesture of "designating an object”, i.e. “representing a mathematical object by means of a natural language expression or a symbol”. The data collected during the research supports the role of this gesture in the reformulation of the conjecture entailing its enrichment: introduction of objects (e.g. prime numbers, congruence), production of intermediate conjectures, formalization of methods, etc. In some cases, there is evidence that this gesture is likely to foster a back-and-forth between semantics and syntax (Gardes 2012). Nevertheless, the a posteriori analysis of the data collected during the experiment showed that in some cases, students were unable to make explicit the relationships between the objects that they introduced, which prevented them from moving beyond the successful production of decompositions by trial and error to a more general method. The authors provide the example of two groups who introduced a variable t corresponding to the successor of the integral part of д-, which allowed them to engage in the proving process, but the syntheses they provided at the end of their research show strong differences. In one group, the students explicitly wrote the relation і = £'(j) + 1, and provided a general decomposition that allowed them to engage successfully in the proving process, to reach an important intermediate result and to identify the cases that needed further study. In the other group, the students did not make this relation between t and n explicit; this prevented them from moving to a general method for decomposition. The comparison between the syntheses of both groups supports the claim that, beyond developing the gesture of designation of objects as a key competence, it is also necessary to develop the capability to identify relationships between the objects that are introduced, this last point requiring interplay between mathematical knowledge and logical skills.

The authors conclude that

[this point] should [be taken] into account when elaborating the milieu of such didactical engineering, aiming at fostering the development of students’ skills for solving mathematical research problems. The way to do this is an open research question.

(Gardes & Durand-Guerrier, 2016, p.292)

Analysing regressive reasoning at university level

Barbero and Gomez-Chacon (2018) focus on the epistemic and cognitive characterization of regressive reasoning in resolving strategic games. The authors explore the use of the Finer Logic of Inquiry' Model, an adaptation of the Logic of Inquiry by Hintikka (1995), as a tool for examining the way in which university students acquire an ability to use regressive reasoning. They investigate in particular how the Finer Logic of Inquiry Model can be a valid tool to analyse the interplay between the cognitive and epistemic aspects of regressive reasoning. They report the results of a study carried out on 32 undergraduate students preparing a mathematics degree at a university in Spain. For the authors, regressive (or backwards) reasoning refers to the analysis part of the “analysis and synthesis reasoning” as elaborated by Polya (1945) and Hintikka and Remes (1974). They proposed three specific modalities of a logical nature for the deductive components: the detached modality, logical control and deductive modality.

Detached modality is the moment in which a conjecture, which has not arisen immediately after an exploration, is formulated. Logical control is the time when an exploration-control is done without using instruments. It is characterized by the use of formal language. Deductive modality characterizes control phases where instruments are involved. Deductive Steps and Logical Chains are added to the Inquiry Component actions. (Barbero & Gomez-Chacon, 2018, pp. 206-207).

The authors notice that, in problem solving activities, inquiry and deductive components are intertwined. They exemplify the use of the Finer Logic Inquiry Model in a case study of a university student solving a strategy game. Triangular Solitaire is a single-player game that requires a board with 15 boxes as the figure shows. These are the rules:

• 1. Place the pegs in all boxes, except in the one marked in black.
• 2. The player can move as many pegs as they like as long as they are able to jump over an adjacent peg and onto an empty space (along the line). At the same time, he "eats'1 the peg that was jumped over and that peg gets taken out of the game. All pegs move in the same way. Pegs can move around the table in any direction. Objective: The player wins when there is only one peg on the table.

FIGURE 7.1 Triangular Solitaire (Barbero & Gomez-Chacon, 2018, p. 208)

This strategic game was chosen because it favours the use of regressive reasoning. The experiment was conducted with 32 students, but in the paper a single case is analysed. The authors use the Finer Logic of Inquiry Model to analyse the written work of an individual student. They claim that this student is representative of the group because she was among the 60% of those who used regressive reasoning. In addition, this student introduced a lot of graphical representations to support her resolution process. In the paper, the entire protocol has been translated from Spanish. After a familiarization phase, the student entered an exploration phase and carried out her strategy. The protocol shows consistent use of regressive (backward) reasoning. At the end of the exploratory phase, the student started from a position she conjectured to be successful and progressively filled the triangle in order to get to the initial position. She finally reversed the list of drawings starting from the initial position to the final one.

The authors conclude that analysis using the Finer Logic of Inquiry Model allows to model student’s cognitive movement during the problem-solving activity. On the cognitive side, they point out that strategic aspects are more dominant in the ascending and descending modalities, while epistemic ones are prevailing in the neutral modality'5. They also point out that regressive reasoning involves auxiliary intuition elements that are necessary to achieve the solution, and that abductive reasoning should have been used during the resolution process, but that the protocol does not allow confirming it. (Barbero & Gomez-Chacon, 2018, p. 212).

Conclusion of the second part

The four studies briefly presented in this section support the relevance of considering logical issues in mathematics education. The first and second examples shed light on the logical complexity of concepts’ definitions and of proving processes at university level, while the third and fourth ones aim at better understanding the links between logical skills and students’ activity in proof and proving. We will elaborate in the last part of the chapter on the logic needs for mathematics and computer science instruction.

Logic needs for mathematics and computer science

In this section, we aim to clarify the role that logic may play in the learning and teaching of mathematics and computer science, taking into consideration different aspects of various proving activities and their dependence on the topics at stake. There are strong parallels between logic, computer science and mathematics. In particular, both computer science and mathematics involve the study and use of formalism, proof and deduction systems, and provide ways of giving them meaning; therefore, the dialectic between syntax and semantics plays an essential role in their teaching and learning (Weber & Alcock, 2004; Durand-Guerrier & Dawkins, 2018; Durand-Guerrier et al., 2019). The content of this section relies mainly on the discussion on logical issues which took place in the working group “Number, Algebra, Logic” at INDRUM 2018.

Logical issues in mathematics instruction

We mentioned earlier in the text the perceived lack of logical skill of young university students. As teachers ourselves, we can attest to the considerable difficulties students face in dealing with the logical issues that arise when they attempt to learn about the process of reasoning and proving, especially when confronted with a higher requirement for accurate formalism.

As claimed by Durand-Guerrier and Dawkins (2018), it is not easy to determine what kind of work with students will help them overcome these difficulties. Looking at professional mathematicians’ assumptions on the role of logic in mathematical activity shows a diversity of points of view (Mathieu-Soucy, 2016; Durand-Guerrier et al., 2012). However, considering university students’ mathematical activity, things are likely to be different. Indeed, as pointed out by Durand-Guerrier and Arsac (2005), and evidenced in Brown (2018), there are differences between expert mathematicians and novices, the former using semantic controls informed by their knowledge and practices, which is not the case with the latter. In this respect, it seems worthwhile to investigate the knowledge and skills undergraduates need in formal logic in order to solve the mathematical tasks given to them. Mathieu-Soucy (2016) reports on research aiming to address the following question: how does knowledge of formal logic, or a course in formal logic, change the way undergraduate mathematics students produce and validate proofs? She asked eight university students from Quebec, Canada in the second half of a 3-year mathematics program (20-21 years old) with various levels of knowledge in formal logic to produce and validate proofs through a non-routine task. In this paper, the author focuses on an adaptation of the first three of Hilbert’s incidence axioms in a non-mathematical context (dogs, robots, friendship relationships). The empirical results suggest that a course in logic changes the way students do mathematical work, in particular by developing alertness. However, the author notices that this alertness is not enough to allow students to proceed towards complete mathematical proof, in particular in cases where the mathematical notions at stake are not well mastered. This is consistent with the claim by Durand-Guerrier and Arsac (2005) that in the proof and proving process, logical and mathematical issues are closely intertwined.

The exploratory and constructive phases of reasoning require frequent practice and a mastery of objects, properties and relationships, and the ability to draw upon relevant conjectures, definitions and theorems. Such practice necessitates an intensive use of inference rules, which may occur subconsciously, but requires controls in order to be developed into an actual proof. Working explicitly on the logical aspects of mathematical reasoning may help students not only reason about logic but also learn to coordinate logical tools with their reasoning about particular mathematical topics (Durand-Guerrier & Dawkins, 2018).

In mathematics, natural deduction provides opportunities for using inference rules from the logic of propositions and from predicate calculus, such as deduction by cut-off, deduction by simplification, modus ponens, modus tollens, disjunction of cases, the contradiction rule, the converse rule and so forth. When one reasons with conditional statements that are not equivalences, only two valid inference rules are available (namely modus ponens and modus tollens). These rules form the very core of the Copi natural deduction. Using Copi’s (1954) rules, and based on the work carried out in didactics of mathematics (Chellougui, 2016; Durand-Guerrier & Arsac, 2005), four additional inference rules from predicate logic were identified, which also have crucial importance in logic and mathematic proofs. The presentation below is adapted from Durand-Guerrier et al. (2012, p.374)

• 1. Given that a result is known to be tine for all objects of a certain kind, universal instantiation allows us to conclude that the result is true for any particular object of that kind. This rule is used constantly in the manipulation of algebraic expressions and in providing justifications for most steps in a proof.
• 2. When an object of a certain type is known to exist, existential instantiation allows one to give it a name. Learning how to use this rule correctly is a significant challenge for most students (Durand-Guerrier & Arsac, 2005).
• 3. When one knows or hypothesizes that a particular object of a certain type satisfies a property, then one can assert the statement “there exists an object of that type satisfying this property”. This rule is named “existential generalization”. One uses it, at least implicitly, when asserting the negation of a universal statement “for all x, P(x)” by providing an example of “not P(x)”.
• 4. If one can show that a certain property holds true for a particular but arbitrarily chosen object of a certain type, universal generalization allows us to conclude that the property holds true for all objects of that type. This rule is the basis for almost all mathematical proofs.

We consider that having some level of understanding of the fundamental rules of predicate logic would help students check logical deductions and mathematicalstatements that are in doubt, to avoid invalid deductions, and to comprehend the basic structures of both proof and disproof by counterexample. Drawing on their research and teaching experience, Epp (2003), Durand-Guerrier and Arsac (2005) and Durand-Guerrier et al. (2012) support the claim that teaching students the basic principles of predicate logic (e.g. Copi, 1954) might provide them with a relevant tool for successful mathematical activity.

Logic and proof in computer science

It is today widely acknowledged that some logic and reasoning skills are required in computer science. There are many examples of situations where logic-inspired objects, tools and notions are used in the various areas of computer science: Boolean expressions in a computer program; logical gates in computer architecture; bit-wise operators and arithmetic modulo 2, etc. Here, elementary propositional logic plays a large role, if only as an inspiration.

Other examples relate to classical first-order (or predicate) logic. The way variable introduction and scope work in many programming languages is similar to the way variables in first-order logic are introduced (or captured) using quantifiers, and their scope delimited using parentheses. Programming languages such as Prolog use logical rules consisting of one or several premises and a conclusion, which may be used to deduce new knowledge.

Finally, one may draw several parallels between programming and proving in a more or less formalized manner. For instance, it is common in mathematics to decompose a large demonstration into lemmas, in order to clarify the text or to better control the level of detail. Similarly, a programmer decomposes a large program into various sub-procedures, functions or modules.

In Durand-Guerrier et al. (2019) the authors list some further examples of situations where computer science draws from mathematics in general, and from logic in particular. We briefly summarize some of these examples, from the most theoretical to the most applied.

Computation models and their links to logic

For almost a century, mathematicians and logicians have been investigating ways to formalize the notion of computability. This can be seen through Hilbert’s 1928 Entscheidungsproblem asking about the existence of an algorithm to determine the universal validity of a first-order logic statement, and the negative answer independently brought by computer science pioneers Church and Turing in 1936. This type of questions led to the famous Church-Turing thesis, which essentially defines a class of equivalent formalisms corresponding to the intuitive notion of computability (see for instance Hopcroft, Motwani and Ullman (2007), Section 8.2.1 for a brief summary). This result and the work surrounding it are now widely considered as one of the cornerstones of theoretical computer science. Over the years, more restricted classes of computation models were also defined and studied, for instance that of finite automata, taught in most computer science curricula. In the 1960s, a deep connection between finite automata and a fragment of second-order logic was discovered by Biichi, effectively opening a new avenue of research (see for instance Straubing and Weil (2012) for an introduction).

Reasoning about problems, algorithms and programs

As outlined in Part 1, reasoning about programs or algorithms draws upon an assortment of proof techniques and mathematical concepts, including notions attributed to discrete mathematics. In this respect, some knowledge of formal logic is useful. The notion of worst-case complexity is a relevant illustration of this claim: to accurately present it to students needs great care, proficiency with several objects and concepts, and a non-trivial use of quantification. It is however an important notion which is a part of almost every computer science syllabus.

Formal rules to describe the semantics and prove the correctness of programs

Beyond short proofs performed by hand about simple programs, it is sometimes necessary to leverage the power of formalism in order to accurately express the meaning of programs, and to prove some of their properties. University textbooks on the formal semantics of programming languages, for instance Winskel (1993), present several mathematical formalisms able to express the meaning of each syntactical construct in a programming language. One such formalism, called operational semantics, is presented in the form of rules in which atoms are statements about the effect of a piece of program. Evaluating the overall meaning of a program then comes up to writing down a valid proof using this set of rules and a deduction system similar to natural deduction in classical logic. Another deduction system called Hoare rules or Hoare logic, provides a tool to prove the partial correctness of imperative programs. Again, it uses deduction to prove assertions about programs, which are essentially written using classical logic and arithmetic predicates.

Through these three examples, which are representative of the discussions held at the last INDRUM meeting, we have tried to make it apparent that the evolution and growth of computer science is tightly related to its pioneers’ mathematical culture and proficiency, in this case with a strong emphasis on logic. The ideas these examples convey are general and permeate algorithmic thinking, and are still present in most university computer science curricula today. One may therefore postulate that appropriate training in logic is a requirement for any student in computer science. It is our opinion that further research in this direction is called for.

Conclusion of the third part

Knowledge of the principles of logical reasoning becomes most important when familiarity with the mathematical and computer science subject matter does not suffce by itself to ascertain truth or falsity in a given situation. In addition, following Wilkerson-Jerde and Wilensky (2011) and Modeste (2016), we hypothesize that understanding the role of logic in the activities of expert mathematicians and computer scientists would help in designing relevant activities for improving university students’ logical abilities.

Finally, including instruction in logical principles as one part of mathematics and computer science education provides a balance between two extreme positions: that checking the validity of a proof requires that it be completely formalized; and that success in proving requires no explicit knowledge of logical principles (Durand-Guerrier et al., 2012).

Conclusion

In this chapter, we have addressed some of the challenges raised by the teaching and learning of discrete mathematics, computer science, logic, proof and proving, taking in consideration their relationships. Although the research questions evoked in this chapter have already been addressed in the literature, the point of view adopted here, leaning on the papers and discussions from the two INDRUM conferences, open new avenues for research focusing on the relationships between these domains.

In the first part of the chapter, we have highlighted the potential of the teaching and learning of discrete mathematics as a didactical means to make visible the relationships between mathematics and computer science. In the second part, we emphasized the necessity to take into account the logical complexity of the mathematical topics studied at university, and to consider the logical issues underlying mathematics and computer science instruction. There is research evidence of the potentiality of discrete mathematics for developing proof and proving skills, linked to logical issues, and hypotheses regarding a similar role for computer science. Finally, the third part of this text has put forward hypotheses concerning the specific characteristics of formal logic as a teaching topic, in the context of mathematics or computer science curricula, and with a particular emphasis on proof and proving. One may for instance question the expected or possible benefits of training students in formalism and logic on their ability to leam mathematics or computer science. Alternatively, one may try to identify the specific uses of logic in both disciplines as they are taught at undergraduate or graduate levels.

A next step would be to design interdisciplinary didactical engineering aiming to help university students get a deeper understanding of the conceptual relationships between discrete mathematics, computer science, logic and proof. For this purpose, leading further inquiries regarding the dialectic between syntax and semantics seems promising.

Notes

• 1 Here “proof refers to both the process of proving and the product.
• 2 For a presentation in English, see Artigue (1994); for specificities in University mathematics, see Gonzalez-Martin, Bloch, Durand-Guerrier & Maschietto (2014).
• 3 The notion of zero-definition was introduced by Lakatos (1961). According to Ouvrier-Buffet (2006, p.266) zero-definitions can assume a denominative function, and are used for practical purposes at the beginning of the research process before the proper mathematical terms are defined.
• 4 An AE alternative corresponds to the form: “for all x, there exists y, P(x,y)” (Dubinsky & Yiparaki, 2000)
• 5 This refers to Soldano (2017) who characterized the cognitive dimension of reasoning through the sequence of actions in three different modalities: ascending, neutral and descending.(Barbgero & Gomez-Chacon, 2018, 206).

References

Abdallah, E. (2018). Contemporary Research Practices in Discrete Mathematics - A way to enrich the understanding of Discrete Mathematics at University Level. INDRUM 2018 Proceedings, pp. 194—203.

Alcock, L. (2009). Teaching proof to undergraduates: semantic and syntactic approaches. Proceedings of the ICMI 19 conference: Proof and Proving in Mathematics Education 1 (pp. 29-34). Taipei: The Department of Mathematics, National Taiwan Normal University.

Antonini, S., & Mariotti, M. A. (2008). Indirect Proof: What is specific to this way of proving? ZDM: The International Journal on Mathematics Education, 40, 401-412.

Artigue, M. (1994). Didactic engineering as a framework for the conception of teaching products. In R. Bidder, R. W. Scholz, R. StriiBer, & B. Winkelmann (Eds.), Didactics of mathematics as a scientific discipline (pp. 27—39). Dordrecht: Kluwer Academic.

Barbero, M., & Gômez-Chacôn, I. M. (2018). Analysing regressive reasoning at university level. INDRUM 2018 Proceedings, pp. 204—213.

Brown, S. (2018). A Study of Students’ Reasoning About “There exists no ...”. INDRUM 2018 Proceedings, pp. 214—223.

Cavaillès, J. (1981). Méthode axiomatique et Formalisme. Paris: Hermann.

Châtelet, G. (1993). Les enjeux du mobile. Mathématique, physique, philosophie. Paris: Editions du Seuil.

Chellougui, F (2016). Approfondissement du questionnement didactique autour du concept de "borne supérieure”. INDRUM 2016 Proceedings, pp. 266-275.

Copi, I. (1954). Symbolic logic (2nd edition, 1965). New York: Macmillan.

Dubinsky, E. 8c Yiparaki, O. (2000). On student understanding of AE and EA quantification, Research in Collegiate Mathematics Education IT, CBMS Issues in Mathematics Education, 8, pp. 239—289. Providence: American Mathematical Society.

Durand-Guerrier, V., & Arsac, G. (2005). An epistemological and didactic study of a specific calculus reasoning rule, Educational Studies in Mathematics, 60(2), 149—172.

Durand-Guerrier, V., Boero, P., Douek, N.. Epp, S. S., 8c Tanguay, D. (2012). Examining the Role of Logic in Teaching Proof. In G. Hanna & M. de Villiers (Eds.), ICMI Study 19 Book: Proof and Proving in Mathematics Education (pp. 369—389). New York: Springer.

Durand-Guerrier, V., & Dawkins, P. C. (2018). Logic in University Mathematics Education. In

S. Lerman (Ed.) Encyclopedia of Mathematics Education (2nd edition). New York: Springer.

Durand-Guerrier, V., Meyer, A., & Modeste, S. (2019). Didactical issues at the interface of mathematics and computer science. In G. Hanna 8c M. de Villiers (Eds.) Proof Technology in Mathematics Research and Teaching (pp. 115-138). New York: Springer.

Durand-Guerrier, V., & Tanguay, D. (2018). Working on proof as contribution to conceptualisation — The case of R-completeness. In A. J. Stylianides & G. Hard (Eds.) Advances in Mathematics Education Research on Proof and Proving. An international perspective. ICME-13 Monographs, (pp. 19—34). New York: Springer.

Epp, S. S. (2003). The role of logic in teaching proof. American Mathematical Monthly 110(10), 886-899.

Epp, S. S. (2016). Discrete mathematics for computer science. Proceedings of the 13th International Congress on Mathematical Education. Hamburg.

Gardes, M.-L. (2012). Intérêts et limites des méthodes algébriques dans un problème de recherche en théorie des nombres. Actes du 36ènte séminaire SFIDA. Nice2011. https:// sites.google.com/site/actessfida/.

Gardes, M.-L. (2013). Etude de processus de recherche de chercheurs, élèves et étudiants, engagés dans la recherche d’un problème non résolu en théorie des nombres. Doctoral Dissertation, Université Lyon 1 (France).

Gardes, M.-L., & Durand-Guerrier, V. (2016). Designation at the core of the dialectic between experimentation and proving: a study in number theory. INDRUM 2016 Proceedings, pp. 286—295.

Gonzalez-Martin, A. S., Bloch, 1., Durand-Guerrier, V., & Maschictto, M. (2014). Didactic Situations and Didactical Engineering in university mathematics: cases from the study of Calculus and proof. Research in Mathematics Education, 16(2), 117—134.

Grenier, D., & Payan, C. (1998). Spécificités de la preuve et de la modélisation en mathématiques discrètes. Recherches en Didactique des Mathématiques, 18(1), 59-100.

Hintikka, J. (1995). The Games of Logic and the Games of Inquiry. Dialectica, 49, 229—249.

Hintikka, J., & Kernes, U. (1974). The Method of Analysis: Its Geometrical Origin and Its General Significance. Dordrecht: Reidel.

Hopcroft, J., Motwani, R., Ullman, J. (2007). Introduction to Automata Theory, Languages, and Computation (3rd edition). Boston: Addison-Wesley.

Knuth, D. E. (1974). Computer Science and its Relation to Mathematics. The American Mathematical Monthly, 81(4), 323—343.

Lakatos, I. (1961). Essays in the Logic of Mathematical Discovery, Cambridge: Cambridge University Press.

Lockwood, E. (2013). A model of students’ combinatorial thinking. Journal of Mathematical Behavior, 32, 251—265.

Lockwood, E., & Reed, Z. (2018). Leveraging Specific Contexts and Outcomes to Generalize in Combinatorial Settings. INDRUM 2018 Proceedings, pp. 244—254.

Longo, G. (2005). The Cognitive Foundations of Mathematics: human gestures in proofs and mathematical incompleteness of formalisms. In M. Okada et al. (Eds.) Images and Reasoning. Tokyo: Keio University Press.

Mason, J., & Pimm, D. (1984). Generic examples: seeing the general in the particular. Educational Studies in Mathematics, 15(3), 277—289.

Mathieu-Soucy, S (2016). Should university students know about formal logic: an example of nonroutine problem. INDRUM 2016 Proceedings, pp. 316—325.

Modeste, S. (2012). Enseigner l’algorithme pour quoi? Quelles nouvelles questions pour les mathématiques? Quels apports pour l’apprentissage de la preuve? Doctoral dissertation, Université de Grenoble (France).

Modeste, S. (2016). Impact of informatics on mathematics and its teaching. On the importance of epistemological analysis to feed didactical research. In F. Gadducci, M. Tavosanis (Eds.) History and Philosophy of Computing, IFIP Advances in Information and Communication Technology, New York: Springer.

Ouvrier-Buffet, C. (2006). Exploring mathematical definition construction processes. Educational Studies in Mathematics, 63(3), 259—282.

Ouvrier-Buffet, C„ Meyer, A., & Modeste S. (2018). Discrete mathematics at university level. Interfacing mathematics, computer science and arithmetic. INDRUM 2018 Proceedings, pp. 255-264.

Polya, G. (1945). How to solve if?Princeton: Princeton University Press.

Selden, A., & Selden, J. (1995). Unpacking the logic of mathematical statements. Educational Studies in Mathematics, 29, 123—151.

Soldano, C. (2017). Learning with the logic of inquiry. A game-approach within DGE to improve geometric thinking. PhD Dissertation. Universita di Torino.

Straubing, H., Weil, P. (2012). An introduction to finite automata and their connection to logic, in D. D’Souza (Ed.). Modern applications of automata theory, IISc Research Monographs (pp. 3-43). Singapore: World Scientific

Tarski, A. (1933). The concept of truth in the language of deductive sciences. (English translation 1983)

Weber, K., & Alcock, L. (2004). Semantic and syntactic proof productions. Educational Studies in Mathematics, 56(2—3), 209—234.

Wilkerson-Jerde, M. H., & Wilensky, U. J. (2011). How do mathematicians learn math? Resources and acts for constructing and understanding mathematics. Educational Studies in Mathematics, 78, 21—43.

Winskel, G. (1993). The formal semantics of programming languages: an introduction. Cambridge MA: MIT Press.