Zorn's Lemma, how formalize it in DC Proof

[Mostowski Collapse]

So whats the plan for proving Zorn's Lemma
in DC Proof? Translate FOL to DC Proof?

[Dan Christensen]

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]

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]

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]

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

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

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]

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]

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

[Mostowski Collapse]

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]

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]

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

[Mostowski Collapse]

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]

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]

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]

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]

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]

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]

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.

[Peter]

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]

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

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]

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]

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]

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]

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]

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]

What does f : A -> B mean?

[Me]

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

[Me]

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]

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]

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]

partial sums increases without bound implies
divergence in R, whats wroung with you?

[Mostowski Collapse]

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

[Me]

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]

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]

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]

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]

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]

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)

[Vincenzo Carratelli]

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]

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]

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]

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]

Google it. Millions of hits.


> and what if x+y=0?

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

[Me]

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]

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]

Why is that important? Does 0^0 actually come up in applications?

[Me]

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]

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]

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]

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]

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]

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]

Corr.:
∀x∀y(x≠y => P(x) v P(y)) => ∃x∀y(x≠y => P(y))

[Mostowski Collapse]

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]

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]

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

[Mostowski Collapse]

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]

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]

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]

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]

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

[Dan Christensen]

On Tuesday, November 24, 2020 at 4:52:39 PM UTC-5, Mostowski Collapse wrote:

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

Try it yourself, Jan.

Hint:

1 EXIST(a):U(a) (Axiom)

2 U(c) (E Spec, 1)
.
.
.
26 ALL(a):[U(a) => [a=c => P(a)]] <=> EXIST(a):[U(a) & [a=c & P(a)]] (Iff-And, 25)

[Dan Christensen]

On Tuesday, November 24, 2020 at 5:20:36 PM UTC-5, Mostowski Collapse wrote:
> 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
>

Try it yourself, Jan.

Hint:

1 EXIST(a):U(a) (Axiom)

2 U(alf) (E Spec, 1)
.
.
.
11 ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf) (Conclusion, 3)

[Mostowski Collapse]

There is obviously a counter model to what you proved.
Take this model, where bert≠alf:

U={bert}
F={bert}
G={bert}

How on earth can you prove ALL(a):[U(a) => [F(a) => G(a)]] &
ALL(a):[U(a) => F(a)] => G(alf). Thats just nonsense.

Maybe draw a Venn diagram. The part:
ALL(a):[U(a) => [F(a) => G(a)]] Says U n F subset G,
and the part: ALL(a):[U(a) => F(a)] Says U subset F.

How on earth can you conclude alfe e G ?

LoL

[Mostowski Collapse]

Dang you are a moron, you proved something else:

EXIST(alf):[U(alf)
& [ALL(a):[U(a) => [F(a) => G(a)]]

& ALL(a):[U(a) => F(a)]

=> G(alf)]]
http://dcproof.com/AlfIsGreen.htm

So you have arbitrary rules, not only Ax (P(x)) ----> ALL(x):[U(x) => P(x)]
and Ex (P(x)) ----> EXIST(x):[U(x) & P(x)]. Thats interesting. What
are your students saying? Do they like it?

Maybe try the simpler axiom ALL(a):U(a). LoL

[Mostowski Collapse]

But it seems on line 11 you indeed prove:

11 ALL(a):[U(a) => [F(a) => G(a)]]
& ALL(a):[U(a) => F(a)]
=> G(alf)

4 Conclusion, 3

So I guess DC Proof has bug, we found a bug.

Because the above is not a theorem. Even not with
the assumption EXIST(a):U(a). I saved the proof here on gist:
https://gist.github.com/jburse/51cd3886c7ceef5035ea7e2860b096a2#gistcomment-3539726

There something wrong with your E Spec rule.

[Me]

On Wednesday, November 25, 2020 at 4:47:09 AM UTC+1, Dan Christensen wrote:

> Try it yourself, Jan.
>
> Hint:
>
> 1 EXIST(a):U(a) (Axiom)
> 2 U(alf) (E Spec, 1)
> .
> .
> .
> 11 ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf) (Conclusion, 3)

Nope.

Hint: You introduced "alf" with an application of E Spec (usually called Existential Instantiation) here:

2 U(alf) (E Spec, 1)

And you stop here:

11 ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf) (Conclusion, 3)

In this case, 11 is not a proven theorem! (Note that 11 still contains "alf".)

Hint:

"In predicate logic, existential instantiation [...] is a rule of inference which says that, given a formula of the form Ex Phi(x), one may infer Phi (c) for a new constant symbol c. The rule has the restrictions that the constant c introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof."

You will find explained that in detail below:

"[...] we have kept the Existential-Elimination (∃-Elimination) rule used by Lemmon [and ND by Genzten --me]. [Note that] at any point in a proof using ∃-elimination, some argument has been proven. [...] In a system using ∃-instantiation, however, this feature is absent: there are correct proofs some of whose lines do not follow from previous lines, since the rule of ∃-instantiation is not a valid rule. For instance, the following is the beginning of a proof using ∃-instantiation.

1 (1) ∃xFx assumption
1 (2) Fa 1 ∃-instantiation

Line 2 does not follow from line 1. This difference between ∃-elimination and ∃-instantiation can be put as follows: in an ∃-elimination proof, you can stop at any time and still have a correct proof of some argument or other, but in an ∃-instantiation proof, you cannot stop whenever you like. It seems to us that these implications of ∃-instantiation's invalidity outweigh the additional complexity of ∃-elimination. In an ∃-elimination system, not only is the system sound as a whole, but every rule is individually valid; this is not true for an ∃-instantiation system."

(Colin Allen and Michael Hand, Logic Primer)

So I'd say: "Something is rotten in the state of Denmark …"

Actually, Allen and Hand write:

"[....] at any point in a proof using ∃-elimination, some argument has been proven. If the proof has reached a line of the form

m,...,n (k) z ...

then the sentence z has been established as provable from the premise set {m,...,n}. (Here the right-hand ellipsis indicates which rule was applied to yield z, and which earlier sentences it was applied to.) This is quite useful in helping the student understand what is going on in a proof."

Indeed! :-)

[Me]

On Wednesday, November 25, 2020 at 9:53:32 AM UTC+1, Mostowski Collapse wrote:

> There something wrong with your E Spec rule.

Well, it's not a VALID rule of derivation (and I abhor that "feature" of that "rule of derivation"). See my reply to Dan (above).

Lit.: https://en.wikipedia.org/wiki/Existential-instantiation

In respect to DC Proof (considered as a proof system) we might state "Something is rotten in the state of Denmark" though.

[Mostowski Collapse]

There is a Trump meme now, in conclusion:

DC-Proof, E Spec
Sounds good, doesn't work

https://gist.github.com/jburse/51cd3886c7ceef5035ea7e2860b096a2#gistcomment-3539903

[Me]

On Tuesday, November 24, 2020 at 11:20:36 PM UTC+1, Mostowski Collapse wrote:

> 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

This example can be simplified:

∀xFx |- Fa

Everything is a frog
:. Alf is a frog

This can be shown/proven in FOPL. But Dan is right concerning the "implicit assumption" in FOPL that the universe is not empty. Otherwise this might not be a valid "argument".

So in Free Logic we would have

∀xFx, E!a |- Fa ,

iirc.

Everything (that exists) is a frog
Alf exists
:. Alf is a frog

[Dan Christensen]

(Correction)

On Wednesday, November 25, 2020 at 3:40:30 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 25. November 2020 um 04:47:09 UTC+1:
> > On Tuesday, November 24, 2020 at 5:20:36 PM UTC-5, Mostowski Collapse wrote:
> > > 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
> > >
> > Try it yourself, Jan.
> >
> > Hint:
> >
> > 1 EXIST(a):U(a) (Axiom)
> > 2 U(alf) (E Spec, 1)
> > .
> > .
> > .
> > 11 ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf) (Conclusion, 3)

