Konrad, I should definitely read Description's chapter Derived Inference
Rules, which seems to be doing much the same
thing as I was attempting in my post. I noticed that Gordon Melham's
book is only mentioned much later and is not in
your bibliography. Could that be because Gordon wrote the
Bill,
On 25 Mar 2014, at 07:27, Bill Richter rich...@math.northwestern.edu wrote:
So the similarity is that in both FOL and HOL,
1) You can define a set of statements to study (wffs and proto-sequents).
Proto-sequent and “sequent” are usually referred to as “sequent” and
“theorem”
