On Sunday, 4 December 2022 at 00:37:07 UTC+2, richar...@gmail.com wrote:
> I figured you could understandthe meaning of the terms from the
> predefioned terms of the theory.
You figured I would read your mind? Yeah... you keep expecting me to do that.

Your implicit theoretical biases are not explicit definitions.

> At least in my number theory classes, 0, =, and 'S' as a symbol for the
> successor function were assumed symbols.
And in my type theory classes "=" is a decidable proposition.

> Maybe I overestimated your intelegence.
Maybe you overestimated your own intelligence.

You went and assumed your theoretical biases are everyone's biases.

> Or maybe it shows the problem with assuming proofs actually need to be
> writtten as programs.
In what way is making ALL of your biases explicit a "problem"?

On 12/3/22 4:00 PM, olcott wrote:

> He has a masters in EE from MIT so he is not stupid.
> When someone with those credentials makes such a "stupid"
> mistake and we rule our {stupid} what does that leave?

That I'm right?

Something that seems to be outside your understanding.

In some ways you and Skep Dick are very similar, but in others you are
quite different.

Skep Dick seems intelegent, and is just playing stupid because he is
just a dick about things. It might be he doesn't really understand that
Proofs aren't just programs, but he shows intelegency in his replies.

You on the other hand, show little intellegence in your replies and are
either challenged in your ability to learn things related to logic, ar
just a pthological liar, or have just gas-lite yourself enough that you
killed off your ability to think rationally about these things.

Your only response is to just repeat your same error over and over and
over. You have cemented this as your eternal reputation.

Even if you were innocent of those charges in the past, I think you are
introducing enough doubt about it, people won't really believe it,
because you have show how poorly you treat handling truth.

On Sunday, 4 December 2022 at 00:37:07 UTC+2, richar...@gmail.com wrote:
> At least in my number theory classes, 0, =, and 'S' as a symbol for the
> successor function were assumed symbols.

Also... you are talking about "symbols". Surely you are familiar that ALL symbolic manipulations are just higher-order algebras. Right?
So it's really really strange that you can't explain any your symbolic knowledge to a computer. It's even stranger that you don't understand WHY proofs are programs...

https://en.wikipedia.org/wiki/Computer_algebra

On 12/3/22 5:46 PM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 00:37:07 UTC+2, richar...@gmail.com wrote:
>> I figured you could understandthe meaning of the terms from the
>> predefioned terms of the theory.
> You figured I would read your mind? Yeah... you keep expecting me to do that.

So, you don't know the standard meaning of the symbol 0?

You presumed the definitions of
1 = suc zero
2 = suc suc zero
etc,

So I presumed you actually knew something, I guess I was wrong.

>
> Your implicit theoretical biases are not explicit definitions.

Wrong. A basis of language is the implicit determination of appropriate
context.

2 + 2 = 4 defines a logical context.

>
>> At least in my number theory classes, 0, =, and 'S' as a symbol for the
>> successor function were assumed symbols.
> And in my type theory classes "=" is a decidable proposition.
>
>> Maybe I overestimated your intelegence.
> Maybe you overestimated your own intelligence.
>
> You went and assumed your theoretical biases are everyone's biases.

Nope, I persume people know the established defaults for the field of
discussion.

>
>> Or maybe it shows the problem with assuming proofs actually need to be
>> writtten as programs.
> In what way is making ALL of your biases explicit a "problem"?

Then you better actually make ALL your assumption explicit.

For instance, what namespace are you pulling your package "Relaiton" out of?

You are putting assumptions there.

On Sunday, 4 December 2022 at 00:56:57 UTC+2, richar...@gmail.com wrote:
> On 12/3/22 5:46 PM, Skep Dick wrote:
> > On Sunday, 4 December 2022 at 00:37:07 UTC+2, richar...@gmail.com wrote:
> >> I figured you could understandthe meaning of the terms from the
> >> predefioned terms of the theory.
> > You figured I would read your mind? Yeah... you keep expecting me to do that.
> So, you don't know the standard meaning of the symbol 0?
It doesn't have any meaning. Only a type. 0 is a number.

> You presumed the definitions of
> 1 = suc zero
> 2 = suc suc zero
> etc,
Those are not definitions. Those are encodings.