[snip]

> How on earth can you prove ALL(a):[U(a) => [F(a) => G(a)]] &
> ALL(a):[U(a) => F(a)] => G(alf). Thats just nonsense.
>

You implicitly introduced an element of the "domain of discourse" and named it "alf". I just made that step explicit in lines 1 and 2.

> Maybe draw a Venn diagram. The part:
> ALL(a):[U(a) => [F(a) => G(a)]] Says U n F subset G,
> and the part: ALL(a):[U(a) => F(a)] Says U subset F.
>
> How on earth can you conclude alfe e G ?
>

It's unavoidable. Draw the diagram (3 overlapping circles for U, F and G). Since alf is in U, it must be in G.

[Dan Christensen]

On Wednesday, November 25, 2020 at 6:39:02 AM UTC-5, Me wrote:
> On Wednesday, November 25, 2020 at 4:47:09 AM UTC+1, Dan Christensen wrote:
>
> > Try it yourself, Jan.
> >
> > Hint:
> >
> > 1 EXIST(a):U(a) (Axiom)
> > 2 U(alf) (E Spec, 1)
> > .
> > .
> > .
> > 11 ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf) (Conclusion, 3)
> Nope.
>
> Hint: You introduced "alf" with an application of E Spec (usually called Existential Instantiation) here:
> 2 U(alf) (E Spec, 1)

There, I am just making explicit that which was implicit in Jan's original presentation of the problem.

> And you stop here:
> 11 ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf) (Conclusion, 3)
> In this case, 11 is not a proven theorem! (Note that 11 still contains "alf".)
>

I have since gone on to generalize:

13 EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]] (E Gen, 12)

See: http://dcproof.com/AlfIsGreen.htm

[Me]

On Wednesday, November 25, 2020 at 4:46:55 PM UTC+1, Dan Christensen wrote:

> You [refered to] an element of the "domain of discourse" [using the name] "alf".

Right.

> I just made that step explicit in lines 1 and 2.

Nonsense. Look,

ExFx |- Fa

(where a is a constant) is simply not a logically valid argument.

"[...] the rule of ∃-instantiation [your E Spec, Dan --me] is not a valid rule. For instance, the following is the beginning of a proof using ∃-instantiation.

(1) ExFx assumption
(2) Fa 1 E-instantiation

Line 2 does not follow from line 1." (See my other posts.)

When will you learn, Dan?

[Me]

On Wednesday, November 25, 2020 at 5:04:08 PM UTC+1, Dan Christensen wrote:

> I have since gone on to [...]:

>
> 13 EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]] (E Gen, 12)

So "alf" is a VARIABLE here. Bad idea to ignore the distinction between variables and constants (or "arbitrary names") in variant of ND.

See: https://en.wikipedia.org/wiki/Existential_instantiation

[Dan Christensen]

On Wednesday, November 25, 2020 at 11:15:48 AM UTC-5, Me wrote:
> On Wednesday, November 25, 2020 at 5:04:08 PM UTC+1, Dan Christensen wrote:
>
> > I have since gone on to [...]:
> >
> > 13 EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]] (E Gen, 12)
> So "alf" is a VARIABLE here. Bad idea to ignore the distinction between variables and constants (or "arbitrary names") in variant of ND.
>

I make no formal distinction between variables in constant in DC Proof. I haven't found any need to. When I say informally that x is a constant, I am simply saying that, strictly for readability, I don't intend to generalize on x even though I could easily do so.

[Mostowski Collapse]

But then DC Proof format does not exist. You can produce DC Proofs
in your format, which are nowhere in logic Proofs.

Even if Alf is a variable and not a constant, this here
is not generally valid:

∃xUx, ∀x(Ux→(Fx→Gx)), ∀x(Ux→Fx) does not entail Ga.

You can check here:

https://www.umsu.de/trees/#%E2%88%83xUx,%20%E2%88%80x%28Ux%20%E2%86%92%20%28Fx%20%E2%86%92%20Gx%29%29,%20%E2%88%80x%28Ux%20%E2%86%92%20Fx%29%20|=%20Ga

There is a countermodel over a domain of size 2 consisting
of the elements {0,1}, where the variable gets assigned the value 0.

Countermodel:
a: 0
G: { 1 }
U: { 1 }
F: { 1 }

But to be a variable, there must be never a countermodel.

[Me]

On Wednesday, November 25, 2020 at 5:30:49 PM UTC+1, Dan Christensen wrote:
> On Wednesday, November 25, 2020 at 11:15:48 AM UTC-5, Me wrote:
> > On Wednesday, November 25, 2020 at 5:04:08 PM UTC+1, Dan Christensen wrote:
> > >
> > > I have since gone on to [...]:
> > >
> > > 13 EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]] (E Gen, 12)
> > >
> > So "alf" is a VARIABLE here. Bad idea to ignore the distinction between variables and constants (or "arbitrary names")

> > in a variant of ND.
> >
> I make no formal distinction between variables in constant in DC Proof. I <whatever>

Yeah, I just told you: Bad idea to ignore the distinction between variables and constants (or "arbitrary names") in a variant of ND.

When will you ever learn?

[Dan Christensen]

On Wednesday, November 25, 2020 at 12:34:46 PM UTC-5, Mostowski Collapse wrote:

> But to be a variable, there must be never a countermodel.
> Dan Christensen schrieb am Mittwoch, 25. November 2020 um 17:30:49 UTC+1:
> > On Wednesday, November 25, 2020 at 11:15:48 AM UTC-5, Me wrote:
> > > On Wednesday, November 25, 2020 at 5:04:08 PM UTC+1, Dan Christensen wrote:
> > >
> > > > I have since gone on to [...]:
> > > >
> > > > 13 EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]] (E Gen, 12)
> > > So "alf" is a VARIABLE here. Bad idea to ignore the distinction between variables and constants (or "arbitrary names") in variant of ND.
> > >

> > I make no formal distinction between variables and constants in DC Proof. I haven't found any need to. When I say informally that x is a constant, I am simply saying that, strictly for readability, I don't intend to generalize on x even though I could easily do so.

> But then DC Proof format does not exist. You can produce DC Proofs
> in your format, which are nowhere in logic Proofs.
>
> Even if Alf is a variable and not a constant, this here
> is not generally valid:
>
> ∃xUx, ∀x(Ux→(Fx→Gx)), ∀x(Ux→Fx) does not entail Ga.
>

Assuming EXIST:U(a), I proved:

EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]]

Deal with it.

> You can check here:
>
> https://www.umsu.de/trees/#%E2%88%83xUx,%20%E2%88%80x%28Ux%20%E2%86%92%20%28Fx%20%E2%86%92%20Gx%29%29,%20%E2%88%80x%28Ux%20%E2%86%92%20Fx%29%20|=%20Ga
>
> There is a countermodel over a domain of size 2 consisting
> of the elements {0,1}, where the variable gets assigned the value 0.
>
> Countermodel:
> a: 0
> G: { 1 }
> U: { 1 }

Should be U: {0, 1} in this context.

> F: { 1 }
>

In this model, there exists x such that U(x) and ~F(x), namely x=0. So, this is NOT a model.

[Dan Christensen]

Please explain why you think it is a bad idea. What inconsistencies or other problems do you think might arise from it.

[Me]

On Wednesday, November 25, 2020 at 7:34:40 PM UTC+1, Dan Christensen wrote:

> Please explain why you think it is a bad idea.

A formula like

F(x)

where "x" is a variable is not even a /statement/ (in a certain sense). That's why I don't like such an approach (in the context of a logical system).

For example, if we know that "AxFx" is true then the claim that, say, "F(Dan) is true" is justified (where "Dan" is considered a "singular term", say, a constant). In other words, we have

