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



> 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
> 
> 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.
> 
> 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,
> 
> Andreas
> 
> 
> 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...
>>> 
>>> Cheers,
>>> 
>>> Andreas
>>> 
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.