442 views

Skip to first unread message

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?

in DC Proof? Translate FOL to DC Proof?

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).
> So whats the plan for proving Zorn's Lemma

> in DC Proof? Translate FOL to DC Proof?

Dan

Sep 23, 2020, 12:22:03 AM9/23/20

to

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.

Sep 23, 2020, 8:07:48 AM9/23/20

to

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.

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."
> 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.

>

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

> strength.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com

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

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?
> 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.

>

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

derivable.

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?

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)

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)

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)

P & ~P => Q(a)

Can we prove this in DC Proof?

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

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

to

See my reply just now to your identical posting at sci.math

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.

mathematics, you would not come up with some

empty name nonsense from philosophy department.

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.
> If you would knew how "undef" is handled in

> mathematics, you would not come up with some

> empty name nonsense from philosophy department.

>

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.
> I don't know about the philosophy department, but in mathematics, we

> say, for example, that 0/0 is "undefined." Likewise 0^0.

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?

"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?

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:
> 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.

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

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?

You write it yourself in your blog.

exp(0,0)=1 is possible, exp'(0,0)=2 is possible.

Whats wrong with you?

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.

>

See my reply your identical posting at sci.math today.
> 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.

>

Sep 26, 2020, 8:20:40 AM9/26/20

to

(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.

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.

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.

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

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

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

>

1. n^2 = n*n

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

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

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.
> "_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.

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

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

> .

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.

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.

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

>

Sep 26, 2020, 2:46:08 PM9/26/20

to

What does f : A -> B mean?

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.
> I have shown that 0^0 is indeterminate on N.

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

Message has been deleted

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.
> 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?

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?

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

1. n^2 = n*n

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

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.

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.

Sep 26, 2020, 8:10:46 PM9/26/20

to

partial sums increases without bound implies

divergence in R, whats wroung with you?

divergence in R, whats wroung with you?

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

this with your Dan-O-Matik nonsense:

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

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>
> > But it is only indeterminate in as much as you have chosen not to

> > determine it.

> >

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.

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

>

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.

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

>

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.

Sep 27, 2020, 12:14:21 PM9/27/20

to

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!)

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

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?

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.

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

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.
> 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?

https://en.wikipedia.org/wiki/Macro_(computer_science)

Message has been deleted

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

> 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

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!)

>

>

> 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)^n

= x+y for x=1

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

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:

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

> (x+y)^n

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

>

> This way, you never have to calculate 0^0.
>

What if x+y=0?

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?
> 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.

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

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.

x = 0, y = 0

x = 1, y = -1

x = -1, y = 1

x = 2, y = -2

x = -2, y = 2

:

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

to

"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)

Sep 27, 2020, 6:05:01 PM9/27/20

to

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/.
> Does 0^0 actually come up in applications?

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

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

>

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 .

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.

x = 0, y = 0

x = 1, y = -1

x = -1, y = 1

x = 2, y = -2

x = -2, y = 2

:

(x + y)^n .

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

> :

>

Dan

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. :-)
> Idiot! How many cases do you imagine is covered by (x+(-x))^0 = 1? One or two?

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)

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

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

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

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!

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!

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:
> ∀x∀y(x≠y => P(x) v P(y)) => ∃x∀y(x≠y => P(y))

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

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

https://www.youtube.com/watch?v=E27v83WWiGo

empty universe issue? LoL

BTW: I forgot to give the reference to the puzzle.

Take P(_) as corrupt politician:

Raymond Smullyan on Carson, 1982

https://www.youtube.com/watch?v=E27v83WWiGo

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

now. Dan-O-Matik busy inserting U(_) in the proof

of Zorns Lemma, because it doesn't work otherwise.

LoL

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)
> 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.

>

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)]]]

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

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)]

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)]

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

∀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

Nov 24, 2020, 10:42:08 PM11/24/20