Bill,
On 26 Mar 2014, at 09:37, Bill Richter <rich...@math.northwestern.edu> wrote:
> Rob, thanks for the excellent post! Let me more clearly tell you what I
> think I'm doing, using your terminology, and maybe we can discuss your
> classes a--e.
>
> Take HOL Light and possibly some extra types, constants and axioms created by
> commands like new_type, new_constant, and new_axiom. Let S be the set of
> sequents, and T be the subset of S consisting of the sequents which are
> theorems, i.e. which have HOL Light formal proofs.
>
> Let me ask a dumb question right now: Is T a model?
In the very abstract sense of my post, yes it is. However, it is rather
unsatisfactory in that it doesn’t give any insight into what the assertions in
the language are intended to mean. Something like the model described in the
HOL4 Logic manual gives you an independent way of assessing the correctness or
utility of the deductive system. However, logicians do sometimes work with
models defined completely syntactically like your T (called term models or
Lindenbaum algebras in the literature).
>
> I contend that we can give informal mathematical theorems about the set T.
> All our HOL Light axioms become informal mathematical theorems, e.g.
>
> Axiom REFL:
> For any term t, the sequent
> |- t = t
> is a theorem (i.e. belongs to the set T).
>
> Axiom INST:
> For any theorem
> A |- t
> and any list of variables x1,...,xn and terms t1,...,tn such that xi and ti
> have the same type, such that none of the free variables of t1,...,tn occur
> are bound variables of t, we have the theorem
> A |- t[t1,...,tn/x1,...,xn]
Note that your “axioms” are just part of the description of the set T.
> Then we can prove consequences of the axioms, such as the one you explained
> to me was easy:
>
> Theorem BETA_CONV:
> For any variable v and any terms bod and arg, the sequent
> |- ((\v. bod) arg) = bod[arg,v]
> is a theorem (i.e. belongs to the set T).
>
> Proof:
> By axiom BETA, the sequent
> |- ((\v. bod) v) = bod
> is a theorem. Now applying axiom INST with [arg,v] and this theorem.
> \qed
>
> Let me now try to place myself in your a--e. If T is a model, then it looks
> like I'm working in your class (a):
>
> (a) Informal mathematical proofs that an assertion is valid in some
> agreed model (or set of models) of a language.
>
> Is T only a model if we have soundness? I contend we can prove informal
> theorems about T even if we don't have soundness, or haven't proved we have
> soundness. In any case I'm not going to make any soundness arguments or
> claims, and that rules out your class (b).
>
> Whether T is a model or not, I think it obvious to everyone that these
> informal mathematical proofs about the set T will imply that the
> corresponding formal HOL Light proofs exist, and that sounds like I'm working
> in class (c) as well:
>
> (c) Informal mathematical proofs that an assertion is provable in
> some agreed deductive system.
>
> I would then agree with you that
>
> Your point (3) is about class (a) or (c).
>
Your point (3) read: "We can try to give informal mathematical proofs
wffs/proto-sequents are actually theorems/sequents”. I was reading that as
meaning giving proofs of the validity or provability of particular sequents,
like “|- x^2 + 1 /= 0”, not proofs about validity or provability in general.
> However, I think I disagree with you about class (d):
>
> When you talk about "informal mathematical proofs of the FOL rules
> of HOL” you are in class (b) or (d).
>
> I think I'm still in class (a) or (c) when I do this. I'm certainly not in
> class (b), lacking your elaborate apparatus, as I think you noted:
>
> I think the apparatus you need to do soundness proofs (class (b))
> is more elaborate than that for admissibility proofs (class (d)).
>
> But I don't see why my I'm informal proofs of that "HOL implies FOL" puts me
> in your class (d):
>
> (d) Informal mathematical proofs that a new rule of inference is
> admissible in some agreed deductive system. I.e., informal
> mathematical proofs that if an assertion can be proved using the
> new rule of inference, then it can be proved using only the axioms
> and inference rules of the deductive system. (In the cases in point
> here, this can done by giving a schematic derivation of the new
> rule of inference as a combination of the inference rules of the
> deductive system.)
>
> Perhaps I don't even understand what class (d) means. Let's take my last
> informal theorem of the HOL implies FOL sort, updated with your new
> terminology:
>
> Theorem CONJUNCT1:
> Let l and r be terms and A be a set of assumptions such that we have the
> theorem.
> A |- l ∧ r. Then we have the theorem A |- l.
>
> Proof:
> Since ∧ has type bool->bool->bool, l and r both have type bool.
> By theorem ALPHA, the AND_DEF theorem, and axiom TRANS, we have the theorem
> |- (∧) = (λp' q'. (λf':bool->bool->bool. f' p' q') = (λf'. f' T T))
> where f', p' and q' are not free in either l or r. Applying theorem AP_THM
> twice to the AND_DEF sequent l, and r we have the theorem
> |- (∧) l r = (λp' q'. (λf':bool->bool->bool. f' p' q') = (λf'. f' T T)) l r.
> Applying theorem BETA_CONV and axiom TRANS twice to the RHS yields
> |- l ∧ r = ((λf':bool->bool->bool. f' l r) = (λf'. f' T T)).
> Since we have the theorem A |- l ∧ r by assumption, axiom EQ_MP yields the
> theorem
> A |- (λf':bool->bool->bool. f' l r) = (λf'. f' T T)
> Choose free variables p and q of type bool that are not free in l or r.
> Applying AP_THM to this equation theorem and the term (λp q. p) yields the
> theorem
> A |- (λf':bool->bool->bool. f' l r) (λp q. p) = (λf'. f' T T) (λp q. p).
> Applying theorem BETA_CONV, axiom TRANS and theorem SYM a number of times, we
> obtain the theorem
> A |- l = T.
> By theorem EQT_ELIM, we're done.
> \qed
>
> Now I don't see any difference between this informal mathematical theorem and
> theorem BETA_CONV above. I don't see why we need an extra class just because
> we're working out the FOL rules in HOL. Quite likely I'm missing some
> important point here.
I talked about the FOL rules, because that is what your post was about. What I
said applies equally well to your derivation of BETA_CONV. 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.
Regards,
Rob.
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
