The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

If the criterion is representing all of mathematics, then ZFC is unsatisfactory.

Of course, a language capable of doing so requires dependent types.

Therefore, I have extended Q0 (simple type theory) to R0,

which provides some of the means for dependent types, see pp. 11 f. of

http://doi.org/10.4444/100.3

For the definition of the universal quantifier in R0, see p. 359.

(The logical constant 'Q' was replaced by '=', since 'Q' has no own syntactic function.)

This definition simply defines the universal quantifier as the set of properties (sets) in which

all objects of the given type are mapped to true (are element of), hence the proposition holds 'for all'.

Moreover, the variable binders are reduced to a single one (lambda).

I share Bertrands Russell's program of logicism (that mathematics is reducible to formal logic),

hence a sharp distinction between both of them is rather difficult.

A preliminary distinction may be the limitation of the language to rather simple definitions

(such as on pp. 359 f., using basic types like 'o' and similar only; for comparison, see

the rather complex group definition on p. 362).

Types naturally express the distinctions between different kinds of mathematical objects

(e.g., between numbers and operators) made by the mathematician intuitively.

There are some excellent quotes on this in Andrews' 2002 textbook.

Indeed, types are more fundamental than objects of first-order logic, as you,

for example, wish to distinguish between propositions (of type 'o'), operators ('oo'),

and connectives ('ooo' = '((oo)o)'). Type theory naturally expresses the grammar

of formal logic (and mathematics).

In lambda calculus, variables are clearly distinguished from constants (primitive symbols,

lambda abstractions and lambda applications) by the fact that only variables can be

bound by lambda (and by Theorem 5215 [Andrews, 2002, p. 221], instantiated freely).

Lambda calculus allows the reduction of functions of more than one argument to

those of just one argument (implementing Schönfinkel's concept), so "we can avoid explicitly

admitting into our language functions of more than one argument." [Andrews, 2002, p. 206]

All of mathematics can be expressed using just a few principles, which Andrews calls

"expressiveness" (I prefer the term "reducibility").

For the references, please see: http://doi.org/10.4444/100.111

Ken

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

Am 03.05.2018 um 22:52 schrieb Jan Burse <bursejan AT gmail.com>:

I did NOT say its unsatisfactory. Its very satisfactory,
since its very flexible, and still doesn't have too much
assumptions built in.

Also I don't know what you mean by type theory. Simple
types, dependent types? In ZFC the logic part is delegated
to FOL=, and the domain part is ZFC itself built on the

logic part, thats a very nice separation, how do you apply
your type theory? For example if you define in Q0 the forall
operator (later used in the forall quantifier) as follows:

   Π_ο(οα) stands for [Q_{ο(οα)(οα)} [λx_α T_ο] ]
   https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu

Then things are somehow upside-down. You use types,
a kind of domain, to define logic. How do you justify such
a proceedings?

Am Donnerstag, 3. Mai 2018 22:31:55 UTC+2 schrieb Ken Kubota:

Hi Jan,

I definitely agree on that ZFC is unsatisfactory: This is why I prefer type theory.

But historically ZFC (axiomatic set theory) was designed exactly for this purpose

in the aftermath of Russell's paradox, see [Zermelo, 1908] (English translation [Zermelo, 1967]).

For the references, please see: http://doi.org/10.4444/100.111

Ken

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

Am 03.05.2018 um 22:08 schrieb Jan Burse <burs... AT gmail.com>:

For example Ramsey Cardinal and V=L seem to be two
opposite extensions of ZFC, in some aspects.

So I am very currious how this would look like in metamath,
the other post "Definition of L" form 6. April,

and more...

Am Donnerstag, 3. Mai 2018 22:03:51 UTC+2 schrieb Jan Burse:

I don't agree with what Ken wrote: "But all the systems in discussion
here (e.g., ZFC) implicitly or explicitly claim to represent (significant
parts of) mathematics".

If you read Levy, Basic Set Theory, you see that ZFC has a lot of
holes, and isn't in itself interesting mathematics. Its a foundation you
need to apply and/or extend.

Am Donnerstag, 3. Mai 2018 17:22:59 UTC+2 schrieb Ken Kubota:

Hi Russell,

While your statement (a "proof" always refers to a proof within a certain formal system) is correct looked at in an isolated way,
I find it problematic as it overlooks that the formal systems (deduction systems) in discussion here are designed to represent mathematics.

Of course, this is the standard use of the terminology ("Now we prove the theorem MUIIU." - p. 179),
even in toy systems such as the MIU system, cf. pp. 177 ff. at
        http://us.metamath.org/downloads/metamath.pdf

But all the systems in discussion here (e.g., ZFC) implicitly or explicitly claim to represent (significant parts of) mathematics,
making it difficult to follow a pure relativism (denying provability "in any absolute sense").
For example, if one of the systems mentioned previously would be shown to be inconsistent (or otherwise not sound), it would be discarded.

Moreover, I would even argue that some of these formal systems are better than others in representing mathematics,
e.g., type theory is superior to (axiomatic) set theory, and the ideal system should follow the concept of expressiveness of Q0
by Peter B. Andrews, who regularly emphasizes that mathematics should be expressed "naturally".

Hence, there should be an ideal formal system for representing mathematics, and proofs in it would be proofs in an "absolute sense".

I still owe Randy an answer in the HOL mailing list, which I hope to finish soon.

Best regards,

Ken

____________________________________________________


Ken Kubota
http://doi.org/10.4444/100



> Am 03.05.2018 um 02:57 schrieb roco... AT theorem.ca:
>
> On Thu, 3 May 2018, Jose Manuel Rodriguez Caballero wrote:
>
>> Russell said:
>> "I also want to point out that proving that PA is consistent doesn't by itself mean that there isn't a proof that PA is inconsistent”
>> Ok, we are not talking the same language. In my world: PA is consistent means that there isn't a proof that PA is inconsistent (a proof that 1=0 formalized inside PA). I’m following
>> Hilbert’s metamathematical standards: https://plato.stanford.edu/entries/hilbert-program/

> Firstly, your statement is incomplete.  There isn't a proof according to what system?  Please, if you are going to dive into logic like this, don't use the term "proof" unaddorned like this.  Mathematical statements are not provable in any absolute sense.  Mathematical statements are only provable or not within some deduction system.  Coq can prove something, or ZFC can prove something or PA can prove something, and these different systems form completely different classes of statements of what they can or cannot prove.

> Let me reiterate again that "Essential Incompleteness of Arithmetic Verified by Coq" is only claiming that "PA is consistent" is provable in Coq (and this is just a side remark within that paper).  This is a claim that you can directly verify yourself by downloading the development and checking it in Coq and seeing for yourself that Coq indeed considers the deduction valid.  The paper does not directly claim that "PA is consistent" is true; that would only follow if you assume that Coq is sound, and the paper doesn't discuss the soundness of Coq.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u... AT googlegroups.com.
To post to this group, send email to meta... AT googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe AT googlegroups.com.
To post to this group, send email to metamath AT googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.