Bill,
On 25 Mar 2014, at 07:27, Bill Richter <rich...@math.northwestern.edu> wrote:
> So the similarity is that in both FOL and HOL,
> 1) You can define a set of statements to study (wffs and proto-sequents).
"Proto-sequent" and “sequent” are usually referred to as “sequent” and
“theorem” respectively. E.g., see the HOL4 Logic manual section 2.2. (The code
in the various implementations of HOL may also use “goal” for “sequent".)
> 2) It's a mathematical question of which of the statements have formal proofs
> using the axioms and inference rules (and so are are provable (theorems or
> sequence).
Yes. Both FOL and HOL are examples of deductive systems. The study of deductive
systems is a major concern of the branch of mathematics known as mathematical
logic.
> 3) We can try to give informal mathematical proofs wffs/proto-sequents are
> actually theorems/sequents.
Yes. But see above about the terminology. I will use “assertion” below for the
things you try to prove in either FOL (wffs) or HOL (sequents) and “language”
to mean the set of all assertions. I will use “model” very abstractly to mean
some mathematical recipe that identifies a subset of the language. The
assertions in that subset are said to be “valid" with respect to the model in
question.
(So a language might comprise assertions about rings. A model would be a ring
A, with the valid assertions being the assertions that are true in A. An
assertion like “x^2 + 1 /= 0” would then be valid with respect to the real
numbers but not with respect the complex numbers.)
>
> Now with ZFC/FOL, everyone says that informal mathematical proofs are much
> more readable than formal ZFC proofs. So why shouldn't the same be true for
> HOL?
> Perhaps it's even true that informal mathematical proofs of the FOL rules of
> HOL are quite easy to understand,
> while understanding the formal proofs is no easier than reading the source
> code of our proof HOL assistants HOL Light, HOL4, ProofPower, HOL Zero.
You need to be careful to distinguish between several classes of things here:
(a) Informal mathematical proofs that an assertion is valid in some agreed
model (or set of models) of a language.
(b) Informal mathematical proofs that a rule of inference is sound in some
agreed model (or set of models) of a language. I.e.,informal mathematical
proofs, that if the hypotheses of the rule are valid, then the conclusion is
valid.
(c) Informal mathematical proofs that an assertion is provable in some agreed
deductive system.
(d) Informal mathematical proofs that a new rule of inference is admissible ins
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.)
(e) Formal proofs of an assertion in an agreed deductive system.
What “everyone” is saying is that the objects in class (a) are more readable
than the objects in class (e). By and large, “everyone” isn’t a logician and
therefore never even thinks of objects in classes (b), (c) and (d). Your point
(3) is about class (a) or (c). When you talk about "informal mathematical
proofs of the FOL rules of HOL” you are in class (b) or (d). So you need to
make a choice out which of these classes you want to work in.
I think the apparatus you need to do soundness proofs (class (b)) is more
elaborate than that for admissibility proofs (class (d)). I think you are
probably currently really concerned with admissibility: admissibility proofs
often require a lot more ingenuity than soundness proofs, but, happily, the
hard part of the work has already been done, e.g., in the paper by Henkin (or
in the HOL Light source code or ...). 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.
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
