Dear Mario,
In order to preserve the font and layout information required to display
the formulae properly, let me copy to the Metamath list.
> Am 05.06.2018 um 01:22 schrieb Mario Xerxes Castelán Castro
> <marioxcc...@yandex.com>:
>
> On 02/06/18 09:33, Ken Kubota wrote:
>> Set theory (e.g., ZFC, the variant of Zermelo set theory in use today)
>> takes a very different approach by giving the class status by default,
>> and giving the set status only to those constructions often used.
>> Compared with the type theoretic approach this means that the set theoretic
>> solution is to simply forbid all reasoning first, and then to allow only
>> certain
>> constructions (a positive list).
>> The result (ZFC) is a not systematic solution of the problem (Russell's
>> antinomy),
>> but a preliminary solution based on the explored fields of mathematics at
>> that time.
>
> ZFC is the formalization of the intuitive concept of the cumulative
> hierarchy of sets. It is not just a collection of ad-hoc axioms.
The word "intuitive" is the keyword here, exposing the concept (the cumulative
hierarchy of sets) as a subjective one.
But the criterion should be only the original problem, i.e., Russell's paradox
(the classical philosophical antinomy).
Only this (or maybe other forms of paradoxes) should be avoided,
but any whitelist inevitably rules out much more, resulting in an arbitrary list
of axioms (from a systematic point of view).
> There is a mental trick at play with type theories. They only seem to be
> more natural than ZFC because the domain of quantification is hidden by
> default in many proof assistants based on type theories. If you did the
> same with ZFC, it would likewise be perceived as natural. If you build a
> proof assistant for set theory you _can_ introduce syntactical sugar for
> restricted quantification as in type theory and automatic “typing” (sets
> used as the quantification domain are inferred instead of being made
> explicit).
This holds only for type theory _without_ explicit quantification over types
(e.g., HOL, Q0),
but not for type theory _with_ explicit quantification over types (e.g., R0).
For example, while the principle of the excluded middle (tertium non datur)
in Q0 is expressed as Axiom 1
[gT ∧ gF] = ∀x[gx]
[gοοTο ∧ gοοFο] = ∀xο[gοοxο]
( [Andrews, 2002, p. 213] or
https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu
<https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu> )
in R0 it is expressed as
[gT ∧ gF] = ∀ox[gx]
[gοοTο ∧ gοοFο] = ∀o(o\3)τoτxο[gοοxο]
– Note that the type o is specified at the term level here, and not only
at the type level (as type information) –
( http://www.owlofminerva.net/files/formulae.pdf
<http://www.owlofminerva.net/files/formulae.pdf>, p. 354 )
since the universal quantifier is defined with _type abstraction_ in R0, as
[λtτ .[λpot.(=o(ot)(ot)[λxt.To]pot)o](o(ot))]
( http://www.owlofminerva.net/files/formulae.pdf
<http://www.owlofminerva.net/files/formulae.pdf>, p. 359 )
where t ranges over the domain of types (tau: the type of types).
Binding over type variables with lambda creates a link between the term level
and the type (subscript) level, which makes type (domain) information explicit.
A special example is the Quantified Axiom of Choice (without a free type
variable)
∀tτ[AC]
or – in more explicit notation with lambda –
∀τ[λtτ.AC]
where the domain of the variable t is the type of types τ:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-March/msg00051.html
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-March/msg00051.html>
http://www.kenkubota.de/files/ac_instantiation.r0.out.pdf
<http://www.kenkubota.de/files/ac_instantiation.r0.out.pdf>
>> For example, ZFC is not sufficient to handle large cardinals (which require
>> an
>> additional axiom), and it should be easy to construe other examples not
>> covered
>> by ZFC by introducing other axioms.
>
> It has large enough cardinals for all ordinary purposes. The “large” in
Again, the term "ordinary" is the keyword here.
Any definition of it remains vague, showing that the "solution" is just
a preliminary solution and not the result of a systematic approach
(which should address nothing else than Russell's paradox,
not some concepts emphasizing the notion of set).
> “large cardinal axioms” is meant to be interpreted in a relative sense.
> Adding large cardinals axioms typically gives a model of ZFC, or
> ZFC+large (but not as large) cardinal. You can even find a diagram of
> which large cardinal axioms imply the consistency of which ZFC+not so
> large cardinals. The issue thus is consistency. There is no way to
> escape that situation by the well known results of Tarski on
> undefinability of arithmetical truth and Gödel on consistency and
> completeness.
I'm not sure what you are aiming at here, as quite different topics are
mentioned.
Concerning consistency, if one allows logical axioms only
(the five axioms of Q0 or R0), requiring all other (non-logical) "axioms"
(e.g., those of group theory) to be introduced in the form of a definition,
the logic itself never becomes inconsistent, but instead the defined
set proves to be empty (which is the desired result).
Concerning (in-)completeness, while Gödel's formal proof is correct,
the philosophical interpretation as incompleteness depends on the
semantic approach, as argued at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html>
If one follows a purely syntactic approach (as I do), the meaning of
Gödel's theorem is of little philosophical significance, since with
a syntactic approach, completeness is given by definition (syntax = semantics).
In particular, I reject all kinds of metatheory as a foundation
(e.g., the semantic approach, where a mathematical theory is
used to define mathematical truth).
Concerning the definability of mathematical truth, my argument is that
there are two kind of mathematical theorems: simple theorems (e.g.,
the theorems of the basic formal system such as Q0/R0), or
metatheorems resulting from studying the properties of the system,
see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-May/msg00013.html
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-May/msg00013.html>
> We do not have, say, a set of all ordinals, or of all cardinals, that is
> because it is incompatible with the separation axiom, so any set theory
> which has an universal set and separation is inconsistent. Jensen’s
> version of New Foundations (NFU) has an universal set and a set of all
> ordinals and moreover can be proved consistent in ZFC (even less than
> that). The downside is of course, that the separation axiom does not hold.
The question is why the combination of the universal set and
the separation axiom (such as the ZF Separation Schema, see
https://plato.stanford.edu/entries/set-theory/ZF.html
<https://plato.stanford.edu/entries/set-theory/ZF.html> )
results in inconsistency.
The reason is that without type restrictions one can establish a set definition
combining the two properties of an antinomy (self-reference and negation).
With type restrictions, one cannot.
I would argue that R0 has both a universal set (see below) and some kind
of separation schema
( http://www.owlofminerva.net/files/formulae.pdf
<http://www.owlofminerva.net/files/formulae.pdf>, p. 11 ),
but is consistent since it has the type restrictions that rule out the antinomy.
> Higher order logic has the counter-part of the axiom of separation in
> set theory, but it does not have a real universal set. It only has, for
> each type, the set of all elements of all type, and that is called
> “universal”, but that is a bit of a misuse.
R0 does have a real universal set: V
( http://www.owlofminerva.net/files/formulae.pdf
<http://www.owlofminerva.net/files/formulae.pdf>, p. 361 )
Kind regards,
Ken
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