AxFx |= F(Dan)

See: https://en.wikipedia.org/wiki/Singular_term

Actually, I would not allow for "open sentences" (formula containin free variables) in my logical system.

[Me]

On Wednesday, November 25, 2020 at 8:01:55 PM UTC+1, Me wrote:

> Actually, I would not allow for "open sentences" (formula containin free variables) in my logical system.

Of course it's possible to use such logical calculi (from a formal point of view), but I don't like them from a more "philosophical" point of view, they just don't make much "sense".

I guess that's why many (if not most) systems of ND adopt "constants" (and some even so called "abitrary names", or "parameters") besides variables.

You will see that even the "E Spec" rule as formulated in the following article is referring to a /constant/:
https://en.wikipedia.org/wiki/Existential_instantiation

[Dan Christensen]

Good luck selling that! I still don't understand your objection.

[Me]

On Wednesday, November 25, 2020 at 8:48:03 PM UTC+1, Dan Christensen wrote:

> Good luck selling that!

There is no need to "sell" that, you silly dumbfuck!

I already told you that many (if not most) systems of ND adopt "constants" (and some even so called "abitrary names", or "parameters") besides variables.

> I still don't understand your objection.

Agree with you.

EOD

[Mostowski Collapse]

You don't get it? If you say:

EXIST(a):U(a)

This doesn't mean U: {0, 1}.

[Mostowski Collapse]

Also EXIST(a):U(a) and EXIST(alf):U(alf)
doesn't mean U: {0, 1}. So to speak you could
have a = alfa. And why would you want U: {0, 1},

the counter model with U:{1} for this formula,
under the assumption EXIST(a):U(a). The formula
has undeniable a counter model:

ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)

And DC Proof shows it as a theorem. I don't
see any flag that would say its not a theorem.
Or does it? How do I see that something is

not a theorem? You said its a theorem. It says only:

11 ALL(a):[U(a) => [F(a) => G(a)]]

& ALL(a):[U(a) => F(a)]
=> G(alf)

4 Conclusion, 3

Where does it say the proof is not complete?
The red color of alf?

[Dan Christensen]

On Wednesday, November 25, 2020 at 3:36:59 PM UTC-5, Mostowski Collapse wrote:
> Mostowski Collapse schrieb am Mittwoch, 25. November 2020 um 21:23:58 UTC+1:
> > Dan Christensen schrieb am Mittwoch, 25. November 2020 um 19:31:28 UTC+1:

> > > Assuming EXIST:U(a), I proved:

> > > EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]]

> > > Deal with it.

> > > > There is a countermodel over a domain of size 2 consisting
> > > > of the elements {0,1}, where the variable gets assigned the value 0.
> > > >
> > > > Countermodel:
> > > > a: 0
> > > > G: { 1 }
> > > > U: { 1 }
> > > Should be U: {0, 1} in this context.
> > >
> > > > F: { 1 }
> > > >
> > >
> > > In this model, there exists x such that U(x) and ~F(x), namely x=0. So, this is NOT a model.

> > You don't get it? If you say:
> >
> > EXIST(a):U(a)
> >
> > This doesn't mean U: {0, 1}.

U is the domain of discourse. In your example, you have U = {0, 1}.

> the counter model with U:{1} for this formula,

[snip]

This contradicts your requirement of "a domain of size 2 consisting of the elements {0,1}."

[Mostowski Collapse]

No U is predicate. Like F and G. Its the same
like in DC Proof.

Even if Alf is a variable and not a constant, this here
is not generally valid:

∃xUx, ∀x(Ux→(Fx→Gx)), ∀x(Ux→Fx) does not entail Ga.

You can check here:

https://www.umsu.de/trees/#%E2%88%83xUx,%20%E2%88%80x%28Ux%20%E2%86%92%20%28Fx%20%E2%86%92%20Gx%29%29,%20%E2%88%80x%28Ux%20%E2%86%92%20Fx%29%20|=%20Ga

