A. Foretrees work and are ready to be added to the grammar.
B. Aftertrees have a problem with parentheticals.
I think I have a way of making aftertrees work. The idea is that a simple formula can be followed by aftertrees or a parenthetical sentence, but not by both. There slight kludge in the interpretation in the sense that terms that precede the simple formula (within the core formula) have inner scope while the afterthought trees have outer scope. Another way of putting it: To restore logical form, the aftertrees have to shift in front of the entire core formula even though they're technically part of the simple formula production. I don't think it's a problem at all, but it should be noted. The grammar itself (as far as I can tell) is unambiguous.
Here are a hypothetical revision of the rules with foretrees and aftertrees added:
sentence := illocutionary-operator? formula | interjection
formula := core-formula | foretree formula
foretree := he | term foretree | coordinator foretree foretree
aftertree := hi | term aftertree | coordinator aftertree aftertree
core-formula := simple-formula | term core-formula
term := unary-operator | binder formula | coordinator formula