> So I presumed you actually knew something, I guess I was wrong.
I mean, I know that I know nothing, but it's becoming quite evident that you know even less.

> > Your implicit theoretical biases are not explicit definitions.
> Wrong. A basis of language is the implicit determination of appropriate
> context.
Nonsense. That's the basis of an incomplete language.

The basis for a complete language is an explicit context.

> 2 + 2 = 4 defines a logical context.
No, it doesn't. You could parse that string any way you want.

> > You went and assumed your theoretical biases are everyone's biases.
> Nope, I persume people know the established defaults for the field of
> discussion.
The defaults of a field are the biases of a field.

So you went and assumed your theoretical biases are everyone's biases.

> >> Or maybe it shows the problem with assuming proofs actually need to be
> >> writtten as programs.
> > In what way is making ALL of your biases explicit a "problem"?
> Then you better actually make ALL your assumption explicit.
I did.

> For instance, what namespace are you pulling your package "Relaiton" out of?
> You are putting assumptions there.
All of those are explicit in the broader codebase and the standard library. Which you can find on Github.

Unlike your biases. Which are only in your head.

On 12/3/22 5:54 PM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 00:37:07 UTC+2, richar...@gmail.com wrote:
>> At least in my number theory classes, 0, =, and 'S' as a symbol for the
>> successor function were assumed symbols.
>
> Also... you are talking about "symbols". Surely you are familiar that ALL symbolic manipulations are just higher-order algebras. Right?
> So it's really really strange that you can't explain any your symbolic knowledge to a computer. It's even stranger that you don't understand WHY proofs are programs...
>
> https://en.wikipedia.org/wiki/Computer_algebra

Not that I can't, but I don't see the need to.

And Proofs are NOT programs but can be converted into programs, or
represented in a program. SOME programs can be proofs in them selves,
but not all are (except for the trivial case that a program reaching its
end is proof that it is a halting program).

On Sunday, 4 December 2022 at 01:19:02 UTC+2, richar...@gmail.com wrote:
> Not that I can't, but I don't see the need to.
You don't see the need to make your assumptions explicit?

That's like... intellectually dishonest or something.

> And Proofs are NOT programs but can be converted into programs, or
> represented in a program. SOME programs can be proofs in them selves,
> but not all are (except for the trivial case that a program reaching its
> end is proof that it is a halting program).

Weren't you the one telling me to mind my context? This is comp.theory, right?

Proofs are programs. Shut up and show us the code.

On 12/3/2022 4:36 PM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 00:06:14 UTC+2, olcott wrote:
>> Hence not the {identical to} relation.
>> string_length("2+2") != string_length("4") thus not identical
> Idiot. Do you actually understand the difference between syntax and semantics?
>

"Identical" means in every possible way.
"Equivalent" is not as strict.

> The symbolic expression 2+2 and the symbolic expression 4 point to the exact same semantic object. They are identical. De-reference the pointers first.
>
> identity is equivalent to equivalence. Univalence axiom... (A = B) ≃ (A ≃ B)

--
Copyright 2022 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

On 12/3/2022 5:31 PM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 01:19:02 UTC+2, richar...@gmail.com wrote:
>> Not that I can't, but I don't see the need to.
> You don't see the need to make your assumptions explicit?
>
> That's like... intellectually dishonest or something.
>
>> And Proofs are NOT programs but can be converted into programs, or
>> represented in a program. SOME programs can be proofs in them selves,
>> but not all are (except for the trivial case that a program reaching its
>> end is proof that it is a halting program).
>
> Weren't you the one telling me to mind my context? This is comp.theory, right?
>
> Proofs are programs. Shut up and show us the code.

In programming language theory and proof theory, the Curry–Howard
correspondence (also known as the Curry–Howard isomorphism or
equivalence, or the proofs-as-programs and propositions- or
formulae-as-types interpretation) is the direct relationship between
computer programs and mathematical proofs.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

--
Copyright 2022 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

On Sunday, 4 December 2022 at 02:02:13 UTC+2, olcott wrote:
> "Identical" means in every possible way.
> "Equivalent" is not as strict.
Distinction without a difference.

When you de-reference the pointers the object 2+2 points to is identical to the object 4 points to.

