Thanks, Rob! Then since I only technically have a model, I would say I'm working in your class (c):
(c) Informal mathematical proofs that an assertion is provable in some agreed deductive system. I still don't understand what you're saying about class (d), or why this is true: Your theorems are entirely in class (d): the statement of each one proposes a new rule of inference and the proof shows how to use rules that are already given to achieve the same effect as the new rule. Perhaps the terminology a--e isn't important. What's important is what you wrote in your previous post: If you present the admissibility proofs in the style of the derivations in section 2.3 of the HOL4 description manual that Konrad kindly pointed us to, then there should be absolutely no need for anyone who wants to understand the derivation of the FOL inference rules from the HOL Light deductive system to read any source code. I think my informal mathematical proofs of my theorems about T are similar to the Description proofs. I'm not writing in the "two column proof" style used by Description, and I'm explicitly writing things like ''For any term t'' that I think are implicit in the Description proofs. Am I wrong? Is Description not also really giving informal mathematical proofs about the set T? Maybe it would help for us to settle this: Note that your “axioms” are just part of the description of the set T. I wasn't trying to get any credit for proving the ``axioms''! All I did to obtain them was to insert phrases like ''For any term t'' into the on-line help from HOL Light for the functions which comprise ``HOL Light's 10 primitive inference rules.'' My point was the that the deduction rules of HOL Light could be immediately translated into theorems about the subset T of S, and now we're in the realm of pure math. -- Best, Bill ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
