Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Using Dieudonne's wonderful determinant, taking values in the abelian quotient $Z = K^\times / [K^\times, K^\times]$, characterized by the axioms that say that scaling a row by $z$ scales the determinant by the image of $z$ in $Z$, switching rows or columns changes the sign of the determinant, and adding one row or column to another leaves the determinant unchanged.
Regarding Bhaskara I, I am just about ready to call it bunk. It is all over the internet, so it is popular bunk. I think that the bunk comes from misinterpreting the following: In Vol. 2, Ch II, p.59 of his "History of the Theory of Numbers", Dickson explains how both "Ibn al-Haitam (about 1000)" and "Bhascara (born, 1114 A.D.)" treated similar problems about finding a number which has given remainders when divided by 2,3,4,5,6. From the date, this would appear to be Bhaskara II. Al-Haitam's problem leads him to "Wilson's Theorem" context, but Wilson's theorem is absent from Bhaskara II.
Ibn al-Haytham: "This being shown we say that this is a necessary property for any prime number, that is to say that for any prime number - which is the number that is a multiple only of the unit - if you multiply the numbers that precede each other in the way that we have introduced, and if we add one to the product, and if we divide the sum by each of the numbers before the prime number, there is one, and if it is divided by the prime number, nothing is left."
Indeed, from Rashed's scholarly translation of Ibn al-Haytham, we find that Ibn al-Haytham knew "Wilson's theorem". An English translation can be found in "The Development of Arabic Mathematics: Between Arithmetic and Algebra" by the same Rashed. Since this large book is not all available on google books, I will provide an English translation of Rashed's French translation of the Arabic manuscript MSS Loth 734 (f. 121), which is the relevant section of al-Haytham's Oposcula.
I can't quite answer my own question, but I just found the paper "Describing Groups" by Andre Nies, in Bull. Symbolic Logic 13 (2007), no. 3. It seems like the theory $(p^{- \infty} {\mathbb Z}, =, +, 0)$ is decidable since it is "finite-automaton presentable" (FA-presentable). A quick guess is that the additional structure, $1$, ${\mathbb Z}$, and the predicate $\phi$ might also fit into the FA-presentable framework and give a proof of decidability. But I'd still apreciate the opinion of an expert!
It's not a problem if every real number in [-1,1] occurs from some ultrafilter on the primes. This is expected by Cebotarev and Sato-Tate. The question is how to construct the real number $cos(\theta_u)$ directly from the elliptic curve $E$ and the generic automorphism of an algebraically closed field of characteristic zero defined by $u$. My hope was for a (possibly new) cohomology theory in characteristic zero (perhaps with coefficients in a Laurent series field like $C((t))$ ) from which $cos(\theta_u)$ can be extracted.