On 12/3/22 6:31 PM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 01:19:02 UTC+2, richar...@gmail.com wrote:
>> Not that I can't, but I don't see the need to.
> You don't see the need to make your assumptions explicit?
>
> That's like... intellectually dishonest or something.

No, You ALWAYS need to start from assumptions. The question becomes how
much is reasonable.

I understand that when working inside a field, you can adopt, without
needing to be explicit, the terminoloy of the field.

After all, where did your program define what "import" meant?

It needs to some how define the "language" it is written it, but that
needs some assumption to define what that means.

So, your arguement dies on its own sword.

>
>> And Proofs are NOT programs but can be converted into programs, or
>> represented in a program. SOME programs can be proofs in them selves,
>> but not all are (except for the trivial case that a program reaching its
>> end is proof that it is a halting program).
>
> Weren't you the one telling me to mind my context? This is comp.theory, right?
>
> Proofs are programs. Shut up and show us the code.

comp theory, as in the theory about computers/computations.

The context of that field is NOT that proofs are programs.

In fact, "Computation Theory" predates the existance of "Com[puter
Languages"

The coding language COULD be "English"

After all, the "Computers" were the title of PEOPLE who followed the
"program" as tehy performed computations according to the algorithm of
their instructions.

You are just showing you failures.

On Sunday, 4 December 2022 at 02:17:03 UTC+2, richar...@gmail.com wrote:
> On 12/3/22 6:31 PM, Skep Dick wrote:
> > On Sunday, 4 December 2022 at 01:19:02 UTC+2, richar...@gmail.com wrote:
> >> Not that I can't, but I don't see the need to.
> > You don't see the need to make your assumptions explicit?
> >
> > That's like... intellectually dishonest or something.
> No, You ALWAYS need to start from assumptions. The question becomes how
> much is reasonable.
Which part confused you when I drew a distinction between implicit and explicit assumptions?

> I understand that when working inside a field, you can adopt, without
> needing to be explicit, the terminoloy of the field.
And how do you go about adopting any terminology of any field if the terminology is implicit and not explicit?

> After all, where did your program define what "import" meant?
The meaning of the "import" symbol is explicit in the compiler source code.

> It needs to some how define the "language" it is written it, but that
> needs some assumption to define what that means.
Have you heard of self-hosting compilers? The C compiler is written in C.

https://en.wikipedia.org/wiki/Self-hosting_(compilers)

> So, your arguement dies on its own sword.
No, it doesn't. My argument pulls itself up by its own bootstraps.

https://en.wikipedia.org/wiki/Bootstrapping_(compilers)

> The context of that field is NOT that proofs are programs.
> In fact, "Computation Theory" predates the existance of "Com[puter
> Languages"
And then we spent 100 years learning about computation before realising that different programming languages are just different models of computation.

> The coding language COULD be "English"
And the decoder/interpreter/compiler would be in... ?

> After all, the "Computers" were the title of PEOPLE who followed the
> "program" as tehy performed computations according to the algorithm of
> their instructions.
Precisely. Computation has always been rule-based symbol manipulation!

That's an algebra.

On 12/3/2022 6:13 PM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 02:02:13 UTC+2, olcott wrote:
>> "Identical" means in every possible way.
>> "Equivalent" is not as strict.
> Distinction without a difference.

Not at all. You are merely not very careful to say exactly what you mean
and mean exactly what you say.

>
> When you de-reference the pointers the object 2+2 points to is identical to the object 4 points to.

--
Copyright 2022 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

On 12/3/22 7:29 PM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 02:17:03 UTC+2, richar...@gmail.com wrote:
>> On 12/3/22 6:31 PM, Skep Dick wrote:
>>> On Sunday, 4 December 2022 at 01:19:02 UTC+2, richar...@gmail.com wrote:
>>>> Not that I can't, but I don't see the need to.
>>> You don't see the need to make your assumptions explicit?
>>>
>>> That's like... intellectually dishonest or something.
>> No, You ALWAYS need to start from assumptions. The question becomes how
>> much is reasonable.
> Which part confused you when I drew a distinction between implicit and explicit assumptions?

But don't do it yourself, so you are just showing yourself to be a
hypocrite.

