Recent literature on the role of pictorial representation in the life sciences has focused on the relationship between detailed representations of empirical data and more abstract, formal representations of theory. The standard argument is that in both a historical and epistemic sense, this relationship is a directional one: beginning with raw, unmediated images and moving towards diagrams that are more interpreted and more theoretically rich. Using the neural network diagrams of Warren McCulloch and Walter Pitts as a case study, I (...) argue that while in the empirical sciences, pictorial representation tends to move from data to theory, in areas of the life sciences that are predominantly theoretical, when abstraction occurs at the outset, the relationship between detail and abstraction in pictorial representations can be of a different character. (shrink)

Las máquinas aceleradas de Turing (ATMs) son dispositivos capaces de ejecutar súper-tareas. Sin embargo, el simple ejercicio de definirlas ha generado varias paradojas. En el presente artículo se definirán las nociones de súper-tarea y ATM de manera exhaustiva y se aclarará qué debe entenderse en un contexto lógico-formal cuando se pregunta por la existencia de un objeto. A partir de la distinción entre posibilidades lógicas y físicas se disolverán las paradojas y se concluirá que las ATMs son posibles y existen (...) como objetos abstractos. (shrink)

In spite of their practical importance, the connections between technology and mathematics have not received much scholarly attention. This article begins by outlining how the technology–mathematics relationship has developed, from the use of simple aide-mémoires for counting and arithmetic, via the use of mathematics in weaving, building and other trades, and the introduction of calculus to solve technological problems, to the modern use of computers to solve both technological and mathematical problems. Three important philosophical issues emerge from this historical résumé: (...) how mathematical knowledge depends on technology, the definition of the hybrid concept of a computation, and the usefulness of mathematics in technology. Each of these issues is briefly discussed, and it is shown that in order to analyze them, we need to combine tools and ideas from both the philosophy of technology and the philosophy of mathematics. In conclusion, it is argued that much more of interest can be found in the historically and philosophically unexplored terrains of the technology–mathematics relationship. (shrink)

This paper reviews Benjamin Noys’ recent attempt in Malign Velocities: Accelerationism and Capitalism to mount a critique of accelerationism. The book, persuasive in certain respects, bypasses the institutional dynamics of accelerationism’s theoretical progenitors, viz. Nick Land and the Cybernetic Culture Research Unit of Warwick University, and instead portrays it as a “defeatist strategy” of the post-’68 conjuncture of “Deleuzian Thatcherism.” Such portrayal is debatable to the extent that it exhibits a questionable appropriation of “theory” in the strict sense of the (...) term; a term the paper attempts to define with reference to Matthew Arnold, Louis Althusser and Gilles Grelet. (shrink)

Computer simulations and experiments share many important features. One way of explaining the similarities is to say that computer simulations just are experiments. This claim is quite popular in the literature. The aim of this paper is to argue against the claim and to develop an alternative explanation of why computer simulations resemble experiments. To this purpose, experiment is characterized in terms of an intervention on a system and of the observation of the reaction. Thus, if computer simulations are experiments, (...) either the computer hardware or the target system must be intervened on and observed. I argue against the first option using the non-observation argument, among others. The second option is excluded by e.g. the over-control argument, which stresses epistemological differences between experiments and simulations. To account for the similarities between experiments and computer simulations, I propose to say that computer simulations can model possible experiments and do in fact often do so. (shrink)

A version of the Church-Turing Thesis states that every effectively realizable physical system can be simulated by Turing Machines (‘Thesis P’). In this formulation the Thesis appears to be an empirical hypothesis, subject to physical falsification. We review the main approaches to computation beyond Turing definability (‘hypercomputation’): supertask, non-well-founded, analog, quantum, and retrocausal computation. The conclusions are that these models reduce to supertasks, i.e. infinite computation, and that even supertasks are no solution for recursive incomputability. This yields that the realization (...) of hypercomputing devices is implausible, and that Thesis P is not essentially different from the standard Church-Turing Thesis. (shrink)

We examine the verification of simple quantifiers in natural language from a computational model perspective. We refer to previous neuropsychological investigations of the same problem and suggest extending their experimental setting. Moreover, we give some direct empirical evidence linking computational complexity predictions with cognitive reality.<br>In the empirical study we compare time needed for understanding different types of quantifiers. We show that the computational distinction between quantifiers recognized by finite-automata and push-down automata is psychologically relevant. Our research improves upon hypothesis and (...) explanatory power of recent neuroimaging studies as well as provides<br>evidence. (shrink)

