dankane comments on Logical Pinpointing - Less Wrong

62 Post author: Eliezer_Yudkowsky 02 November 2012 03:33PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (338)

You are viewing a single comment's thread. Show more comments above.

Comment author: dankane 02 November 2012 09:31:13PM 5 points [-]

OK then. As soon as you can explain to me exactly what you mean when you say "for any collection of numbers there is a corresponding property being quantified over", I will be satisfied. In particular, what do you mean when you say "any collection"?

Comment author: Eliezer_Yudkowsky 03 November 2012 12:22:33AM 2 points [-]

Are you claiming that this term is ambiguous? In what specially favored set theory, in what specially favored collection of allowed models, is it ambiguous? Maybe the model of set theory I use has only one set of allowable 'collections of numbers' in which case the term isn't ambiguous. Now you could claim that other possible models exist, I'd just like to know in what mathematical language you're claiming these other models exist. How do you assert the ambiguity of second-order logic without using second-order logic to frame the surrounding set theory in which it is ambiguous?

Comment author: dankane 03 November 2012 07:19:17AM 3 points [-]

I'm not entirely sure what you're getting at here. If we start restricting properties to only cut out sets of numbers rather than arbitrary collections, then we've already given up on full semantics.

If we take this leap, then it is a theorem of set theory that all set-theoretic models of the of the natural numbers are isomorphic. On the other hand, since not all statements about the integers can be either proven or disproven with the axioms of set theory, there must be different models of set theory which have different models of the integers within them (in fact, I can build these two models within a larger set theory).

On the other hand, if we continue to use full semantics, I'm not sure how you clarify to be what you mean when you say "a property exists for every collection of numbers". Telling me that I should already know what a collection is doesn't seem much more reasonable than telling me that I should already know what a natural number is.

Comment author: Eliezer_Yudkowsky 03 November 2012 05:36:38PM 3 points [-]

On the other hand, since not all statements about the integers can be either proven or disproven with the axioms of set theory, there must be different models of set theory which have different models of the integers within them

Doesn't the proof of the Completeness Theorem / Compactness Theorem incidentally invoke second-order logic itself? (In the very quiet way that e.g. any assumption that the standard integers even exist invokes second-order logic.) I'm not sure but I would expect it to, since otherwise the notion of a "consistent" theory is entirely dependent on which models your set theory says exist and which proofs your integer theory says exist. Perhaps my favorite model of set theory has only one model of set theory, so I think that only one model exists. Can you prove to me that there are other models without invoking second-order logic implicitly or explicitly in any called-on lemma? Keep in mind that all mathematicians speak second-order logic as English, so checking that all proofs are first-order doesn't seem easy.

Comment author: dankane 04 November 2012 12:28:54AM 2 points [-]

I am admittedly in a little out of my depth here, so the following could reasonably be wrong, but I believe that the Compactness Theorem can be proved within first order set theory. Given a consistent theory, I can use the axiom of choice to extend it to a maximal consistent set of statements (i.e. so that for every P either P or (not P) is in my set). Then for every statement that I have of the form "there exists x such that P(x)", I introduce an element x to my model and add P(x) to my list of true statements. I then re-extend to a maximal set of statements, and add new variables as necessary, until I cannot do this any longer. What I am left with is a model for my theory. I don't think I invoked second order logic anywhere here. In particular, what I did amounts to a construction within set theory. I suppose it is the case that some set theories will have no models of set theory (because they prove that set theory is inconsistent), while others will contain infinitely many.

My intuition on the matter is that if you can state what you are trying to say without second order logic, you should be able to prove it without second order logic. You need second order logic to even make sense of the idea of the standard natural numbers. The Compactness Theorem can be stated in first order set theory, so I expect the proof to be formalizable within first order set theory.

Comment author: Eugine_Nier 03 November 2012 10:39:08PM *  2 points [-]

If you're already fine with the alternating quantifiers of first-order logic, I don't see why allowing branching quantifiers would cause a problem. I could describe second order logic in terms of branching quantifiers.

Comment author: dankane 04 November 2012 12:40:04AM 2 points [-]

Huh. That's interesting. Are you saying that you can actually pin down The Natural Numbers exactly using some "first order logic with branching quantifiers"? If so, I would be interested in seeing it.

Comment author: Eugine_Nier 04 November 2012 03:33:27AM *  2 points [-]

Sure:

It is not the case that: there exists a z such that for every x and x’, there exists a y depending only on x and a y’ depending only on x’ such that Q(x,x’,y,y’,z) is true

where Q(x,x’,y,y’,z) is ((x=x' ) → (y=y' )) ∧ ((Sx=x' ) → (y=y' )) ∧ ((x=0) → (y=0)) ∧ ((x=z) → (y=1))

Comment author: dankane 04 November 2012 04:16:38AM 3 points [-]

Cool. I agree that this is potentially less problematic than the second order logic approach. But it does still manage to encode the idea of a function in it implicitly when it talks about "y depending only on x", it essentially requires that y is a function of x, and if it's unclear exactly which functions are allowed, you will have problems. I guess first order logic has this problem to some degree, but with alternating quantifiers, the functions that you might need to define seem closer to the type that should necessarily exist.