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? 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] 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). 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. -- Best, Bill ------------------------------------------------------------------------------ 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
