Thanks, Rob! You seem to be correct about Andrews's book To Truth Through
Proof. His Chapter 5 Type Theory is 56 pages long, and it's mostly about Q_0
which is based on equality, which he calls Q:A->A->bool, and I notice that he
prove the only "truth table" result I was able to prove:
|- T ∧ T = T
And, yes, as I said in an earlier post, mathematical logic is a
branch of pure mathematics (sadly one that seems to be undervalued
in the pure mathematics community).
I agree, and I wish my mathematical logic was better. I have a 400+ line draft
of a new paper below which I think has some unsettled mathematical logic
issues. Perhaps you can look at it.
OK, so I'm not working in your class (c) because of your def of assertion, but
I'm think this is great:
Yes, the description manual is giving informal mathematical proofs
about T. The two column style is clearer (in my opinion) when it
works (which it will in the derived rules you are currently
interested in, I believe).
I'm guessing that's not a well understood fact, that the HOL4 manual
Description is giving informal mathematical proofs. Perhaps you can look at
some of my "paragraph" proofs below and tell me how they compare to Description
two column proofs.
--
Best,
Bill
An informal mathematics description of HOL Light
I contend that the only way for humans to understand formal proofs (e.g. in the
proof assistant HOL Light) is through the informal mathematics studied by pure
mathematicians. I contend that formal proofs can not be understood by humans
formally. Partly I mean that formal proofs create mathematical rigor by
weeding out the errors that humans are so prone to make, and not because our
formal machinery is by itself more rigorous. Now a perfectly rigorous
description of HOL Light is given by the HOL Light source code, but we are
probably not smart enough to read it and understand it, and we can not
communicate it to each other without using informal mathematics. In
particular, the HOL Light on-line documentation is essentially written in
informal mathematics. Most of what I write below holds for any HOL (HOL4, HOL
Zero, Isabelle and ProofPower), and the best documtation seems to be from HOL4,
which I'll refer to when I can. All HOLs seem to have different axioms, and
I'll use the HOL Light axioms. I think it will be obvious to everyone that my
informal mathematical description actually describes HOL Light, but I do not
know how to prove this rigorously, or even how to state such a result. HOL
Light is a computer program in which the phrase ``for all terms t'' never
arises, so perhaps there is an unsolvable ``apples vs oranges'' problem.
Thanks to Mark Adams, Rob Arthan Konrad Slind, and Vladimir Voevodsky for some
helpful conversations.
Knowledge of the lambda calculus (LC) is probably essential, e.g. found in
Barendregt's book. For instance it's very helpful to understand that
beta-reduction is well defined on alpha-equivalence classes. This is proved by
DeBruijn trees, which replaces variables with numbers. In HOL we are using
typed LC, rather than Barendregt's untyped LC, but the proofs are the same.
We have a set of types TYPE freely generated by variables and type constants,
which can be specified by the user (with new_type in HOL Light). Initially we
have only three type constants, the types bool and ind, and the type function
->, so for two types α and β, we have the type α->β.
We have a set of terms TERM which is defined inductively as a disjoint union of
variables, constants, lambda abstractions, and function applications by the
following rules. Every term t has a type, say α, and this is indicated by the
type annotation t:α. A variable is an identifier together with a type x:α.
Constants can be defined by the user (with new_constant in HOL Light).
Initially we have only the constant = of type α->α->bool. Given a variable x
of type α and term t of type β, we have the lambda abstractions λx. t of type
α->β. Given a term f of type α->β and a term a of type α, we have the function
application f a. So we can describe our inductively defined set TERM in BNF
form as on p 15 of the HOL4 manual Logic
VAR ::= <ident>:type
TERM ::= VAR | CONSTANT | λ VAR. TERM | TERM TERM
Note that even though TERM is a disjoint union of four subsets, we will prove
many theorems of the sort term1 = term2, where term1 and term2 belong to
different subsets. As we'll see later, this is primarily due to
beta-reduction, which tells us how to evaluate a function application. The
point to understand now is that equal terms are not identified with each other.
The theorem term1 = term2 will not mean that term1 and term2 become the same
element of the set TERM. The fact that = has this technical HOL Light meaning
takes some getting used to. We have to forego the usual usage of ``replacing
equals with equals''.
An equality-related difficulty is given by the HOL Light parser, which
systematically replaces many readable terms with their actual equivalents. The
parser e.g. replaces
∀x. t with (∀)(λx. t),
p ∧ q with (∧) p q
⇔:bool->bool->bool with =:bool->bool->bool.
Let us not strain ourselves by arguing that e.g. p ∧ q is ``equal'' to (∧) p q
and so can be substituted for the other. Let us instead say that the text
below is to be subjected to a parser which will systematically replace the
readable forms with their HOL Light equivalents prior to us reading the text.
So any p ∧ q below is to replaced with the correct (∧) p q etc.
A sequent is of the form
A |- t
where A is a finite set of terms of type bool, and t is a term of type bool.
Let's call SEQUENT the set of sequents.
SEQUENT has a subset THEOREM, whose elements are called theorems. The subset
THEOREM is defined inductively by the 10 HOL Light primitive inference rule
functions REFL, TRANS, MK_COMB, ABS, BETA, ASSUME, EQ_MP, DEDUCT_ANTISYM_RULE,
INST_TYPE and INST, new_definition and new_axiom. It would take some work to
construct this subset THEOREM, but I'll assume this is understood, and now list
the informal mathematical theorems which follow from these deductive rules.
Notational Remark: I'll refer indiscriminately to all of the ``basic'' informal
mathematical theorem as axioms, on the grounds that it's enough of a challenge
to distinguish between the two uses of the word theorem, elements of THEOREM,
and informal mathematical theorems proved about the set THEOREM. The first 9
primitive inference rules yield the axioms
Axiom REFL:
For any term t, we have the theorem
|- t = t
Axiom TRANS:
Take any terms t1, t2, t2' and t3 with t2 and t2' alpha-equivalent and assume
we have theorems
A1 |- t1 = t2 A2 |- t2' = t3
Then we have the theorem
A1 ∪ A2 |- t1 = t3
Axiom MK_COMB:
Take any terms f, g, x and y and assume we have theorems
A1 |- f = g A2 |- x = y
Then we have the theorem
A1 ∪ A2 |- f x = g y
Axiom ABS:
For any variable x and any theorem
A |- t1 = t2
we have the theorem
A |- (λx.t1) = (λx.t2)
Axiom BETA:
For any variable x and any term t, we have the theorem
|- (λx. t) x = t
Axiom ASSUME:
For any term t, we have the theorem
{t} |- t
Axiom EQ_MP:
Take any terms t1, t1' and t2 with t1 and t1' alpha-equivalent and assume we
have theorems
A1 |- t1' ⇔ t2 A2 |- t1
Then we have the theorem
A1 ∪ A2 |- t2
Axiom DEDUCT_ANTISYM_RULE:
For any two theorems
A |- p B |- q
we have the theorem
(A - {q}) ∪ (B - {p}) |- p ⇔ q
Axiom INST_TYPE:
For any theorem
A |- t
and any list of type variables tv1,...,tvn and any list of types ty1,...,tyn,
we have the theorem
A[ty1,...,tyn/tv1,...,tvn] |- t[ty1,...,tyn/tv1,...,tvn]
obtained by systematically replacing all instances of each type variable tvi by
the corresponding type tyi in both assumptions and conclusions.
Let's discuss alpha-equivalence before stating the last axiom INST. Take any
term t and any list of variables x1,...,xn and terms t1,...,tn such that xi and
ti have the same type. Then
t[t1,...,tn/x1,...,xn]
means any term obtained by replacing the free occurrences of each xi with ti,
performing alpha-equivalences on bound variables to avoid variable capture
errors. So t[t1,...,tn/x1,...,xn] is not well-defined, as there are many ways
to perform these alpha-equivalences, but Barendregt proves that
t[t1,...,tn/x1,...,xn] is well-defined up to alpha-equivalence. These
alpha-equivalent term are all = by
Theorem ALPHA:
Take any two terms tm1 tm2 that are alpha-equivalent. Then we have the theorem
|- tm1 = tm2
For any theorem
A |- t
and any term t' which is alpha-equivalent to t, we have the theorem
A |- t'
Proof:
By axiom REFL we have the theorems
|- tm1 = tm1 |- tm2 = tm2
By axioms TRANS we have our first theorem
|- tm1 = tm2
Now assume we have a theorem
A |- t
with alpha-equivalent terms t and t'. By the first part we have the theorem
|- t = t'.
Applying axiom EQ_MP to these two theorems, we have the theorem
A |- t'
since A ∪ ∅ = A.
\qed
Now we state the last axiom given by the primitive inference rules.
Axiom INST:
Take any theorem
A |- t
and any list of variables x1,...,xn and terms t1,...,tn such that xi
and ti have the same type. Then we have the theorem
A |- t[t1,...,tn/x1,...,xn]
Note that by theorem ALPHA that even though t[t1,...,tn/x1,...,xn] is only
well-defined up to alpha-equivalence, we have the theorem for all such versions
of versions of t[t1,...,tn/x1,...,xn] if we have the theorem for a single
version.
The next basic theorems we'll look at are the ``axioms'' given by the
occurrences of new_basic_definition in bool.ml defining the logical constants
∀, T, F, ∧, ⇒, ¬, ∨ and ∃.
Axiom FORALL_DEF:
We have the theorem
|- (∀) = λP:A->bool. P = λx. T
Axiom T_DEF:
We have the theorem
|- T = ((λp:bool. p) = (λp:bool. p))
Axiom F_DEF:
We have the theorem
|- F = ∀p:bool. p
Axiom AND_DEF:
We have the theorem
|- (∧) = λp q. (λf:bool->bool->bool. f p q) = (λf. f T T)
Axiom IMP_DEF:
|- (⇒) = λp q. p ∧ q ⇔ p
Axiom NOT_DEF:
We have the theorem
|- (¬) = λp. p ⇒ F
Axiom OR_DEF:
We have the theorem
|- (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
Axiom EXISTS_DEF:
We have the theorem
|- (∃) = λP:A->bool. ∀q. (∀x. P x ⇒ q) ⇒ q
In HOL Light, ∀ and ∃ are binders, so as explained above, every occurence in
the text here of ∀x. t is to replaced automatically by (∀)(λx. t) prior to us
having to think about it. Similarly ∧, ⇒, and ∨ are HOL Light infixes, so
every occurence of p ⇒ q is to be replaced automatically by (⇒) p q.
Now we begin proving theorems, starting with general beta-conversion.
Theorem BETA_CONV:
For any variable v and terms bod and arg, we have the theorem
|- ((\v. bod) arg) = bod[arg,v]
Proof:
By axiom BETA, the sequent
|- ((\v. bod) v) = bod
is a theorem. Now apply axiom INST with [arg,v] and this theorem.
\qed
From the code of AP_TERM, AP_THM, SYM, ALPHA and ALPHA_CONV in equal.ml we
easily glean simple proofs of the four theorems
Theorem AP_TERM:
For all terms f, x and y and for all theorems
A |- x = y
we have the theorem
A |- f x = f y.
Proof:
By axiom REFL, we have the theorem
|- f = f.
Now apply axiom MK_COMB to this theorem and our assumption, noting that
A ∪ ∅ = A.
\qed
Theorem AP_THM:
For all terms f, g and x and for all theorems
A |- f = g
we have the theorem
A |- f x = g x.
Proof:
Apply axiom MK_COMB to our assumption and the axiom REFL theorem |- x = x.
\qed
Theorem SYM:
For all terms l and r and for all theorems
A |- l = r
we have the theorem
A |- r = l.
Proof:
For precision, let α be the type of l, which is also the type of r. Applying
=:α->α->bool to our assumption and using theorem AP_TERM, we have the theorem
A |- (= l) = (= r)
By axiom REFL we have the theorem
|- (l = l).
Applying axiom EQ_MP to these two theorems, we have the theorem
A |- (= l) l = (= r) l
since A ∪ ∅ = A. We rewrite this as the theorem
A |- (l = l) = (r = l).
By our REFL theorem above, axiom EQ_MP and A ∪ ∅ = A, we're done.
\qed
The next result follows, which we note for completeness, immediately from
theorem ALPHA and the definition of alpha-equivalence, although below we will
only use theorem ALPHA.
Theorem ALPHA_CONV:
For any abstractions λx. t and any variable y of the same type as x which does
not occur free in t, we have the theorem
|- (λx. t) = (\y. t[y/x]).
Now we prove the first results of bool.ml.
Theorem TRUTH:
We have the theorem
|- T
Proof:
By axiom T_DEF and theorem SYM have the theorem
|- ((λp:bool. p) = (λp:bool. p)) = T
By axiom REFL we have the theorem
|- (λp:bool. p) = (λp:bool. p)
Applying axiom EQ_MP to these two theorems, we are done.
\qed
Our next result follows immediately from theorem SYM, theorem TRUTH and axiom
EQ_MP.
Theorem EQT_ELIM:
For all terms tm and all theorems
A |- tm ⇔ T
we have the theorem
A |- tm.
The converse takes a little more work.
Theorem EQT_INTRO:
For all terms tm and all theorems
A |- tm
we have the theorem
A |- tm ⇔ T.
Proof:
By axiom ASSUME and theorem TRUTH we have the theorems
{tm} |- tm
|- T
so by axiom DEDUCT_ANTISYM_RULE we have the theorem
{tm} |- tm ⇔ T.
By axiom ASSUME applied to tm ⇔ T and theorem EQT_ELIM, we have the theorem
{tm ⇔ T} |- tm.
Applying axiom DEDUCT_ANTISYM_RULE to these "converse" theorems, we have the
theorem
|- tm ⇔ (tm ⇔ T)
Applying axiom EQ_MP to this and our assumption, we are done.
\qed
Note this gives a proof 2 lines shorter than the version in bool.ml
let EQT_INTRO th =
let th1 = DEDUCT_ANTISYM_RULE (ASSUME (concl th)) TRUTH in
let th2 = EQT_ELIM(ASSUME(concl th1)) in
let pth = DEDUCT_ANTISYM_RULE th2 th1 in
EQ_MP pth th;;
which I checked actually works.
Theorem CONJ:
Assume we have two two terms p and q and two theorems
A1 |- t1
A2 |- t2
Then we have the theorem
A1 ∪ A2 |- t1 ∧ t2
Proof:
Choose a variable fof type bool->bool->bool which is not free in t1 or t2.
By our assumptions and theorem EQT_INTRO, we have the theorems
A1 |- t1 ⇔ T
A2 |- t2 ⇔ T
Applying theorem AP_TERM with f to the first gives the theorem
A1 |- f t1 ⇔ f T
Applying axiom MK_COMB to this and the previous theorem yields
A1 ∪ A2 |- f t1 t2 ⇔ f T T
By axiom ABS, we have the theorem
A1 ∪ A2 |- (λf. f t1 t2) ⇔ (λf. f T T)
Apply theorem AP_TERM twice to axiom AND_DEF with first t1 and then t2 to
obtain the theorem
|- (∧) t1 t2 = (λp q. (λf:bool->bool->bool. f p q) = (λf. f T T)) t1 t2
Applying theorem BETA_CONV twice and axiom TRANS twice, we have the theorem
|- t1 ∧ t2 = ((λf. f t1 t2) ⇔ (λf. f T T))
By theorem SYM, axiom EQ_MP and our A1 ∪ A2 theorem above, we're done.
\qed
Theorems CONJ, TRUTH and EQT_INTRO immediately gives us our first AND "truth
table" result:
Theorem CONJ_EZ:
|- T ∧ T ⇔ T
The next two results comprise something of a converse of theorem CONJ, and rest
on the well-known LC facts that an ordered pair (x, y) can be implemented as
the abstraction (λf. f x y), and applying an ordered pair to (λp q. p) (resp.
(λp q. q)) gives the projection on the first (resp. 2nd) coordinate.
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, axiom AND_DEF theorem and axiom TRANS, we have
|- (∧) = (λ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 axiom AND_DEF with first l and then r, we have
|- (∧) 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 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 theorem equation and the term (λp q. p) yields
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
By the same argument using (λp q. q) instead (λp q. p), we have
Theorem CONJUNCT2:
Let l and r be terms and A be a set of assumptions such that
A |- l ∧ r. Then A |- r.
Now we turn to ⇒.
Theorem MP:
Given two terms t1 and t2, and two sets of assumptions A1 and A2, assume we
have theorems
A1 |- t1 ⇒ t2 and A2 |- t1.
Then we have the theorem
A1 ∪ A2 |- t2.
Proof:
Choose variables p' and q' of type bool that are not free in either t1 or t2.
By axiom IMP_DEF and theorem ALPHA we have the theorem
|- (⇒) = (λp' q'. p' ∧ q' ⇔ p')
Applying theorem AP_THM twice to this theorem, using first t1 and then t2, we
have the theorem
|- (⇒) t1 t2 = (λp' q'. p' ∧ q' ⇔ p') t1 t2
Using theorem BETA_CONV and axiom TRANS twice each, we have the theorem
|- t1 ∧ t2 = (t1 ∧ t2 ⇔ t1).
By our assumption theorem, axiom MP and A ∪ ∅ = A, we have the theorem
A |- t1 ∧ t2 ⇔ t1.
By theorem EQT_INTRO and axiom TRANS, we have the theorem
A |- t1 ∧ t2 ⇔ T
and by theorem EQT_ELIM, we have the theorem
A |- t1 ∧ t2.
By theorem CONJUNCT2, we are done.
\qed
Theorem DISCH:
For any term u and any theorem
A |- t
we have the theorem
A - {u} |- u ⇒ t.
Proof:
Choose variables p' and q' of type bool that are not free in either u or t. By
axiom IMP_DEF and theorem ALPHA we have the theorem
|- (⇒) = (λp' q'. p' ∧ q' ⇔ p')
Applying AP_THM to this theorem twice using the terms t and u yields the theorem
|- (⇒) u t = (λp' q'. p' ∧ q' ⇔ p') u t
Applying theorem BETA_CONV and axiom TRANS twice each yields the theorem
|- (u ⇒ t) = (u ∧ t ⇔ u)
Applying theorem REFL yields the theorem
|- (u ∧ t ⇔ u) = (u ⇒ t)
By axiom ASSUME we have the theorems
|- u |- u
|- u ∧ t |- u ∧ t
Apply theorem CONJ to this theorem and our assumption theorem to the first, and
apply theorem CONJUNCT1 to the second. We have the theorems
A ∪ {u} |- u ∧ t
{u ∧ t} |- u
Applying axiom DEDUCT_ANTISYM_RULE to these theorems yields the theorems
A - {u} |- u ∧ t ⇔ u
Now apply axiom EQ_MP to the theorems of the last two paragraphs.
\qed
The converse is nicely proved in sec 2.3.2 of Description, with the same proof
as bool.ml.
Theorem UNDISCH:
For any implicative theorem
A |- t1 ⇒ t2
we have the theorem
A ∪ {t1} |- t2
Proof:
By axiom ASSUME we have the theorems
|- t1 |- t2
Now apply Theorem MP to the assumption theorem and this theorem.
\qed
Theorem IMP_ANTISYM_RULE:
For any two theorems
A1 |- t1 ⇒ t2 A2 |- t2 ⇒ t1, we have the theorem
A1 ∪ A2 |- t1 ⇔ t2
Proof:
Applying theorem UNDISCH to our assumption theorems yields the theorem
A2 ∪ {t2} |- t1 A1 ∪ {t1} |- t2
By axiom DEDUCT_ANTISYM_RULE, we're done.
\qed
Theorem EQ_IMP_RULE:
For any terms t1 and t2 of type bool and any theorem
A |- t1 ⇔ t2
we have the theorems
A |- t1 ⇒ t2 A |- t2 ⇒ t1
Proof:
\qed
Applying axiom ASSUME to the terms t1 ⇔ t2 and t1 yields the theorems
{t1 ⇔ t2} |- t1 ⇔ t2
{t1} |- t1
Applying axiom EQ_MP to these theorems yields the theorem
{t1, t1 ⇔ t2} |- t2
Applying theorem DISCH twice yields the theorem
|- (t1 ⇔ t2) ⇒ t1 ⇒ t2
Applying axiom EQ_MP to our assumption theorem and this theorem yields the
theorem
A |- t1 ⇒ t2
This proves the first part our result.
Applying theorem SYM to to our assumption theorem yields the theorem
A |- t2 ⇔ t1
Applying the first part our result to this theorem, we're done.
\qed
Theorem IMP_TRANS:
Take any terms t1, t2, and t3 of type bool, and assume we have theorems
A1 |- t1 ⇒ t2 A2 |- t2 ⇒ t3
Then we have the theorem
A1 ∪ A2 |- t1 ⇒ t3
Proof:
By an argument similar to the proof of theorem EQ_IMP_RULE, axioms ASSUME and
EQ_MP yield the theorem
{t1, t1 ⇒ t2, t2 ⇒ t3} |- t3
Applying theorem DISCH three times yields the theorem
|- (t2 ⇒ t3) ⇒ (t1 ⇒ t2) ⇒ t1 ⇒ t3
Applying theorem MP twice using our assumption theorems, we're done.
\qed
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
