Timeline for How is Gödel's incompleteness theorem interpreted in intuitionistic logic?
Current License: CC BY-SA 4.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 19 at 19:09 | history | edited | Dennis | CC BY-SA 4.0 |
deleted 68 characters in body
|
| Sep 12, 2016 at 6:23 | comment | added | user21820 | Concerning your comment, consider that most mathematicians do not use induction as a first-order schema, but rather they consider it as a single axiom that gives induction for every property of the natural numbers. Arguably, that is meta-logical in nature, which is somewhat like having higher-order logic with Henkin semantics. That is why most of them will call it "the axiom of induction" rather than "an instance of the axiom schema of induction". | |
| Jun 1, 2016 at 5:35 | comment | added | Dennis | (Final comment on these matters for now.) I'll definitely grant you that most ordinary mathematics -- i.e., everything outside of math logic and some of the rest of pure math -- things are done somewhat less formally and in a way that seems more amenable to second-order treatment (in that, as you say, they seem to quantify over functions). I don't know, however, to what extent these mathematicians conceive of themselves as working within a first- or second-order system. That isn't a skeptical worry, just a genuine bit of ignorance. | |
| Jun 1, 2016 at 5:25 | comment | added | Dennis | Interspersed with all of this are difficult questions about where to draw the line between logic and math. Clearly FOL is logic, but what about a property-theoretic interpretation of Second-Order Logic? That might seem fine, but the set-theoretic interpretations have been commonly thought to veer too far in the mathematical direction (e.g., Quine on Second-order Logic as "set theory in sheep's clothing). TL;DR Philosophy remains hard. | |
| Jun 1, 2016 at 5:25 | comment | added | Dennis | I guess the only thing I'm somewhat sure of is that FOL is the better logic for capturing inferential patterns and SOL is the better logic for dealing with issues of definability and meaning. Essentially, it's the syntax-semantics divide. If you think syntactic (deductive) entailment is the end-all-be-all of logic, go first-order. If you think logic is about modeling certain concepts, especially generating categorical theories concerning these concepts, then maybe second-order logic is the way to go. (cont.) | |
| Jun 1, 2016 at 5:24 | comment | added | Dennis | The crucial distinction might seem to be whether the semantics appeals to the notion of an arbitrary subset/property/plurality -- i.e., whether it's the full semantics for SOL. Clearly that goes beyond first-order logic. But it still isn't clear to me that it goes beyond first-order set theory, especially given that you have perfectly parallel questions to, e.g., the continuum hypothesis, in both cases -- it's just a matter of whether those questions arise for the object or metalanguage. (cont.) | |
| Jun 1, 2016 at 5:15 | comment | added | Dennis | Of course, however, the most standard semantics for Second-Order logic is set-theoretical and so this really muddies the waters. In the years since I've posted this answer I've grown somewhat puzzled as to what the first- vs. second-order logic dispute boils down to. Is a theory second-order if it is syntactically second-order but with a seemingly first-order semantics? Forget full second-order semantics and just consider Henkin semantics. That's provably reducible to first-order logic and so seems like a distinction without a difference. (cont.) | |
| Jun 1, 2016 at 5:11 | comment | added | Dennis | @DavidTonhofer Yea, I think I somewhat overstated my case in this post. Superficially, most mathematics is cast in a first-order form and the standard semantics is a set-theoretic one where the "second-order entities" (properties, functions, relations, etc.) are treated as first-order entities -- sets of various sorts (e.g., a 2-place relation is just a set of ordered pairs, a function is just a set of ordered pairs where the first member of the pair is never related to more than one other object, etc.) (cont.) | |
| May 31, 2016 at 21:49 | comment | added | David Tonhofer | @Dennis First-order logic is the language most mathematics is formalized in. I think most mathematics is actually formalized in what can be called "second-order" logic, as you seriously need to quantify over function symbols rather often. | |
| Jun 8, 2015 at 19:40 | comment | added | Dennis | @mcb This isn't actually all that surprising. (Classical) First-order logic is the language most mathematics is formalized in. First-order logic is complete, but very few mathematical theories couched in it will be. So yes, you're right, there are additional axioms you add to a base of intuitionistic logic that cause the incompleteness of constructive maths. In particular, whatever axioms you add that allow you to define an arithmetic at least as strong as Robinson Arithmetic are the axioms that will cause the incompleteness theorem to apply. | |
| Jun 8, 2015 at 15:32 | comment | added | Lenar Hoyt | @Dennis I find it surprising that intuitionistic logic is complete, while constructive mathematics is not, which would mean that there are additional axioms which cause the incompleteness? | |
| S Jun 7, 2013 at 21:17 | history | suggested | user3164 | CC BY-SA 3.0 |
typos; several links; minor edits
|
| Jun 7, 2013 at 20:49 | review | Suggested edits | |||
| S Jun 7, 2013 at 21:17 | |||||
| Jun 7, 2013 at 20:11 | comment | added | Mozibur Ullah | You said "it is both sound and complete it is not incomplete" and then "whether it is suceptible to incompleteness. The answer here is yes". I think its those two notions of completeness I had mixed up - simply because they have similar names. | |
| Jun 7, 2013 at 19:59 | comment | added | Dennis | @MoziburUllah I'm afraid that I'm not quite getting what difference you're pointing to. As far as I know, there is just one form of (in)completeness: (not) being able to formally prove every truth of your theory. | |
| Jun 7, 2013 at 19:54 | comment | added | Mozibur Ullah | thanks for the references, they look useful. No need to apologise - You read my intentions correctly! I think I was confusing completeness which refers to syntax & semantics, and incompleteness which refers to solely 'formal proof' syntax only through the inference/deductive/proof system if I've read you right. Which is the standard name to use - inference/deductive/proof - they seem to all be used?! | |
| Jun 7, 2013 at 19:44 | history | edited | Dennis | CC BY-SA 3.0 |
added 2 characters in body
|
| Jun 7, 2013 at 19:40 | vote | accept | Mozibur Ullah | ||
| Jun 7, 2013 at 19:23 | history | answered | Dennis | CC BY-SA 3.0 |