[isabelle] Some corrections and amendments
Dear Andrei Popescu, dear Ramana Kumar,
dear Members of the Research Community,
As a matter of fairness, I have to correct one of my earlier statements.
Andrei Popescu correctly pointed out at
that neither "being based on a meta-logic" (i.e., a logical framework) nor
"featuring a natural deduction system" creates a problem.
There has been a misunderstanding on my part.
However, I have to say that Paulson's definition of the turnstile as a symbol
for the predicate "hfthm" in
"inductive hfthm :: "fm set => fm => bool" (infixl "â" 55)"
somewhere hidden in the proof files without being prominently announced in his
articles is strongly misleading and inevitably creates misinterpretations.
Usually (such as in [Andrews, 2002]), the turnstile is used to indicate the
provability of a theorem of the logic in which the proof is undertaken, not the
provability of theorems of the embedded logic. Also, for the predicate of
provability of theorems of the embedded (represented, formalized) logic, a
label is usually used, not a symbolic notation (e.g., Goedel uses "Bew" - for
"beweisbare Formel", the German expression for "provable formula" -, and
O'Connor in Coq uses "SysPrf"). Moreover, without some short introduction to
the notation and the type system it is nearly impossible to analyze the proof
in detail unless one has advanced experience with the Isabelle proof assistant,
leaving aside that with a logical framework there are not only three, but four
language levels involved, all of which one would ideally need to understand in
order to verify the proof.
The result of the formal proof
~Bew(g) /\ ~Bew(not g)
can be interpreted in the sense that it is possible to construe a formula with
the form of a sentence (i.e., a boolean-valued well-formed formula with no free
variables) neither provable nor refutable.
Nevertheless, the claim of "incompleteness" depends on a philosophical
One who shares the semantic view (model theory) will conclude that there is a
meaningful (and true) sentence that is neither provable nor refutable, and will
call the discrepancy between syntax and semantics "incompleteness".
But one who shares the syntactic view will conclude that it is possible to
create a meaningless formula which has the form of a syntactically correct
sentence (similar, in natural language, to a grammatically correct but
meaningless statement like "mathematics is liquid").
Concerning the two objections of Ramana Kumar at
the first one was a misunderstanding clarified at
But the second, Ramana Kumar's claim that type "tm" can be defined like type
"nat", is not correct. Andrews' logic Q0, being an improved variant of Church's
original simple type theory, only allows the types iota (i) and omicron (o),
and combinations of them.
Andrews' type "nat" is such a combination ( nat := (o(oi)) ). On the contrary,
Paulson's type "tm" is an inductively defined type, which is not possible in Q0:
"nominal_datatype tm = Zero | Var name | Eats tm tm"
In an e-mail, Paulson basically argued that there should be ways to introduce
further types (instead of restricting oneself to combinations of 'i' and 'o').
This is, of course, correct, but doesn't justify the specific mode of type
introduction used here, namely the Backus-Naur form (BNF). The BNF was designed
to specify formal grammars in computer science, but (mathematical) types are
objects that must have certain logical properties, such as being non-empty.
Thus the introduction of additional mathematical types should be subject to
proof, and not a matter of mere declaration via the BNF.
With some more knowledge about the concept of the current proof assistants, I
can answer Ramana Kumar's question at
concerning the motivation of my project announcement at
from his perspective now.
Current proof assistants seem to follow the semantic approach, in which the
theory is distinguished from a specific linguistic (formal) formulation, or use
of model theoretic notions like satisfiability is made. For example, in
Isabelle there are implementations of both axiomatic set theory (Isabelle/ZF)
and type theory (Isabelle/HOL), but neither one is explicitly preferred, and
the question of which is more adequate for representing mathematics is not even
raised. (Although, unlike in informal mathematics, in formalized proofs type
theory seems to prevail, e.g., within Isabelle the logic Isabelle/HOL, a
polymorphic version of Church's simple type theory.)
If one follows the syntactic approach, then there is a desire for something
like the ideal formulation or the natural language of formal logic and
mathematics. The main criterion is expressiveness [cf. Andrews, 2002, p. 205],
or, vice versa, the reducibility of mathematics to a minimal set of primitive
rules and symbols. If we leave away for a moment the restrictions of Q0 of
still being a formulation of simple type theory (i.e., without type variables
and dependent types), all of formal logic and mathematics can be expressed on
the basis of only a "single rule of inference (substitution, from which the
rule of modus ponens is derived)" and "only two basic types (individuals and
truth values) and only two basic constants (identity/equality and its
Paulson argued that natural deduction is far superior to Hilbert-style systems
for automated proof. This is, of course, correct, since Hilbert-style
metatheorems become symbolically representable in natural deduction as regular
theorems (and not just metatheorems), but this only reflects the engineer's
perspective with the pragmatic aim of quickly obtaining proofs. For the
philosopher it is not proof automation but expressiveness that is the main
criterion, such that the method with the least amount of rules of inferences,
i.e., a Hilbert-style system, is preferred, and all other rules become derived
Hence, from the perspective of the syntactic view, Andrews' elegant logic Q0 is
the natural point to start with. Overcoming its restrictions by extending it to
a polymorphic (with type variables) and dependent type theory (with dependent
types) is the motivation of my logic R0, which I hope to be able to publish
soon. A preliminary excerpt with some definitions and a sample proof is
available online at
This archive was generated by a fusion of
Pipermail (Mailman edition) and