There is a countermodel over a domain of size 2 consisting
of the elements {0,1}, where the variable gets assigned the value 0.

Countermodel:
a: 0
G: { 1 }
U: { 1 }

F: { 1 }

You don't see the domain in FOL. There is no predicate D per se,
for the domain. Also no Theorem Prover will assume that when
you name a predicate U, that it means universe.

[Mostowski Collapse]

If you want U(_) to be the FOL universe, you
must introduce an axiom:

∀xUx

You don't use this in your DC Proof formulation,
and I also didn't supply a formula with

the above axiom to the model finder. As long
as you don't have such an axiom, U can be smaller

than the FOL universe.

[Mostowski Collapse]

Maybe FOL is too edgy for Dan-O-Matik. He is asking
very strange question about U(_) must be {0,1}
in a FOL model with such a domain.

As if a theorem prover would make an exception
if he sees the letter "U" and especially for lazy
Dan-O-Matik would add this axiom:

∀xUx

To the best of my knowledge theorem provers
are WYSIWYG (What You Say Is What You Get).

[Dan Christensen]

On Wednesday, November 25, 2020 at 4:16:08 PM UTC-5, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Mittwoch, 25. November 2020 um 22:12:58 UTC+1:
> > > On Wednesday, November 25, 2020 at 3:36:59 PM UTC-5, Mostowski Collapse wrote:
> > > > Mostowski Collapse schrieb am Mittwoch, 25. November 2020 um 21:23:58 UTC+1:
> > > > > Dan Christensen schrieb am Mittwoch, 25. November 2020 um 19:31:28 UTC+1:
> > >
> > > > > > Assuming EXIST:U(a), I proved:
> > >
> > > > > > EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]]
> > >
> > > > > > Deal with it.
> > > > > > > There is a countermodel over a domain of size 2 consisting
> > > > > > > of the elements {0,1}, where the variable gets assigned the value 0.
> > > > > > >
> > > > > > > Countermodel:
> > > > > > > a: 0
> > > > > > > G: { 1 }
> > > > > > > U: { 1 }
> > > > > > Should be U: {0, 1} in this context.
> > > > > >
> > > > > > > F: { 1 }
> > > > > > >
> > > > > >
> > > > > > In this model, there exists x such that U(x) and ~F(x), namely x=0. So, this is NOT a model.
> > > > > You don't get it? If you say:
> > > > >
> > > > > EXIST(a):U(a)
> > > > >
> > > > > This doesn't mean U: {0, 1}.
> > > U is the domain of discourse. In your example, you have U = {0, 1}.
> > > > the counter model with U:{1} for this formula,
> > > [snip]
> > >
> > > This contradicts your requirement of "a domain of size 2 consisting of the elements {0,1}."

No comment?

> > No U is predicate. Like F and G. Its the same
> > like in DC Proof.

Do try to be consistent, Jan.

> > Even if Alf is a variable and not a constant, this here
> > is not generally valid:
> >
> > ∃xUx, ∀x(Ux→(Fx→Gx)), ∀x(Ux→Fx) does not entail Ga.

Again, assuming EXIST(a): U(a), I proved:

EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]]

Deal with it.


> > There is a countermodel over a domain of size 2 consisting
> > of the elements {0,1}, where the variable gets assigned the value 0.
> >
> > Countermodel:
> > a: 0
> > G: { 1 }
> > U: { 1 }

Again, should be U: {0, 1}. You wanted "a domain of size 2 consisting of the elements {0,1}"

> > F: { 1 }
> >
> > You don't see the domain in FOL. There is no predicate D per se,
> > for the domain.

Could be one of the reasons that standard FOL is not a required subject in pure math programs.

[Me]

On Wednesday, November 25, 2020 at 10:46:53 PM UTC+1, Dan Christensen wrote:

> Again, assuming EXIST(a): U(a), I proved:
> EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]]