The existence of non-standard numbers in first-order arithmetics is a semantic obstacle for modelling our arithmetical skills. This article argues that so far there is no adequate approach to overcome such a semantic obstacle, because we can also find out, and deal with, non-standard elements in Turing machines.

This article presents three extracts from the introductory course in mathematical logic that Gödel gave at the University of Notre Dame in 1939. The lectures include a few digressions, which give insight into Gödel's views on logic prior to his philosophical papers of the 1940s. The first extract is Gödel's first lecture. It gives the flavour of Gödel's leisurely style in this course. It also includes a curious definition of logic and a discussion of implication in logic and natural language. (...) The second extract is a discussion on undecidability and on Leibniz. The third extract concerns the paradoxes and Russell's theory of types. (shrink)

“Rationality” in Simon's “bounded rationality” is the principle that humans make decisions on the basis of step-by-step reasoning using systematic rules of logic to maximize utility. “Bounded rationality” is the observation that the ability of a human brain to handle algorithmic complexity and large quantities of data is limited. Bounded rationality, in other words, treats a decision maker as a machine carrying out computations with limited resources. Under the principle of embodied cognition, a cognitive mind is an interactive machine. Turing-Church (...) computations are not interactive, and interactive machines can accomplish things that no Turing-Church computation can accomplish. Hence, if “rationality” is computation, and “bounded rationality” is computation with limited complexity, then “embodied bounded rationality” is both more limited than computation and more powerful. By embracing interaction, embodied bounded rationality can accomplish things that Turing-Church computation alone cannot. Deep neural networks, which have led to a revolution in artificial intelligence, are both interactive and not fundamentally algorithmic. Hence, their ability to mimic some cognitive capabilities far better than prior algorithmic techniques based on symbol manipulation provides empirical evidence for the principle of embodied bounded rationality. (shrink)

The topic of this article is Hilbert’s axiom of solvability, that is, his conviction of the solvability of every mathematical problem by means of a finite number of operations. The question of solvability is commonly identified with the decision problem. Given this identification, there is not the slightest doubt that Hilbert’s conviction was falsified by Gödel’s proof and by the negative results for the decision problem. On the other hand, Gödel’s theorems do offer a solution, albeit a negative one, in (...) the form of an impossibility proof. In this sense, Hilbert’s optimism may still be justified. Here I argue that Gödel’s theorems opened the door to proof theory and to the remarkably successful development of generalized as well as relativized realizations of Hilbert’s program. Thus, the fall of absolute certainty came hand in hand with the rise of partially secure and reliable foundations of mathematical knowledge. Not all was lost and much was gained. (shrink)

Digital physics claims that the entire universe is, at the very bottom, made out of bits; as a result, all physical processes are intrinsically computational. For that reason, many digital physicists go further and affirm that the universe is indeed a giant computer. The aim of this article is to make explicit the ontological assumptions underlying such a view. Our main concern is to clarify what kind of properties the universe must instantiate in order to perform computations. We analyse the (...) logical form of the two models of computation traditionally adopted in digital physics, namely, cellular automata and Turing machines. These models are computationally equivalent, but we show that they support different ontological commitments about the fundamental properties of the universe. In fact, cellular automata are compatible with a rather traditional form of physicalism, whereas Turing machines support a dualistic ontology, which could be understood as a realism about the laws of nature or, alternatively, as a kind of panpsychism. (shrink)

Problem-solving software that is not-necessarily infallible is central to AI. Such software whose correctness and incorrectness properties are deducible by agents is an issue at the foundations of AI. The Comprehensibility Theorem, which appeared in a journal for specialists in formal mathematical logic, might provide a limitation concerning this issue and might be applicable to any agents, regardless of whether the agents are artificial or natural. The present article, aimed at researchers interested in the foundations of AI, addresses many questions (...) related to that theorem, including differences between it and results of Gödel and Turing that have sometimes played key roles in Minds and Machines articles. This study also suggests that—if one is willing to assume a thesis due to Donald Knuth—the Comprehensibility Theorem is the first mathematical theorem implying the impossibility of any AI agent or natural agent—including a not-necessarily infallible human agent—satisfying a rigorous and deductive interpretation of the self-comprehensibility challenge. Some have pointed out the difficulty of self-comprehensibility, even according to presumably a less rigorous interpretation. This includes Socrates, who considered it to be among the most important of intellectual tasks. Self-comprehensibility in some form might be essential for a kind of self-reflection useful for self-improvement that might enable some agents to increase their success. We use the methods of applied mathematics, rather than philosophy, although some topics considered could be of interest to philosophers. (shrink)

