Logical endpoints

More on Aaronson (see previous post for context):

I was struck by this commment Scott made on Gil Kalai’s blog:

Yes, I admit, I do have the moral philosopher’s (or for that matter, the mathematician’s) habit of trying to take stated principles to their logical conclusions, even if many people would regard those conclusions as “irrelevant” or “absurd.” (To take a different example: “People should have the right to own whatever weapon they want, since merely owning it doesn’t harm anyone.” “OK then, what about nuclear missiles?” “That’s irrelevant and absurd! I was talking about guns.”) Is this habit something I should apologize for?

and this reddit comment he quotes approvingly:

I think the reason Dworkin comes up in discussions like this is because her thinking is the logical endpoint of mainstream feminist theory.
It goes something like this:
1) Women are systematically oppressed by men
2) If 1 is true, how can a woman ever consent to sex or practically anything else with men? Any “consent” a woman gives will be given under duress because she is being systematically oppressed.
3) If any “consent” a woman gives is under duress (because every decision and choice a woman makes is under duress because she’s being systematically oppressed), then women can never ever give consent in any dealing with men.
Dworkin, to her credit, was so logical that she came to this conclusion and accepted it. All logical thinkers will probably come to this conclusion which is why nerds and STEM people will like and understand Dworkin. She’s logical. She makes sense.

For my own part, I find this idea of taking political and moral principles to their logical conclusions to be very weird.  And I don’t think it’s “the mathematician’s habit,” as Scott says.  At least, it’s not this mathematician’s habit.  Being a mathematician doesn’t incline me to apply Boolean operations to ethical principles; on the contrary, I think being a mathematician makes me more alive than the average person to the difference between mathematical assertions (which do behave really well under logical operations) and every other kind.

In particular, I don’t find the argument by the reddit commenter very compelling.  There are lots of feminists (I think almost all feminists!) who sound nothing like Andrea Dworkin, and who pretty obviously think that there exists sex between men and women that isn’t rape.  Is that because they can’t do logic?  I am a STEM person and a feminist and I think systematic sexism exists in the world and I don’t think heterosexual sex is rape.  Is that because I can’t do logic?

No — it’s because I think there are very few assertions about sex, power and feminism which stand in a relation of authentic logical entailment.

I now understand one thing about type theory

I was frustrated by my inability to get anything out of the brief writeup about Voevodsky’s univalent foundations in this month’s Notices.  Fortunately, one of our graduate students, who has been reading the homotopy type theory book, has promised to explain it to me.  I’m excited!

Already, hardly understanding anything, I have learned one interesting thing about type theory.  (I haven’t yet learned anything about homotopy type theory.)  It asks us to throw aside assertions like “P is true” as the basic objects of mathematical interest, and instead to concentrate on assertions like “p is a proof of P.”

In this context, what is conjunction?  To say “x is a proof of P and Q” is to say that x is a pair (p,q) where p is a proof of P and q is a proof of Q.”

What is disjunction?  In other words, what do we mean by “a proof of P or Q”?  Well, there are two kinds of proofs of P or Q; there are proofs of P, and there are proofs of Q.

And this is why intuitionistic logic (which as I understand it is the kind of logic you get when you take this point of view seriously) rejects the law of the excluded middle.  In the logic I know, you can just check from the truth table that (P or not-P) is always true, so (P or not-P) is the same thing as T.

But in type land, a proof of (P or not-P) must be either a proof of P or a proof of not-P.  If neither of these is available, then there’s no proof of (P or not-P), so it can’t be the same as T.

I know in some sense this seems tautological — but I do find it rather striking as an illustration of an actual substantial difference between the two set-ups.

As Vladimir teaches me more, I’ll keep posting!

P.S.:  by the way:  in type theory, a proof of an implication “P implies Q” is a function from proofs of P to proofs of Q.  (Or does it have to be an explicit algorithm that returns a proof of Q given a proof of P?  I don’t know.)  This is not the same as a proof of “not-P or Q”, which would have to be either a proof of not-P or a proof of Q, a completely different thing.  So the logical account of implication I’m used to also dies!

