Email Gateway (Aug 18 2022 at 20:25): Email Gateway (Aug 18 2022 at 20:25):From: Luke Serafin <lserafin@andrew.cmu.edu>
Mr. Richter,
It might be helpful to look at a mathematical logic book which develops
HOL rather than set theory as the foundation of mathematics, such as Peter
Andrews' _An Introduction to Mathematical Logic and Type Theory: To Truth
Trough Proof_ (let us abbreviate this TTTP; note that type theory is
essentially another term for HOL). There we find (remark after the proof
of theorem 5402) that the primitive version of HOL which the author calls
Q0 is a conservative extension of FOL. The basic logic used in Isabelle
and HOL Light is also a conservative extension of FOL (Coq uses
constructive logic which is more restrictive than classical logic; I don't
know whether its basic logic is a conservative extension of constructive
predicate logic). Any stronger HOL system (e.g. Q0^\infty from the book
mentioned above; this system is adequate for the formalization of a very
significant portion of mathematics), can be viewed as this basic HOL
together with a set of axiom schemata. Choose such a stronger HOL system,
and denote its set of axioms by H. Then a sentence A is a theorem of this
stronger system iff there exists a finite subset H0 of H such that H0 |- A
(because proofs are finite, at least in this context). Note that the
turnstile means provable from basic HOL, e.g. Q0. This is equivalent to |-
B --> A, where B is the conjunction of all elements of H0. Hence any
theorem of any (recursively axiomatized) version of HOL can be viewed as a
theorem of a conservative extension of FOL. Furthermore, we could
introduce type predicates and axioms about them into FOL and thereby fully
import Q0 into FOL (this construction is elementary but tedious), which by
the above argument means that we can effectively translate any HOL system
into FOL. In this sense, you are right that HOL does not go beyond FOL.
However, the notion of proof is completely different between FOL and HOL.
In the second paragraph of the remark referred to above (TTTP p. 243), we
find quoted a result of Statman that "the minimal length of a proof in
first-order logic of a wff of first-order logic may be extraordinarily
longer than the minimal length of a proof of the same (as in, translated
canonically) wff in second-order logic." The paper referred to may be
found here: <http://deepblue.lib.umich.edu/handle/2027.42/22467>, I have
not studied it carefully but do know that the function from n to the
maximal m such that m is a minimal-length FOL proof of a HOL wff which has
a proof of length n asymptotically grows at least as fast as a
hyper-exponential function. Thus, using HOL wffs and rules of inference is
of great practical advantage when doing proofs with a computer. If we
insist on everything being done in FOL, we could change our definition of
proof to allow derived rules of inference to be used directly, and then
derive translated versions of HOL rules of inference for some translation
of HOL into FOL. However, it is practically much simpler to just think in
terms of using HOL directly.
Regarding set theory, ZF is strictly stronger than Q0^\infty, but its lack
of intrinsic types makes proof searches in ZF much more difficult than
those in Q0^\infty. Thus it is often advantageous to work with a typed HOL
theory than directly with ZF. Isabelle allows the dynamic addition of new
axioms, so if we ever need to go beyond Q0^\infty (say), we can just add
whatever new facts we need as axioms, and perhaps prove the validity of
these axioms in ZF if we believe that is necessary. Also, though ZF is
normally considered to be based on FOL, there is no danger of introducing
a contradiction if we conservatively extend its background logic, and so
we can just as easily consider ZF in the context of HOL (e.g.
Isabelle/ZF). This brings with it the possibility of gaining the
advantages of types and HOL's much shorter proofs for ZF (e.g. we can
define type-parameterized isomorphism predicates between types with
associated operations and sets with associated operations, and use these
to port theorems between HOL and ZF within this unified system).
Hopefully this clarifies things somewhat, let me know if you have any
questions about what is written above.
Sincerely,
Luke Serafin
Last updated: Apr 26 2024 at 01:06 UTC