The shift from electromechanical computing to fully electronic, digital, Turing-complete computing was one of the most in?uential technological developments of the twentieth century. The social, economic, political, interdisciplinary, and cultural aspects behind that shift were signi?cant, but are often ignored. When the contingencies and controversies behind the birth of modern computing are forgotten, the history of computing is often misrepresented as one of uncomplicated linear progress. In this article some of the sociocultural aspects of the birth of modern computing are (...) reviewed. The signi?cance of interdisciplinary work is discussed. The concept of the stored-program paradigm is introduced, and some sociocultural factors behind its birth are discussed. Finally, it is argued that some traits of research that are often considered to be negative, such as opportunism, eclecticism, and stubbornness, have played a positive role in the birth of modern computing technology. (shrink)

En este trabajo examino cómo el Funcionalismo de Máquina de Turing resulta compatible con una forma de dualismo, lo que aleja a la IA clásica o fuerte del materialismo que la inspiró originalmente en el siglo XIX. Para sostener esta tesis, argumento que efectivamente existe una notable cercanía entre el pensamiento cartesiano y dicho funcionalismo, ya que el primero afirma que es concebible/posible separar mente y cuerpo, mientras que el segundo sostiene que no es estrictamente necesario que los estados mentales (...) se realicen en las propiedades físicas de engranajes y máquinas reales. This article deals with how Turing Machine Functionalism turns out to be compatible with a form of Dualism, which involves that strong AI is not close to the original Materialism that inspired it in the nineteenth century. To support this thesis, I argue that there is a compelling coincidence between Descartes' philosophy and this version of Functionalism, since the former holds that it is conceivable/possible to separate mind and body, while the latter holds that it is not strictly necessary that mental states are realized by the physical properties of real cogs and machines. (shrink)

In this paper, I try to accomplish two goals. The first is to provide a general characterization of a method of proofs called — in mathematics — the diagonal argument. The second is to establish that analogical thinking plays an important role also in mathematical creativity. Namely, mathematical research make use of analogies regarding general strategies of proof. Some of mathematicians, for example George Polya, argued that deductions is impotent without analogy. What I want to show is that there exists (...) a direct line leading from Cantor’s diagonal argument to constructions that underlies of the proofs of several important theorems of the mathematical logic (in particular, Church’s theorem concerning the undecidability of formal arithmetic, Gödel’s theorem concerning the incopleteness of formal arithmetic, Tarski’s theorem concerning truth, and Turing’s theorem concerning the Halting Problem), and that the line could be described as an analogical mapping. In other words, Cantor’s diagonal argument and the proofs of the limitative theorems are structurally the same. Hence they can be represented as instances (or special cases) of the same general scheme. (shrink)

Philosophers of information, according to Luciano Floridi (The philosophy of information. Oxford University Press, Oxford, 2010, p 32), study how information should be “adequately created, processed, managed, and used.” A small number of epistemologists have employed the concept of information as a cornerstone of their theoretical framework. How this concept can be used to make sense of seemingly intractable epistemological problems, however, has not been widely explored. This paper examines Fred Dretske’s information-based epistemology, in particular his response to radical epistemological (...) skepticism. We discuss the relationship between information, evidence and knowledge in relation to the problem of skepticism and the options available to an information-based epistemology for dealing with it. (shrink)

We discuss a number of topics that are central in Brouwer's intuitionism. A complete treatment is beyond the scope of the paper, the reader may find it a useful introduction to Brouwer's papers.

