# Zorn's Lemma, how formalize it in DC Proof

442 views

### Mostowski Collapse

Sep 22, 2020, 8:46:01 PM9/22/20
to
So whats the plan for proving Zorn's Lemma
in DC Proof? Translate FOL to DC Proof?

### Dan Christensen

Sep 22, 2020, 11:18:15 PM9/22/20
to
On Tuesday, September 22, 2020 at 8:46:01 PM UTC-4, Mostowski Collapse wrote:
> So whats the plan for proving Zorn's Lemma
> in DC Proof? Translate FOL to DC Proof?

All I am certain of is that a proof of ZL is not dependent on the quirks of standard FOL, e.g. foolishness like ALL(x):P(x) => EXIST(x):P(x).

Dan

### Me

Sep 23, 2020, 12:22:03 AM9/23/20
to
What's the matter with you, you fucking idiot? I alreay told you that there's nothing wrong with AxPhi[x] -> ExPhi[x] in the context of set theory.

Hint: In this context (a) THERE ARE objects and (b) if Phi holds for EVERY object than certainly there IS an object such that Phi holds for that object (see (a)). Too dumb again to get that simple logical fact?

(a) means that Ex(x = x) will hold in the context of set theory (if in the usual/standard way) and (b) means that AxPhi[x] -> ExPhi[x] will hold too (if in the usual/standard way).

You should rather hope that a proof of ZL is not inhibited by the quirks of DC Proof, dumbo.

### Peter

Sep 23, 2020, 8:07:48 AM9/23/20
to
Zorn's lemma says that, if (P,<) is a poset, and if every subset Q of P
that is totally ordered by < has an upper bound in P, then P has a
maximal element.

(Totally ordered subsets Q of posets are often called chains in the
poset, so a briefer statement is: if (P,<) is a poset, and if every
chain in P has an upper bound in P, then P has a maximal element.)

In your world P may be empty, but Zorn's lemma for such a set is
vacuously true. So only non-empty sets posets are worth considering.

You must append to DC Proof the axiom of choice or something of equal
strength. (AxCh holds iff ZL holds.) AxCh says something about all
collections of pairwise disjoint non-empty sets; but the collections
themselves need not be non-empty.

### Dan Christensen

Sep 23, 2020, 8:54:15 AM9/23/20
to
On Wednesday, September 23, 2020 at 8:07:48 AM UTC-4, Peter wrote:
> Dan Christensen wrote:
> > On Tuesday, September 22, 2020 at 8:46:01 PM UTC-4, Mostowski Collapse wrote:
> >> So whats the plan for proving Zorn's Lemma
> >> in DC Proof? Translate FOL to DC Proof?
> >
> > All I am certain of is that a proof of ZL is not dependent on the quirks of standard FOL, e.g. foolishness like ALL(x):P(x) => EXIST(x):P(x).
> >
> >
> > Dan
> >
>
> Zorn's lemma says that, if (P,<) is a poset, and if every subset Q of P
> that is totally ordered by < has an upper bound in P, then P has a
> maximal element.
>
> (Totally ordered subsets Q of posets are often called chains in the
> poset, so a briefer statement is: if (P,<) is a poset, and if every
> chain in P has an upper bound in P, then P has a maximal element.)
>
> In your world P may be empty, but Zorn's lemma for such a set is
> vacuously true. So only non-empty sets posets are worth considering.
>

