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

Reply via email to