[isabelle] Isabelle design decisions, natural deduction vs. Hilbert-style, model theory vs. dependent type theory, and the class of all sets
Although this mailing list is dedicated to the proof assistant, some basic
issues appear relevant as they are implicit to the design of Isabelle, and for
this reason should be mentioned in the documentation, too.
For example, Isabelle seems to follow the semantic approach (model theory) with
its independence of specific axiomatizations (particular linguistic
formulations), resulting in a plurality of (object) logics, which is
unsatisfactory to some, including myself, as I follow the syntactic approach
and believe in the existence of an optimal formulation, of a natural
Also, many other major decisions, such as opting for natural deduction or the
non-standard use of the turnstile symbol (either in the "system infrastructure
for local context management" or freely definable as in Paulson's Goedel
proof), should at least be shortly explained in some form of introduction that
is easy to find, as the lack of information causes misunderstanding.
Of course, natural deduction is better suited for automation, but not every
logician or mathematician has a long history of automated theorem proving, such
that for one trying to understand the concept of the software from scratch, it
is tedious to have to search older articles even from as far back as the 1980s
in order to follow the major design decisions of the software, as, for example,
published in 1989: "Natural deduction is far superior for automated proof."
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (p. 3)
In the same sense, a logician or mathematician may not be familiar with the
concept of a logical framework (also called "meta-logic") of computer science,
which would make a short introduction to the terminology ("meta-logic", "object
logics") desirable, as it easily leads to confusion with metamathematical
notions, may it be Hilbert-style metatheorems or the arithmetization of proofs,
or notions of the semantic approach, where the evaluation is performed at a
meta-level. A short reference for the type system of both meta-logic and object
logics would do away with the effort of having to scan hundreds of pages of
If the focus is expressiveness instead of automation, axiomatic (Hilbert-style)
deductive systems (e.g., Andrews' Q0) are the natural choice. So I definitely
agree with the statements made by Andreas RÃhler and Joachim Breitner about
"natural deduction" being rather artificial, and a misnomer which should be
replaced by "Gentzen-style" systems.
Concerning model theory, new light is shed on the field when dependent type
theory becomes available. In traditional model theory, the syntax (the formal
language, the theory) is expressed in a sphere separated from its semantics
(the interpretation or evaluation) as well as the statement that a certain
model satisfies the theory. In dependent type theory, the latter statement can
be expressed within (!) the logic in which the proof is undertaken, for
example, that (o, XOR) is a group consisting of the set (type) of truth values
('o'), and the operation XOR, can be expressed as the proven theorem
Grp o XOR
formed simply by lambda-application as wff 6955 at
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 416)
where "Grp" is defined (p. 359; note the prefix notation) on the basis of the
group properties of associativity, identity element, and inverse element:
:= Grp [Îg.[Îl.(â GrpAss (â g [Îe.(â GrpIdy GrpInv)]))]]
Since in R0 every non-empty set becomes a type, no language restrictions apply,
and any (non-empty) set can be the first argument of the binary predicate
"Grp". The first argument has type "tau" (Ï), which is the type of types.
Hence, from the perspective of dependent type theory, model theory was the only
possibility of expressing a mathematical fact in a deficient way (outside of
the logic, "outward"), while now, with dependent type theory, it can be
expressed within the logic ("immanent"), i.e., using the means of the language
in which the proof is undertaken, yielding a higher expressiveness.
A stronger variant of type theory than the current Isabelle/HOL, which is just
a polymorphic version of Church's simple type theory, would be desirable.
"The class of all sets, V, cannot be a set without admitting Russell's Paradox."
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/logics-ZF.pdf (p. 20)
is incorrect, as for Russell's Paradox not only self-reference, but also
negation is required ("the set of all sets that are NOT members of
themselves"). The philosophical antinomy always has both properties
(self-reference and negativity) in its main form.
The set of all sets (the universal class/set V) is usually referred to in the
context of Cantor's paradox, saying that the power set of the set of all sets
must have a larger cardinality, although, at the same time, it must be a subset
of the set of all sets, and therefore have a smaller or equal cardinality.
In dependent type theory, due to its subtle type system, it is easy to
demonstrate that neither Russell's Paradox nor Cantor's paradox can be
expressed, since both of them violate type restrictions [cf. Kubota, 2015, pp.
24 f.]. Nevertheless, it is possible (in the dependent type theory R0) to
construe a universal set V without, as I believe, rendering the system
inconsistent, cf. "Definition of the universal set" at
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 358)
R0 also has the universal type "omega" (Ï), which replaces the primitive type
for individuals "iota" ('i') used by Church and Andrews (and which is, in some
sense, identical with the universal set V).
Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18,
2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5
011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See:
Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356-364, pp. 411-420, and
pp. 754-755). Available online at
(January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c
> Am 12.07.2016 um 09:43 schrieb Andreas RÃhler <andreas.roehler at easy-emacs.de>:
> Hi Lawrence,
> just to give an example: please consider from
> Which version of axiomatic set theory?
> The class of all sets,~$V$,cannot be a set without admitting Russell's Paradox.
> And above:
> ZF does nothave a finite axiom system because of its Axiom Scheme of Replacement.
> This makes it awkward to use with many theorem provers, since instances
> of the axiom scheme have to be invoked explicitly. Since Isabelle has no
> difficulty with axiom schemes, we may adopt either axiom system.
> Probably you will agree saying "we may adopt either axiom system" --while true, as it's all about models-- doesn't sound satisfying.
> There will be no reliable system, if the basement isn't certain.
> With all due respect,
> On 11.07.2016 15:08, Lawrence Paulson wrote:
>> Iâm afraid your question is off topic for this mailing list. Please ask questions directly connected with Isabelle. There are plenty of forums where you can discuss the philosophy of mathematics.
>> Larry Paulson
>>> On 11 Jul 2016, at 13:40, Andreas RÃhler <andreas.roehler at easy-emacs.de> wrote:
>>> Hi all,
>>> the Russel's Paradox constitutes a surprise:
>>> Doesn't it ignore the Subject-Object-Relation of all statement?No definition might define it's own definition. As someone upheld a recursive function here: Any recursive function must be defined before calling it, the recursion is no defining-process, it comes afterwards.
>>> Kind of a tautological error?
>>> As far as Cantor is the guilty, well, Russell should have rejected Cantors exaggeration...
This archive was generated by a fusion of
Pipermail (Mailman edition) and