The class of simple groups isn't elementary. To see this, first note that if it were, then an ultraproduct of simple groups would be simple. But an ultraproduct of the finite alternating groups is clearly not simple. (An $n$-cycle cannot be expressed as a product of less than $n/3$ conjugates of $(1 2 3)$ and so an ultraproduct of $n$-cycyles doesn't lie in the normal closure of the ultraproduct of $(1 2 3)$. )
It turns out that an ultraproduct $\prod_{\mathcal{U}} Alt(n)$ has a unique maximal proper normal subgroup and the corresponding quotient $G$ is an uncountable simple group. This group $G$ has the property that a countable group $H$ is sofic if and only if $H$ embeds into $G$. For this reason, $G$ is said to be a universal sofic group.
As for your third question, Shelah has constructed a group $G$ of cardinality $\omega_{1}$ which has no uncountable proper subgroups. Clearly $Z(G)$ is countable. Consider $H = G/Z(G)$. Then $H$ also has no uncountable proper subgroups.Furthermore, every nontrivial conjugacy class of $H$ is uncountable and it follows that $H$ is simple.
From a proof-theoretic point of view, Lamport essentially suggests is writing proofs in natural deduction style, along with a system of conventions to structure proofs by the relevant level of detail. (It would be very interesting to study how to formalize this kind of convention -- it's something common in mathematical practice missing from proof theory.)
I have written proofs in this style, and once taught it to students. I find that this system -- or indeed any variant of natural deduction -- is extremely valuable for teaching proof to students, because it associates to each logical connective the exact mathematical language needed to use it and to construct it. This is particularly helpful when you are teaching students how to manipulate quantifiers, and how to use the axiom of induction.
When doing proofs myself, I find that this kind of structured proof works fantastically well, except when working with quotients -- i.e., modulo an equivalence relation. The reason for this is that the natural deduction rules for quotient types are rather awkward. Introducing elements of a set modulo an equivalence relation is quite natural:
$$
\frac{\Gamma \vdash e \in A \qquad R \;\mathrm{equivalence\;relation}}
{\Gamma \vdash [e]_R \in A/R}
$$
That is, we just need to produce an element of $A$, and then say we're talking about the equivalence class of which it is a member.
But using this fact is rather painful:
$$
\frac{\Gamma \vdash e \in A/R \qquad \Gamma, x\in A \vdash t \in B \qquad \Gamma \vdash \forall y,z:A, (y,z) \in R.\;t[y/x] = t[z/x]}{\Gamma \vdash \mbox{choose}\;[x]_R\;\mbox{from}\;e\;\mbox{in}\;t \in B}
$$
This rule says that if you know that
- $e$ is an element of $A/R$, and
- $t$ is some element of $B$ with a free variable $x$ in set $A$, and
- if you can show that for any $x$ and $y$ in $R$, that $t(y) = t(z)$ (ie, $t$ doesn't distinguish between elements of the same equivalence class)
Then you can form an element of $B$ by picking an element of the equivalence class and substituting it for $x$. (This works because $t$ doesn't care about the specific choice of representative.)
What makes this rule so ungainly is the equality premise -- it requires proving something about the whole subderivation which uses the member of the quotient set. It's so painful that I tend to avoid structured proofs when working with quotients, even though this is when I need them the most (since it's so easy to forget to work mod the equivalence relation in one little corner of the proof).
I would pay money for a better elimination rule for quotients, and I'm not sure I mean this as a figure of speech, either.
Best Answer
Sela does not have an objective view of Kharlampovich, Myasnikov's work. We will post a paper dismissing his statements about "fatal mistakes". It just takes time. There are some typos and inessential errors that were fixed in later works. Sela himself has many such mistakes. The objects in the two works (Sela's and our work) are similar but not identical. They are not amenable to a crude direct interpretation; some of our statements would not be true if interpreted via a ``computer translation'' into his language (and vice versa). One example is
Sela's wrong Theorem 7 from his paper 6 on Diophantine Geometry. This theorem describes groups elementarily equivalent to a non-abelian free groups. Sela claims that our Theorem 41 is wrong too. But our theorem is stated using our concept of regular NTQ groups and is correct. This shows that regular NTQ groups are not completely identical to hyperbolic $\omega$-residually free towers. Many of his critical comments resulted from such an exact translation of our concepts into his language. Additional misrepresentations result from not remembering that some statement was made two pages before (such as that we only consider fundamental sequences satisfying first and second restrictions).
The decidability of the elementary theory of a free group is used in the proof of the decidability of the theory of a torsion free hyperbolic group (our recent preprint in the arxiv) and to make quantifier elimination algorithmic. One can use it to approach the theory of a free product of groups with decidable elementary theories (Malcev's problem). One can also use it to deal with Right Angled Artin groups.
The algorithm to find the abelian JSJ decomposition of a limit group was constructed in our paper "Effective JSJ decompositions" that appeared before, it is used in the proof of the decidability of the theory. Actually many Algebraic Geometry over free groups questions are solved algorithmically (see references on pages 508-514), finding irreducible components of finite systems of equations, analogs of elimination and parametrization theorems in classical Algebraic Geometry etc Olga Kharlampovich