Thanks, Rob! I think we're in agreement on the substantive issues, after I agree with your true correction:
If you replace “true” by “provable”, then this is how one would state Andrews’ claim that the rules of N are admissible in FOL. Yes, thanks for the correction. So we're just talking about the best way to write HOL documentation. You are consistently using “informal” where the standard term in the logic literature is “meta”. So if I replace every occurrence of ``informal mathematics'' with ``metamathematics'', you'll be happy? And doesn't ``informal mathematics'' actually mean the same thing as what is called ``metamathematics''? What Andrews means is that the rules of inference of N can be seen by metamathematical reasoning (i.e., by reasoning about the deductive system, rather than in it) to have the same deductive closure as (some other system of rules for) FOL. Great, and that's what I thought. But isn't this reasoning about the deductive system my informal math? That is, I think we're doing the following. We understand that a deductive system such as FOL is defined by certain rules, and we're proving theorems about this deductive system the same way we would prove anything in informal math. So the subject of group theory is largely working out the logical consequences of the group theory axioms, but we don't call this metamathematics. When we're ``reasoning about the deductive system'', we're doing the same kind of mathematical thinking we would in group theory. So the reason for calling it metamathematics when studying proving theorems about a deductive system such as FOL is to not be confusing, since we use the word ``theorem'' in FOL itself? > So it's better, I contend, to think of Andrew's system N of > natural deduction as informal math theorems that allow us to give > nice proofs of our FOL results. Yes, but there are important distinctions (like the distinction between “truth” and “provability”) that you need to be careful and precise about in your informal account. Great! But don't I just need to use the word `provability' and not `truth'? To me the question is what's the clearest way to explain HOL. If HOL users are happy with the term metamathematics (and meta-theorem, meta-proof, and meta-qed???), then we should use this terminology. To me, the term metamathematics is only useful when one is discussing one's primary logical framework. But the HOL4 manual LOGIC (derived from Andy Pitt's work, I think) clearly says that the meaning of HOL4 is given by a model of ZFC. Surely that holds for HOL Light as well, and I assume ProofPower. So that puts HOL more on the level of group theory, rather than our preferred logical framework, and so I don't see the point of the term metamathematics, except of course to avoid confusion. But bringing in terms like meta-theorem, meta-proof, and meta-qed seem to me to increase confusion. Here's a more substantive point that's always bothered me. Suppose if one is working in one's preferred logical framework (e.g. ZFC), and one engages in metamathematics. On what grounds to we believe the metamathematics? The point of ZFC was to foundationalize our mathematics, so what justifies our ``reasoning about the deductive system''? I speak in ignorance of Mathematical Logic here of course, and also with the bias of Pure Mathematics, which tends to not think that Mathematical Logic provides any firm foundations of math anyway. To me, Math Logic, HOL, Voevodsky's new HoTT/UF, are fantastic ways to remove the human error from proof checking, but they aren't ways to put our math on firm foundations, so that our theorems become truly true. -- Best, Bill ------------------------------------------------------------------------------ "Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE Instantly run your Selenium tests across 300+ browser/OS combos. Get unparalleled scalability from the best Selenium testing platform available. Simple to use. Nothing to install. Get started now for free." http://p.sf.net/sfu/SauceLabs _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