DC Proof can easily handle vacuously true propositions. (See "The Arbitrary Consequent (Arb Cons) Rule."

> You must append to DC Proof the axiom of choice or something of equal
> strength.

In DC Proof, AC is included in the built-in axioms of set theory. If another version is required, the user can insert it as an axiom at the beginning of a proof.

Dan

Visit my Math Blog at http://www.dcproof.wordpress.com

### Dan Christensen

Sep 23, 2020, 9:00:52 AM9/23/20
to
On Wednesday, September 23, 2020 at 12:22:03 AM UTC-4, Me wrote:
> On Wednesday, September 23, 2020 at 5:18:15 AM UTC+2, Dan Christensen wrote:
> > On Tuesday, September 22, 2020 at 8:46:01 PM UTC-4, Mostowski Collapse wrote:
> > >
> > > So whats the plan for proving Zorn's Lemma in DC Proof? Translate FOL to DC Proof?
> > >
> > > All I am certain of is that a proof of ZL is not dependent on the quirks
> > > of standard FOL, e.g. foolishness like ALL(x):P(x) => EXIST(x):P(x).
>
> What's the matter with you, you fucking idiot? I alreay told you that there's nothing wrong with AxPhi[x] -> ExPhi[x] in the context of set theory.
>

Why introduce something so counter-intuitive when it is simply not required in the ordinary rules of logic implicit in most mathematical proofs?

### Peter

Sep 23, 2020, 10:15:29 AM9/23/20
to
Dan Christensen wrote:
> On Wednesday, September 23, 2020 at 12:22:03 AM UTC-4, Me wrote:
>> On Wednesday, September 23, 2020 at 5:18:15 AM UTC+2, Dan Christensen wrote:
>>> On Tuesday, September 22, 2020 at 8:46:01 PM UTC-4, Mostowski Collapse wrote:
>>>>
>>>> So whats the plan for proving Zorn's Lemma in DC Proof? Translate FOL to DC Proof?
>>>>
>>>> All I am certain of is that a proof of ZL is not dependent on the quirks
>>>> of standard FOL, e.g. foolishness like ALL(x):P(x) => EXIST(x):P(x).
>>
>> What's the matter with you, you fucking idiot? I alreay told you that there's nothing wrong with AxPhi[x] -> ExPhi[x] in the context of set theory.
>>
>
> Why introduce something so counter-intuitive when it is simply not required in the ordinary rules of logic implicit in most mathematical proofs?

I don't think anyone is claiming that it's required, merely that it is
derivable.

### Mostowski Collapse

Sep 23, 2020, 10:18:36 AM9/23/20
to

How do you think a FOL ZFC theorem is
to be realized in DC Proof?

### Mostowski Collapse

Sep 23, 2020, 11:35:22 AM9/23/20
to
cogito ergo sum

if X thinks then X exists.
Descartes thinks
----------------------
So Descartes exists.

Therefore:

if X thinks then X exists.
DC Proof doesn't exists.
----------------------
DC Proof does not think.

Are these inferences even possible in DC proof?
I dont think so. Dan-O-matik will object,
that descartes (or DC Proof) comes out

of nowhere. We cannot prove in DC Proof:

/* not provable in DC Proof? */

Ax(thinks(x) => exists(x))
thinks(descartes)
----------------------
exists(descartes)

Because in an empty universe Ax is still
true. There is no existential import
when the universe can be empty.

Same this here, possibly different matter
in negative free logic, but without some
negative free logic, it would be just:

/* not provable in DC Proof? */

Ax(thinks(x) => exists(x))
~exists(dcproof)
----------------------
~thinks(dcproof)

### Mostowski Collapse

Sep 23, 2020, 11:37:19 AM9/23/20
to
Proving this caused problems in DC Proof:

P & ~P => Q(a)

Can we prove this in DC Proof?

∀(P(x)=>Q(x))&P(a)=>Q(a)

### Dan Christensen

Sep 23, 2020, 1:48:58 PM9/23/20
to

### Mostowski Collapse

Sep 25, 2020, 10:49:13 AM9/25/20
to
If you would knew how "undef" is handled in
mathematics, you would not come up with some
empty name nonsense from philosophy department.

### Dan Christensen

Sep 25, 2020, 11:34:02 AM9/25/20
to
On Friday, September 25, 2020 at 10:49:13 AM UTC-4, Mostowski Collapse wrote:
> If you would knew how "undef" is handled in
> mathematics, you would not come up with some
> empty name nonsense from philosophy department.
>

I don't know about the philosophy department, but in mathematics, we say, for example, that 0/0 is "undefined." Likewise 0^0. I hope this helps.

### Peter

Sep 25, 2020, 1:39:25 PM9/25/20
to
Dan Christensen wrote:

> I don't know about the philosophy department, but in mathematics, we
> say, for example, that 0/0 is "undefined." Likewise 0^0.

Not so.

### Mostowski Collapse

Sep 25, 2020, 3:19:54 PM9/25/20
to
You write:

"This suggests that, in our definition of exponentiation
on N, we should simply leave 0^0 undefined."

But you don't know what undefined means in
mathematics. Take this function:

f(x) = abs(x)

And then its derivative:

/ 1 x > 0
f'(x) = < undef x = 0
\ -1 x < 0

Do you think f'(0)=2 is possible?

### Dan Christensen

Sep 25, 2020, 4:09:19 PM9/25/20
to
On Friday, September 25, 2020 at 3:19:54 PM UTC-4, Mostowski Collapse wrote:
> You write:
>
> "This suggests that, in our definition of exponentiation
> on N, we should simply leave 0^0 undefined."
>
> But you don't know what undefined means in
> mathematics.

Here is the definition of the partial binary function ^ on N:

ALL(a):ALL(b):[a in N & b in N => [~[a=b=0] => a^b in N]]

& 0^1=0

& ALL(a):[a in N => [~a=0 =>a^0=1]]

& ALL(a):ALL(b):[a in N & b in N => [~[a=b=0] => a^(b+1)=a^b*a]]

As even you might be able to see, Jan, by this definition, x^y is unambiguously defined for all x, y in N such that ~[x=y=0]. And 0^0 is undefined.

Get it? Didn't think so. Oh, well....

### Mostowski Collapse

Sep 25, 2020, 4:47:11 PM9/25/20
to
It does not show exp=exp'.
You write it yourself in your blog.
exp(0,0)=1 is possible, exp'(0,0)=2 is possible.

Whats wrong with you?

### Dan Christensen

Sep 25, 2020, 6:00:24 PM9/25/20
to
On Friday, September 25, 2020 at 4:47:11 PM UTC-4, Mostowski Collapse wrote:
> It does not show exp=exp'.
> You write it yourself in your blog.
> exp(0,0)=1 is possible, exp'(0,0)=2 is possible.
>

### Peter

Sep 26, 2020, 8:20:40 AM9/26/20
to
You have defined a function x^y on pairs of natural numbers except
(0,0). So 0^0 being undefined is just a matter of _you choosing_ not to
define your x^y function at a certain point.

0/0 is a completely different matter. x/y is defined to be the z such
that x = yz; and that is a problem if we put x=y=0. No one _chooses_
not to define 0/0, rather its being undefined is forced on us.

### Mostowski Collapse

Sep 26, 2020, 8:37:50 AM9/26/20
to
"_you choosing_ not to define" has different
connotations. He got it wrong, concernig
modern mathematics. In modern mathematics

undef means not unspecified, undef means
punctuated. Lets make a Kindergarden example.
Assume we have a total function f : {red,green,blue} -> N.

A total function could be:

f = {<red,42>,<green,99>,<blue,13>}

A partial function g : {red,green,blue} -> N
with domain {green,blue} could be:

/* correct modelling of "red" mathematically undef */

g = {<green,69>,<blue,22>}

Means "undef" is modelled ass absence of
the function argument "red". It does not
mean leaving "red" unspecified:

/* incorrect modelling of "red" mathematically undef */

g = {<red,??>, <green,69>,<blue,22>}

John Gabbermonkey raided a long rant
on sci.math that punctuated functions do
not exist. Now we have an other crank

Dan-O-Matic who thinks punctuated functions
are underspecified functions.

### Mostowski Collapse

Sep 26, 2020, 8:51:54 AM9/26/20
to
If you leave "red" unspecified but require
besides <green,69> and <blue,22> and total on
{"red", "green", "blue"} then these functions are possible:

g1 = {<red,77>, <green,69>,<blue,22>}

g2 = {<red,43>, <green,69>,<blue,22>}

Etc...

If we drop totality requirement on {"red", "green", "blue"},
then such a function is also possible:

g3 = {<green,69>,<blue,22>}

Etc...

But claiming g1 = g2 = g3 is absured. But that
is exactly what Dan-O-Matik is doing:

vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv
"There exists a unique exponent function on n
with 0^0 left undefined."
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
http://dcproof.com/PowPartialFunction.htm

Which utter nonsense, since he interprets "left
undefined", left unspecified. His proof doesn't
make any sense. He cannot prove:

~Ex(<0,0,x> e exp)

which would confirm mathematical undef, i.e.
a punctuation at <0,0>.

### Dan Christensen

Sep 26, 2020, 12:22:48 PM9/26/20
to
On Saturday, September 26, 2020 at 8:20:40 AM UTC-4, Peter wrote:
> Peter wrote:
> > Dan Christensen wrote:
> >
> >
> >> I don't know about the philosophy department, but in mathematics, we
> >> say, for example, that 0/0 is "undefined." Likewise 0^0.
> >
> > Not so.
>
> You have defined a function x^y on pairs of natural numbers except
> (0,0). So 0^0 being undefined is just a matter of _you choosing_ not to
> define your x^y function at a certain point.
>

I have shown that 0^0 is indeterminate on N. Any value would work. Other than for n=m=0, n^m is fully determined on N by

1. n^2 = n*n
2. n^(m+1) = n^m * n

So, we leave 0^0 undefined on N, as on R.

### Dan Christensen

Sep 26, 2020, 12:29:49 PM9/26/20
to
On Saturday, September 26, 2020 at 8:37:50 AM UTC-4, Mostowski Collapse wrote:
> "_you choosing_ not to define" has different
> connotations. He got it wrong, concernig
> modern mathematics. In modern mathematics
>
> undef means not unspecified, undef means
> punctuated.

Huh??? Play with words all you want, Jan, but in the case of exponentiation on N, I am suggesting that 0^0 be left unspecified in its definition (or undefined). AFAIK this is a common usage.

### Peter

Sep 26, 2020, 12:40:55 PM9/26/20
to
Dan Christensen wrote:
> On Saturday, September 26, 2020 at 8:20:40 AM UTC-4, Peter wrote:
>> Peter wrote:
>>> Dan Christensen wrote:
>>>
>>>
>>>> I don't know about the philosophy department, but in mathematics, we
>>>> say, for example, that 0/0 is "undefined." Likewise 0^0.
>>>
>>> Not so.
>>
>> You have defined a function x^y on pairs of natural numbers except
>> (0,0). So 0^0 being undefined is just a matter of _you choosing_ not to
>> define your x^y function at a certain point.
>>
>
> I have shown that 0^0 is indeterminate on N.

But it is only indeterminate in as much as you have chosen not to
determine it. This is you: 'in mathematics, we say, for example, that
0/0 is "undefined." Likewise 0^0' implying that 0^0 being predefined is
like 0/0 being undefined. It isn't. 0/0 is undefined because

x/y = z iff x = zy. . . . . . . . . . (***)

And that is forced on us unless someone wishes to define division such
that x/y = z iff x = zy doesn't hold. But the result would be a
kind of division quite unlike that which we are used to. There is no
fact about ^ analogous to (***) that forces 0^0 being undefined on us.
The fact is just that Dan hasn't defined 0^0. And since other people
_have_ defined 0^0 [for natural numbers 0 and 0] in a way that causes no
problems at all, it seems you are in a minority.

You sometimes write as if you think that 0^0 = 1 is dangerous and
might lead to inconsistencies. Do you think that?

> Any value would work. Other than for n=m=0, n^m is fully determined on N by
>
> 1. n^2 = n*n
> 2. n^(m+1) = n^m * n
>
> So, we leave 0^0 undefined on N, as on R

That "we" is Dan.

> .

### Mostowski Collapse

Sep 26, 2020, 12:46:30 PM9/26/20
to
If you cannot model punctuated functions
in DC Proof, its quite hopeless to do
mathematics in it.

We want to express things like:

1 + x + x^2 + ... diverges for x>=1

Usually this means the expression becomes
undefined. It doesn't mean the expression
can have any value.

### Dan Christensen

Sep 26, 2020, 1:07:36 PM9/26/20
to
On Saturday, September 26, 2020 at 12:46:30 PM UTC-4, Mostowski Collapse wrote:
> If you cannot model punctuated functions
> in DC Proof, its quite hopeless to do
> mathematics in it.
>
> We want to express things like:
>
> 1 + x + x^2 + ... diverges for x>=1
>
> Usually this means the expression becomes
> undefined.

No, it means that the partial sums increases without bound.

> It doesn't mean the expression
> can have any value.
>

Just admit you were wrong, Jan. As I have defined exponentiation on N, 0^0 is actually undefined. Deal with it.

### Mostowski Collapse

Sep 26, 2020, 2:46:08 PM9/26/20
to
What does f : A -> B mean?

### Me

Sep 26, 2020, 3:08:50 PM9/26/20
to
On Saturday, September 26, 2020 at 6:22:48 PM UTC+2, Dan Christensen wrote:

> I have shown that 0^0 is indeterminate on N.

No, you haven't.

Hint: https://www.wolframalpha.com/input/?i=n%5E0%2C+n+%3D+0
Message has been deleted

### Me

Sep 26, 2020, 3:40:52 PM9/26/20
to
On Saturday, September 26, 2020 at 6:40:55 PM UTC+2, Peter wrote:
> Dan Christensen wrote:

> You sometimes write as if you think that 0^0 = 1 is dangerous and
> might lead to inconsistencies. Do you think that?

Yes, I got that impression too.

Though there really is no reason to think so. After all we may just define ^ recursively:

n ^ 0 = 1
n ^ s(m) = (n ^ m) * n .

Save enough. :-P

In the context of set theory we may define ^ in a rather natural "set theoretic" way (implying 0^0 = 1).

Then we can easily show that these two definitions "coincide".

So what the heck is Dan's problem with 0^0 = 1 in the context of the natural numbers?

### Dan Christensen

Sep 26, 2020, 4:35:56 PM9/26/20
to
On Saturday, September 26, 2020 at 12:40:55 PM UTC-4, Peter wrote:
> Dan Christensen wrote:
> > On Saturday, September 26, 2020 at 8:20:40 AM UTC-4, Peter wrote:
> >> Peter wrote:
> >>> Dan Christensen wrote:
> >>>
> >>>
> >>>> I don't know about the philosophy department, but in mathematics, we
> >>>> say, for example, that 0/0 is "undefined." Likewise 0^0.
> >>>
> >>> Not so.
> >>
> >> You have defined a function x^y on pairs of natural numbers except
> >> (0,0). So 0^0 being undefined is just a matter of _you choosing_ not to
> >> define your x^y function at a certain point.
> >>
> >
> > I have shown that 0^0 is indeterminate on N.
>
> But it is only indeterminate in as much as you have chosen not to
> determine it.

No, it is indeterminate in as much as there are infinitely many binary functions on N that satisfy

1. n^2 = n*n
2. n^(m+1) = n^m * n

And they differ ONLY in the value they assign to 0^0, which can have any value whatsoever, hence the indeterminacy. This also has the benefit of being consistent with exponentiation on R.

### Mostowski Collapse

Sep 26, 2020, 8:06:39 PM9/26/20
to
No answer yet? Maybe you can prove these
two equivalent:

ALL(a):ALL(b):[(a,b) e f & a e A => b e B]

ALL(a):ALL(b):[(a,b) e f => a e A & b e B]

You might get an Able prize. The same prize that
John Gabbermonkey claims

for his New Calculoose.

### Mostowski Collapse

Sep 26, 2020, 8:10:46 PM9/26/20
to
partial sums increases without bound implies
divergence in R, whats wroung with you?

### Mostowski Collapse

Sep 26, 2020, 8:16:31 PM9/26/20
to

"In mathematics, a divergent series is an
infinite series that is not convergent,
meaning that the infinite sequence of
the partial sums of the series does not
have a finite limit."
https://en.wikipedia.org/wiki/Divergent_series

This means this partial function f : R+ -> R+:

f(x) = 1 + x + x^2 + ..

= lim n->oo sum_i=0^m x^i

Is punctuated, it is for example undefined for x>=1.
But undefined for x>=1 doesn't mean you can
arbitrarly choose for example f(2)=3. It would

mean ~Ex((2,x) e f). You cannot capture

Ax(x e R+ & x<1 => f(x) e R+)

### Me

Sep 26, 2020, 9:03:09 PM9/26/20
to
On Saturday, September 26, 2020 at 10:35:56 PM UTC+2, Dan Christensen wrote:

> > But it is only indeterminate in as much as you have chosen not to
> > determine it.
> >
> No, it is indeterminate in as much as <bla>

No, dumbo it's NOT indeterminate if you use the standard recursive equations for "defining" functions on IN.

n ^ 0 = 1 << base case
n ^ (m + 1) = (n ^ m) * n

What's the matter with you, idiot?

Note: You don't have a "choice" here concerning the "value" of the base case if you want to have n^2 = n*n. So, no, no "indeterminacy".

Moreover: From Concrete Mathematics p.162 (R. Graham, D. Knuth, O. Patashnik):

Some textbooks leave the quantity 0^0 undefined, because the
functions x^0 and 0^x have different limiting values when x
decreases to 0. But this is a mistake. We must define x^0=1 for all
x , if the binomial theorem is to be valid when x = 0 , y = 0 ,
and/or x = -y . The theorem is too important to be arbitrarily
restricted! By contrast, the function 0^x is quite unimportant.

### Dan Christensen

Sep 26, 2020, 11:31:44 PM9/26/20
to
On Saturday, September 26, 2020 at 9:03:09 PM UTC-4, Me wrote:
> On Saturday, September 26, 2020 at 10:35:56 PM UTC+2, Dan Christensen wrote:
>
> > > But it is only indeterminate in as much as you have chosen not to
> > > determine it.
> > >
> > No, it is indeterminate in as much as <bla>
>
> No, dumbo it's NOT indeterminate if you use the standard recursive equations for "defining" functions on IN.
>
> n ^ 0 = 1 << base case
> n ^ (m + 1) = (n ^ m) * n
>

Yes, very convenient, but not very convincing. You simply defined 0^0=1. For convenience.

A thousand years from now, I'm sure they will be laughing at us for defining it thus for nothing more than the convenience of it in certain applications. And looking the other way when it comes to the the reals.

### Peter

Sep 27, 2020, 7:11:05 AM9/27/20
to
Dan Christensen wrote:
> On Saturday, September 26, 2020 at 9:03:09 PM UTC-4, Me wrote:
>> On Saturday, September 26, 2020 at 10:35:56 PM UTC+2, Dan Christensen wrote:
>>
>>>> But it is only indeterminate in as much as you have chosen not to
>>>> determine it.
>>>>
>>> No, it is indeterminate in as much as <bla>
>>
>> No, dumbo it's NOT indeterminate if you use the standard recursive equations for "defining" functions on IN.
>>
>> n ^ 0 = 1 << base case
>> n ^ (m + 1) = (n ^ m) * n
>>
>
> Yes, very convenient, but not very convincing. You simply defined 0^0=1. For convenience.
>
> A thousand years from now, I'm sure they will be laughing at us for defining it thus for nothing more than the convenience of it in certain applications. And looking the other way when it comes to the the reals.
>

The bad thing about Usenet is that you can't delete what you want to
ignore. This

From Concrete Mathematics p.162 (R. Graham, D. Knuth, O. Patashnik):

Some textbooks leave the quantity 0^0 undefined, because the
functions x^0 and 0^x have different limiting values when x
decreases to 0. But this is a mistake. We must define x^0=1 for all
x , if the binomial theorem is to be valid when x = 0 , y = 0 ,
and/or x = -y . The theorem is too important to be arbitrarily
restricted! By contrast, the function 0^x is quite unimportant.

is still in Me's post; and so still needs to be addressed.

### Dan Christensen

Sep 27, 2020, 12:14:21 PM9/27/20
to
ME's weakest, least interesting argument, I thought. An appeal to authority? Really? One has only so much time for this sort of thing. How dare I, etc.

As I have said, there are some easy workarounds that can be used, e.g. (x+0)^2 = (x)^2, no need for 1 * x^2 * 0^0 + 2 * x^1 * 0^1 + 1 * x^0 * 0^2 in this case.

Anyway, I am curious as to why arbitrarily assigning 0^0=1 gives the required result in BT. Is there a more rigorous approach to BT using purely arithmetical methods? (Hmmm... Sounds more interesting than another proof of Zorn's Lemma!)

### Peter

Sep 27, 2020, 1:01:15 PM9/27/20
to
Dan Christensen wrote:
> On Sunday, September 27, 2020 at 7:11:05 AM UTC-4, Peter wrote:
>> Dan Christensen wrote:
>>> On Saturday, September 26, 2020 at 9:03:09 PM UTC-4, Me wrote:
>>>> On Saturday, September 26, 2020 at 10:35:56 PM UTC+2, Dan Christensen wrote:
>>>>
>>>>>> But it is only indeterminate in as much as you have chosen not to
>>>>>> determine it.
>>>>>>
>>>>> No, it is indeterminate in as much as <bla>
>>>>
>>>> No, dumbo it's NOT indeterminate if you use the standard recursive equations for "defining" functions on IN.
>>>>
>>>> n ^ 0 = 1 << base case
>>>> n ^ (m + 1) = (n ^ m) * n
>>>>
>>>
>>> Yes, very convenient, but not very convincing. You simply defined 0^0=1. For convenience.

That's right - for convenience. Do you think definitions should be
framed to be inconvenient?

>>>
>>> A thousand years from now, I'm sure they will be laughing at us for defining it thus for nothing more than the convenience of it in certain applications. And looking the other way when it comes to the the reals.
>>>
>>
>> The bad thing about Usenet is that you can't delete what you want to
>> ignore. This
>>
>> From Concrete Mathematics p.162 (R. Graham, D. Knuth, O. Patashnik):
>>
>> Some textbooks leave the quantity 0^0 undefined, because the
>> functions x^0 and 0^x have different limiting values when x
>> decreases to 0. But this is a mistake. We must define x^0=1 for all
>> x , if the binomial theorem is to be valid when x = 0 , y = 0 ,
>> and/or x = -y . The theorem is too important to be arbitrarily
>> restricted! By contrast, the function 0^x is quite unimportant.
>>
>> is still in Me's post; and so still needs to be addressed.
>
>
> ME's weakest, least interesting argument, I thought. An appeal to authority? Really?

That's right - an appeal to authority. Do you think appeals should be
to those who lack authority?

> One has only so much time for this sort of thing. How dare I, etc.
>
> As I have said, there are some easy workarounds that can be used, e.g. (x+0)^2 = (x)^2, no need for 1 * x^2 * 0^0 + 2 * x^1 * 0^1 + 1 * x^0 * 0^2 in this case.
>
> Anyway, I am curious as to why arbitrarily assigning 0^0=1 gives the required result in BT.

Something for you to look into.

> Is there a more rigorous approach to BT using purely arithmetical methods? (Hmmm... Sounds more interesting than another proof of Zorn's Lemma!)

If you can find the time when not bullying Mr Plutonium, then go for it.

### FredJeffries

Sep 27, 2020, 1:28:20 PM9/27/20
to
On Sunday, September 27, 2020 at 10:01:15 AM UTC-7, Peter wrote:
> Dan Christensen wrote:
> >>>
> >>> Yes, very convenient, but not very convincing. You simply defined 0^0=1. For convenience.
> That's right - for convenience. Do you think definitions should be
> framed to be inconvenient?

Indeed. In (formal) mathematics, definitions are nothing BUT mere conveniences, since the definiendum can always be replaced by the definiens.

https://en.wikipedia.org/wiki/Macro_(computer_science)
Message has been deleted

### Vincenzo Carratelli

Sep 27, 2020, 2:37:01 PM9/27/20
to
Dan Christensen wrote:

> I think I suggested this some time ago. How about: (x+y)^n
> = x^n + Sum(k=1,n-1):[nCk * x^(n-k) * y^(k)] + y^n for n >= 1 = 1
> for n=0 and x+y =/= 0 This way, you never have to calculate 0^0.

not true. The corona covid is not a hoax. It's proper organized crime.
Like the former "antrax" scam and the "swine flu" scam 2009, where
capitalist mafia governments, by purpose, are put to buy snake oil
quackery said "vaccines". Because big money, PUBLIC MONEY, people are to
pay. 100% profit, no risk whatsoever.

Dr.Hofmann describes CRIMINAL DIRTY PIG BIO-MEDICAL CARTEL
https://www.brighteon.com/d101fcce-7464-4c5f-b2f4-111d93ddc018

The Covid-19 Scam Is The Greatest Crime Of The Century
https://www.brighteon.com/dd27d268-4f35-43d9-a80a-c6a72ff3bbb7

### Dan Christensen

Sep 27, 2020, 3:22:11 PM9/27/20
to
On Sunday, September 27, 2020 at 12:14:21 PM UTC-4, Dan Christensen wrote:

>
> As I have said, there are some easy workarounds that can be used, e.g. (x+0)^2 = (x)^2, no need for 1 * x^2 * 0^0 + 2 * x^1 * 0^1 + 1 * x^0 * 0^2 in this case.
>
> Anyway, I am curious as to why arbitrarily assigning 0^0=1 gives the required result in BT. Is there a more rigorous approach to BT using purely arithmetical methods? (Hmmm... Sounds more interesting than another proof of Zorn's Lemma!)
>

I think I suggested this some time ago. How about:

(x+y)^n

= x^n + Sum(k=1,n-1):[nCk * x^(n-k) * y^(k)] + y^n for n > 1

= x+y for x=1

= 1 for n=0 and x+y =/= 0

This way, you never have to calculate 0^0 or empty sums.

### Peter

Sep 27, 2020, 3:23:12 PM9/27/20
to
Dan Christensen wrote:
> On Sunday, September 27, 2020 at 12:14:21 PM UTC-4, Dan Christensen wrote:
> I think I suggested this some time ago. How about:
>
> (x+y)^n
> = x^n + Sum(k=1,n-1):[nCk * x^(n-k) * y^(k)] + y^n for n >= 1
> = 1 for n=0 and x+y =/= 0
>
> This way, you never have to calculate 0^0.

What if x+y=0?

### Peter

Sep 27, 2020, 3:31:58 PM9/27/20
to
Dan Christensen wrote:
> On Sunday, September 27, 2020 at 12:14:21 PM UTC-4, Dan Christensen wrote:
>
>>
>> As I have said, there are some easy workarounds that can be used, e.g. (x+0)^2 = (x)^2, no need for 1 * x^2 * 0^0 + 2 * x^1 * 0^1 + 1 * x^0 * 0^2 in this case.
>>
>> Anyway, I am curious as to why arbitrarily assigning 0^0=1 gives the required result in BT. Is there a more rigorous approach to BT using purely arithmetical methods? (Hmmm... Sounds more interesting than another proof of Zorn's Lemma!)
>>
>
> I think I suggested this some time ago. How about:
>
> (x+y)^n
>
> = x^n + Sum(k=1,n-1):[nCk * x^(n-k) * y^(k)] + y^n for n > 1
>
> = x+y for x=1
>
> = 1 for n=0 and x+y =/= 0
>
> This way, you never have to calculate 0^0 or empty sums.

Two questions - where is the binomial theorem, and what if x+y=0?

### Dan Christensen

Sep 27, 2020, 4:54:21 PM9/27/20
to

> and what if x+y=0?

Then (x+y)^0 would be undefined. Not great loss AFAICT.
Message has been deleted

### Me

Sep 27, 2020, 5:16:39 PM9/27/20
to

On Sunday, September 27, 2020 at 10:54:21 PM UTC+2, Dan Christensen wrote:
> >
> > and what if x+y=0?
> >
> Then (x+y)^0 would be undefined. Not great loss AFAICT.

Yeah, we only lose infinitely many cases:

x = 0, y = 0
x = 1, y = -1
x = -1, y = 1
x = 2, y = -2
x = -2, y = 2
:

### Me

Sep 27, 2020, 5:19:58 PM9/27/20
to
Hint:

"Some textbooks leave the quantity 0^0 undefined [...].
But this is a mistake. We must define x^0 = 1 for all x,
if the binomial theorem is to be valid when x = 0, y = 0,
and/or x = -y. The theorem is too important to be arbitrarily
restricted!"

(R. Graham, D. Knuth, O. Patashnik, Concrete Mathematics, p.162)

### Dan Christensen

Sep 27, 2020, 6:05:01 PM9/27/20
to
Why is that important? Does 0^0 actually come up in applications?

### Me

Sep 27, 2020, 7:25:45 PM9/27/20
to
On Monday, September 28, 2020 at 12:05:01 AM UTC+2, Dan Christensen wrote:

> Does 0^0 actually come up in applications?

Yeah, one such "application" is called /binomial theorem/.
See: https://en.wikipedia.org/wiki/Binomial_theorem

For more applications see: "What is 0^0? - Examples"
here: https://www.maa.org/book/export/html/116806

### Dan Christensen

Sep 27, 2020, 10:42:50 PM9/27/20
to
On Sunday, September 27, 2020 at 7:25:45 PM UTC-4, Me wrote:
> On Monday, September 28, 2020 at 12:05:01 AM UTC+2, Dan Christensen wrote:
>
> > Does 0^0 actually come up in applications?
>
> Yeah, one such "application" is called /binomial theorem/.
> See: https://en.wikipedia.org/wiki/Binomial_theorem
>

Not necessarily as it turns. The only result that it seems cannot be obtained without defining 0^0=1, is, not surprisingly, (x+(-x))^0 = 1.

### Me

Sep 27, 2020, 10:54:14 PM9/27/20
to
On Monday, September 28, 2020 at 4:42:50 AM UTC+2, Dan Christensen wrote

concerning the /binomial theorem/:

> The only result that it seems cannot be obtained without defining 0^0=1, is,
> not surprisingly, (x+(-x))^0 = 1.

Actually, there are infinitely many cases, dumbo:

x = 0, y = 0
x = 1, y = -1
x = -1, y = 1
x = 2, y = -2
x = -2, y = 2
:

You know, (if we consider /n/ as a parameter here) there are two independent variables in:

(x + y)^n .

### Dan Christensen

Sep 27, 2020, 11:31:28 PM9/27/20
to
On Sunday, September 27, 2020 at 10:54:14 PM UTC-4, Me wrote:
> On Monday, September 28, 2020 at 4:42:50 AM UTC+2, Dan Christensen wrote
>
> concerning the /binomial theorem/:
>
> > The only result that it seems cannot be obtained without defining 0^0=1, is,
> > not surprisingly, (x+(-x))^0 = 1.
>
> Actually, there are infinitely many cases, dumbo:
>
> x = 0, y = 0
> x = 1, y = -1
> x = -1, y = 1
> x = 2, y = -2
> x = -2, y = 2
> :
>

Idiot! How many cases do you imagine is covered by (x+(-x))^0 = 1? One or two?

Dan

### Me

Sep 28, 2020, 12:33:52 AM9/28/20
to
On Monday, September 28, 2020 at 5:31:28 AM UTC+2, Dan Christensen wrote:

> Idiot! How many cases do you imagine is covered by (x+(-x))^0 = 1? One or two?

You don't know what you are talking about, dumbo. :-)

### Mostowski Collapse

Nov 21, 2020, 7:52:24 PM11/21/20
to
Hi Dan-O-Matik, can you prove Smullyan's riddle:

∀x∀y(P(x) v P(y)) => ∃x∀y(x≠y => P(y)) v ∀xP(x)

### Mostowski Collapse

Nov 21, 2020, 8:08:43 PM11/21/20
to
Corr.:
∀x∀y(x≠y => P(x) v P(y)) => ∃x∀y(x≠y => P(y))

### Mostowski Collapse

Nov 22, 2020, 3:31:30 AM11/22/20
to
Can you show the two formulas equivalent in DC Proof?

Its not so difficult to prove. The left hand side
is logically equivalent to. It says that there is
a unique ~P element if one exists:

∀x∀y(~P(x) & ~P(y) => x=y)

The right hand side is logically equivalent to. It also
says that there is a unique ~P element if
one exists:

∃x∀y(~P(y) => x=y)

So both statements in Smullyan's riddle are stripped
down uniqueness quantifiers ∃! . Where as the uniqueness
quantifier additionally would say ∃x~P(x) and giving

the uniqueness quantifier the meaning of exactly
one, ∃! = ∃=1, do the two formulas express maximally
one, i.e. ∃=<1. Since the ordinary existential quantifier

says at least one, i.e. ∃>=1, it is clear that if we would
add ∃x~P(x) we would indeed get ∃!x~P(x), since
∃! = ∃=1 = ∃=<1 & ∃>=1.

So can you show the two formulas equivalent in DC Proof?

Have Fun!

### Me

Nov 23, 2020, 5:50:45 AM11/23/20
to
On Sunday, November 22, 2020 at 2:08:43 AM UTC+1, Mostowski Collapse wrote:

> ∀x∀y(x≠y => P(x) v P(y)) => ∃x∀y(x≠y => P(y))

In Lemmon's System of ND:

|- AxAy(~(x = y) -> Fx v Fy) -> ExAy(~(x = y) -> Fy)

1 (1) AxAy(~(x = y) -> Fx v Fy) A
(2) AxFx v ~AxFx TI (P v ~P)
3 (3) AxFx A
3 (4) Fb 3 AE
3 (5) ~(a = b) -> Fb 4 SI (R |- S -> R)
3 (6) Ay(~(a = y) -> Fy)) 5 AI
3 (7) ExAy(~(x = y) -> Fy) 6 EI
8 (8) ~AxFx A
8 (9) Ex~Fx 8 SI (~AvQv |- Ex~Qx)
10 (10) ~Fa A
1 (11) Ay(~(a = y) -> Fa v Fy) 1 AE
1 (12) ~(a = b) -> Fa v Fb 11 AE
13 (13) ~(a = b) A
1,13 (14) Fa v Fb 12,13 ->E
1,10,13 (15) Fb 10,14 SI (~T, T v U |- U)
1,10 (16) ~(a = b) -> Fb 13,15 ->I
1,10 (17) Ay(~(a = y) -> Fy) 16 AI
1,10 (18) ExAy(~(x = y) -> Fy) 17 EI
1,8 (19) ExAy(~(x = y) -> Fy) 9,10,18 EE
1 (20) ExAy(~(x = y) -> Fy) 2,3,7,8,19 vE
(21) AxAy(~(x = y) -> Fx v Fy) -> ExAy(~(x = y) -> Fy) 1,20 ->I

### Mostowski Collapse

Nov 23, 2020, 6:44:22 AM11/23/20
to
Noice! Not possible in DC Proof because of some
empty universe issue? LoL

BTW: I forgot to give the reference to the puzzle.
Take P(_) as corrupt politician:

Raymond Smullyan on Carson, 1982

### Mostowski Collapse

Nov 24, 2020, 8:10:04 AM11/24/20
to
Now we might see Zorns Lemma, 100 years from
now. Dan-O-Matik busy inserting U(_) in the proof
of Zorns Lemma, because it doesn't work otherwise.

LoL

### Dan Christensen

Nov 24, 2020, 11:03:15 AM11/24/20
to
On Tuesday, November 24, 2020 at 8:10:04 AM UTC-5, Mostowski Collapse wrote:
> Now we might see Zorns Lemma, 100 years from
> now. Dan-O-Matik busy inserting U(_) in the proof
> of Zorns Lemma, because it doesn't work otherwise.
>

DC Proof can be used to reveal the hidden, behind-the-scenes machinations of standard FOL by making the non-empty domain of discourse explicit. See, for example, my recently poste proof of Smullyan's "Riddle" at https://www.dcproof.com/SmullyansRiddle.htm (81 lines in the DC Proof 2.0 format)

There, I restrict every quantifier by the same unary predicate U and start with an axiom: EXIST(x): U(x).

Quantifiers are translated from as follows:

Ax (P(x)) ----> ALL(x):[U(x) => P(x)]

Ex (P(x)) ----> EXIST(x):[U(x) & P(x)]

Some adjustments must be made for the fact that, in DC Proof (as in most math textbooks) new free variables cannot be introduced by universal specification (A elimination).

The theorem then becomes:

ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]] <=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

### Me

Nov 24, 2020, 11:42:29 AM11/24/20
to
On Tuesday, November 24, 2020 at 5:03:15 PM UTC+1, Dan Christensen wrote:

> DC Proof can be used to reveal the hidden, behind-the-scenes machinations of standard FOL by making the non-empty
> domain of discourse explicit.

Fair enough. There's certainly a place for an "inclusive logic" in certain contexts.

### Mostowski Collapse

Nov 24, 2020, 4:52:39 PM11/24/20
to
You were lucky that the Smullyan Riddle, didn't
need ALL(x):U(x) as well. Examples were made
in the past here on sci.logic, that needed this as well.

Try proving:

ALL(x):[x = c => P(x)] <=> EXIST(x):[x = c & P(x)]

### Mostowski Collapse

Nov 24, 2020, 5:20:36 PM11/24/20
to
This possibly doesn't work either:

∀x(Fx => Gx), ∀xFx |- Ga

Its from here:

All frogs are green
Everything is a frog
:. Alf is green

over 550 solved problems
https://epdf.pub/schaums-outline-of-theory-and-problems-of-logic-.html