Intuitionism and computing with partial information

在数学中，我们试图确定哪些数学陈述——关于数字、连续函数、向量空间等的精确陈述——是真的，哪些是假的。要确定一个陈述是真的，你必须提供一个论证来解释为什么这个陈述是真的，而要确定一个陈述是假的，你必须提供一个论证来解释为什么这个陈述是假的。数学论证是很难提出的。有些甚至需要数年！所以，想象一下，当另一位数学家对你花了如此难以置信的努力完善的最新论点提出异议时，你的失望。也许她在你的推理中发现了错误。或者她不同意你的一个基本前提。数学在19世纪变得越来越抽象，到20世纪初，在经历了多次争论、分歧和悖论之后，数学家们意识到我们需要正式地修正我们的游戏规则。这个想法是在一组基本公理和一组推理规则上达成一致（例如，如果“ a ”和“ a暗示B ”都为真，那么“ B ”也必须为真），这样，任何数学陈述的真假都可以通过从公理和根据规则进行推理来确定。因此，公理在直观上应该是真的，而将推理规则应用于真前提的演绎应该产生真结论。固定直觉上正确的公理和推理规则，以保持真理，这似乎是给数学奠定坚实基础的自然而明显的方式。然而，对于L. E. J.布劳威尔来说，这种基于真伪的古典基础过于宽容了。布劳威尔的抱怨本质上是，数学对象（如连续函数、向量空间等）并不一定对应于现实中的任何东西，也不存在客观的、绝对的数学真理概念。相反，数学对象是某种心理建构的结果，这种建构在某种程度上可以被数学家的直觉所证明。因此，数学推理规则的设计应该保留这些证明，而不仅仅是真理。布劳威尔的立场后来被称为“直觉主义”。著名数学家安德烈·柯尔莫哥洛夫（Andrey Kolmogorov）有很多兴趣，包括直觉主义，他对直觉主义提出了一种非正式的解释，即“解决问题的逻辑”和“问题的微积分”。尤里•梅德韦杰夫（Yuri Medvedev）在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对直觉主义的类似计算解释。关键的区别在于Dyment的解释是基于部分信息的计算，而Medvedev的解释是基于完全信息的计算。我们试图描述戴蒙的解释所产生的逻辑，并确定它是否与梅德韦杰夫的解释所产生的逻辑不同。

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.