Which is correct:
https://www.umsu.de/trees/#%E2%88%83xUx%20|=%20%E2%88%83y(Uy%20%E2%88%A7%20%E2%88%80x(Ux%20%E2%86%92%20(Fx%20%E2%86%92%20Gx))%20%E2%88%A7%20%E2%88%80x(Ux%20%E2%86%92%20Fx)%20%E2%86%92%20Gy)

On the other hand, MC just asked for a proof of

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

You REALLY think that DC Proof SIMPLYFIES things?!

Well... see: https://de.wikipedia.org/wiki/Realit%C3%A4tsverlust#:~:text=Realit%C3%A4tsverlust%20beschreibt%20den%20geistigen%20Zustand,sie%20sich%20befindet%2C%20zu%20begreifen.

[Dan Christensen]

On Wednesday, November 25, 2020 at 5:04:42 PM UTC-5, Me wrote:
> On Wednesday, November 25, 2020 at 10:46:53 PM UTC+1, Dan Christensen wrote:
>
> > Again, assuming EXIST(a): U(a), I proved:
> > EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]]
> Which is correct:
> https://www.umsu.de/trees/#%E2%88%83xUx%20|=%20%E2%88%83y(Uy%20%E2%88%A7%20%E2%88%80x(Ux%20%E2%86%92%20(Fx%20%E2%86%92%20Gx))%20%E2%88%A7%20%E2%88%80x(Ux%20%E2%86%92%20Fx)%20%E2%86%92%20Gy)
>
> On the other hand, MC just asked for a proof of
>
> ∀x(Fx => Gx), ∀xFx |- Ga .
>
> You REALLY think that DC Proof SIMPLYFIES things?!
>

Standard FOL looks simpler only because so much is hidden from view making it harder to learn and understand.
In practice, DC Proof is simpler, more intuitive and more like the logic implicitly used in most math textbooks.

[Mostowski Collapse]

I wanted a FOL domain {0,1}, not a simulated universe {0,1}.

Can you really explain the reason why ∀xUx is not provable?

[Mostowski Collapse]

FOL is too edgy, because it is built around the KISS principle.

Keep It Simple Stupid. On the other hand DC Proof cannot
prove Zorns Lemma 100 years from now,

because Dan-O-Matik is still busy inserting U(_). And marveling
why ∀xU(x) is not provable.

[Dan Christensen]

On Wednesday, November 25, 2020 at 6:40:56 PM UTC-5, Mostowski Collapse wrote:
> Dan Christensen schrieb am Mittwoch, 25. November 2020 um 22:46:53 UTC+1:

> > > > Even if Alf is a variable and not a constant, this here
> > > > is not generally valid:
> > > >
> > > > ∃xUx, ∀x(Ux→(Fx→Gx)), ∀x(Ux→Fx) does not entail Ga.

> > Again, assuming EXIST(a): U(a), I proved:
> > EXIST(alf):[U(alf) & [ALL(a):[U(a) => [F(a) => G(a)]] & ALL(a):[U(a) => F(a)] => G(alf)]]
> >
> > Deal with it.
> >

> > > > There is a countermodel over a domain of size 2 consisting
> > > > of the elements {0,1}, where the variable gets assigned the value 0.
> > > >
> > > > Countermodel:
> > > > a: 0
> > > > G: { 1 }
> > > > U: { 1 }

> > Again, this should be U: {0, 1}. You wanted "a domain of size 2 consisting of the elements {0,1}"

> > > > F: { 1 }

With this correction, your "countermodel" violates the requirement that all of U are frogs. Here, we have both U(0) and ~F(0).

> > > >
> > > > You don't see the domain in FOL. There is no predicate D per se,
> > > > for the domain.

> > Could be one of the reasons that standard FOL is not a required subject in pure math programs.

> Can you really explain the reason why ∀xUx is not provable?

There is nothing to rule out the existence of y such that ~U(y). Again, you wanted "a domain of size 2 consisting of the elements {0,1}". In that case, there are infinitely many such y. Deal with it, Jan Burse.