If you don't accept that a discussion of primative number theory uses
the classic nomenclature of primative number theory, or you needed to
make it explicit what programming languag your program was written in to
define what 'import' means.
>
>
>> I understand that when working inside a field, you can adopt, without
>> needing to be explicit, the terminoloy of the field.
> And how do you go about adopting any terminology of any field if the terminology is implicit and not explicit?
>
>> After all, where did your program define what "import" meant?
> The meaning of the "import" symbol is explicit in the compiler source code.

Nope. No more than the use of the classic symbol 0.

>
>> It needs to some how define the "language" it is written it, but that
>> needs some assumption to define what that means.
> Have you heard of self-hosting compilers? The C compiler is written in C.
>
> https://en.wikipedia.org/wiki/Self-hosting_(compilers)

Yep, and they still deal with the implicit assumption that the code
given is in C.

>
>> So, your arguement dies on its own sword.
> No, it doesn't. My argument pulls itself up by its own bootstraps.
>
> https://en.wikipedia.org/wiki/Bootstrapping_(compilers)

Which are still based on the initial implicit assumptions of the
definition of the language.

>
>
>> The context of that field is NOT that proofs are programs.
>> In fact, "Computation Theory" predates the existance of "Com[puter
>> Languages"
> And then we spent 100 years learning about computation before realising that different programming languages are just different models of computation.
>
>> The coding language COULD be "English"
> And the decoder/interpreter/compiler would be in... ?
>
>> After all, the "Computers" were the title of PEOPLE who followed the
>> "program" as tehy performed computations according to the algorithm of
>> their instructions.
> Precisely. Computation has always been rule-based symbol manipulation!
>
> That's an algebra.
>

But computation theory goes beyond algerbra, because it doesn't limit
itself to the algebraic operations. Computation USES Algerbra as a tool,
but isn't limited to it.

Maybe thats your problem.

On Saturday, December 3, 2022 at 12:36:13 PM UTC-8, olcott wrote:
> Successor(Successor(0)) + Successor(Successor(0)) =
> Successor(Successor(Successor(Successor(0))))
>
Associativity of + is crucial here
(1+1)+(1+1) =((1+1)+1)+1
where 2 is defined as 1+1, 3 as 2+1and 4 as 3+1

On Sunday, 4 December 2022 at 02:39:38 UTC+2, olcott wrote:
> On 12/3/2022 6:13 PM, Skep Dick wrote:
> > On Sunday, 4 December 2022 at 02:02:13 UTC+2, olcott wrote:
> >> "Identical" means in every possible way.
> >> "Equivalent" is not as strict.
> > Distinction without a difference.
> Not at all. You are merely not very careful to say exactly what you mean
> and mean exactly what you say.

I was as careful as I can be when I said: identity is equivalent to equivalence

On Sunday, 4 December 2022 at 02:45:21 UTC+2, richar...@gmail.com wrote:
> But don't do it yourself, so you are just showing yourself to be a
> hypocrite.
I don't need to do it **myself** for the assumptions to be explicit. They are explicit in the compiler. In the source code. In the runtime.

They are explicit in the explicit foundation/theory.

> If you don't accept that a discussion of primative number theory uses the classic nomenclature of primative number theory
Doesn't change anything - your theory's no menclature is implicit.

>or you needed to make it explicit what programming languag your program was written in to define what 'import' means.
I made it explicit. It's Agda.

> Nope. No more than the use of the classic symbol 0.
The irony. Look at you designating 0 as a "symbol" and not a "number"; or a "string"

Would you like me to refer you to the portion of the compiler which handles type-checking?

> > https://en.wikipedia.org/wiki/Self-hosting_(compilers)
> Yep, and they still deal with the implicit assumption that the code
> given is in C.
The compiler doesn't care much about the designation/name of the language it's written it.

The compiler cares whether it can compile itself. Irrespective of the language it's written in.

> > https://en.wikipedia.org/wiki/Bootstrapping_(compilers)
> Which are still based on the initial implicit assumptions of the
> definition of the language.
The compiler is the definition of the language. If the definition was "implicit" what is the compiler compiling exactly?

> But computation theory goes beyond algerbra, because it doesn't limit
> itself to the algebraic operations. Computation USES Algerbra as a tool,
> but isn't limited to it.
>
> Maybe thats your problem.
*yawn* Computation limits itself to operations. Algebraic or otherwise.

