Intuitionism and computing with partial information

在数学中，我们试图确定哪些数学陈述-关于数字、连续函数、向量空间等的精确陈述-是真的，哪些是假的。要确定语句为真，必须提供解释语句为真的理由的参数；要确定语句为假的，必须提供解释语句为假的理由的参数。数学论证可能很难产生。有些甚至要花好几年时间！所以，想象一下，当另一位数学家对你花费了如此惊人的努力完善的最新论点提出异议时，你会有多么失望。也许她在你的推理中发现了错误。也许她不同意你的一个基本前提。在19世纪的过程中，数学变得越来越抽象，到20世纪初，在经历了许多争论、分歧和悖论之后，数学家们意识到我们需要正式地确定我们的游戏规则。这个想法是同意一个基本公理的集合和一个推理规则的集合(例如，如果‘A’和‘A暗示B’都是真的，那么‘B’也必须是真的)，这样任何数学陈述的真假都可以通过从公理出发并根据规则进行推理来确定。因此，公理应该是直观真实的，通过将推理规则应用于真实前提而进行的演绎应该产生真实的结论。固定直观真实的公理和保留真理的推理规则显然是给数学奠定坚实基础的自然和显而易见的方式。然而，对于L·E·J·布劳威尔来说，这种建立在真伪基础上的经典基础太过宽容了。从本质上讲，布劳威尔的抱怨是，数学对象(如连续函数、向量空间等)不一定对应于现实中的任何东西，并且没有关于数学真理的客观、绝对的概念。相反，数学对象是某种心理结构的结果，这种心理结构以某种方式被数学家的直觉所证明是合理的。因此，数学的推理规则应该被设计成保存这些理由，而不仅仅是真理。布劳威尔的观点后来被称为“直觉主义”。著名数学家安德烈·科尔莫戈罗夫有很多兴趣，包括直觉主义，他提出了一种非正式的解释，将直觉主义解释为“解决问题的逻辑”和“问题演算”。20世纪50年代，尤里·梅德韦杰夫第一个将科尔莫戈罗夫的计算解释正式化。梅德韦杰夫的想法是说，如果有一个统一的计算程序将问题Q的解决方案转化为问题P的解决方案，那么一个数学问题P(适当地形式化)就会简化为另一个数学问题Q。梅德韦杰夫用这个想法展示了如何将原子逻辑命题-类似于A暗示(B或C)的表达式中的A、B和C--解释为数学问题。传统上，我们认为‘A’、‘B’和‘C’都是真或假，而短语‘A暗示(B或C)’的意思是，如果‘A’为真，那么‘B’或‘C’也必须为真。在梅德韦杰夫的形式化理论下，我们把‘A’、‘B’和‘C’看作是数学问题，把‘A暗示(B或C)’看作是指，如果问题‘A’是可解的，那么问题‘B’或问题‘C’也一定是可解的。在这个项目中，我们研究了Elena Dyment引入的对直觉主义的类似的计算解释。关键的区别在于，戴蒙的解释是基于部分信息的计算，而梅德韦杰夫的解释是基于完全信息的计算。我们试图刻画戴蒙特解释产生的逻辑的特征，并确定它是否与梅德韦杰夫解释产生的逻辑不同。

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.