Lambda the Ultimate

devotes several chapters to translation from English into the language of the first-order predicate logic. The book explains in great detail peculiarities of translating 'each' and 'some' sentences. Sentences such as "more than a half of the students liked the class" cannot be expressed with the traditional quantifiers. The book explains why (the determiner "more than a half" is irreducible) and what to do about it. The book also examines the differences between the logical implication and a conversational implicature.

Incidentally, the book discusses the ambiguity of a sentence like the following:
Every minute a man is mugged in New York City.

There are two translations:

  a weak reading:
      all x. (Minute(x)  -> exists y. (Man(y) & MuggedDuring(y, x)))


  a strong reading:
      exists y.( Man(y) & all x.(Minute(x) -> MuggedDuring(y,x)))

The weak reading says that every minute some man is robbed -- not necessarily the same man. The second reading specifically says that there is an unfortunate man who is being mugged minute after minute. The readings are called 'weak' and 'strong' because the latter implies the former, but not vice versa.

In the above case, the weak reading is more natural (and the one that first comes to mind). The book points out the following "Saturday Night Live" joke that brings up the strong reading:
"Every minute a man is mugged in New York City. We are going to interview him tonight."

The gist of the joke is this ambiguity and the low likelihood of the strong reading.

More interesting examples (of so-called "Donkey sentences")
"Every cube in back of a dodecahedron is also smaller than it."

The 'it' is especially troublesome. The translation therefore looks nothing like the original sentence:

      all x.(Dodec(x) -> all y.((Cube(y) & BackOf(x,y)) -> Smaller(y,x)))

"If you always do right, you will gratify some people and astonish the rest."

   all x.(RightThing(x) -> DoThing(you,x)) -> 
      exists y. (Person(y) & Gratify(you,y)) &
      all y.(Person(y) -> Gratify(you,y) || Astonish(you,y)))

  (call/cc ..... (call/cc call/cc))      <=v=> (lambda (p) (p p))
  (call/cc ..... (call/cc (call/cc id))) <=v=> (lambda (p) (p p))

Since the self-application (lambda (p) (p p)) is the "core" of the fixed-point combinator, it follows that (call/cc call/cc) can be used to express Y. It was pointed out that Andrzej Filinski has already done that in 1994:
Recursion from Iteration
http://citeseer.nj.nec.com/filinski94recursion.html

A more recent work is by Masahito Hasegawa and Yoshihiko Kakutani "Axioms for Recursion in Call-by-Value"
http://www.kurims.kyoto-u.ac.jp/~hassei/papers/hosc.html

Incidentally, it seems I can derive Filinski's results using a bit different line of reasoning and motivation.

There is now, finally, a write up available.