https://en.wikipedia.org/wiki/Operator_theory

"The description of operator algebras is part of operator theory."

On 12/4/22 12:54 AM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 02:45:21 UTC+2, richar...@gmail.com wrote:
>> But don't do it yourself, so you are just showing yourself to be a
>> hypocrite.
> I don't need to do it **myself** for the assumptions to be explicit. They are explicit in the compiler. In the source code. In the runtime.
>
> They are explicit in the explicit foundation/theory.

But it is implicit as to WHICH compiler you use,

And I claim my choices come out explicitly by the fact that we were
talking primitive number theory, with no explicit exception to notation.

>
>> If you don't accept that a discussion of primative number theory uses the classic nomenclature of primative number theory
> Doesn't change anything - your theory's no menclature is implicit.
>
>> or you needed to make it explicit what programming languag your program was written in to define what 'import' means.
> I made it explicit. It's Agda.
>
>> Nope. No more than the use of the classic symbol 0.
> The irony. Look at you designating 0 as a "symbol" and not a "number"; or a "string"

0 is a symbol that represents the number we call 0. Thats how a lot of
concepts exist.

The concept isn't the symbol itself, which is why we can use different
symbols for the same concept at different times.

>
> Would you like me to refer you to the portion of the compiler which handles type-checking?
>
>>> https://en.wikipedia.org/wiki/Self-hosting_(compilers)
>> Yep, and they still deal with the implicit assumption that the code
>> given is in C.
> The compiler doesn't care much about the designation/name of the language it's written it.
>
> The compiler cares whether it can compile itself. Irrespective of the language it's written in.
>
>>> https://en.wikipedia.org/wiki/Bootstrapping_(compilers)
>> Which are still based on the initial implicit assumptions of the
>> definition of the language.
> The compiler is the definition of the language. If the definition was "implicit" what is the compiler compiling exactly?
>
>> But computation theory goes beyond algerbra, because it doesn't limit
>> itself to the algebraic operations. Computation USES Algerbra as a tool,
>> but isn't limited to it.
>>
>> Maybe thats your problem.
> *yawn* Computation limits itself to operations. Algebraic or otherwise.
>
> https://en.wikipedia.org/wiki/Operator_theory
>
> "The description of operator algebras is part of operator theory."

On Sunday, 4 December 2022 at 14:23:02 UTC+2, richar...@gmail.com wrote:
> On 12/4/22 12:54 AM, Skep Dick wrote:
> > On Sunday, 4 December 2022 at 02:45:21 UTC+2, richar...@gmail.com wrote:
> >> But don't do it yourself, so you are just showing yourself to be a
> >> hypocrite.
> > I don't need to do it **myself** for the assumptions to be explicit. They are explicit in the compiler. In the source code. In the runtime.
> >
> > They are explicit in the explicit foundation/theory.
> But it is implicit as to WHICH compiler you use,
It's not. I've told you twice now. Agda.

You want the explicit source code? Here: https://github.com/agda/agda

> And I claim my choices come out explicitly by the fact that we were
> talking primitive number theory, with no explicit exception to notation.
So show me the source code for this theory.

Perhaps you haven't come across Naur's perspective? Programming as theory building.

https://pages.cs.wisc.edu/~remzi/Naur.pdf

> 0 is a symbol that represents the number we call 0. Thats how a lot of
> concepts exist.
You are confusing syntax with semantics. Exactly like Olcott!

If the only number which exists was 0 how many numbers do we have?

> The concept isn't the symbol itself, which is why we can use different
> symbols for the same concept at different times.
But the concept is the concept itself, right?

So given the concept of "numbers", and the concept of "the number 0". How many numbers do you have in total if all you have is the number 0?

On 12/5/22 1:50 AM, Skep Dick wrote:
> On Sunday, 4 December 2022 at 14:23:02 UTC+2, richar...@gmail.com wrote:
>> On 12/4/22 12:54 AM, Skep Dick wrote:
>>> On Sunday, 4 December 2022 at 02:45:21 UTC+2, richar...@gmail.com wrote:
>>>> But don't do it yourself, so you are just showing yourself to be a
>>>> hypocrite.
>>> I don't need to do it **myself** for the assumptions to be explicit. They are explicit in the compiler. In the source code. In the runtime.
>>>
>>> They are explicit in the explicit foundation/theory.
>> But it is implicit as to WHICH compiler you use,
> It's not. I've told you twice now. Agda.

