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

mathematical language.

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

documentation.

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 statement

"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).

Ken Kubota

References

Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18,

2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5

45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50

011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See:

http://dx.doi.org/10.4444/100.10

Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356-364, pp. 411-420, and

pp. 754-755). Available online at

http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf

(January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c

9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783

3d1047d1831bc357eb57b263b44c885b.

____________________

Ken Kubota

doi: 10.4444/100

http://dx.doi.org/10.4444/100

*Post by Andreas Röhler*Hi Lawrence,

just to give an example: please consider from

Isabelle2016/src/Doc/Logics_ZF/document/ZF.tex

Which version of axiomatic set theory?

[...]

The class of all sets,~$V$,cannot be a set without admitting Russell's Paradox.

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,

Andreas

*Post by Lawrence Paulson*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

*Post by Andreas Röhler*Hi all,

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...

Cheers,

Andreas