What examples do we have of mathematicians who explicitly and publicly expressed their personal confidence that mainstream modern logic, as used in mathematics, either as object of study in itself or simply as a tool, was an appropriate representation of the sense of logic most of us have without having to study formal logic?
15
-
2It is not easy to define what our natural "sense of logic" must be ...– Mauro ALLEGRANZAMay 13, 2018 at 9:58
-
Formal logic started with Aristotle and since then has been characterized as the "scientific" way to represent/codify how reason is "implemented" into human language and discourse.– Mauro ALLEGRANZAMay 13, 2018 at 10:00
-
2@Conifold - I don't often disagree with you but this comment seems very wrong. We all have an inbuilt sense of logic or we wouldn't get through the day, and this would be true for stone-age man, horses and sheep. . .– user20253May 15, 2018 at 11:38
-
1@Conifold - You yourself talk of the "intuition of implication" and of "natural reasoning" in the very piece you just linked in your comment! You seem to have contradicted yourself twice, at least according to my own sense of logic and my arithmetic expertise.– SpeakpigeonMay 15, 2018 at 11:53
-
1The "inbuilt sense" is not supported by modern cognitive psychology, not even more basic "sense" that Chomsky termed "universal grammar". I am not even sure what your basis for assuming it is, it is a sense because we call it "sense" is circular. As for intuitions, logical or linguistic, they are culturally accumulated and developmentally acquired, the time when Kant and others thought them a priori is long gone.– ConifoldMay 16, 2018 at 19:37
|
Show 10 more comments
2 Answers
Nobody is going to claim that things like 'Ex Falso Quodlibet' or the Zermelo-Frankel constructions represent natural human logic. They are formal dodges that avoid confusing aspects of naive logic on purpose.
One important example: The idea that you cannot have a set of all sets is not reasonable to most humans, naively. It has to be motivated by a need to evade paradoxes, and they eventually accept it, but it clearly contradicts a very natural impulse.
We go so far as to have different set-theories (e.g. Zermelo-Frankel and Godel-Bernays-von-Neumann) that do or do not allow for a universal set, because not having one seems too counter-intuitive to some mathematicians. In the latter, you can have sets that include all the sets, but you still can't have a set of all sets, because Russel's paradox still can't be permitted.
So the already artificial notion of 'too big a collection to be contained', the closest intuition we can usually impart for why there should not be such a set, actually fails to capture what is going on. There is a real gap here between the formalized solution and our vocabulary that humans don't actually seem to be able to accommodate fully.
But in the end, the purpose of formalization is to improve the system in some way. If it captured all the confusing parts and all the potential paradoxes, it would not actually achieve anything.
-
It does not seem that difficult to come up with a concept of set that is immune to Russell's paradox. What may be problematic is using such a concept in the context of the usual mathematical formalism. My guess is that the current situation merely results from the contingencies of historical convenience. Same thing with formal logic. Jan 14, 2019 at 15:16
-
1@Speakpigeon We certainly have a system that is immune to Russell's paradox, and that is easy to use. The point is that it is not a model of intuition, it is not intuitive itself, and the way of identifying exceptions is not any more intuitive, either (because the intuition itself is not ultimately logical -- human beings are flawed). That is what the question actually asked.– user9166Jan 14, 2019 at 15:19
-
Sorry, I should have been more explicit. I meant a concept of set reflecting our ordinary intuitive notion and immune to Russell's paradox. Humans are flawed, but their brain is the end result of several hundred million years of natural selection of neurobiological systems evolved over an enormous biomass. On the face of it, evolution is a much better guarantor than a few mathematicians spread over two millennia in terms of producing good logic. Formal logic is still very young. So, I don't see any good reason to think there's likely nothing better than current logic and current set theory. Jan 14, 2019 at 16:10
-
1@Speakpigeon No. Our intuition has a contradiction built into it. And another intuition of ours rejects contradiction. You cannot axiomatize naive set theory. Period. You can relax our natural intuition about contradiction, the way Intuitionism does, as it just seems wise to be less arrogant. But that is not the same thing as solving the problem, which really is impossible. If there is a future solution facilitated by evolution it will have to come because inborn human intuition itself has moved forward. We cannot model what we have now.– user9166Jan 14, 2019 at 16:27
-
And so we disagree. You cannot axiomatise naive set theory as it has been initially formalised. You haven't articulated any good reason to think we can't do better. Jan 14, 2019 at 16:39
Automated theorem provers, such as Otter, or Prover9 usually use a subset of first-order logic. There have existed open mathematical conjectures which first got solved by theorem provers, such as the Robbins problem. There are some mathematicians, such as Ken Kunnen, who use theorem provers extensively in their work also. So, I think the answer to your question is 'yes'.
-
As I understand now, mathematicians overwhelmingly stick to using their intuitive sense of logic to prove their theorems. Theorem provers don't seem to be used very much. And for what I read about them, they in effect apply some variation of the Gentzen method of proof, which seems to me to be strictly a generalisation of Aristotle. Further, Gentzen relies on the use of a set of rules of inference, which are themselves not proven but merely accepted as obviously true. Jan 14, 2019 at 15:26
-
@Speakpigeon From what I've seen many, and I would guess most, theorem provers use resolution. I don't think that's what you mean by a Gentzen method of proof. Additionally, though no rules of inference can get proven, rules of inference can often get checked for validity. The question as stated also doesn't concern what mathematicians do, but rather their personal confidence. If mathematicians were not confident that theorem provers proved things correctly, then, if asked at least, they will reject the results of those theorem provers or express doubts about those proofs. Jan 17, 2019 at 18:18
-
According to what I read recently on theorem provers, they will typically use a small set of fairly obvious logical truths used as rules of inference. Resolution itself seems to be a sort of generalisation of that method. As to proving the obvious logical truths used as rules of inference, as I see it, they are the empirical evidence that allow you to validate any method of proof, not the other way round as you seem to suggest here. Jan 17, 2019 at 19:25
-
My point was that confidence seems to rest almost entirely in sticking with the empirical evidence of the logical truths identified by the tradition, whether it's proof by mathematician or proof by theorem prover. The few exceptions I was able to find seem to be "wild explorations", for example assuming that A and not A implies not A. Jan 17, 2019 at 19:26
-
@Speakpigeon No rules of inference are not logical truths. A truth consist of an accurate statement. Rules of inference are not statements. Thus, to call rules of inferences truths makes for a category error. Rules of inference are also not empirical, in that they do not rely on sense data or perception in any way, though perhaps I misunderstand what you mean by 'empirical'. There is no way to observe the law of identity for example, since it applies to an indefinite, if not also potentially infinite, if not also actually infinite universe of statements. Jan 17, 2019 at 19:46