Intuitionism and computing with partial information
Lead Research Organisation:
University of Leeds
Department Name: Pure Mathematics
Abstract
In mathematics, we try to determine which mathematical statements---which precise statements about numbers, continuous functions, vector spaces, and the like---are true and which are false. To determine that a statement is true, you must provide an argument explaining why the statement is true, and to determine that a statement is false, you must provide an argument explaining why the statement is false. Mathematical arguments can be very difficult to produce. Some even take years! So imagine your disappointment when another mathematician takes issue with the latest argument you spent such incredible effort perfecting. Perhaps she found a mistake in your reasoning. Or perhaps she disagrees with one of your basic premises.
Mathematics became more and more abstract over the course of the 1800s, and by the early 1900s, after more than a few controversies, disagreements, and paradoxes, mathematicians realized that we needed to formally fix the rules of our game. The idea was to agree on a collection of basic axioms and on a collection of reasoning rules (such as if 'A' and 'A implies B' are both true, then 'B' must also be true) so that the truth or falsity of any mathematical statement could be determined by starting from the axioms and reasoning according to the rules. Thus the axioms should be intuitively true, and deductions made by applying the reasoning rules to true premises should yield true conclusions.
Fixing intuitively true axioms and reasoning rules that preserve truth certainly seems like the natural and obvious way to give mathematics a solid foundation. However, to L. E. J. Brouwer, this classical foundation based on truth and falsity was far too permissive. Brouwer's complaint was, essentially, that mathematical objects (like continuous functions, vector spaces, and so on) do not necessarily correspond to anything in reality and that there is no objective, absolute notion of mathematical truth. Instead, a mathematical object is the result of some mental construction that is somehow justifiable by the mathematician's intuition. The reasoning rules for mathematics should therefore be designed to preserve these justifications instead of mere truth. Brouwer's position came to be called 'intuitionism.'
The famous mathematician Andrey Kolmogorov had many interests, including intuitionism, and he proposed an informal interpretation of intuitionism as a 'logic of problem solving' and a 'calculus of problems.' Yuri Medvedev, in the 1950s, was the first to formalize Kolmogorov's computational interpretation. Medvedev's idea was to say that a mathematical problem P (appropriately formalized) reduces to another mathematical problem Q if there is a uniform computational procedure that translates solutions to problem Q into solutions to problem P. Using this idea, Medvedev showed how to interpret atomic logical propositions---the 'A,' 'B,' and 'C' in an expression like 'A implies (B or C)'---as mathematical problems. Classically, we think of 'A,' 'B,' and 'C' as each being either true or false and the expression 'A implies (B or C)' as meaning that if 'A' is true, then either 'B' or 'C' must also be true. Under Medvedev's formalization, we instead think of 'A,' 'B,' and 'C' as mathematical problems and of 'A implies (B or C)' as meaning that if problem 'A' is solvable, then either problem 'B' or problem 'C' must also be solvable. In this project, we study a similar computational interpretation of intuitionism introduced by Elena Dyment. The key difference is that Dyment's interpretation is based on computing with partial information, whereas Medvedev's interpretation is based on computing with complete information. We seek to characterize the logic that arises from Dyment's interpretation and determine whether or not it differs from the logic that arises from Medvedev's interpretation.
Mathematics became more and more abstract over the course of the 1800s, and by the early 1900s, after more than a few controversies, disagreements, and paradoxes, mathematicians realized that we needed to formally fix the rules of our game. The idea was to agree on a collection of basic axioms and on a collection of reasoning rules (such as if 'A' and 'A implies B' are both true, then 'B' must also be true) so that the truth or falsity of any mathematical statement could be determined by starting from the axioms and reasoning according to the rules. Thus the axioms should be intuitively true, and deductions made by applying the reasoning rules to true premises should yield true conclusions.
Fixing intuitively true axioms and reasoning rules that preserve truth certainly seems like the natural and obvious way to give mathematics a solid foundation. However, to L. E. J. Brouwer, this classical foundation based on truth and falsity was far too permissive. Brouwer's complaint was, essentially, that mathematical objects (like continuous functions, vector spaces, and so on) do not necessarily correspond to anything in reality and that there is no objective, absolute notion of mathematical truth. Instead, a mathematical object is the result of some mental construction that is somehow justifiable by the mathematician's intuition. The reasoning rules for mathematics should therefore be designed to preserve these justifications instead of mere truth. Brouwer's position came to be called 'intuitionism.'
The famous mathematician Andrey Kolmogorov had many interests, including intuitionism, and he proposed an informal interpretation of intuitionism as a 'logic of problem solving' and a 'calculus of problems.' Yuri Medvedev, in the 1950s, was the first to formalize Kolmogorov's computational interpretation. Medvedev's idea was to say that a mathematical problem P (appropriately formalized) reduces to another mathematical problem Q if there is a uniform computational procedure that translates solutions to problem Q into solutions to problem P. Using this idea, Medvedev showed how to interpret atomic logical propositions---the 'A,' 'B,' and 'C' in an expression like 'A implies (B or C)'---as mathematical problems. Classically, we think of 'A,' 'B,' and 'C' as each being either true or false and the expression 'A implies (B or C)' as meaning that if 'A' is true, then either 'B' or 'C' must also be true. Under Medvedev's formalization, we instead think of 'A,' 'B,' and 'C' as mathematical problems and of 'A implies (B or C)' as meaning that if problem 'A' is solvable, then either problem 'B' or problem 'C' must also be solvable. In this project, we study a similar computational interpretation of intuitionism introduced by Elena Dyment. The key difference is that Dyment's interpretation is based on computing with partial information, whereas Medvedev's interpretation is based on computing with complete information. We seek to characterize the logic that arises from Dyment's interpretation and determine whether or not it differs from the logic that arises from Medvedev's interpretation.
Planned Impact
The proposed project is short-term and sharply focused on achieving a very specific mathematical goal. Nevertheless, we expect that the international nature of the project will eventually yield modest yet lasting economic and societal benefits.
A successful collaboration between the United Kingdom and Italy will strengthen the research connection between the two countries. The success of the this project will lead to many future international collaborations and will eventually attract top postgraduate and postdoctoral researchers in mathematical logic and computability theory to the UK. This benefits the UK, not only because attracting the best researchers helps produce the best research output, training, and education, but also because most people who begin as academic researchers in computability theory make their careers in critical fields such as teaching, software engineering, finance, security, and defense.
Furthermore, we expect this project to have interdisciplinary impact. The project concerns computational interpretations of intuitionism, and intuitionism is a well-studied topic in the philosophy of mathematics. Thus we will work to connect with researchers in the philosophy of mathematics and in philosophical logic.
A successful collaboration between the United Kingdom and Italy will strengthen the research connection between the two countries. The success of the this project will lead to many future international collaborations and will eventually attract top postgraduate and postdoctoral researchers in mathematical logic and computability theory to the UK. This benefits the UK, not only because attracting the best researchers helps produce the best research output, training, and education, but also because most people who begin as academic researchers in computability theory make their careers in critical fields such as teaching, software engineering, finance, security, and defense.
Furthermore, we expect this project to have interdisciplinary impact. The project concerns computational interpretations of intuitionism, and intuitionism is a well-studied topic in the philosophy of mathematics. Thus we will work to connect with researchers in the philosophy of mathematics and in philosophical logic.
People |
ORCID iD |
| Paul Shafer (Principal Investigator) |
Publications
Shafer P
(2018)
Comparing the degrees of enumerability and the closed Medvedev degrees
in Archive for Mathematical Logic
| Description | The purpose of the research funded on this grant is to study a family of mathematical structures, the so-called Medvedev, Muchnik, and Dyment degrees, particularly as computational interpretations of intuitionistic logic, which is, very roughly speaking, a sort of logic based on justification rather than on truth. There are two groups of key findings. The first group of key findings concerns computational interpretations of intuitionistic logic. It is known that in the context of computation from complete information (meaning that computations are given all information about their inputs), the Medvedev and Muchnik degrees can be used to give computational interpretations of intuitionistic logic. The new findings are in the context of computation from *partial* information, where computations are only given partial information about their inputs. Here, the Dyment degrees form the relevant structure. In fact, their are two versions of the Dyment degrees: uniform and non-uniform. The findings show that the non-uniform version of the Dyment degrees give a computational interpretation of intuitionistic logic in the context of partial information in much the same way that the Muchnik degrees give a computational interpretation of intuitionistic logic in the context of complete information. Research into the uniform Dyment degrees is ongoing. The second group of key findings concerns technical questions about the distribution of the enumeration degrees within the Medvedev degrees. The enumeration degrees are the partial-information version of the classic Turing degrees. Both the Turing degrees and the enumeration degrees sit inside the larger Medvedev degrees, but the Turing degrees are even definable in the Medvedev degrees, which is a particularly nice way of sitting inside. Whether or not the enumeration degrees are definable in the Medvedev degrees is a longstanding open question that motivates the work done here. In an attempt to make some sense of the distribution of the enumeration degrees within the Medvedev degrees, the enumeration degrees are compared to the Medvedev degrees of closed sets. The findings are that, overall, the enumeration degrees seem to be distributed rather erratically even with respect to the degrees closed sets. However, it is found that an enumeration degree corresponds to the Medvedev degree of a closed set if and only if the enumeration degree is what is called 'co-total', which is an unexpected discovery. |
| Exploitation Route | The findings of this project address research questions in pure mathematics and thus will be taken forward by other pure mathematicians. It is envisioned, however, that the findings will bridge mathematical communities and stir new collaborations between, for example, researchers interested in computability theory and researchers interested in constructivism and intuitionism. |
| Sectors | Education |
| URL | https://link.springer.com/article/10.1007/s00153-018-0648-x |
| Description | University of Siena |
| Organisation | University of Siena |
| Department | Department of Information Engineering and Mathematics |
| Country | Italy |
| Sector | Academic/University |
| PI Contribution | Expertise |
| Collaborator Contribution | Expertise Office space IT |
| Impact | Paul Shafer and Andrea Sorbi. Comparing the degrees of enumerability and the closed Medvedev degrees. Archive for Mathematical Logic 58 (2019). |
| Start Year | 2017 |