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

Reply via email to