Timeline for Syntax/semantics conflation leads to infinitary logic
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 4, 2023 at 18:15 | comment | added | Lave Cave | In what way is $\exists$ like uniform convergence and $\vee$ like point wise convergence? | |
| Jan 3, 2019 at 9:08 | comment | added | Andrej Bauer | Sure, my worry (or excitement) is that computers might do such complex mathematics that humans will be completely unable to follow them, even though it will all be expressed by finitary means. (I think MO is about to tell us not to use comments as a chat system.) | |
| Jan 3, 2019 at 9:03 | comment | added | Monroe Eskew | But there is no indication that real-world computers can handle anything other than finitary syntax. | |
| Jan 3, 2019 at 8:59 | comment | added | Andrej Bauer | I think it's safe to describe the situation as a difference of opinion (and not a very essential one). And I'll bet on computer capacities to do mathematics in this millennium. Us humans might be left behind. | |
| Jan 3, 2019 at 8:55 | comment | added | Monroe Eskew | I am with you that foundations of math is not all about the study of finitary syntax. But I think it does play a “paramanount” and “primary” role in foundations of math for the reasons mentioned above. We can study many things, but we must have an unambiguous foundation for what counts as a proof that matches actual human capacities. | |
| Jan 3, 2019 at 8:49 | comment | added | Andrej Bauer | @MonroeEskew: I stated it's important, didn't I? I quote myself: "Your remark justifies the importance of finitary syntax". What I dislike is the attitude that the foundations of mathematics cannot be about anything else, or that other things matter less. The philosophers of language did not sell us the goal, but the method for achieving certainty. Why is the method so closely linked to language? Does it have to be? | |
| Jan 3, 2019 at 7:27 | comment | added | Monroe Eskew | So you don’t think epistemic certainty about proof is important for foundations of math? I think this goal is not something that comes from “philosophers of language.” | |
| Jan 3, 2019 at 7:12 | comment | added | Andrej Bauer | @MonroeEskew: (continued) However, the kind of foundation you speak of is only one aspect of foundations of mathematics, the part which focuses on how to reach objectivity in mathematical activity by multiple independent agents. Your remark therefore justifies the importance of finitary syntax, but does not give it a primary role, unless you assume that the primary business of logic is to give mathematics a foundation of the kind that the philosophers of language would appreciate. I myself do not subscribe to that view so easily. | |
| Jan 3, 2019 at 7:10 | comment | added | Andrej Bauer | @MonroeEskew: that is precisely the influence of the philosophy of lanugage I mentioned in my answer. Of course, it is difficult to imagine how it could be otherwise (myself included), as we're still in its grips. A similar, but perhaps a little more objective and modern standard is: verification of proofs and mathematics constructions must be doable by computers. | |
| Jan 2, 2019 at 19:51 | comment | added | Monroe Eskew | Mathematics must be founded on fintary syntax. It is the only choice that is transparent and unambiguous for humans to read, manipulate, and understand. Everything else is an abstraction that can ultimately be explained only in fintary language. | |
| Jan 2, 2019 at 19:02 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 4 characters in body
|
| Jan 2, 2019 at 17:18 | vote | accept | Mallik | ||
| Jan 2, 2019 at 17:16 | comment | added | Mike Shulman | Of course finitary logic also depends on the (finitary) metatheory (e.g. whether or not Con(PA) is provable is a finitary statement about syntax that is true in some metatheories and false in others), but at least a particular proof in a finitary logic (of a feasible size) can be written down completely and verified by a human or a computer. | |
| Jan 2, 2019 at 17:16 | comment | added | Mike Shulman | I agree, the Moore quote in the question definitely sounded to me like it was describing someone who was using an "internal language" without realizing it. On the other hand I do think there is something special about finitary syntax: it requires less of the metatheory. The behavior of infinitary logic can be highly dependent on the set-theoretic axioms assumed in the metatheory that determines the meaning of "infinite" (e.g. compact cardinals etc.). | |
| Jan 2, 2019 at 11:34 | history | answered | Andrej Bauer | CC BY-SA 4.0 |