Timeline for Infinitary reasoning in Godel's Completeness Proof
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 23, 2019 at 10:24 | comment | added | user21820 | I think the point is that you cannot necessarily have a model less you have some way of separating disjoint computably enumerable sets, which is 'half' infinitary, having no finitary computable solution. What's worse is when we use transfinite induction to get a model of an uncountable finitely-satisfiable theory. I heard that Skolem didn't like that. | |
| Jul 18, 2019 at 22:45 | comment | added | Noah Schweber | @Max Oh I see, my bad - I fully agree with you. I interpreted "completeness result" much more narrowly. | |
| Jul 18, 2019 at 22:45 | comment | added | Maxime Ramzi | I'm not sure you disagree, as I agree with what you said in that last comment ! When I said "some completeness result" I didn't imply a r.e. system or even a finitary one ! I meant that one can always expect some form of completeness through some Lindenbaum-Tarski-type construction; of course one expects said construction to be horrendous and far from r.e. or even finitary in general. So the surprise is that the completeness theorem is completeness wrt to such a nice system (same as for propositional logic : boolean algebras, not so surprising, $\{0,1\}$, very surprising) | |
| Jul 18, 2019 at 9:03 | comment | added | Maxime Ramzi | More specifically, I would say it's not "there is a completeness result" that is surprising, it's "this tiny easy list of axioms that we know and understand gives a complete system" that is surprising. | |
| Jul 18, 2019 at 6:03 | comment | added | Noah Schweber | But completeness goes further. A priori the compactness theorem only says that there is some "finitely-based" proof system characterizing validity, but $(i)$ it doesn't say that there needs to be a computable such system and $(ii)$ it certainly doesn't suggest that such a system could be simply describable - and indeed already discovered! Think of it this way: why, barring the completeness theorem itself, would you expect some particular list of sequent rules to be complete? Completeness is something that is often taken for granted, but it's quite surprising. | |
| Jul 18, 2019 at 5:59 | comment | added | Noah Schweber | @Mallik "The existence of a proof is a nonconstructive result though, right, just by contraposition of the model existence formulation." No, you need the completeness theorem to say that - and that's what we're talking about proving in the first place! Pre-completeness theorem, and using anachronistic notation, the set of valid sentences is a priori $\Pi^1_1$ - to check whether a sentence is valid you would need to check every possible (countable) model. Why should there be a "combinatorial" description of validity? The compactness theorem is already incredibly surprising here. (continued) | |
| Jul 18, 2019 at 3:56 | comment | added | Mallik | The existence of a proof is a nonconstructive result though, right, just by contraposition of the model existence formulation. Can you say a bit more about why that result was surprising to you? (That answer was very relevant to my purposes). | |
| Jul 18, 2019 at 3:24 | vote | accept | Mallik | ||
| Jul 18, 2019 at 3:09 | history | edited | Noah Schweber | CC BY-SA 4.0 |
added 1 character in body
|
| Jul 18, 2019 at 3:04 | history | answered | Noah Schweber | CC BY-SA 4.0 |