Résumé La numérisation actuelle du droit permet de revenir sur les liens historiques entre le droit et la logique moderne. En se fondant sur la différence établie par J. Van Heijenoort entre logique «comme calcul» et logique «comme langage», l’article établit des analogies entre différentes interprétations de la logique et différents types de systèmes ou d’instances juridiques : «Common law», systèmes «civils», «cour de cassation», cette dernière notion caractérisant le formalisme hilbertien. Ce formalisme a tenté de réduire la logique «comme (...) langage» à la logique «comme calcul» mais la découverte des limitations internes des formalismes y a mis un terme : d’où le parallèle entre l’échec du programme hilbertien et les difficultés rencontrées dans la numérisation actuelle du droit. Le droit n’est pas réductible à un calcul formel sur des marques écrites : il reste une discipline dans laquelle la parole et le dialogue sont indispensables pour réaliser les buts qu’il s’assigne. (shrink)

In contrast to dominant approaches to human reason involving essentially a logical and instrumental conception of rationality easily modeled by artificial intelligence mechanisms, I argue that the specific capacities of the human mind are meta-analytic in nature, understood as irreducible to the analytic or the logical, or else the computational. Firstly, the assumption of a meta-analytical level of rationality is derived from key insights developed in various branches of the social sciences. This meta-analytical level is then inferred from Gödel’s incompleteness (...) theorem. On these bases, and with the help of psychological approaches to consciousness, I argue that human rationality may be characterized as the capacity to make meaningful use of signs. (shrink)

The Turing Machine presents itself as the very landmark and initial design of digital automata present in all modern general-purpose digital computers and whose design on computable numbers implies deeply ontological as well as epistemological foundations for today’s computers. These lines of work attempt to briefly analyze the fundamental epistemological problem that rose in the late 19th and early 20th century whereby “machine cognition” emerges. The epistemological roots addressed in the TM and notably in its “Halting Problem” uncovers the tension (...) between determinism and uncertainty, regarded here as the primal and inherent features of machine cognition. Resumen La Máquina de Turing se presenta como el hito y el diseño inicial de un autómata digital presente en todas las computadoras digitales modernas de propósito general y cuyo diseño en números computables establece bases profundamente ontológicas y epistemológicas para las computadoras de hoy. Estas líneas de trabajo intentan analizar brevemente el problema epistemológico fundamental que surgió a finales del siglo XIX y principios del XX mediante el cual emerge la “cognición de la máquina”. Las raíces epistemológicas que se abordan en la TM y, en particular, en su “Problema de detención” ponen al descubierto la tensión entre el determinismo y la incertidumbre, consideradas aquí, como las características primordiales e inherentes de la cognición de la máquina. (shrink)

From the initial analysis of John Morris in 1976 about if computers can lie, I have presented my own treatment of the problem using what can be called a computational lying procedure. One that uses two Turing Machines. From there, I have argued that such a procedure cannot be implemented in a Turing Machine alone. A fundamental difficulty arises, concerning the computational representation of the self-knowledge a machine should have about the fact that it is lying. Contrary to Morris’ claim, (...) I have thus suggested that computers – as far as they are Turing Machines – cannot lie. Consequently, I have claimed that moral agency attribution to a robot or any other automated AI system, cannot be made, strictly grounded on imitating behaviors. Self-awareness as an ontological grounding for moral attribution must be evoked. This can pose a recognition problem from our part, should the sentient system be the only agent capable of acknowledging its own sentience. (shrink)

The history of laboratories may become controversial in social sciences. In this paper, the story of Sciences Po Médialab told by Venturini et al. is discussed and completed by demonstrating the incoherence in the choice of digital methods at the Médialab from the actor network theory perspective. As the Médialab mostly used web topologies as structural analysis of social positions, they were not able to account for the propagation of ideas, considered in actor network theory as non-humans that have their (...) own agency. The main arguments in favour of the ‘more continuous social’ developed at the Médialab proved to be as misleading as the network metaphor. The distribution of agency that actor network theory so successfully expands was paradoxicallty reduced to structures and individual preferences, to the detriment of the agency of replications that circulate entities in the form of messages, content or memes, and that should now become the next step for actor network theory-style digital methods. (shrink)

If we take "experimental philosophy" in a wider sense, it is almost the same as methodological naturalism in philosophy. Experiments of this kind would be available and also fruitful in the philosophy of mathematics. They surely will have a substantial contribution to epistemology of mathematics. At present, however, the phrase "experimental philosophy" is used in a much narrower sense. It refers exclusively to a branch of naturalized philosophy that uses the data gathered through questionnaire surveys to investigate the intuitions of (...) ordinary people. We claim that experimental philosophy in this narrower sense will have little relevance to the philosophy of mathematics, since the philosophy of mathematics is not engaged in conceptual analysis despite of its appearance. (shrink)

