Bill, On 26 Mar 2014, at 23:01, Bill Richter <rich...@math.northwestern.edu> wrote:
> 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. No. When I wrote "an assertion", I meant one specific assertion, something like "|- 1 = 1". Compare this with: for any term "t", "|- t - t" is provable. > > 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: Yes, the description manual is giving informal mathematical proofs about T. The two column style is clearer (in my opinion) when it works (which it will in the derived rules you are currently interested in, I believe). > > 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''! Understood. My note was just a lead-in to what I wanted to say about your theorems. > 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. So in the statements of your theorems, you are quantifying over bits of syntax, i.e., terms and types, This is why I classified your theorems as admissibilty proofs: they make general claims about what is provable, not specific claims that such-and-such an assertion is provable. And, yes, as I said in an earlier post, mathematical logic is a branch of pure mathematics (sadly one that seems to be undervalued in the pure mathematics community). Regards, Rob. ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
