Cognitive Reductionism about Proofs
This is a quick comment on the issue about Mochizuki's claimed proof of the abc conjecture that Catarina wrote about a couple of days ago. (I don't know much about this number theory stuff.)
Are proofs cognitive entities? Is every proof cognized? Known? Knowable?
Maybe related to this is the following result, a consequence of Church's Theorem (on the undecidability of predicate logic), which is an indication of how complicated proofs can be even of theorems of predicate logic:
This means that proofs of valid theorems of logic can get larger and larger with no recursively specifiable bound. Consequently, there is no reason whatsoever to suppose that every proof can be cognized, or recognized, by some finite agent.
George Boolos (1987, "A Curious Inference") has given a very nice example of a first-order theorem $\phi_{Bool}$ of logic whose shortest proof in first-order predicate logic is astronomically vast. The underlying idea is that the formula "encodes" the Ackermann function $A$, and a predicate logic proof requires a step-by-step computation of length about equal to the value of this function ($A(4,4)$, if I recall right). He notes, however, that $\phi_{Bool}$ has a short proof in second-order predicate logic. (This is an example of "speed-up".) I wrote a short paper about this issue in Analysis several years ago (2005, "Some More Curious Inferences").
Are proofs cognitive entities? Is every proof cognized? Known? Knowable?
Cognitive Reductionism about ProofsThis claim is analogous to certain verificationist claims more generally (e.g., every truth is knowable). I believe that this claim is mistaken, or, at least, not justified. For all I know, Mochizuki has found a proof, but unfortunately, it is simply not cognized yet, by anyone else. This is a bit annoying, of course. So far as I, or anyone else can tell, he has not done anything mathematically wrong. If something is "wrong" here, it belongs to social epistemology.
Every proof P of a mathematical claim is cognizable by some one (or more) agent.
Maybe related to this is the following result, a consequence of Church's Theorem (on the undecidability of predicate logic), which is an indication of how complicated proofs can be even of theorems of predicate logic:
Let $L$ be a first-order language with a binary predicate $R$. Let $|\phi|$ be the number of symbols in $\phi$. There is no recursive function $f : \mathbb{N} \to \mathbb{N}$ such that, for all $\phi \in L$, where $|\phi| = n$, then if $P$ is a proof of $\phi$ in predicate logic, then $\phi$ has a proof $P^{\ast}$ such that $|P^{\ast}| \leq f(n)$.[Proof: Suppose that there is such a function $f$. Let $M_f$ be a TM that computes $f$. Now suppose we are given a formula $\phi \in L$. We have the query:
$\vdash \phi$?Compute $n = |\phi|$ and compute $f(n)$ using $M_f$. Predicate logic proofs can be recursively enumerated in increasing size. Run through the predicate logic proofs in such an enumeration. If a proof $P$ of $\phi$ is reached with $|P| \leq f(n)$, then we have that $\vdash \phi$. If a proof of $\phi$ is NOT reached at this point, then we can conclude, by the defining property of $f$, that $\nvdash \phi$. This is a decision procedure for logical validity in $L$, contradicting Church's Theorem.]
This means that proofs of valid theorems of logic can get larger and larger with no recursively specifiable bound. Consequently, there is no reason whatsoever to suppose that every proof can be cognized, or recognized, by some finite agent.
George Boolos (1987, "A Curious Inference") has given a very nice example of a first-order theorem $\phi_{Bool}$ of logic whose shortest proof in first-order predicate logic is astronomically vast. The underlying idea is that the formula "encodes" the Ackermann function $A$, and a predicate logic proof requires a step-by-step computation of length about equal to the value of this function ($A(4,4)$, if I recall right). He notes, however, that $\phi_{Bool}$ has a short proof in second-order predicate logic. (This is an example of "speed-up".) I wrote a short paper about this issue in Analysis several years ago (2005, "Some More Curious Inferences").
The claim is not so much that Mochizuki's purported proof is not yet a proof because no one has checked the details yet. Suppose someone wrote a crystal-clear proof, but just as she is done some natural disaster happens, and the proof gets buried under collapsed buildings. I'm still prepared to call it a proof because it would satisfy a counterfactual condition: *were* it to be surveyed by a competent opponent, it would fulfill its explanatory, persuasive function. But that's not what happens to M's proof currently: the point is that the way he set it up (for now) makes it unintelligible to anyone but himself.
ReplyDeleteThe point of infinitary proofs is a different one, and it's a point I was discussing with Lavinia Piccolo last week in Munich. I haven't made up my mind on that one yet :)
And yes, proofs most certainly are cognitive entities! Just as there is no such thing as a language independent from the speakers who instantiate it -- so again, our good old fundamental disagreement :)
ReplyDeleteHi Catarina,
ReplyDeleteThanks - yes, I was trying to get to the heart of what the debate was about, and I think it's got to do with what you say in the second comment.
On my view, languages needn't be cognitively accessed, and proofs might be much like that too.
Cheers,
Jeff
Jeffrey,
ReplyDeleteThat is an interesting point, but I wonder whether the connection between the length of proofs in predicate logic and the purported) proof of the ABC-conjecture is very tight.
It seems that for this connection to be tight we have to assume that any mathematical proof (i.e. a proof that is accepted by mathematicians) is a proof in first-order predicate logic. One could argue that there could be mathematical theorems whose proofs go beyond standard predicate logic. But even if we assume that every mathematical theorem can be proved within first order logic, it does not follow that any valid proof is a first-order proof. In particular, although the length of first-order proofs of mathematical theorems is recursively unbounded, it does not follow that proofs of these results in other systems are likewise unbounded (the example of the Ackermann-function being a case in point). Since for something to be a mathematical theorem it suffices that there is a valid proof (not necessarily rendered in predicate logic), it certainly does not follow that the theorem implies that there are mathematical theorems all of whose proofs are to long/complicated to be cognized.
Karim,
ReplyDeleteMany thanks - yes, I agree with these points.
Still, if there are certain cognitive bounds of finite agents (which seems reasonable), then, given that proofs can be of any finite length, and there's no guarantee of short proofs, then there isn't a reason for making the assumption (a strong one) that every proof (even informal ones) can be cognized/accessed.
Whether these considerations can yield a stronger conclusion, that there are proofs that cannot be cognized, is more complicated to address. I'm not sure about that.
Jeff
Jeffrey,
DeleteThanks for your reply.
I tend to agree with Catarina, that proofs in mathematics have to be cognized and have to be accepted by a community of mathematicians as being valid. However, I understand that this seems to reduce mathematics to a mind-dependent and socially constructed body of statements. But this has not to be the case.
What if we accept that mathematical truths are mind-independent, i.e. the fact that Fermat's Last Theorem or the ABC-conjecture is true, is independent of the fact that somebody knows that these mathematical statements are true. Proofs are the method by which mathematicians convince themselves and their peers about the truth of a mathematical statement. They are ways to convince one's opponent, as Catarina would say, about the truth value of a statement. Whether a given argument counts as a proof of a mathematical statement depends on how it is received by the relevant community. Therefore, whether there exists a proof of a theorem is not a mind-independent fact (or a fact that is independent of social facts). (This perhaps needs qualifying: it might be a mind-independent fact whether there exists a proof of a mathematical statement in a given axiomatic system - say in Peano Arithmetic. But I think we should not be misled by this fact, since the existence of a proof does not imply the existence of a proof in Peano Arithmetic or any other fixed formal system).
Proofs on this account are part of the technology that mathematicians use to discover true mathematical statements. And just like an object is a hammer if it is recognized and used as a hammer, an argument is a proof if its recognized as a proof. In particular, on this view, then, proofs have to be cognized but mathematical truths do not.
Perhaps this is wide of the mark?
Karim
Karim,
DeleteMany thanks - yes the hammer example is a nice example. Rather than say that any particular hammer is socially constructed, we might better say that the property of being a hammer, i.e., a functional property, is mind-dependent in some way (hard to make precise). In particular, something is hammer in virtue of how it is used. So, is the property of "being a proof of $\phi$" similar? Here, there is the important distinction between proofs in the epistemological sense and proofs in a formal system (i.e., a finite sequence $(\phi_0, \dots, \phi_n)$ satisfying certain conditions). We're here concerned with the former sense.
A proof in the epistemological sense is some sort of structure, or syntactical entity, that "generates justification for belief". But then the questions are: belief by which agent? Just one? Must they be human? Are angels allowed? If more than one, must they be well-credited experts.
In practice, the degree of conceptual and syntactical complexity of ordinary mathematical proofs is low enough for most accredited experts to check them (with some notable exceptions, of course!). So, in this case, "agreement amongst accredited experts" might count as the criterion whereby an alleged proof becomes a genuine proof. So, the explication is something like this:
Syntactical object $P$ is a genuine proof of result $\phi$ iff there is agreement amongst relevant accredited experts that $P$ proves $\phi$.
(On this explication, Cognitive Reductionism follows: if P is a proof of $\phi$, then someone cognizes this proof.)
But this bothers me ... Mochizuki seems to have developed a whole new world of notions and results, and even if we agree that a community of accredited experts is needed for a genuine proof, the community here might in fact just be the unit set {Mochizuki}.
So, here a lot depends on the definition of "community". I agree that one can, more or less by ostension, define "mathematical community" by, say, listing faculty members of maths depts. But as soon as one gets into specialized subdisciplines, one gets smaller and smaller subcommunities. Maybe in this case, the subcommunity has only one element.
However, in the end, I just reject Cognitive Reductionism for proofs. If he proved it, he proved it, and no one else knows. I can live with that, even though it's a bit annoying for the broader mathematical community to be in this uncertain epistemic state.
Jeff
Jeff,
DeleteAgain thanks for your comments. There is indeed a problem of how to define the relevant community. You argue that the relevant community might be a singleton. I think I disagree with that. The reason I'm unhappy with that is the following. There are quite a few people who claim for example that Cantor's proof of the uncountability of the reals is wrong and go on to offer an argument purporting to show that the reals are in fact countable. Now, arguably they have a convinced themselves that the statement "the reals are countable" is true and hence they consider themselves to have a proof of that statement However, we do not accept these arguments as proofs. You could say that we don't accept these arguments because they are wrong. But, arguably, saying that these arguments are wrong is saying that they do not convince their opponents. And saying that these arguments do not convince the relevant community is saying that they do not obey the norms accepted by the community. This, I think, indicates that an argument that convinces just one person can not be a proof.
Now, the problem remains how to define the relevant community. I would define the relevant community as those who have an interest in knowing whether a given mathematical statement is true or not. Hence the relevant community for the ABC-conjecture is not just the singleton {Mochizuki} but consists (at least) of the community of number theorists. If the members of that community get convinced that the argument indeed shows the ABC-conjecture to be true, then Mochizuki's argument deserves the honorific title "proof".
There is, perhaps, an objection to this proposal. Namely the fact that the status of an argument/structure changes from being merely an argument that convinces the person who devised it to that argument being a proof, without any changes in the argument/structure. This might seem counterintuitive. But note that in most cases that time interval between someone presenting his or her argument and it being accepted is very short. So most arguments get the honorific title "proof" pretty quickly. In these cases, the events "X has an argument by which he is convinced of the truth of a mathematical statement" and "X's argument is accepted by the community as a valid proof" are pretty much simultaneous and hence we just say that "X has a proof" to describe the first event (although strictly speaking that is only a description of the second event). In rare cases, as with the ABC-conjecture, that time interval is substantially longer and we are bothered by the fact that an the status of an argument can change without there being any change in the argument itself. But I guess on this point we have diverging opinions. I'm happy to accept this fact, especially since accepting this fact (the social nature of proofs) does not imply that we have accept that the truth of a mathematical statement depends on it being accepted as true by the community.
Karim
Karim,
DeleteThanks
"However, we do not accept these arguments as proofs."
I think the big issue here is "we"! There's a relevant community $C$, and $C$ doesn't accept these arguments.
"... But, arguably, saying that these arguments are wrong is saying that they do not convince their opponents. And saying that these arguments do not convince the relevant community is saying that they do not obey the norms accepted by the community. This, I think, indicates that an argument that convinces just one person can not be a proof."
But still, can't the relevant community be a singleton? In this case, by virtue of his prior achievements and peer status, Mochizuki is not a crank of some sort, and belongs to all supersets of any relevant community for this particular result.
"If the members of that community get convinced that the argument indeed shows the ABC-conjecture to be true, then Mochizuki's argument deserves the honorific title "proof"."
But it seems to me that there's still no reason yet to insist on the full community even of number theorists. For as a result become more and more conceptually, or combinatorially, sophisticated, the community shrinks. Others, even within peer communities, accept results on the basis of reliable testimony and peer review. In this case, it may have shrunken to a singleton!
Maybe I can put what I think by saying that proof is not quite the right concept here for what is at stake. The relevant concept seems to be "appropriately accredited proof". Mochizuki has presented a syntactical entity $P$ (well, several). And $P$ may, or may not, be a proof of the abc conjecture. On the other hand, I agree that $E$ is not "appropriately accredited" in some sense. So, in short, I'm still not at all convinced by the cognitive reductionist conditional:
(CRP) If $P$ is a proof of a mathematical claim $\phi$, then $P$ is appropriately accredited as a proof of $\phi$.
So, I'm happy to say:
(i) Mochizuki's syntactic entity $P$ is not appropriately accredited.
(ii) We simply don't know if it's a proof or not (for all we know, it may be).
On the other hand, by accepting (CRP), and the premise (i), one is compelled to conclude that it isn't a proof! I can remain neutral, and see what happens ...
Jeff
Catarina,
ReplyDelete"Just as there is no such thing as a language independent from the speakers who instantiate it"
Right, this is cognitive reductionism: all languages are cognized by some speaker(s).
Whereas my view is cognitive anti-reductionism: there are languages (e.g., infinitary, permuted, weird tokens, etc.) not cognized by anyone.
Jeff
I take it that in interpreting this kind of argument, we have to be careful about the order of the quantifiers.
ReplyDeleteYou seem to establish: For every finite agent x, there exists a result y, the shortest proof of which is beyond x's grasp.
But not: There exists a result y, such that for every finite agent x, the shortest proof of y is beyond x's grasp.
That is, when you are faced with a very big proof, you can always go and find a suitably large agent. That may not be physically possible in our universe, of course, on account of constraints like the Bekenstein bound. But again, we could always go and find a universe that was big enough for the large agent that we needed, so long as we started with the result and its proof, and then went and found the tools to do the job.
Now I have had another cup of coffee, it occurs to me that there is something else very important in what you say about the lack of a recursive function. We may go out looking for large agents, but we cannot work out in advance, how large an agent we would need. So we might waste a lot of time using enormous agents, who were still not big enough.
DeleteAs a separate point, I suppose we would need to have some ground to trust the huge agent who eventually said "Yes, that's a proof". As we could not keep up with that agent's thought processes, and we would not have designed those processes (unlike the processes that we design into theorem-proving computers), it is not obvious what that ground would be.
Thanks, Richard.
DeleteI guess, in a sense, Mochizuki is a "large agent", that has sprouted off from the mathematical community, travelling off in his own direction for years. So, he says "P"; but we, who have not travelled with him, don't know if this assertion is trustworthy.
We know, for independent reasons, that he is reliable on a great many other intersubjectively checkable claims, and is an accredited expert. However, that seems not to be enough here ...
Jeff
I pretty much agree with everything that Karim said. A frequent objection to the idea that proofs are cognitive entities is indeed that this would lead us straight into mathematical relativism of some sort. However, one must distinguish between this claim and the claim that mathematical *truths* are mind-dependent. And while some social constructivists seem to endorse this claim, it certainly doesn't follow from the functionalist idea that proofs have a cognitive and social function: that of convincing peers and explaining why something is the case.
ReplyDeleteAs for proofs in a given formal system: it is most certainly a mathematical objective fact whether a derivation is or is not correct according to the rules of the system. But this is, in my opinion, a derivative notion of proof. The primitive one is the one arising from the practices of mathematicians, which is not system-relative. In fact, this is related to what van Benthem calls 'system imprisonment', which I talked about here:
http://m-phi.blogspot.nl/2011/09/van-benthem-on-system-imprisonment.html
Hi Catarina,
ReplyDeleteAs I see it, the central problem with epistemically relativizing "$\phi$ is true", as "$\phi$ is true relative to agent A" (i.e., "A accepts, or would accept under ideal circumstances, $\phi$") is that "$\phi$ is true relative to A" isn't a truth predicate: it doesn't commute with connectives & quantifiers, and so on, unless the agent A is extremely special. So, to make this work, one has to inflate the epistemic powers of A massively. For example, the agent's epistemic states must be closed under the $\omega$-rule. So, A has to be transcendental in her epistemic powers. Roughly, relativism about truth implies the existence of epistemically transcendental agents.
Relativism about proofs doesn't quite face the same problem, but a similar one. It's epistemically elitist in requiring that the relevant individual or community be very special or epistemically privileged (e.g, certain success and closure conditions must be satisfied). So, the idea is that:
A syntactic entity $P$ is a proof of $\phi$ only if there is a special elite community $C$ such that $P$ convinces them of $\phi$.
So, if $P$ doesn't convince them, then $P$ isn't a "proof" in the required sense. I.e., it's "wrong". That is, in this case, Mochizuki's syntactic entity doesn't convince anyone else in the relevant community $C$, and therefore it's "wrong". The whole difficulty, I think, is now located in specifying the epistemically elite community $C$, and why its members are "special". Why isn't the community simply $\{Mochizuki\}$?
Intersubjectivity usually is understood as involving modal accessibility of epistemic states, rather than actuality: the syntactic object could be checked by epistemic peers. Often this isn't too hard. But, in this case, it may well be intersubjectively ok; it's just that no one has sufficient time and energy to do it. That is, the proof may be fine (for all we know); it's just not feasible for anyone else, at least at the moment.
Cheers,
Jeff