[benkuykendall]

That's an interesting dichotomy to establish. At first, it appears to mirror the theoretical/applied division we see in a lot of fields. But in addition to an applied mindset, you seem to be demanding something stronger out of logic: applicability to philosophical discourse. To me, this seems like a very lofty goal: I would be very surprised if someone treated religion (to use your example) productively with formal logic.

However, just because it's not immediately applicable in one domain does not make logic useless. A great example of this is Prolog, a logical programming language which uses declarative statements reminiscent of first order logic. It can solve real world problems, though it has not yet seen wide adoption as a programming language. People do use automatic theorem provers, which have their roots in logic. The are used not only to further the "game" of mathematics, but to find also bugs in real hardware and software systems. These application have very little to do with philosophy, and nothing to do with translating between English language and logical sentences. However, I think they are quite interesting.

(I'm not sure what to tell you about logic "sounding stupid". In the end, things like definitions of connectives are just conventions. Although it's good to understand their motivations, I'm not sure how much good objecting to them does. It kind of reminds me of half serious attempts to adopt tau := 2 pi as mathematical notation; maybe using a different constant makes more sense to you, but finally, it won't make a big difference, and you should probably just continue to use pi for interoperability with the rest of the world.)

[fizixer]

I'm wondering what would be your take on a concrete example that I just posted here: https://news.ycombinator.com/item?id=15115319

[benkuykendall]

Personally, I don't really like the translation "information about A and B is insufficient to rule out implication". At least when I say "A implies B" I mean exactly "A => B". But maybe I hang out with too many mathematicians.

Other common translations you might be interested in are "A suffices for B" or "B is necessary for A". Though admittedly these particular words have a bit of a mathy tone, so no wonder they are so precisely tied to the definition of implication.

As far as your idea of "outside information" goes, I'm afraid it kind of breaks outside the bounds of sentential logic, which cannot deal with numbers in the manner you are attempting. However, that does not mean we cannot analyze it with logic. It should be simple to put your sentences into the logical "language" of Arithmetic and to prove more or less what you would expect: A is false (because John never leaves the office before 5), B is false (because it takes him 30 minutes to get home), and that "A => B" is true (by the definition of material implication, however vacuously).