Not when you gave the code!

Just like I have told you I am working in the classical theory.

So if you expect me to remember, you need to too.

>
> You want the explicit source code? Here: https://github.com/agda/agda
>
>> And I claim my choices come out explicitly by the fact that we were
>> talking primitive number theory, with no explicit exception to notation.
> So show me the source code for this theory.
>
> Perhaps you haven't come across Naur's perspective? Programming as theory building.

Which talks about programs as theories, not that all theories are programs.

So, you seem to be doing it backwards.

>
> https://pages.cs.wisc.edu/~remzi/Naur.pdf
>
>> 0 is a symbol that represents the number we call 0. Thats how a lot of
>> concepts exist.
> You are confusing syntax with semantics. Exactly like Olcott!
>
> If the only number which exists was 0 how many numbers do we have?
>
>> The concept isn't the symbol itself, which is why we can use different
>> symbols for the same concept at different times.
> But the concept is the concept itself, right?
>
> So given the concept of "numbers", and the concept of "the number 0". How many numbers do you have in total if all you have is the number 0?

The problem is you don't get the "concept" of "numbers" until you build
a system with more interelated concepts.

That is the result of First Principles.

You can't have a concept of numberS until you have a plurality. So you
can either define a finite ring (which normally can't talk about its own
cardinality) or an infinte set by defining the successor operator.

You can define A Number, but then you don't have the concept of
cardinality yet to ask the question of how many.

On Monday, 5 December 2022 at 16:02:54 UTC+2, richar...@gmail.com wrote:
> On 12/5/22 1:50 AM, Skep Dick wrote:
> > On Sunday, 4 December 2022 at 14:23:02 UTC+2, richar...@gmail.com wrote:
> >> On 12/4/22 12:54 AM, Skep Dick wrote:
> >>> On Sunday, 4 December 2022 at 02:45:21 UTC+2, richar...@gmail.com wrote:
> >>>> But don't do it yourself, so you are just showing yourself to be a
> >>>> hypocrite.
> >>> I don't need to do it **myself** for the assumptions to be explicit. They are explicit in the compiler. In the source code. In the runtime.
> >>>
> >>> They are explicit in the explicit foundation/theory.
> >> But it is implicit as to WHICH compiler you use,
> > It's not. I've told you twice now. Agda.
> Not when you gave the code!
Liar!

This is precisely what I said right before I gave you the code: While we are at it... Here is the proof that I "wouldn't understand". In Agda."

> Just like I have told you I am working in the classical theory.
> So if you expect me to remember, you need to too.
So where is the source code for the compiler of your theory?

> > Perhaps you haven't come across Naur's perspective? Programming as theory building.
> Which talks about programs as theories, not that all theories are programs.
Not doesn't. It talks about theory-building. a.k.a programming.

> So, you seem to be doing it backwards.
Obviously. I've told you this a bunch of times. Reverse Mathematics.

Axioms from theorems, not theorems from axioms.

> > So given the concept of "numbers", and the concept of "the number 0". How many numbers do you have in total if all you have is the number 0?
> The problem is you don't get the "concept" of "numbers" until you build
> a system with more interelated concepts.
>
> That is the result of First Principles.
The thought-experiment I've constructed for you is the result of first principles.

Imagine a universe in which..... First principles.

> You can't have a concept of numberS until you have a plurality.
Look! The sophist is avoiding the question. Surprise, surprise!

Lets try again. Imagine the universe in which you have ONLY the numbers 0 and 1. How many numbers are there in this universe?

> can either define a finite ring (which normally can't talk about its own
> cardinality) or an infinte set by defining the successor operator.
I don't want to define such a universe.

I want the universe which contains ONLY the objects 0 and 1 and nothing else.

How many objects does that universe contain?

> You can define A Number, but then you don't have the concept of
> cardinality yet to ask the question of how many.
See! You don't understand the difference between statements in the system and statements about the system.