This paper represents such an amateur approach; hence any comments backed up by professional erudition will be highly appreciated. Let me start from an attempt to sketch a relationship between professionals’ and amateurs’ contributions. The latter may be compared with the letters to the Editor of a journal, written by perceptive readers, while professionals contribute to the very content of the journal in question. Owing to such letters, the Editor and his professional staff can become more aware of the responses (...) of educated public to the journal’s output. (shrink)

Whole brain emulation aims to re-implement functions of a mind in another computational substrate with the precision needed to predict the natural development of active states in as much as the influence of random processes allows. Furthermore, brain emulation does not present a possible model of a function, but rather presents the actual implementation of that function, based on the details of the circuitry of a specific brain. We introduce a notation for the representations of mind state, mind transition functions (...) and transition update functions, for which elements and their relations must be quantified in accordance with measurements in the biological substrate. To discover the limits of significance in terms of the temporal and spatial resolution of measurements, we point out the importance of brain region and task specific constraints, as well as the importance of in-vivo measurements. We summarize further problems that need to be addressed. (shrink)

The reductionist/holist debate seems an impoverished one, with many participants appearing to adopt a position first and constructing rationalisations second. Here I propose an intermediate position of pragmatic holism, that irrespective of whether all natural systems are theoretically reducible, for many systems it is completely impractical to attempt such a reduction, also that regardless if whether irreducible `wholes' exist, it is vain to try and prove this in absolute terms. This position thus illuminates the debate along new pragmatic lines, and (...) refocusses attention on the underlying heuristics of learning about the natural world. (shrink)

A logic is said to admit an equational completeness theorem when it can be interpreted into the equational consequence relative to some class of algebras. We characterize logics admitting an equational completeness theorem that are either locally tabular or have some tautology. In particular, it is shown that a protoalgebraic logic admits an equational completeness theorem precisely when it has two distinct logically equivalent formulas. While the problem of determining whether a logic admits an equational completeness theorem is shown to (...) be decidable both for logics presented by a finite set of finite matrices and for locally tabular logics presented by a finite Hilbert calculus, it becomes undecidable for arbitrary logics presented by finite Hilbert calculi. (shrink)

The development of the social sciences needs to rely on precise methods. The nomological model of explanation adopted in the natural sciences is ill-suited for the social sciences. An algorithmic model of society can be a promising solution to existing problems. In its most general form, an algorithm is a generally understood prescription for what actions to perform and in what order to achieve the desired result. Any algorithm can be represented as a set of rules of the form «If (...) A, do D to get P». People are the bearers of this kind of rules that apply in different areas of their activities. The rules are subject to change based on personal and collective experience. There is a special mathematical discipline that studies the laws of evolution of such rules. This discipline is called genetic programming. Contrary to the threatening name, the algorithmic model does not imply the deprivation of a person’s right to free choice, but it needs this right as a necessary condition for the evolution of social algorithms. These algorithms allow us to give a non-causal, but law-like explanation of many well-known social phenomena, as well as to effectively model the future, which is critically important today. A retrospective look at the evolution of social algorithms shows that the current global crisis of human society is associated with the approach to the point of singularity in their evolution. This is due to the fact that there is no need for direct human participation in the implementation of social algorithms, which is reflected in a fundamental change in the sphere of employment and less need for further development of the sciences. (shrink)

In recent decades, there has been a proliferation among the scientific community of works that focus on Alan Turing’s contributions to the design and development of the modern computer. However, there are significant discrepancies among these studies, to such a point that some of them cast serious doubts on Alan Turing’s work with respect to today’s computer, and there are others that staunchly defend his leading role, as well as other studies that set out more well-balanced opinions. Faced with this (...) situation, the aim of this paper is to analyse the evidence existing today in order to be able to draw a conclusion about whether or not Turing anticipated the trivialisation of the modern computer memory and, likewise, if his universal a-machine is the precursor of the general-purpose computer so omnipresent today. As a result of our research, the authors conclude that Turing did indeed play a leading role in the appearance of the modern computer, although he was not the only one or the first in the field of Computing Science, albeit he was the most influential, both in scope and in depth. (shrink)

The automation of many repetitive or dangerous human activities yields numerous advantages. In order to automate a physical task that requires a finite series of sequential steps, the translation of those steps in terms of a computational procedure is often required. Even apparently menial tasks like following a cooking recipe may involve complex operations that can’t be perfectly described in formal terms. Recently, several studies have explored the possibility to model cooking recipes as a computational procedure based on a set (...) of instructions. This vision is the foundation for the construction of robotics kitchen, as Moley. These kitchen robots have shown promising results. Moley, for instance, is the very first example of a new generation of bioinspired robotics, based on the reproduction of particular movement, cooking, through artificial arms and hands. It is entirely different from the current appliances present in our domestic domain because Moley is able to manipulate ingredients and interact with kitchen equipment in order to prepare a dish autonomously. Nonetheless, they have also shown several limitations. In particular, Moley is an entirely autonomous robot in a structured environment in which it knows precisely the object position and manipulates the ingredients based on a list of instructions and a training phase made by Machine Learning. In this contribution we contend that these limitations arise from an essential mismatch between computational procedures, as originally described by Turing in his seminal 1936 paper, and recipes. Computational procedures have been originally created to observe and modify formal symbols with formal operators. Thus, they are independent from time and they are ideally executed in a closed environment, in which the computer directly produces all the relevant changes required to produce the intended result. Recipes, instead, are followed in an open environment, in which, while time goes by, changes happen independently from the cook’s intervention: the cook puts the butter on the pan, starts the fire and then waits until the butter is melted. To operate effectively in the open environment a kitchen robot must couple computational procedures with sensors, e.g a sensor which provides a time signal. These sensors are de facto oracles for the procedures and yet are required to bridge the gap from the formal to the physical world. (shrink)

Which function is computed by a Turing machine will depend on how the symbols it manipulates are interpreted. Further, by invoking bizarre systems of notation it is easy to define Turing machines that compute textbook examples of uncomputable functions, such as the solution to the decision problem for first-order logic. Thus, the distinction between computable and uncomputable functions depends on the system of notation used. This raises the question: which systems of notation are the relevant ones for determining whether a (...) function is computable? These are the acceptable notations. I argue for a use criterion of acceptability: the acceptable notations for a domain of objects D\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal {D}}$$\end{document} are the notations that we can use for the usual D\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal {D}}$$\end{document}-activities. Acceptable notations for natural numbers are ones that we can count with. Acceptable notations for logical formulas are the ones that we can use in inference and logical analysis. And so on. This criterion makes computability a relative notion—whether a function is computable depends on which notations are acceptable, which is relative to our interests and abilities. I argue that this is not a problem, however, since there is independent reason for taking the extension of computable function to be relative to contingent facts. Similarly, the fact that the use criterion makes a mathematical distinction depend on practical concerns is also not a problem because it dovetails with similar phenomena in other areas of computability theory, namely the roles of notation in computation over real numbers and of Extended Church’s Thesis in complexity theory. (shrink)

This paper explores the functional role of noise in synthetic biology and its relation to the concept of randomness. Ongoing developments in the field of synthetic biology are pursuing the re-organisation and control of biological components to make functional devices. This paper addresses the distinction between noise and randomness in reference to the functional relationships that each may play in the evolution of living and/or synthetic systems. The differentiation between noise and randomness in its constructive role, that is, between noise (...) as a perturbation in routine behaviours and noise as a source of variability that cells may exploit, indicates the need for a clarification and rectification of the conflicting uses of the notion of noise in the studies of the so-called noise biology. (shrink)

Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame (...) is a definitional extension of Zermelo–Fraenkel set theory and has a hierarchically organized structure of concepts and operations, and (3) the construction of formal proofs is deeply connected to the frame through rules for definitions and lemmas. To bring these general ideas to life, we examine, as a case study, proofs of the Cantor–Bernstein Theorem that do not appeal to the principle of choice. A thorough analysis of the multitude of “different” informal proofs seems to reduce them to exactly one. The natural formalization confirms that there is one proof, but that it comes in two variants due to Dedekind and Zermelo, respectively. In this way it enhances the conceptual understanding of the represented informal proofs. The formal, computational work is carried out with the proof search system AProS that serves as a proof assistant and implements the above inference mechanism; it can be fully inspected at (see link below). (shrink)