On the other hand, a proof of Q is a proof of (not-P or Q).  What’s more, if I have a proof q of Q, then the constant function sending every proof of P to q is a proof of (P implies Q).

I think the above paragraph is a correct proof in the type-theoretic sense of (Q implies (not-P or Q)) and also (Q implies (P implies Q)).  What do you think?

(Note that I haven’t told you what a type is yet.  That’s because I don’t know.  I told you, I only understand one thing so far.)

 

 

De-mystify me about nonstandard finite fields

In their paper, “Definable subgroups of algebraic groups over finite fields,” Hrushovski and Pillay write

… if V is an absolutely irreducible variety of dimension d over the finite field F_q, then the cardinality of V(F) is “roughly” q^d.  So for nonstandard q, the cardinality of V(F) is exactly q^d.

Do I have any nonstandard readers who can explain what is meant by this provocative statement?

Warning signs of a possible collapse of contemporary mathematics

“The belief that exponentiation, superexponentiation, and so forth, applied to numerals yield numerals is just that—a belief.” Heterodox opinions about what we should and shouldn’t think of as “known” about integers from Ed Nelson, previously seen thoughtfully smoking a pipe here.

Diophantineness: Mazur-Rubin and Kollar

Last year I blogged about an argument of Bjorn Poonen, which shows that Hilbert’s tenth problem has a negative solution over the ring of integers O_K of a number field K whenever there exists an elliptic curve E/Q such that E(Q) and E(K) both have rank 1.  That is:  there’s no algorithm that tells you whether a given polynomial equation over O_K is solvable.  The idea is that under these circumstances one can construct a Diophantine model for Z inside O_K; one already knows (by Matijasevic, Robinson, etc.) that no algorithm can determine whether a polynomial equation over Z has a solution, and the same property is now inherited by the ring O_K.

The necessary fact about existence of low-rank elliptic curves over number fields (actually, not quite the fact Poonen asked for but something weaker that suffices) has now been proven, subject to a hypothesis on the finiteness of Sha, by Mazur and Rubin: see Theorems 1.11 and 1.12.  So, if you believe Sha to be finite, you believe that Hilbert’s tenth problem has a negative answer for the ring of integers of every number field.

The result of Mazur and Rubin is actually much more substantial than the corollary I mention here, giving for instance quite strong lower bounds on the number of twists of an elliptic curve E with specified 2-Selmer rank.  But I haven’t studied the argument sufficiently to say anything serious about what’s inside.

I recently returned from the “Spaces of curves and their interaction with Diophantine problems” conference at Columbia, where Janos Kollar discussed the question:  Which subsets S of C(t) are Diophantine?  That is, which have the property that they can be written as the set of s in C(t) such that for some polynomial f in k+1 variables with coefficients in C(t).  Kollar explained how to prove that the polynomial ring C[t] is not Diophantine in C(t).  The idea is to show that any “sufficiently large” Diophantine subset S of C(t) contains functions whose denominators are essentially arbitrary; more precisely (but not completely precisely!) if X in Sym^d P^1 is the locus of degree-d denominators of elements of S, the Zariski closure of X needs to be — well, it doesn’t have to contain all degree-d polynomials, but it has to contain a set of the form as F,G range over polynomials of degrees s,t with s+rt = d.  In particular, it’s not possible for the denominator to be identically 1, as would be the case if S were C[t].  In fact, this argument shows that no finitely generated C-subalgebra of C(t) is Diophantine over C[t].

Open question:  is the localization of C(t) at t Diophantine over C(t)?

Update: When I first posted this I didn’t notice that Kollar’s result is already out, in the new journal Algebra and Number Theory, so you can go to the source for more details.  ANT, by the way, is a free electronically distributed journal with a terrific editorial board, and I highly recommend submitting there.