Function Spaces of Empty Functions

[Dan Christensen]

The following proof demonstrates how functions, function equality, function spaces and empty functions can be handled in my DC Proof system.

Dan

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

THEOREM

1. On every set, there is exists a unique empty function.

ALL(x):[Set(x)

=> EXIST(f):[ALL(a):[a in null => f(a) in x]

& ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]


2. The function space (fs) of all functions mapping the empty set to any set x has only a single element.

ALL(x):[Set(x)

=> EXIST(fs):EXIST(f1):[Set(fs) & f1 in fs

& [ALL(f):[f in fs <=> ALL(a):[a in null => f(a) in x]] <--- Function space fs

& ALL(f2):[f2 in fs => f2=f1]]]]

Formal proof: https://dcproof.com/EmptyFunctionsUniqueV2.htm (137 lines)

[Mostowski Collapse]

Unfortunately the theorem is not correct.
You have two vacuous truths, so basically you say:

EXIST(f):ALL(g):[g = f]

You say all functions are the same.
Just replace the vacuous truth by *T* and simplify the theorem.

LMAO!

[Dan Christensen]

On Monday, March 28, 2022 at 5:33:33 PM UTC-4, Mostowski Collapse wrote:
> Unfortunately the theorem is not correct.
> You have two vacuous truths, so basically you say:
>
> EXIST(f):ALL(g):[g = f]
>

Maybe you didn't know, but the principle of vacuous truth is a legitimate and widely used method of proof in mathematics. Maybe you can find something about it at Wikipedia.

This is typically how you use it in DC Proof:

1. A
Premise

2. ~A => B
Arb Cons, 1

Where: Arb Cons = Arbitrary Consequent.

If you don' t like doing things the easy way, you could obtain the same result as follows:

1. A
Premise

2. ~A
Premise

3. ~B
Premise

4. A & ~A
Join, 1, 2

5. ~~B
Conclusion, 3

6. B
Rem DNeg, 5

7. ~A => B
Conclusion, 2

[Mostowski Collapse]

A proof A & ~A => B is pretty irrelevant here.
It seems you are not able to simplify formulas with
vacuous truths in it. So I will do it for you.

You proved:

ALL(x):[Set(x)
=> EXIST(f):[ALL(a):[a in null => f(a) in x]
& ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]

Now observe that ALL(a):[a in null => P] is
a vacuous truth. So we can replace it by TRUE.
Lets doit:

You proved:

ALL(x):[Set(x)
=> EXIST(f):[TRUE
& ALL(g):[TRUE => g=f]]]

Now everybody knows the identities [TRUE & P] === P and
that [TRUE => P] === P. So apply these identities and
lets see what we get:

You proved:

ALL(x):[Set(x)
=> EXIST(f):[ALL(g):[g=f]]]

Now since you have the Set(null) == TRUE, its one Axiom of
yours, we can instantiate your theorem by null, and we can
apply again an identity about TRUE and we get:

You proved:

EXIST(f):[ALL(g):[g=f]]]

So as I said, you proved that there is a function f that
equals any functions g. Which is utter rubbish.

LMAO!

Dan Christensen schrieb am Dienstag, 29. März 2022 um 03:43:11 UTC+2:
> ... Gibberish ...

[Dan Christensen]

On Wednesday, March 30, 2022 at 11:52:46 AM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> A proof A & ~A => B is pretty irrelevant here.

I proved that A => [~A => B] since you seemed unfamiliar with the notion.

> It seems you are not able to simplify formulas with
> vacuous truths in it. So I will do it for you.
>
> You proved:

> ALL(x):[Set(x)
> => EXIST(f):[ALL(a):[a in null => f(a) in x]
> & ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]

So, the empty function f: { } --> x is unique, as in the Wikipedia article.

> Now observe that ALL(a):[a in null => P] is
> a vacuous truth. So we can replace it by TRUE.

There is no such constant in DC Proof.

> Lets doit:
>
> You proved:
>
> ALL(x):[Set(x)
> => EXIST(f):[TRUE
> & ALL(g):[TRUE => g=f]]]
>

Gibberish.

> Now everybody knows the identities [TRUE & P] === P and
> that [TRUE => P] === P. So apply these identities and
> lets see what we get:
>
> You proved:
>
> ALL(x):[Set(x)
> => EXIST(f):[ALL(g):[g=f]]]
>
> Now since you have the Set(null) == TRUE, its one Axiom of
> yours, we can instantiate your theorem by null, and we can
> apply again an identity about TRUE and we get:
>
> You proved:
>
> EXIST(f):[ALL(g):[g=f]]]
>
> So as I said, you proved that there is a function f that
> equals any functions g. Which is utter rubbish.
>

Not sure what you are getting at, but if A is true, then ~A is false and the implication ~A => B will always be true for ANY logical proposition B, whether it is true or false. Get it? Didn't think so. Oh, well...

[Mostowski Collapse]

Then use P v ~P you moron.
But P & ~P will buy you nothing.

[Mostowski Collapse]

Or do you deny these propositional identities?

((P v ~P) & Q) <=> Q
((P v ~P) => Q) <=> Q

Whats wrong with you, lost your medis?

[Dan Christensen]

See what I mean, folks? Jan Burse hasn't got a clue.

Dan

[Mostowski Collapse]

The error is on your side, not on Wikipedias side. Wikipedia
uses nowhere a Vacuously True only condition. They have
also the condition f ⊆ X x Y.

Its YOUR PROBLEM Dan-O-Matik. Scape goating Wikipedia
doesn't work. Its YOUR BLUNDER.

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> On Monday, March 28, 2022 at 5:33:33 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
>
>> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
>> > Visit my Math Blog at http://www.dcproof.wordpress.com
>> > ********************************************************************
>> >
>> > THEOREM
>> >
>> > 1. On every set, there is exists a unique empty function.
>> >
>> > ALL(x):[Set(x)
>> >
>> > => EXIST(f):[ALL(a):[a in null => f(a) in x]
>> >
>> > & ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]
>> >
>> >
>> > 2. The function space (fs) of all functions mapping the empty set to any set x has only a single element.
>> >
>> > ALL(x):[Set(x)
>> >
>> > => EXIST(fs):EXIST(f1):[Set(fs) & f1 in fs
>> >
>> > & [ALL(f):[f in fs <=> ALL(a):[a in null => f(a) in x]] <--- Function space fs
>> >
>> > & ALL(f2):[f2 in fs => f2=f1]]]]
>> >
>> > Formal proof: https://dcproof.com/EmptyFunctionsUniqueV2.htm (137 lines)
>

>> Unfortunately the theorem is not correct.
>> You have two vacuous truths, so basically you say:
>>
>> EXIST(f):ALL(g):[g = f]
>

> Your inexperience with formal logic is showing, Jan Burse. Perhaps you
> didn't know, but the principle of vacuous proof is a legitimate method
> of proof.

I am wary of wading into what it obviously a long-standing animosity,
but I am struck by the fact that you don't seem to see what it is that
MC is saying. I had the same thought as he, but decided not to comment
as you had already told me that there is no document explaining your
notation and, in general, I prefer to comment only what I know what I'm
commenting on!

However, in most deductions one can replace <vacuous truth> & X with X
and <vacuous truth> => Y with Y. The vacuous truth part adds nothing.
In

ALL(x):[Set(x) =>
EXIST(f):[
ALL(a):[a in null => f(a) in x] &
ALL(g):[
ALL(a):[a e null => g(a) e x] =>
g=f
]
]
]

both ALL(a):[a in null => f(a) in x] and ALL(a):[a e null => g(a) e x]
appear to be vacuous truths, suggesting that both the conjunction and
the fourth implication could be simplified:

ALL(x):[Set(x) =>
EXIST(f):[
ALL(g):[
g=f
]
]
]

Presumably, in your notation, this sort of simplification is not
permitted, or the two ALL(a) forms are not, in fact, vacuously true, but
you do yourself a disservice by not addressing the point.

--
Ben.

[Mostowski Collapse]

The remaining ALL(x) form need not be vacuously true.
But you can easily specialize it via x=null to get:

EXIST(f):[
ALL(g):[
g=f
]
]

When you have x=null, then Set(x) turns into Set(null),
which is TRUE by this Axiom by Dan:

Define: null (The empty set)
2 Set(null)
Axiom
https://dcproof.com/EmptyFunctionsUniqueV2.htm

And then you have absorbtion again, i.e. TRUE => Q
can be simplified to Q.

[Dan Christensen]

Again, the principle of vacuous is a legitimate method of proof in mathematics.

> In
> ALL(x):[Set(x) =>
> EXIST(f):[
> ALL(a):[a in null => f(a) in x] &
> ALL(g):[
> ALL(a):[a e null => g(a) e x] =>
> g=f
> ]
> ]
> ]

In words, for every set X, there exists a unique function f: { } --> X. Do you agree with this interpretation? If not, how would you formally state this sentence?

> both ALL(a):[a in null => f(a) in x] and ALL(a):[a e null => g(a) e x]
> appear to be vacuous truths,

Agreed.

> suggesting that both the conjunction and
> the fourth implication could be simplified:
> ALL(x):[Set(x) =>
> EXIST(f):[
> ALL(g):[
> g=f
> ]
> ]
> ]

Can you formalize this argument using some form of natural deduction?

Dan

[Mostowski Collapse]

Dan-O-Matik was wondering:

> Can you formalize this argument using some form of natural deduction?

Also you don't need much logic to see that you proved
nonsense. Its only trivial high school logic:

1) Vacuously True <=> TRUE
∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.
https://www.umsu.de/trees/#~6a%28P%28a%29~1~3P%28a%29~5Q%29~4R~2~3R

2) TRUE is Absorbed by Conjunction:
((R∨¬R) ∧ Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~1Q%29~4Q

3) Left Hand Side TRUE is Absorbed by Implication
((R∨¬R) → Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~5Q%29~4Q

Of course you can prove these propositional identities
with natural deduction, Hilbert style calculus, sequent
calculus, semeantic tableaux, etc.., what-ever.

[Dan Christensen]

I think you want to prove:

ALL(null):[Set(null) & ALL(a):~a in null

=> ALL(x):[Set(x) => EXIST(f):[ALL(a):[a in null => f(a) in x]
& ALL(g):[ALL(a):[a in null => g(a) in x] => g=f] ] ]

=> ALL(x):[Set(x) => EXIST(f):ALL(g):g=f] ]

So far, I haven't been able to do so in DC Proof.

[Mostowski Collapse]

The tree tool can do so:

1) Vacuously True <=> TRUE
∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.
https://www.umsu.de/trees/#~6a%28P%28a%29~1~3P%28a%29~5Q%29~4R~2~3R

2) TRUE is Absorbed by Conjunction:
((R∨¬R) ∧ Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~1Q%29~4Q

3) Left Hand Side TRUE is Absorbed by Implication
((R∨¬R) → Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~5Q%29~4Q

Which of 1), 2) or 3) doesn't work in DC Proof?

[Dan Christensen]

On Thursday, March 31, 2022 at 10:04:35 AM UTC-4, Mostowski Collapse wrote:
> The tree tool can do so:
> 1) Vacuously True <=> TRUE
> ∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.

How is this relevant? Here is what I think you want to prove

ALL(null):[Set(null) & ALL(a):~a in null

=> ALL(x):[Set(x)

=> [EXIST(f):[ALL(a):[a in null => f(a) in x] & ALL(g):[ALL(a):[a in null => g(a) in x] => g=f]]

=> EXIST(f):ALL(g):g=f]]]

Using DC Proof, you might start as follows:

Suppose...

1. Set(null) & ALL(a):~a in null
Premise

2. Set(null)
Split, 1

3 ALL(a):~a in null
Split, 1


Suppose...

4. Set(x)
Premise


Suppose...

5. EXIST(f):[ALL(a):[a in null => f(a) in x]

& ALL(g):[ALL(a):[a in null => g(a) in x] => g=f]]

Premise

6. ALL(a):[a in null => f(a) in x]

& ALL(g):[ALL(a):[a in null => g(a) in x] => g=f]

E Spec, 5

7. ALL(a):[a in null => f(a) in x]
Split, 6

8. ALL(g):[ALL(a):[a in null => g(a) in x] => g=f]
Split, 6

Now, prove EXIST(f):ALL(g):g=f

I hope this helps.

[Mostowski Collapse]

1) can be used to replace ALL(a):[a in null => f(a) in x] and
ALL(a):[a in null => g(a) in x] in your theorem:

> ALL(x):[Set(x) =>
> EXIST(f):[
> ALL(a):[a in null => f(a) in x] &
> ALL(g):[

> ALL(a):[a e null => g(a) e x] =>
> g=f
> ]
> ]
> ]

After that you can use 2) and 3). But Ben Bacarisse
explained this already.

[Dan Christensen]

On Thursday, March 31, 2022 at 10:34:44 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:


> Dan Christensen schrieb am Donnerstag, 31. März 2022 um 16:29:12 UTC+2:
> > On Thursday, March 31, 2022 at 10:04:35 AM UTC-4, Mostowski Collapse wrote:
> > > The tree tool can do so:
> > > 1) Vacuously True <=> TRUE
> > > ∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.
> > How is this relevant? Here is what I think you want to prove

> 1) can be used to replace ALL(a):[a in null => f(a) in x] and
> ALL(a):[a in null => g(a) in x] in your theorem:
> > ALL(x):[Set(x) =>
> > EXIST(f):[
> > ALL(a):[a in null => f(a) in x] &
> > ALL(g):[
> > ALL(a):[a e null => g(a) e x] =>
> > g=f
> > ]
> > ]
> > ]

> After that you can use 2) and 3). But Ben Bacarisse
> explained this already.

Jan Burse much prefers handwaving to proving. What he snipped and failed to address:

<QUOTE>

How is this relevant? Here is what I think you want to prove

ALL(null):[Set(null) & ALL(a):~a in null

=> ALL(x):[Set(x)

=> [EXIST(f):[ALL(a):[a in null => f(a) in x] & ALL(g):[ALL(a):[a in null => g(a) in x] => g=f]]

=> EXIST(f):ALL(g):g=f]]]

<UNQUOTE>


Not so easy, is it, Jan Burse? (HA, HA, HA!!!)

Jan Burse has been trying for years to find inconsistencies in DC Proof. Here, he has failed yet again.

[Ben Bacarisse]

You don't have a definition of your notation, so I can't comment on what
is might mean. I am just asking you to clarify just a couple of points
about it.

In set theory, a function from X to Y is just a particular kind of
subset of X x Y. There is only one subset of {} x Y and that's {}.

>> both ALL(a):[a in null => f(a) in x] and ALL(a):[a e null => g(a) e x]
>> appear to be vacuous truths,
>
> Agreed.

Well that's one. Thanks.

>> suggesting that both the conjunction and
>> the fourth implication could be simplified:
>> ALL(x):[Set(x) =>
>> EXIST(f):[
>> ALL(g):[
>> g=f
>> ]
>> ]
>> ]
>
> Can you formalize this argument using some form of natural deduction?

My question is what is it about your notation and/or system that
prevents TRUE & P being replaced by P and TRUE => Q being replaced by Q.

I have an incing as to why, but I don't want hazard a guess when
there's no formal definition of what these symbols mean.
--
Ben.

[Ben Bacarisse]

No, I don't want to prove that. See my reply to the parent article in
case what I am asking is still not clear.

--
Ben.

[Dan Christensen]

The closest I can come to this is, using my version of natural deduction, I can derive:

1. Q
Premise

2. Q & P
Premise

3. P
Split, 2

4. Q & P => P
Conclusion, 2

5. Q => [Q & P => P]
Conclusion, 1

> and TRUE => Q being replaced by Q.
>

1. P
Premise

2. P => Q
Premise

3. Q
Detach, 2, 1

4. P => Q => Q
Conclusion, 2

5. P => [P => Q => Q]
Conclusion, 1

where '=>' is left associative.

I can make some direct replacements within a statement, e.g.

~~A ---> A
A=>B ---> ~[A & ~B]

This is nothing new or radical. It is just my formalization of the basic logic that is widely used in mathematics.

Dan

[Ben Bacarisse]

This does not answer the question. I wondered what it was about the
proof system that allows some apparently valid substitutions and not
others.

> I can make some direct replacements within a statement, e.g.
>
> ~~A ---> A
> A=>B ---> ~[A & ~B]
>
> This is nothing new or radical.

Indeed. But that leaves the puzzle unsolved. It appears that replacing
<vacuous truth> & P with P leads to strange conclusions. Why? What's
going on here?

> It is just my formalization of the basic logic that is widely used in
> mathematics.

But in many systems, if X <=> Y one can replace X by Y (or vice versa)
and still get valid deductions. That appears not to be the case with DC
Proof.

--
Ben.

[Dan Christensen]

Assuming the existence of sets null and x (in undischarged assumptions), I was able to derive ALL(g):[ALL(a):[a in null => g(a) in x] => g=f]. You claim that, from this, we should somehow be able eliminate the antecedent to obtain ALL(g):[g=f]. Is that correct?

Dan

[Mostowski Collapse]

STUDENTS BEWARE: Dan Christensen is the troll who doesn't
know what George Boole (1815 - 1864) already figured out:

1 * X = X

TRUE & P <=> P

That the Boolean TRUE behaves like the real unit 1.

Addendum:
One might also figure out that there is not only a multiplicative
unit 1, but also an additive unit 0:

FALSE | P <=> P

Or slightly recast, one can use (A => B) <=> (~A | B):

(TRUE => P) <=> P

[Mostowski Collapse]

I think DC Proof has even a menu item to interchange (A => B) <=> (~A | B),
still Dan Christensen does not figure out how to simplify

ALL(g):[ALL(a):[a in null => g(a) in x] => g=f]

further into, given that ALL(a):[a in null => g(a) in x] is TRUE?

ALL(g):[g=f]

Seriously? Should we phone the Guiness Book of records for slowest brain?

[Ben Bacarisse]

That's not enough for what I'm talking about, null must be what I call
{} -- a set with no elements.

> (in undischarged
> assumptions), I was able to derive ALL(g):[ALL(a):[a in null => g(a)
> in x] => g=f]. You claim that, from this, we should somehow be able
> eliminate the antecedent to obtain ALL(g):[g=f]. Is that correct?

No. I am asking why you can't.

I'm not sure this is going anywhere. I don't know enough about natural
deduction to answer the question myself and I don't think you can see
anything puzzling.

I think the answer may be something simple like the fact that g is bound
and not free in the vacuously true antecedent.

--
Ben.

[Dan Christensen]

It is a puzzlement alright. From Wikipedia:

"For every set X, there is a UNIQUE FUNCTION, called the empty function, or empty map, from the empty set to X."
https://en.wikipedia.org/wiki/Function_(mathematics)#Standard_functions

For what it's worth, my formal proof confirms that this is true. You methods of proof, such as they are, seem unable to. Have I missed something? Have YOU missed something?

Dan

[Dan Christensen]

Have a look at my new version of the uniqueness proof. It might be a little more readable. There, I prove:

ALL(x):[Set(x)
=> EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence
& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness

https://www.dcproof.com/EmptyFunctionsUniqueV3.htm

I hope this helps.

Dan

[Dan Christensen]

On Friday, April 1, 2022 at 4:13:20 PM UTC-4, Ben Bacarisse wrote:

>
> I think the answer may be something simple like the fact that g is bound
> and not free in the vacuously true antecedent.
>

Yes, it may be a little more obvious in the latest version of my proof where I prove:

ALL(x):[Set(x)

=> EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence

& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness

You cannot say, for example, that ALL(a):[a in null => f1(a) in x] is a theorem since f1 is a bound variable quantified outside of that expression. Also note that, in DC Proof you cannot introduce free variables using vacuous truth. You can only introduce free variables/constants by axiom, premise or existential specification (instantiation).

Dan

[Mostowski Collapse]

LoL, more nonsense. Now you have proved:

EXIST(f):ALL(f1):ALL(f2):[f1=f2]

You don't get it what vacuous truth means, don't you?
Because you can prove such nonsense as above, i.e.

all functions are equal, I guess some of your DC poop
axioms or axiom schemas, that you use in the course

of your proof are buggy, or some logic inferences.

[Dan Christensen]

On Saturday, April 2, 2022 at 5:04:18 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> LoL, more nonsense. Now you have proved:
>
> EXIST(f):ALL(f1):ALL(f2):[f1=f2]
>

Wrong again, Jan Burse. We are STILL waiting for your formal proof of this theorem. Sorry, your handwaving hysterics won't cut it here. Save them for your fellow trolls here. They will believe absolutely anything, the more bizarre, the better.

Dan

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> On Friday, April 1, 2022 at 4:13:20 PM UTC-4, Ben Bacarisse wrote:
>
>>
>> I think the answer may be something simple like the fact that g is bound
>> and not free in the vacuously true antecedent.
>>
>
> Yes, it may be a little more obvious in the latest version of my proof
> where I prove:
>
> ALL(x):[Set(x)
>
> => EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence
>
> & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness
>
> You cannot say, for example, that ALL(a):[a in null => f1(a) in x] is
> a theorem since f1 is a bound variable quantified outside of that
> expression.

Let's look at the EXIST(f):ALL(a):[a in null => f(a) in x] part as it's
simpler. You say that ALL(a):[a in null => f(a) in x] is not a theorem
because f is bound, but ALL(a):[a in null => f(a) in x] has no
counter-model. The EXISTS(f) could be satisfied by {(1,2), (2,3)} (my
notation for a function -- I don't know yours). The part you label with
"<--- Existence" does not seem to live up to the label.

> Also note that, in DC Proof you cannot introduce free variables using
> vacuous truth. You can only introduce free variables/constants by
> axiom, premise or existential specification (instantiation).

I'd love it if this were all written down somewhere. I could probably
answer these questions myself if I knew the rules.

--
Ben.

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> It is a puzzlement alright. From Wikipedia:
>
> "For every set X, there is a UNIQUE FUNCTION, called the empty
> function, or empty map, from the empty set to X."
> https://en.wikipedia.org/wiki/Function_(mathematics)#Standard_functions

What's puzzling about that?

> For what it's worth, my formal proof confirms that this is true.

I don't know how your proof system works so I can't be sure. How do you
know that invalid deductions can't be made? (I'm not saying that they
can be, but without a formal definition of the system, can you be sure?)

> You methods of proof, such as they are, seem unable to. Have I missed
> something? Have YOU missed something?

I don't have a method of proof. I rely on standard methods, but they are
all informal. I think I outlined why {}->X = {{}} for any X, but then
functions are sets as far as I am concerned.

BTW, this is not a competition. I wanted to understand something about
DC Proof that looked puzzling.

--
Ben.

[Mostowski Collapse]

You, Dan-O-Matik, are getting extremly annoying with your incompetence
in logic. Whats wrong in my claim? Could you tell us?

This here:

ALL(x):[Set(x)
=> EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence
& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness

Implies this here:
EXIST(f):ALL(f1):ALL(f2):[f1=f2]

Thats pretty obvious, you only have to use:

1) Vacuously True <=> TRUE
∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.

https://www.umsu.de/trees/#~6a%28P%28a%29~1~3P%28a%29~5Q%29~4R~2~3R

2) TRUE is Absorbed by Conjunction:
((R∨¬R) ∧ Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~1Q%29~4Q

3) Left Hand Side TRUE is Absorbed by Implication
((R∨¬R) → Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~5Q%29~4Q

And this classic helps also:

4) Residuated Lattice
(P → (Q→R)) ↔ ((P∧Q) → R) is valid.
https://www.umsu.de/trees/#%28P~5%28Q~5R%29%29~4%28P~1Q~5R%29

[Mostowski Collapse]

Maybe use this naming for what Dan-O-Matik hasnt
internalized yet about logic. He is such a baby:

1) Vacuously True <=> TRUE
∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.
https://www.umsu.de/trees/#~6a%28P%28a%29~1~3P%28a%29~5Q%29~4R~2~3R

2) TRUE is Multiplicative Identity:

((R∨¬R) ∧ Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~1Q%29~4Q

3) FALSE is Additive Identity & Material Implication

((R∨¬R) → Q) ↔ Q is valid.
https://www.umsu.de/trees/#%28%28R~2~3R%29~5Q%29~4Q

4) Additive Associativity & Material Implication & De Morgan's laws

(P → (Q→R)) ↔ ((P∧Q) → R) is valid.

Material implication: (A => B) <=> (~A | B)
https://en.wikipedia.org/wiki/Material_implication_%28rule_of_inference%29

De Morgan's laws: ~(A & B) <=> (~A | ~B)
https://en.wikipedia.org/wiki/De_Morgan's_laws

https://www.umsu.de/trees/#%28P~5%28Q~5R%29%29~4%28P~1Q~5R%29

[Mostowski Collapse]

Actually you don't really need 4), 2) and then 3) is also
enough to get rid of the double vacuouse truth

ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x]

But somehow I liked to think about it via 4).
Anyway. Please cleanup your bullshit.

What axiom or axiom schema of DC Proof or your
proof, that helps producing such nonsense, is wrong?

[Dan Christensen]

On Saturday, April 2, 2022 at 6:57:23 PM UTC-4, Mostowski Collapse wrote:
> You, Dan-O-Matik, are getting extremly annoying with your incompetence
> in logic. Whats wrong in my claim? Could you tell us?
>
> This here:
> ALL(x):[Set(x)
> => EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence
> & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness
> Implies this here:
> EXIST(f):ALL(f1):ALL(f2):[f1=f2]
>
> Thats pretty obvious, you only have to use:
> 1) Vacuously True <=> TRUE
> ∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.

Still waiting for your formal proof that:

ALL(x):[Set(x)

=> EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence

& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]]

=> EXIST(f):ALL(f1):ALL(f2):[f1=f2]

How about, Jan Burse? Not today? Some day soon then? NO??? Oh, well...

[Archimedes Plutonium]

Re: Proof of Kepler Packing//Jan Burse-Alzheimer faggot//ETH Zurich, Dietmar Salamon, Martin Schweizer, Mete Soner, looking at it
by Dan Christensen Jul 9, 2017, 11:34:05 PM

Homosexual says Zelos Malum, Markus Hennrich, Carl XVI Gustaf, Tommy Ohlsson, Paul Crutzen, stalker-- Zelos Malum, Can't do proper Calculus, thinks electron is .5MeV when it is Dirac's monopole , Real Proton = 840MeV

On Wednesday, December 1, 2021 at 5:25:22 AM UTC-6, zelos...@gmail.com wrote:
> I call him out cause it is hilarious

Zelos, did you point out to John Stillwell a single cone has 1 axis of symmetry not 2 and so the slant cut is a Oval, never the Ellipse, and he still got it wrong?
On Wednesday, March 16, 2022 at 7:24:59 AM UTC-5, zelos...@gmail.com wrote:
> all still fucking wrong

On Friday, March 9, 2018 at 6:27:45 AM UTC-6, zelos...@gmail.com wrote:
> why would one need to do it geometrically?

Zelos Malum, did you point out to John Stillwell that calculus is geometry, and a geometric proof of Fundamental Theorem of Calculus is demanded, yet he still is too dumb to do one.

On Monday, March 7, 2022 at 11:19:30 PM UTC-6, zelos...@gmail.com wrote:
> We know you're homosexual, why do you need to tell us?

Unplugging Dan Christensen and entire Univ Western Ontario uwo from sci.math as a demented racist defaming poster

John Woods, Mario Bunge, Ted Honderich, Brendan Myers, Joachim Lambek, Carrie Jenkins, Katalin Bimbo, Doug Walton.

Re: 1.1Dr. John Baez is a failed mathematician-physicist with his proton of 938MeV when it is 840MeV, electron= muon //his ellipse is a conic when it never was// as phony in math and physics as kibo Parry Moroney's ellipse and Christensen 10 OR 4 =
by Dan Christensen Sep 22, 2019, 9:54:06 AM



Re: A newsgroup like sci.math is a pile of shit when you have paid stalkers like Kibo Parry M. or Dan Christensen lording over sci.math as if he owns the place-- stalking and attacking posters 7-24-365. This is why I now post a roadmap to AP's newsgr
by Alan Mackenzie Jun 29, 2021, 2:36:04 PM


Univ Western Ontario math dept
Janusz Adamus, Tatyana  Barron,   Dan Christensen, Graham Denham, Ajneet Dhillon, Matthias  Franz, John Jardine, Massoud Khalkhali, Nicole Lemire, Jan Mináč, Victoria Olds, Martin Pinsonnault, Lex Renner, David Riley, Rasul Shafikov, Gordon Sinnamon

Chancellor Linda Hasenfratz
President Alan Shepard
Amit Chakma (chem engr)

Univ. Western Ontario physics dept
Pauline Barmby, Shantanu Basu, Peter Brown, Alex Buchel, Jan Cami, Margret Campbell-Brown, Blaine Chronik, Robert Cockcroft, John R. de Bruyn, Colin Denniston, Giovanni Fanchini, Sarah Gallagher, Lyudmila Goncharova, Wayne Hocking, Martin Houde, Jeffrey L. Hutter, Carol Jones, Stan Metchev, Silvia Mittler, Els Peeters, Robert Sica, Aaron Sigut, Peter Simpson, Mahi Singh, Paul Wiegert, Eugene Wong, Martin Zinke-Allmang



Re: 1.2Analbuttfuckmanure Justin Trudeau,Sophie Gregoire, says Dan Christensen or Kibo//Stephen Lecce, Jan Mináč, Victoria Olds, Martin Pinsonnault, Lex Renner, David Riley, Rasul Shafikov, Gordon Sinnamon
by Hoofington P. McSnort Aug 26, 2020, 7:01:28 PM

Re: Bill Blair, David Vigneault please help us put Dan Christensen into a Canadian Asylum or psychiatric treatment where he belongs
By Donald Trump Mar 30, 2020, 11:30:25 PM


Re: 2- Dan Christensen on failed math MIT Gilbert Strang, with his scatterbrained Calculus books, no geometry proof of Fundamental Theorem of Calculus, because Gilbert never knew
by Chris M. Thomasson 6:09 PM On 6/25/2021


Re: Dan Christensen says close all math, physics, chemistry dept. in ALL Canadian Colleges with their fake electron (muon is real electron), fake geometry proof of calculus (Old Math sums up 0 width rectangles), fake Lewis 8 Structure (dissociation...
by Giant Radioactive Easter Bunnie Jan 21, 2021, 5:38:37 PM

Re: Stewart failed Calculus also, and his book should be removed
by Dan Christensen
Jun 24, 2018, 10:52:49 PM

Re: Markus Klyver greatest math fool of Sweden-- thinks an ellipse is a conic section
by
Dan Christensen Aug 2, 2017, 11:52:21 PM


On Monday, October 21, 2019 at 1:29:49 PM UTC-5, Dan Christensen wrote:
>
> Are you ready, kids??? Bend over, er...
>
> Dan


Re: 81,045-Student victims of Rose M. Patten Univ Toronto from stalker Dan Christensen teaching 10 OR 2 = 12 with AND as subtraction, never a geometry proof of Fundamental Theorem of Calculus Univ Toronto, physics, Gordon F. West, Michael B. Walker
by Frank Cassa 12Apr2021 7:00 AM 



Re: 7,744-Student victims of Linda Hasenfratz Univ Western Ontario from stalker Dan Christensen teaching 10 OR 2 = 12 with AND as subtraction, never a geometry proof of Fundamental Theorem of Calculus Chancellor Linda Hasenfratz President Alan Shepard
11:53 AM 10Apr2021
by Wayne Decarlo

Re: 102,852-Student victims of Dominic Barton, Univ Waterloo from stalker Dan Christensen teaching 10 OR 2 = 12 with AND as subtraction, never a geometry proof of Fundamental Theorem of Calculus Dominic Barton, President Feridun Hamdullahpur physics
by konyberg Apr 15, 2021, 3:09:41 PM 

Re: 176,232-Student Victims of Michael Meighen McGill Univ by Dan Christensen teaching 10 OR 2 = 12 with AND as subtraction, never a geometry proof of Fundamental Theorem of Calculus... 0.5MeV electron when in truth it is the muon as the real electron
by Dan Christensen Jul 2, 2021, 9:47:42 AM


Re: 135,568 Student victims Queen's Univ. James Leech, Arthur B. McDonald by Dan Christensen teaching 10 OR 2 = 12 with AND as subtraction, never a geometry proof of Fundamental Theorem of Calculus-- his mindless electron =0.5MeV when real electron of
May 10, 2021
by Professor Wordsmith

Re: 135,566 Student victims Queen's Univ. James Leech, Arthur B. McDonald by Dan Christensen teaching 10 OR 2 = 12 with AND as subtraction, never a geometry proof of Fundamental Theorem of Calculus-- his mindless electron =0.5MeV when real electron o
May 10, 2021
by Michael Moroney



Re: Proof of Kepler Packing//Jan Burse-Alzheimer faggot//ETH Zurich, Dietmar Salamon, Martin Schweizer, Mete Soner, looking at it
by Dan Christensen Jul 9, 2017, 11:34:05 PM


Re: *Fire the entire Univ Western Ontario math dept/ still teaching that the contradictory sine graph as sinusoid when it is really semicircle
by Dan Christensen Nov 21, 2017,



Re: Shit for brains in Logic Morons of logic George Boole, William Jevons, Bertrand Russell, Kurt Godel, Rudolf Carnap, Jan Burse& Dan Christensen as moronette cadets of Boole, Ludwig Wittgenstein, Willard Quine, Alfred North Whitehead, Irving Copi
by zelos...@gmail.com Mar 25, 2021, 12:55:15 AM 

Re: Spamming fuckdog Dan Christensen says fire Stanford's John Lipa, Alexander Fetter, William Little, Douglas Osheroff, David Ritson, H. Alan Schwettman, John Turneaure, Robert Wagoner, Stanley Wojcicki, Mason Yearian rather than let them brainwash our
by Mutt Buncher



Re: 2-fuckdog boston's Kibo Parry Moroney subhuman *stalkers* Dan Christensen, Betsy DeVos, NSF Dr. Panchanathan, barry shein's world std paying how much to stalk AP??
Earl Biggs


Re: Subhuman Kibo Parry Moroney says freedom of speech means freedom to stalk, liar, cheat, steal, kill// Dan Christensen, Uncle Al, NSF Dr. Panchanathan, Dept Educ Betsy DeVos, John Baez, Port563 Gilbert Strang, Barry Shein
Earl Biggs



                              ..
            .- " `-.   ,..-'''  ```....'`-..
           ,      . `.'            '        `.
         .'   .' `    `           '   `..     ;
         .   ;  .'                     . `.    ;
         ;   . '                       `.  .   '
          . '                            ` `.  |
        . '.                                  '
       .          0              0            ' `.
      '                                          `
     ;                                            `
    .'                                             `
    ;                      U                        `
    ;    ';                                         `
    :   | ;..                                 :`     `
    :    `;. ```.                           .-; |    '
    '.      `    ``..,                   .'   :'    '
     ;       `        ;'..          ..-''    '     '  I am Christensen,I am such a stupid insane imp of math and logic that I thought a vertex has a derivative, that distinct means not-distinct, and that 2 OR 1 = 3 with AND as subtraction. And I love spam reading of vvgra and tomato hello, and I am a failure of academics and so I spend most days making out hate-lists of people who actually succeed in science for my pea sized brain is envious and jealous of those who succeed in science yet I failed in science.
      `       `        ;  ````'''""'  ;      '    '
       `       `        ;            ;      '    '
        `       `        ;          ;      '    '
         `       `.       ````''''''      '    '
           `       .                     '    '
         /  `       `.                  '    '        .
        /     `       ..            ..'    .'"""""...'
       /   .`   `       ``........-'     .'` .....'''
      / .'' ;     `                    .'   `
  ...'.'    ;    .' `                .'      `
   ""      .'  .' |    `           .; \       `
           ; .'   |      `. . . . ' .  \       `
           :'     |     '   `       ,   `.     `
                  |    '     `      '     `.    `
                  `   '       `     ;       `.  |
                  `.'          `    ;         `-'
                                `...'

Here is an example of where Dan Christensen seems to act out his classroom fantasies, and whether he is a threat to students along with being a bully in sci.math.

On Monday, October 21, 2019 at 1:29:49 PM UTC-5, Dan Christensen wrote:
>
> Are you ready, kids??? Bend over, er...

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

Here is an example of Dan Christensen fumbling with the most simple of logic reasoning, and yet Canada keeps allowing this misfit to dig deeper into logic.

The stupid Dan Christensen always chokes up when it comes to logic or even just plain commonsense with his 2 OR 1 = 3 and his AND as subtraction.

On Wednesday, January 25, 2017 at 10:08:09 AM UTC-6, Peter Percival wrote:
> Dan Christensen wrote:

> > On Wednesday, January 25, 2017 at 9:47:32 AM UTC-5, Archimedes Plutonium wrote:
> >> On Wednesday, January 25, 2017 at 8:27:19 AM UTC-6, Dan Christensen wrote:
> >>> On Wednesday, January 25, 2017 at 9:16:52 AM UTC-5, Archimedes Plutonium wrote:
> >>>> PAGE58, 8-3, True Geometry / correcting axioms, 1by1 tool, angles of logarithmic spiral, conic sections unified regular polyhedra, Leaf-Triangle, Unit Basis Vector
> >>>>
> >>>> The axioms that are in need of fixing is the axiom that between any two points lies a third new point.
> >>>
> >>> The should be "between and any two DISTINCT points."
> >>>
> >>
> >> What a monsterous fool you are
> >>
> >
> > OMG. You are serious. Stupid and proud of it.
>
> And yet Mr Plutonium is right. Two points are distinct (else they would
> be one) and it is not necessary to say so.
>


Apparently Dan Christensen never took calculus or flunked it with this statement.
On Tuesday, June 2, 2015 at 8:57:54 AM UTC-5, Dan Christensen wrote:
> On Tuesday, June 2, 2015 at 2:32:51 AM UTC-4, Archimedes Plutonium wrote:
> > The nonexistence of a curved angle because there is no way to measure the angle if either one of the rays is not a straightline segment at the vertex,
>
> From the derivative of each curve at the point of contact you have the slopes of their respective tangents there. (Assuming derivatives are defined there.) From these slopes, you should be able to calculate angle formed.
>
>
> Dan

[Dan Christensen]

STUDENTS BEWARE: Don't be a victim of AP's fake math and science

On Saturday, April 2, 2022 at 11:36:32 PM UTC-4, Archimedes Plutonium (AP) wrote:
> Re: Proof of Kepler ...

AP is a malicious internet troll who wants only to mislead and confuse you. He may not be all there, but his fake math and science can only be meant to promote failure in schools. One can only guess at his motives.

In AP's OWN WORDS here:

“Primes do not exist, because the set they were borne from has no division.”
--June 29, 2020

“The last and largest finite number is 10^604.”
--June 3, 2015

“0 appears to be the last and largest finite number”
--June 9, 2015

“0/0 must be equal to 1.”
-- June 9, 2015

“0 is an infinite irrational number.”
--June 28, 2015

“No negative numbers exist.”
--December 22, 2018

“Rationals are not numbers.”
--May 18, 2019

According to AP's “chess board math,” an equilateral triangle is a right-triangle.
--December 11, 2019

Which could explain...

“The value of sin(45 degrees) = 1.”
--May 31, 2019

AP deliberately and repeatedly presented the truth table for OR as the truth table for AND:

“New Logic
AND
T & T = T
T & F = T
F & T = T
F & F = F”
--November 9, 2019

AP seeks aid of Russian agents to promote failure in schools:

"Please--Asking for help from Russia-- russian robots-- to create a new, true mathematics [sic]. What I like for the robots to do, is list every day, about 4 Colleges ( of the West) math dept, and ask why that math department is teaching false and fake math, and if unable to change to the correct true math, well, simply fire that math department until they can find professors who recognize truth in math from fakery...."
--November 9, 2017


And if that wasn't weird enough...

“The totality, everything that there is [the universe], is only 1 atom of plutonium [Pu]. There is nothing outside or beyond this one atom of plutonium.”
--April 4, 1994

“The Universe itself is one gigantic big atom.”
--November 14, 2019

AP's sinister Atom God Cult of Failure???

“Since God-Pu is marching on.
Glory! Glory! Atom Plutonium!
Its truth is marching on.
It has sounded forth the trumpet that shall never call retreat;
It is sifting out the hearts of people before its judgment seat;
Oh, be swift, my soul, to answer it; be jubilant, my feet!
Our God-Pu is marching on.”
--December 15, 2018 (Note: Pu is the atomic symbol for plutonium)

[Archimedes Plutonium]

Re: 135,566 Student victims Queen's Univ. James Leech, Arthur B. McDonald by Dan Christensen teaching 10 OR 2 = 12 with AND as subtraction, never a geometry proof of Fundamental Theorem of Calculus-- his mindless electron =0.5MeV when real electron o
May 10, 2021
by Michael Moroney

Can Dr. McDonald even do proper percentages? For Kibo Parry says 938 is 12% short of 945.

Re: Proof of Kepler Packing//Jan Burse-Alzheimer faggot//ETH Zurich, Dietmar Salamon, Martin Schweizer, Mete Soner, looking at it
by Dan Christensen Jul 9, 2017, 11:34:05 PM

Re: Andrew Wiles flunked the Math Test of a lifetime-generation test
2150 views
by
zelos...@gmail.com
Mar 9, 2018, 6:27:45 AM

Re: Shit for brains in Logic Morons of logic George Boole, William Jevons, Bertrand Russell, Kurt Godel, Rudolf Carnap, Jan Burse& Dan Christensen as moronette cadets of Boole, Ludwig Wittgenstein, Willard Quine, Alfred North Whitehead, Irving Copi

140 views

by
zelos...@gmail.com
Mar 25, 2021, 12:55:15 AM

On Wednesday, December 1, 2021 at 5:25:22 AM UTC-6, zelos...@gmail.com wrote:
> I call him out cause it is hilarious

Zelos, did you point out to John Stillwell a single cone has 1 axis of symmetry not 2 and so the slant cut is a Oval, never the Ellipse, and he still got it wrong?
On Wednesday, March 16, 2022 at 7:24:59 AM UTC-5, zelos...@gmail.com wrote:
> all still fucking wrong

On Friday, March 9, 2018 at 6:27:45 AM UTC-6, zelos...@gmail.com wrote:
> why would one need to do it geometrically?

Zelos Malum, did you point out to John Stillwell that calculus is geometry, and a geometric proof of Fundamental Theorem of Calculus is demanded, yet he still is too dumb to do one.

On Monday, March 7, 2022 at 11:19:30 PM UTC-6, zelos...@gmail.com wrote:
> We know you're homosexual, why do you need to tell us?

Unplugging Dan Christensen and entire Univ Western Ontario uwo from sci.math as a demented racist defaming poster

by Earl Biggs

Re: Subhuman Kibo Parry Moroney says freedom of speech means freedom to stalk, liar, cheat, steal, kill// Dan Christensen, Uncle Al, NSF Dr. Panchanathan, Dept Educ Betsy DeVos, John Baez, Port563 Gilbert Strang, Barry Shein

by Earl Biggs

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

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> On Friday, April 1, 2022 at 4:13:20 PM UTC-4, Ben Bacarisse wrote:
>>
>> I think the answer may be something simple like the fact that g is bound
>> and not free in the vacuously true antecedent.

That may explain why substitution is not permitted, but there seems to
be much more going on...

> Yes, it may be a little more obvious in the latest version of my proof
> where I prove:
>
> ALL(x):[Set(x)
>
> => EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence
>
> & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness
>
> You cannot say, for example, that ALL(a):[a in null => f1(a) in x] is
> a theorem since f1 is a bound variable quantified outside of that
> expression.

Suppose a student, using your system was asked to demonstrate, with a
concrete example, what this meant for, say, x={1,2,3}.

What function might they produce to show that there is indeed an f such
that ALL(a):[a in null => f(a) in {1,2,3}]? Well, they could pull any
function at all out the air and it would work, wouldn't it? The
function that (only) maps apples to oranges would just as well as any
other.

Mind you, they also need to show that, at the same time,

ALL(f1):ALL(f2):[
ALL(a):[a in null => f1(a) in x] &
ALL(a):[a in null => f2(a) in x] => f1=f2
]

so maybe this part will sort things out. But no, because there is an
obvious counter-example: if f1 maps cats to mats and f2 maps bats to
hats we have a true antecedent and a false consequent.

So they are staring at a proof showing, supposedly, the existence and
uniqueness of null-functions for any set x, but the part that shows the
existence of a null function is satisfied by non-null functions, and
anyway, they can pick a counter-example to the whole theorem: x={1,2,3},
f1(cats)=mats, f2(bats)=hats.

--
Ben.

[Mostowski Collapse]

For vacuous truth its irrelevant whether f(a) in x or not.
After all its a vacuous truth.

You can prove:

1) Vacuously True <=> TRUE
∀a((Pa ∧ ¬Pa) → Q) ↔ (R∨¬R) is valid.

https://www.umsu.de/trees/#~6a%28P%28a%29~1~3P%28a%29~5Q%29~4R~2~3R

I took Pa & ~Pa as a replacement for a e null,
i.e. a formula that is always false for any a.

And I took R v ~R as replacement for TRUE,
since Dan-O-Matik doesn't have a TRUE constant in his system.

See also:

∀ x : P ( x ) ⇒ Q ( x ), where it is the case that ∀ x : ¬ P ( x )
https://en.wikipedia.org/wiki/Vacuous_truth#Scope_of_the_concept

The only defining constitutent for a vacuous truth is
∀ x : ¬ P ( x ), there is no constraint whatever on Q( x ),

it can be an arbitrary formula.

[Dan Christensen]

On Sunday, April 3, 2022 at 12:21:40 PM UTC-4, Ben Bacarisse wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Friday, April 1, 2022 at 4:13:20 PM UTC-4, Ben Bacarisse wrote:
> >>
> >> I think the answer may be something simple like the fact that g is bound
> >> and not free in the vacuously true antecedent.
> That may explain why substitution is not permitted, but there seems to
> be much more going on...
> > Yes, it may be a little more obvious in the latest version of my proof
> > where I prove:
> >
> > ALL(x):[Set(x)
> >
> > => EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence
> >
> > & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness
> >
> > You cannot say, for example, that ALL(a):[a in null => f1(a) in x] is
> > a theorem since f1 is a bound variable quantified outside of that
> > expression.
> Suppose a student, using your system was asked to demonstrate, with a
> concrete example, what this meant for, say, x={1,2,3}.
>
> What function might they produce to show that there is indeed an f such
> that ALL(a):[a in null => f(a) in {1,2,3}]?

The Cartesian product of the empty set and x would be the graph set for such a function.

> Well, they could pull any
> function at all out the air and it would work, wouldn't it?

"Work" in what sense?

> The
> function that (only) maps apples to oranges would just as well as any
> other.
>

Your set of "apples" would have to be empty.

> Mind you, they also need to show that, at the same time,
> ALL(f1):ALL(f2):[
> ALL(a):[a in null => f1(a) in x] &
> ALL(a):[a in null => f2(a) in x] => f1=f2
> ]
> so maybe this part will sort things out. But no, because there is an
> obvious counter-example: if f1 maps cats to mats and f2 maps bats to
> hats we have a true antecedent and a false consequent.
>

Your sets of "cats" and "bats" would have to be empty.

> So they are staring at a proof showing, supposedly, the existence and
> uniqueness of null-functions for any set x, but the part that shows the
> existence of a null function is satisfied by non-null functions, and
> anyway,

Wrong. Recall that a pair of functions is comparable only if they have same domains and codomains.

> they can pick a counter-example to the whole theorem: x={1,2,3},
> f1(cats)=mats, f2(bats)=hats.
>

The theorem holds for ANY set x. Nowhere did I put any restrictions on the elements of x. It may even be empty. It may be infinite.

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> On Sunday, April 3, 2022 at 12:21:40 PM UTC-4, Ben Bacarisse wrote:
>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>>
>> > On Friday, April 1, 2022 at 4:13:20 PM UTC-4, Ben Bacarisse wrote:
>> >>
>> >> I think the answer may be something simple like the fact that g is bound
>> >> and not free in the vacuously true antecedent.
>> That may explain why substitution is not permitted, but there seems to
>> be much more going on...
>> > Yes, it may be a little more obvious in the latest version of my proof
>> > where I prove:
>> >
>> > ALL(x):[Set(x)
>> >
>> > => EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence
>> >
>> > & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness
>> >
>> > You cannot say, for example, that ALL(a):[a in null => f1(a) in x] is
>> > a theorem since f1 is a bound variable quantified outside of that
>> > expression.
>> Suppose a student, using your system was asked to demonstrate, with a
>> concrete example, what this meant for, say, x={1,2,3}.
>>
>> What function might they produce to show that there is indeed an f such
>> that ALL(a):[a in null => f(a) in {1,2,3}]?
>
> The Cartesian product of the empty set and x would be the graph set
> for such a function.

As well as many others that are not null functions. That's the problem.

>> Well, they could pull any
>> function at all out the air and it would work, wouldn't it?
>
> "Work" in what sense?

Seriously? By work I mean that (using graphs since you've decided you
like them now) f={(apples, oranges)} would be a satisfying assignment
for the EXISTS(f) quantifier.

>> The
>> function that (only) maps apples to oranges would just as well as any
>> other.
>
> Your set of "apples" would have to be empty.

No. The function maps a single "thing" (denoted by the word apples) (I
have to be vague since your quantifiers don't appear to be over any
particular set) to a single other thing denoted by the word oranges.

It's graph is {(apples, oranges)} -- it maps a word to another word.
But I can see that using plural words has obscured the point. Any
function will do just as well. f could have the graph {(1,1)}.

>> Mind you, they also need to show that, at the same time,
>> ALL(f1):ALL(f2):[
>> ALL(a):[a in null => f1(a) in x] &
>> ALL(a):[a in null => f2(a) in x] => f1=f2
>> ]
>> so maybe this part will sort things out. But no, because there is an
>> obvious counter-example: if f1 maps cats to mats and f2 maps bats to
>> hats we have a true antecedent and a false consequent.
>
> Your sets of "cats" and "bats" would have to be empty.

No. The functions map a single word to a single other word. I regret
using plural words, but can you not see that any two distinct functions
will do just as well?

f1={(0,0), (1,1)}, f2={(0,1), (1,0)} also give rise to a true antecedent
and a false consequent.

>> So they are staring at a proof showing, supposedly, the existence and
>> uniqueness of null-functions for any set x, but the part that shows the
>> existence of a null function is satisfied by non-null functions, and
>> anyway,
>
> Wrong. Recall that a pair of functions is comparable only if they have
> same domains and codomains.

Who says? The functions I learned about do not have that restriction --
they are just sets, and equality is defined between any two sets.

But it makes no odd because the same problem occurs with what you call
"comparable functions" (see f1 and f2 four paragraphs up).

Further more, I thought you had presented a theorem provable in DC Proof
and I see no reference to such a restriction in the theorem. f1=f2
appears to be simple equality between two objects in the domain of
discourse.

I am starting to see why you have no formal specification of DC Proof.
Will all sorts of rules pop up as the discussion progresses, rules that
I could not intuit from what's posted here?

>> they can pick a counter-example to the whole theorem: x={1,2,3},
>> f1(cats)=mats, f2(bats)=hats.
>
> The theorem holds for ANY set x.

The theorem holds for any x. It hold for the Leaning Tower of Piza and
for the number 42 (if they are allowed in the domain of discourse). But
of course a counter-example has to have the outer antecedent, Set(x),
true and the outer consequent false.

> Nowhere did I put any restrictions on the elements of x. It may even
> be empty. It may be infinite.

I find this point truly bizarre. Why do you think I was presenting a
counter-example? It's because the theorem starts with a universal
quantifier. One counter-example is enough.

So, here is a counter-example that does not use words as the things
being mapped by functions, and where all the functions have the same
domain and codomain (since you think that matters):

x={0,1} all functions are from x->x. f1={(0,0), (1,1)}, f2={(0,1),
(1,0)}. Better?

Now, you've said that the notation is not defined, but unless you are
just jerking me around, something is seriously amiss here. I've been
assuming that:

'null' is the empty set.

'in' is the usual set membership, so 'a in null' is false for all a.

'=>' is the usual logical implication.

No theorem of the form ALL(x):[ <formula> ] can have a
counter-example. I.e. there can be no assignment of variables (both
bound and free -- if such are permitted) that makes <formula> evaluate
to false.

Are these assumptions unwarranted?

--
Ben.

[Dan Christensen]

On Sunday, April 3, 2022 at 4:14:51 PM UTC-4, Ben Bacarisse wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Sunday, April 3, 2022 at 12:21:40 PM UTC-4, Ben Bacarisse wrote:
> >> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> >>
> >> > On Friday, April 1, 2022 at 4:13:20 PM UTC-4, Ben Bacarisse wrote:
> >> >>
> >> >> I think the answer may be something simple like the fact that g is bound
> >> >> and not free in the vacuously true antecedent.
> >> That may explain why substitution is not permitted, but there seems to
> >> be much more going on...
> >> > Yes, it may be a little more obvious in the latest version of my proof
> >> > where I prove:
> >> >
> >> > ALL(x):[Set(x)
> >> >
> >> > => EXIST(f):ALL(a):[a in null => f(a) in x] <--- Existence
> >> >
> >> > & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]] <--- Uniqueness
> >> >
> >> > You cannot say, for example, that ALL(a):[a in null => f1(a) in x] is
> >> > a theorem since f1 is a bound variable quantified outside of that
> >> > expression.
> >> Suppose a student, using your system was asked to demonstrate, with a
> >> concrete example, what this meant for, say, x={1,2,3}.
> >>
> >> What function might they produce to show that there is indeed an f such
> >> that ALL(a):[a in null => f(a) in {1,2,3}]?
> >
> > The Cartesian product of the empty set and x would be the graph set
> > for such a function.

> As well as many others that are not null functions. That's the problem.

No, there is only one empty function mapping the empty set to any given set x.

> >> Well, they could pull any
> >> function at all out the air and it would work, wouldn't it?
> >

> > "Work" in what sense?

> Seriously? By work I mean that (using graphs since you've decided you
> like them now) f={(apples, oranges)} would be a satisfying assignment
> for the EXISTS(f) quantifier.
> >> The
> >> function that (only) maps apples to oranges would just as well as any
> >> other.
> >
> > Your set of "apples" would have to be empty.

> No. The function maps a single "thing" (denoted by the word apples) (I
> have to be vague since your quantifiers don't appear to be over any
> particular set) to a single other thing denoted by the word oranges.
>
> It's graph is {(apples, oranges)} -- it maps a word to another word.

OK, but how is this relevant? We are talking about empty functions.

> But I can see that using plural words has obscured the point. Any
> function will do just as well. f could have the graph {(1,1)}.

Yes. But this is not the graph of an empty function. It is f such that f: {1} --> {1}

> >> Mind you, they also need to show that, at the same time,
> >> ALL(f1):ALL(f2):[
> >> ALL(a):[a in null => f1(a) in x] &
> >> ALL(a):[a in null => f2(a) in x] => f1=f2
> >> ]
> >> so maybe this part will sort things out. But no, because there is an
> >> obvious counter-example: if f1 maps cats to mats and f2 maps bats to
> >> hats we have a true antecedent and a false consequent.
> >
> > Your sets of "cats" and "bats" would have to be empty.

> No. The functions map a single word to a single other word. I regret
> using plural words, but can you not see that any two distinct functions
> will do just as well?
>
> f1={(0,0), (1,1)}, f2={(0,1), (1,0)} also give rise to a true antecedent
> and a false consequent.

The domain in both cases is the non-empty set {0, 1}. Not empty functions.

> >> So they are staring at a proof showing, supposedly, the existence and
> >> uniqueness of null-functions for any set x, but the part that shows the
> >> existence of a null function is satisfied by non-null functions, and
> >> anyway,
> >
> > Wrong. Recall that a pair of functions is comparable only if they have
> > same domains and codomains.

> Who says? The functions I learned about do not have that restriction --
> they are just sets, and equality is defined between any two sets.
>

That's one school of thought, but such sets are usually now thought to be the GRAPH of a function as distinct from the corresponding function operator. (See Terrence Tao's "Analysis I" and Wikipedia.)

> But it makes no odd because the same problem occurs with what you call
> "comparable functions" (see f1 and f2 four paragraphs up).
>
> Further more, I thought you had presented a theorem provable in DC Proof
> and I see no reference to such a restriction in the theorem.

See the axiom on line 1 defining the equality of functions. Again, fairly standard AFAICT.

> f1=f2 appears to be simple equality between two objects in the domain of
> discourse.
>

They are labels that I have attached to a pair of empty functions that turn out to be equal.

> I am starting to see why you have no formal specification of DC Proof.
> Will all sorts of rules pop up as the discussion progresses, rules that
> I could not intuit from what's posted here?

I use what, implicitly anyway, seem to be the most commonly used methods and conventions in math textbooks. If sometimes differ with standard FOL and ZFC theory, so be it.

> >> they can pick a counter-example to the whole theorem: x={1,2,3},
> >> f1(cats)=mats, f2(bats)=hats.
> >
> > The theorem holds for ANY set x.

> The theorem holds for any x. It hold for the Leaning Tower of Piza and
> for the number 42 (if they are allowed in the domain of discourse).

Not relevant.

> But
> of course a counter-example has to have the outer antecedent, Set(x),
> true and the outer consequent false.

Your "counter-examples" do not restrict the domain of the functions to empty sets.

> > Nowhere did I put any restrictions on the elements of x. It may even
> > be empty. It may be infinite.

> I find this point truly bizarre. Why do you think I was presenting a
> counter-example? It's because the theorem starts with a universal
> quantifier. One counter-example is enough.
>

x is the codomain. The domain is null in each case, hence the EMPTY function designation.

> So, here is a counter-example that does not use words as the things
> being mapped by functions, and where all the functions have the same
> domain and codomain (since you think that matters):
>
> x={0,1} all functions are from x->x. f1={(0,0), (1,1)}, f2={(0,1),
> (1,0)}. Better?
>

Here, your domain for each is the non-empty set {0, 1}.

You can't list the elements of the graph set of an empty function. It is empty! You get a contradiction if you assume otherwise. And all empty sets are equal.

> Now, you've said that the notation is not defined, but unless you are
> just jerking me around, something is seriously amiss here. I've been
> assuming that:
>
> 'null' is the empty set.
>

Yes. It is defined on lines 2 and 3.

> 'in' is the usual set membership, so 'a in null' is false for all a.
>

Yes.

> '=>' is the usual logical implication.
>

You see, that wasn't so hard!

> No theorem of the form ALL(x):[ <formula> ] can have a
> counter-example.

An expression of the form ALL(x):[ <formula> ] is not a theorem if it has a counter-example.

[Ben Bacarisse]

Is this the level of debate I can expect? Of course that's true.
What's at issue is whether your theorem says that or not.

>> >> Well, they could pull any
>> >> function at all out the air and it would work, wouldn't it?
>> >
>
>> > "Work" in what sense?
>
>> Seriously? By work I mean that (using graphs since you've decided you
>> like them now) f={(apples, oranges)} would be a satisfying assignment
>> for the EXISTS(f) quantifier.
>> >> The
>> >> function that (only) maps apples to oranges would just as well as any
>> >> other.
>> >
>> > Your set of "apples" would have to be empty.
>
>> No. The function maps a single "thing" (denoted by the word apples) (I
>> have to be vague since your quantifiers don't appear to be over any
>> particular set) to a single other thing denoted by the word oranges.
>>
>> It's graph is {(apples, oranges)} -- it maps a word to another word.
>
> OK, but how is this relevant? We are talking about empty functions.

Because your theorem is not talking about empty functions, even though
you think it is.

>> But I can see that using plural words has obscured the point. Any
>> function will do just as well. f could have the graph {(1,1)}.
>
> Yes. But this is not the graph of an empty function. It is f such that
> f: {1} --> {1}

Indeed. But

EXISTS(f):ALL(a):[a in null => f(a) in x]

is satisfied by f = {(1,1)}. You want this to mean there exists an
empty function with x as the codomain, but it does not say that. At
least with my student hat on, it appears to be true about any f I can
dream up.

>> >> Mind you, they also need to show that, at the same time,
>> >> ALL(f1):ALL(f2):[
>> >> ALL(a):[a in null => f1(a) in x] &
>> >> ALL(a):[a in null => f2(a) in x] => f1=f2
>> >> ]
>> >> so maybe this part will sort things out. But no, because there is an
>> >> obvious counter-example: if f1 maps cats to mats and f2 maps bats to
>> >> hats we have a true antecedent and a false consequent.
>> >
>> > Your sets of "cats" and "bats" would have to be empty.
>
>> No. The functions map a single word to a single other word. I regret
>> using plural words, but can you not see that any two distinct functions
>> will do just as well?
>>
>> f1={(0,0), (1,1)}, f2={(0,1), (1,0)} also give rise to a true antecedent
>> and a false consequent.
>
> The domain in both cases is the non-empty set {0, 1}. Not empty
> functions.

Yes. Do you really not see the problem?

ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x]

is true when f1={(0,0), (1,1)} and f2={(0,1), (1,0)}. That gives a true
antecedent and false consequent (f1=f2).

>> >> So they are staring at a proof showing, supposedly, the existence and
>> >> uniqueness of null-functions for any set x, but the part that shows the
>> >> existence of a null function is satisfied by non-null functions, and
>> >> anyway,
>> >
>> > Wrong. Recall that a pair of functions is comparable only if they have
>> > same domains and codomains.
>
>> Who says? The functions I learned about do not have that restriction --
>> they are just sets, and equality is defined between any two sets.
>
> That's one school of thought, but such sets are usually now thought to
> be the GRAPH of a function as distinct from the corresponding function
> operator. (See Terrence Tao's "Analysis I" and Wikipedia.)

Such sets are considered functions in other contexts. There's no point
in arguing about this because it's not why DC Proof appears to be be
flawed.

I will write function graphs, because for small functions is so much
shorter, but you can consider the function to be some ofthe kind of
thing that simply has that set as the graph.

>> But it makes no odd because the same problem occurs with what you call
>> "comparable functions" (see f1 and f2 four paragraphs up).
>>
>> Further more, I thought you had presented a theorem provable in DC Proof
>> and I see no reference to such a restriction in the theorem.
>
> See the axiom on line 1 defining the equality of functions. Again,
> fairly standard AFAICT.

Please post it here. It may well explain what's going on. I'd like to
have the whole thing in one place.

>> f1=f2 appears to be simple equality between two objects in the domain of
>> discourse.
>
> They are labels that I have attached to a pair of empty functions that
> turn out to be equal.
>
>> I am starting to see why you have no formal specification of DC Proof.
>> Will all sorts of rules pop up as the discussion progresses, rules that
>> I could not intuit from what's posted here?
>
> I use what, implicitly anyway, seem to be the most commonly used
> methods and conventions in math textbooks. If sometimes differ with
> standard FOL and ZFC theory, so be it.
>
>> >> they can pick a counter-example to the whole theorem: x={1,2,3},
>> >> f1(cats)=mats, f2(bats)=hats.
>> >
>> > The theorem holds for ANY set x.
>
>> The theorem holds for any x. It hold for the Leaning Tower of Piza and
>> for the number 42 (if they are allowed in the domain of discourse).
>
> Not relevant.

Indeed. But you appeared to want to pick nits.

>> But
>> of course a counter-example has to have the outer antecedent, Set(x),
>> true and the outer consequent false.
>
> Your "counter-examples" do not restrict the domain of the functions to
> empty sets.

Of course. It would not be a counter-example if it did.

>> > Nowhere did I put any restrictions on the elements of x. It may even
>> > be empty. It may be infinite.
>
>> I find this point truly bizarre. Why do you think I was presenting a
>> counter-example? It's because the theorem starts with a universal
>> quantifier. One counter-example is enough.
>
> x is the codomain.

That is nowhere to be seen in the theorem, but none the less I chose a
counter-example in which the chosen x is the codomain of all the
functions.

> The domain is null in each case, hence the EMPTY
> function designation.

That is nowhere to be seen in the theorem. You think it is but my given
f1 and f2 are included in the ALL(f1) and ALL(f2) and cause the theorem
as written here) to be false. If they are not, what hidden rules govern
what ALL(g) can range over?

>> So, here is a counter-example that does not use words as the things
>> being mapped by functions, and where all the functions have the same
>> domain and codomain (since you think that matters):
>>
>> x={0,1} all functions are from x->x. f1={(0,0), (1,1)}, f2={(0,1),
>> (1,0)}. Better?
>
> Here, your domain for each is the non-empty set {0, 1}.

Yup.

> You can't list the elements of the graph set of an empty function. It
> is empty! You get a contradiction if you assume otherwise. And all
> empty sets are equal.

The empty function has graph {}.

>> Now, you've said that the notation is not defined, but unless you are
>> just jerking me around, something is seriously amiss here. I've been
>> assuming that:
>>
>> 'null' is the empty set.
>>
>
> Yes. It is defined on lines 2 and 3.

Where are these lines 2 and 2?

>> 'in' is the usual set membership, so 'a in null' is false for all a.
>
> Yes.
>
>> '=>' is the usual logical implication.
>
> You see, that wasn't so hard!

You want to be patronising do you? Why?

>> No theorem of the form ALL(x):[ <formula> ] can have a
>> counter-example.
>
> An expression of the form ALL(x):[ <formula> ] is not a theorem if
> it has a counter-example.

I was about to say "that's clear, thank you" when I noticed that you
have removed the rest of that paragraph:

I.e. there can be no assignment of variables (both
bound and free -- if such are permitted) that makes <formula> evaluate
to false.

Why did you remove this? Do you not agree with it? If you don't, saying
so it better than cutting it, and if you do agree, keeping it would also
help clarity.

So, what is it about the counter-example that you reject? x={0,1} is
surely one of the sets covered by the ALL(x)[Set(x) => ...]. If the
... part could be false when x={0,1} that would be a counter-example.

This bit: EXISTS(f):ALL(a):[a in null => f(a) in x] is fine (though I
don't think it says what you think. Such a f exists.

But this part is false:

ALL(f1):ALL(f2):[
ALL(a):[a in null => f1(a) in x] &
ALL(a):[a in null => f2(a) in x] => f1=f2
]

because we can find f1 and f2 that are not equal but for which ALL(a):[a
in null => f1(a) in x] and ALL(a):[a in null => f2(a) in x] are both
true.

For x={0,1} and f1={(0,0), (1,1)} then

ALL(a):[a in null => f1(a) in x]

is clearly true. Similarly, for For x={0,1} and f2={(0,1), (1,0)}

ALL(a):[a in null => f2(a) in x]

is also true. This is, of course, using a "natural" interpretation of
the notation. I don't know what it means formally. 'a in null' is
false for all a, so the truth or otherwise of 'f2(a) in x' is
immaterial.

I'm having trouble with the fact that you don't see a problem. It must
be that the notation means something so very un-obvious that I've got
the wrong end of the stick. Could it be that DC Proof can prove
theorems with counter-examples? I.e. could it be that it's inconsistent?

--
Ben.

[Mostowski Collapse]

The trouble is easy to spot and identify. Now Dan-O-Matik was
repeating his nonsense again, in a version 3:

ALL(x):[Set(x)
=> EXIST(f):ALL(a):[a e null => f(a) e x]
& ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x] => f1=f2]]
https://dcproof.com/EmptyFunctionsUniqueV3.htm

Using vacuous truth 3 times which can be eliminated, so in the end he proved:

ALL(f1):ALL(f2):[f1=f2]]

Which has a counter model. It also has a counter model that satisfy his axioms:

2 Set(null)
Axiom
3 ALL(a):~a e null
Axiom

Therefore the wrong axiom is this one:

1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a e dom => f(a) e cod] & ALL(a):[a e dom => g(a) e cod]
=> [f=g <=> ALL(a):[a e dom => f(a)=g(a)]]]

Its easy to undestand what goes wrong fron the above axiom.
ALL(a):[a e dom => f(a)=g(a)]]] does not imply f=g. If you only
look at the values of f and g on dom, this does not necessarily

imply that f = g. Take for example this two functions:

f(x) = x

g(x) = abs(x)

They agree on dom = [0..oo) ⊆ R, but they are not the same,
since they don't agree on full R.

[Mostowski Collapse]

Maybe Dan-O-Matik is still subject to some self alluded witchcraft,
in that he still believes that ALL(a):[a e dom => f(a) e cod] means
f : dom -> cod, this would explain his blooper to some

extend. But he can easily consult wikipedia or some other source
where it is stated that f : dom -> cod also requires f ⊆ dom x cod.
Maybe he would get out of his misery, if he would study this

booklet, which I have already recommended a dozen times:

Basic Set Theory (Dover Books on Mathematics)
Azriel Levy (Author) - ISBN-13: 978-0486420790
https://www.amazon.com/Basic-Theory-Dover-Books-Mathematics/dp/0486420795

But this will not completely break the spell. There is not only
lack of f ⊆ dom x cod there is also confusion between set-like
functions and the function symbols from FOL, which

are admittedly f : V -> V where V is the universe of discourse.
His self hypnosis also contains the idea to have ALL(a):[a e dom
=> f(a) e cod] as a replacement for f : dom -> cod and at the

same time f(a) as a replacement for the Peano apostroph f'a.

So far this quest has not reached its goal.

[Dan Christensen]

My theorem:

ALL(x):[Set(x)
=> EXIST(f):ALL(a):[a in null => f(a) in x]

& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]]

There are functions f, f1 and f2. Each has a domain set of null which defined to an empty set on lines 2 and 3. Each is an EMPTY FUNCTION.

> >> But I can see that using plural words has obscured the point. Any
> >> function will do just as well. f could have the graph {(1,1)}.
> >
> > Yes. But this is not the graph of an empty function. It is f such that
> > f: {1} --> {1}

> Indeed. But
>
> EXISTS(f):ALL(a):[a in null => f(a) in x]
>
> is satisfied by f = {(1,1)}.

That function f has a non-empty domain of {1}. As such, it is not comparable to any empty function. A standard rule AFAICT. (See Terrence Tao's "Analysis I")

> You want this to mean there exists an
> empty function with x as the codomain, but it does not say that. At
> least with my student hat on, it appears to be true about any f I can
> dream up.

> >> >> Mind you, they also need to show that, at the same time,
> >> >> ALL(f1):ALL(f2):[
> >> >> ALL(a):[a in null => f1(a) in x] &
> >> >> ALL(a):[a in null => f2(a) in x] => f1=f2
> >> >> ]
> >> >> so maybe this part will sort things out. But no, because there is an
> >> >> obvious counter-example: if f1 maps cats to mats and f2 maps bats to
> >> >> hats we have a true antecedent and a false consequent.
> >> >
> >> > Your sets of "cats" and "bats" would have to be empty.
> >
> >> No. The functions map a single word to a single other word. I regret
> >> using plural words, but can you not see that any two distinct functions
> >> will do just as well?
> >>
> >> f1={(0,0), (1,1)}, f2={(0,1), (1,0)} also give rise to a true antecedent
> >> and a false consequent.
> >
> > The domain in both cases is the non-empty set {0, 1}. Not empty
> > functions.

> Yes. Do you really not see the problem?

> ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x]

Both f1 and f2 are assumed to be empty functions.

> is true when f1={(0,0), (1,1)} and f2={(0,1), (1,0)}.

Not empty functions. Not the subject of this theorem.

> >> >> So they are staring at a proof showing, supposedly, the existence and
> >> >> uniqueness of null-functions for any set x, but the part that shows the
> >> >> existence of a null function is satisfied by non-null functions, and
> >> >> anyway,
> >> >
> >> > Wrong. Recall that a pair of functions is comparable only if they have
> >> > same domains and codomains.
> >
> >> Who says? The functions I learned about do not have that restriction --
> >> they are just sets, and equality is defined between any two sets.
> >
> > That's one school of thought, but such sets are usually now thought to
> > be the GRAPH of a function as distinct from the corresponding function
> > operator. (See Terrence Tao's "Analysis I" and Wikipedia.)
> Such sets are considered functions in other contexts. There's no point
> in arguing about this because it's not why DC Proof appears to be be
> flawed.
>

> I will write function graphs, because for small functions is so much
> shorter, but you can consider the function to be some ofthe kind of
> thing that simply has that set as the graph.

The graph/function relation avoids Burse's Paradox: The notion that you can make inferences about a function outside of it's domain of definition. Discovered by our own Jan Burse. He calls it a feature. I call it a bug.

> >> But it makes no odd because the same problem occurs with what you call
> >> "comparable functions" (see f1 and f2 four paragraphs up).
> >>
> >> Further more, I thought you had presented a theorem provable in DC Proof
> >> and I see no reference to such a restriction in the theorem.
> >
> > See the axiom on line 1 defining the equality of functions. Again,
> > fairly standard AFAICT
.
> Please post it here. It may well explain what's going on. I'd like to
> have the whole thing in one place.

ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a in dom => f(a) in cod] & ALL(a):[a in dom => g(a) in cod]
=> [f=g <=> ALL(a):[a in dom => f(a)=g(a)]]]

Where
dom = domain of function
cod = codomain of function

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values of x, but not others, then we do not consider f and g to be equal.)"
Terence Tao, "Analysis I - Third Ed.", p. 51

Where do you get the idea that this theorem is about functions in general? It concerns ONLY empty functions.

> You think it is but my given
> f1 and f2 are included in the ALL(f1) and ALL(f2) and cause the theorem
> as written here) to be false. If they are not, what hidden rules govern
> what ALL(g) can range over?
> >> So, here is a counter-example that does not use words as the things
> >> being mapped by functions, and where all the functions have the same
> >> domain and codomain (since you think that matters):
> >>
> >> x={0,1} all functions are from x->x. f1={(0,0), (1,1)}, f2={(0,1),
> >> (1,0)}. Better?
> >
> > Here, your domain for each is the non-empty set {0, 1}.
> Yup.
> > You can't list the elements of the graph set of an empty function. It
> > is empty! You get a contradiction if you assume otherwise. And all
> > empty sets are equal.

> The empty function has graph {}.

In DC Proof, it is actually an empty set of ordered pairs:

Set'(e2) & ALL(a):ALL(b):[~(a,b) in e2]

> >> Now, you've said that the notation is not defined, but unless you are
> >> just jerking me around, something is seriously amiss here. I've been
> >> assuming that:
> >>
> >> 'null' is the empty set.
> >>
> >
> > Yes. It is defined on lines 2 and 3.
> Where are these lines 2 and 2?
> >> 'in' is the usual set membership, so 'a in null' is false for all a.
> >
> > Yes.
> >
> >> '=>' is the usual logical implication.
> >
> > You see, that wasn't so hard!
> You want to be patronising do you? Why?
> >> No theorem of the form ALL(x):[ <formula> ] can have a
> >> counter-example.
> >
> > An expression of the form ALL(x):[ <formula> ] is not a theorem if
> > it has a counter-example.
> I was about to say "that's clear, thank you" when I noticed that you
> have removed the rest of that paragraph:
> I.e. there can be no assignment of variables (both
> bound and free -- if such are permitted) that makes <formula> evaluate
> to false.
> Why did you remove this?

Sorry, but it didn't make sense and didn't seem relevant in any case. To me, a theorem is just a statement the proof of which has no undischarged premises, and no free variables (constants) that were not introduced in axioms.

> So, what is it about the counter-example that you reject? x={0,1} is
> surely one of the sets covered by the ALL(x)[Set(x) => ...].

[snip]

Again, your "counterexamples" were not empty functions, the subject of this theorem.

High level view of my proof:

Define: Equality of functions (1 variable)

Only functions with the same domain and codomain are comparable here.

1. ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a in dom => f(a) in cod] & ALL(a):[a in dom => g(a) in cod]
=> [f=g <=> ALL(a):[a in dom => f(a)=g(a)]]]
Axiom


Define: null (The empty set)

2. Set(null)
Axiom

3. ALL(a):~a in null
Axiom


As Required:

97. ALL(x):[Set(x)

=> EXIST(f):ALL(a):[a in null => f(a) in x]

& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x]
=> f1=f2]]

Conclusion, 4


I am considering hard-coding the above definition of function equality in DC Proof.

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> On Sunday, April 3, 2022 at 6:48:44 PM UTC-4, Ben Bacarisse wrote:
>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:

>> > OK, but how is this relevant? We are talking about empty functions.
>
>> Because your theorem is not talking about empty functions, even though
>> you think it is.
>

> My theorem:

>
> ALL(x):[Set(x)
> => EXIST(f):ALL(a):[a in null => f(a) in x]

> & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]]
>

> There are functions f, f1 and f2. Each has a domain set of null which
> defined to an empty set on lines 2 and 3. Each is an EMPTY FUNCTION.

But that is not what the notation says. The inner clauses are about
ALL(f1), not just those with an empty domain. That's fine (and
necessary) provided that what you state is true for ALL(f1) is true only
for empty functions. It isn't.

ALL(a):[a in null => f1(a) in x] is true for any f1. Surely you can see
that 'a in null => f1(a) in x' says nothing about f1 because there is no
'a' for which 'a in null' is anything but false. And if the antecedent
can't be false, the implication can't be anything but true.

If DC Proof can't prove the following

ALL(x):ALL(f1):ALL(a):[a in null => f1(a) in x]

then something else is wrong with it too. If you disagree that this is
a theorem can you think of a counter-example? Is there any x, f1 and a
that can make

a in null => f1(a) in x

false? No, there is no a that can make the antecedent true, so the
implication is always true regardless of whether 'f1(a) in x' or not.

>> >> But I can see that using plural words has obscured the point. Any
>> >> function will do just as well. f could have the graph {(1,1)}.
>> >
>> > Yes. But this is not the graph of an empty function. It is f such that
>> > f: {1} --> {1}
>
>> Indeed. But
>>
>> EXISTS(f):ALL(a):[a in null => f(a) in x]
>>
>> is satisfied by f = {(1,1)}.
>

> That function f has a non-empty domain of {1}. As such, it is not

> comparable to any empty function. A standard rule AFAICT. (See
> Terrence Tao's "Analysis I")

ALL(a):[a in null => f(a) in x] is true for that f. If you disagree,
what a and x can make 'a in null => f(a) in x' false? You /want/ f to
have an empty domain, but nothing is the proof says it has. The only
constraint on f is the always-true ALL(a):[a in null => f(a) in x].

>> You want this to mean there exists an
>> empty function with x as the codomain, but it does not say that. At
>> least with my student hat on, it appears to be true about any f I can
>> dream up.
>
>> >> >> Mind you, they also need to show that, at the same time,
>> >> >> ALL(f1):ALL(f2):[
>> >> >> ALL(a):[a in null => f1(a) in x] &
>> >> >> ALL(a):[a in null => f2(a) in x] => f1=f2
>> >> >> ]
>> >> >> so maybe this part will sort things out. But no, because there is an
>> >> >> obvious counter-example: if f1 maps cats to mats and f2 maps bats to
>> >> >> hats we have a true antecedent and a false consequent.
>> >> >
>> >> > Your sets of "cats" and "bats" would have to be empty.
>> >
>> >> No. The functions map a single word to a single other word. I regret
>> >> using plural words, but can you not see that any two distinct functions
>> >> will do just as well?
>> >>
>> >> f1={(0,0), (1,1)}, f2={(0,1), (1,0)} also give rise to a true antecedent
>> >> and a false consequent.
>> >
>> > The domain in both cases is the non-empty set {0, 1}. Not empty
>> > functions.
>
>> Yes. Do you really not see the problem?
>
>> ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x]
>

> Both f1 and f2 are assumed to be empty functions.
>

>> is true when f1={(0,0), (1,1)} and f2={(0,1), (1,0)}.
>

> Not empty functions. Not the subject of this theorem.

Not the /intended/ subject of the theorem, but saying so in words does
not make it so in the proof. If f1={(0,0), (1,1)} and f2={(0,1), (1,0)}
make that clause true, then it does not matter what you intended the
theorem to be about.

<cut>

>> >> Now, you've said that the notation is not defined, but unless you are
>> >> just jerking me around, something is seriously amiss here. I've been
>> >> assuming that:
>> >>
>> >> 'null' is the empty set.
>> >>

>> >> 'in' is the usual set membership, so 'a in null' is false for all a.
>> >
>> > Yes.
>> >
>> >> '=>' is the usual logical implication.
>> >
>> > You see, that wasn't so hard!
>>
>> You want to be patronising do you? Why?

No comment?

>> >> No theorem of the form ALL(x):[ <formula> ] can have a
>> >> counter-example.
>> >
>> > An expression of the form ALL(x):[ <formula> ] is not a theorem if
>> > it has a counter-example.
>> I was about to say "that's clear, thank you" when I noticed that you
>> have removed the rest of that paragraph:
>> I.e. there can be no assignment of variables (both
>> bound and free -- if such are permitted) that makes <formula> evaluate
>> to false.
>> Why did you remove this?
>

> Sorry, but it didn't make sense and didn't seem relevant in any
> case. To me, a theorem is just a statement the proof of which has no
> undischarged premises, and no free variables (constants) that were not
> introduced in axioms.

And that's fine. But if the proof system is flawed, there will be
theorems with counter-examples. As seems to be the case here.

>> So, what is it about the counter-example that you reject? x={0,1} is
>> surely one of the sets covered by the ALL(x)[Set(x) => ...].
>

> [snip]
>
> Again, your "counterexamples" were not empty functions, the subject of
> this theorem.

The /intended/ subject. It is, in fact, about more function than you
want it to be about. You can't keep saying that the function are not
empty if they satisfy the constrains of in the theorem.

> High level view of my proof:
>
> Define: Equality of functions (1 variable)
>
> Only functions with the same domain and codomain are comparable here.
>
> 1. ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a in dom => f(a) in cod] & ALL(a):[a in dom => g(a) in cod]
> => [f=g <=> ALL(a):[a in dom => f(a)=g(a)]]]
> Axiom

This does not constrain the f1 and f2 bound in line 97 to be empty
functions so it does not remove the counter-example. (There are other
issues with it, but there is such a large elephant in the room already,
we should address that first.)

> Define: null (The empty set)
>
> 2. Set(null)
> Axiom
>
> 3. ALL(a):~a in null
> Axiom

Neither does this.

> As Required:
>
> 97. ALL(x):[Set(x)

> => EXIST(f):ALL(a):[a in null => f(a) in x]

> & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x]
> => f1=f2]]

> Conclusion, 4

And here, x={0,1}, f1={(0,0), (1,1)}, f2={(0,1), (1,0)} is a
counter-example to line 97. You don't want the antecedent of => f1=f2
to be true for anything but empty functions, but it is.

--
Ben.

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

This appears to be a duplicate. I replied to what looks like an
identical post posted four minutes earlier. If there are important
corrections in this version, I apologise. I've missed them.

--
Ben.

[Dan Christensen]

I did delete reply on Google Group, made a minor correction and resent it. Sorry about any confusion.

[Dan Christensen]

On Sunday, April 3, 2022 at 10:28:33 PM UTC-4, Ben Bacarisse wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> > On Sunday, April 3, 2022 at 6:48:44 PM UTC-4, Ben Bacarisse wrote:
> >> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> >> > OK, but how is this relevant? We are talking about empty functions.
> >
> >> Because your theorem is not talking about empty functions, even though
> >> you think it is.
> >
> > My theorem:
> >
> > ALL(x):[Set(x)
> > => EXIST(f):ALL(a):[a in null => f(a) in x]
> > & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]]
> >
> > There are functions f, f1 and f2. Each has a domain set of null which
> > defined to an empty set on lines 2 and 3. Each is an EMPTY FUNCTION.

> But that is not what the notation says.

What ARE you talking about? What do you think is meant by ALL(a):[a in null => f1(a) in x] ? It is a restriction on the ALL(f1) quantifier to only empty functions mapping { } to x.

>The inner clauses are about
> ALL(f1), not just those with an empty domain. That's fine (and
> necessary) provided that what you state is true for ALL(f1) is true only
> for empty functions. It isn't.
>
> ALL(a):[a in null => f1(a) in x] is true for any f1. Surely you can see
> that 'a in null => f1(a) in x' says nothing about f1 because there is no
> 'a' for which 'a in null' is anything but false. And if the antecedent
> can't be false, the implication can't be anything but true.
>
> If DC Proof can't prove the following
>
> ALL(x):ALL(f1):ALL(a):[a in null => f1(a) in x]
>

Makes no sense.

Maybe something like: ALL(x):[Set(x) => [ALL(f1):[ALL(a):[a in null => f1(a) in x] => P(x,f1)]]]for some binary predicate P.

ALL(a):[a in null => f1(a) in x] is a restriction on the quantifier ALL(f1). What do you want for P(x,f1)? Saying that something is true of every empty function mapping { } to x? Please clarify.

> then something else is wrong with it too. If you disagree that this is
> a theorem can you think of a counter-example? Is there any x, f1 and a
> that can make
> a in null => f1(a) in x
> false?

Can't be done since you cannot introduce new free variables or function images of free variables by vacuous truth.

> No, there is no a that can make the antecedent true, so the
> implication is always true regardless of whether 'f1(a) in x' or not.


> >> >> But I can see that using plural words has obscured the point. Any
> >> >> function will do just as well. f could have the graph {(1,1)}.
> >> >
> >> > Yes. But this is not the graph of an empty function. It is f such that
> >> > f: {1} --> {1}
> >
> >> Indeed. But
> >>
> >> EXISTS(f):ALL(a):[a in null => f(a) in x]
> >>
> >> is satisfied by f = {(1,1)}.
> >
> > That function f has a non-empty domain of {1}. As such, it is not
> > comparable to any empty function. A standard rule AFAICT. (See
> > Terrence Tao's "Analysis I")
>
> ALL(a):[a in null => f(a) in x] is true for that f.

Previous comment applies here.

Previous comment applies here, too. It can't be proven due to restrictions on the use of vacuous truth (Arbitrary Consequent).

You haven't made that case.

> >> So, what is it about the counter-example that you reject? x={0,1} is
> >> surely one of the sets covered by the ALL(x)[Set(x) => ...].
> >
> > [snip]
> >
> > Again, your "counterexamples" were not empty functions, the subject of
> > this theorem.

> The /intended/ subject. It is, in fact, about more function than you
> want it to be about.

Nope. I start with the premise Set(x). Eventually, I introduce the premise: ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x]
That premise postulates the existence of a pair of empty functions, both mapping the empty set to the set x.

> You can't keep saying that the function are not
> empty if they satisfy the constrains of in the theorem.

You cannot prove what you want to prove in DC Proof. Deal with it.

> > High level view of my proof:
> >
> > Define: Equality of functions (1 variable)
> >
> > Only functions with the same domain and codomain are comparable here.
> >
> > 1. ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a in dom => f(a) in cod] & ALL(a):[a in dom => g(a) in cod]
> > => [f=g <=> ALL(a):[a in dom => f(a)=g(a)]]]
> > Axiom

> This does not constrain the f1 and f2 bound in line 97 to be empty
> functions so it does not remove the counter-example.

It defines the equality of functions. It does not postulate the existence of anything.

> (There are other
> issues with it, but there is such a large elephant in the room already,
> we should address that first.)

Your imaginary pink elephant?

> > Define: null (The empty set)
> >
> > 2. Set(null)
> > Axiom
> >
> > 3. ALL(a):~a in null
> > Axiom
> Neither does this.
>

Neither does this WHAT?

> > As Required:
> >
> > 97. ALL(x):[Set(x)
> > => EXIST(f):ALL(a):[a in null => f(a) in x]
> > & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x]
> > => f1=f2]]
> > Conclusion, 4
>
> And here, x={0,1}, f1={(0,0), (1,1)}, f2={(0,1), (1,0)} is a
> counter-example to line 97.

Already debunked here.

> You don't want the antecedent of => f1=f2
> to be true for anything but empty functions, but it is.
>

Try to prove your own theorem about functions in general if you don't want to prove anything about empty functions. They are kind of boring, but they do demonstrate some of the "safeguards" built into DC Proof.

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> On Sunday, April 3, 2022 at 10:28:33 PM UTC-4, Ben Bacarisse wrote:
>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>> > On Sunday, April 3, 2022 at 6:48:44 PM UTC-4, Ben Bacarisse wrote:
>> >> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>>
>> >> > OK, but how is this relevant? We are talking about empty functions.
>> >
>> >> Because your theorem is not talking about empty functions, even though
>> >> you think it is.
>> >
>> > My theorem:
>> >
>> > ALL(x):[Set(x)
>> > => EXIST(f):ALL(a):[a in null => f(a) in x]
>> > & ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) in x] => f1=f2]]
>> >
>> > There are functions f, f1 and f2. Each has a domain set of null which
>> > defined to an empty set on lines 2 and 3. Each is an EMPTY FUNCTION.
>
>> But that is not what the notation says.
>
> What ARE you talking about? What do you think is meant by ALL(a):[a in
> null => f1(a) in x] ? It is a restriction on the ALL(f1) quantifier to
> only empty functions mapping { } to x.

In conventional notation, ∀a(a ∈ Ø → f1(a) ∈ x) is true for any function
f1. The antecedent in the implication does /not/ restrict the
quantifier. It simply means that we only care if the consequent, f1(a)
∈ x, is true or not in those cases with a true antecedent. When the
antecedent is false for all a (as in this case) the whole formula in the
for-all clause is true for all a.

Further, in conventional mathematics, if ∀a(a ∈ Ø → f1(a) ∈ x) is not
true then there will be some individual a, some set x, and some
individual function f1 that makes a ∈ Ø → f1(a) ∈ x false. I.e. there
would be a counter-example. But there is none.

To pick an example that the lovely Tree Proof Generator can verify[1]

∀a(¬a=a → X(a))

is a theorem and does not depend on what X is. Presumably, no matter
what DC Proof uses the symbols to mean, you don't dispute what the
conventional notation means, do you?

I can see why you think the antecedent restricts the quantifier because
in many cases that is the apparent effect:

∀x(Set(x) → P(x))

is a theorem if and only if P is true of all sets because for x's that
are not sets, P(x) is irrelevant to the truth of the whole clause. But
when the first predicate is true of no x's (for example ¬x=x) then you
get a theorem regardless of what P is.

Unfortunately, if DC Proof is used for teaching, the meanings of ALL(a),
'in' and '=>' should match those of conventional mathematics. This is
why I asked for the definition of your notation. I've looked at a
couple of theorems you've posted which, when translated into
conventional, were nonsense.

Most of the rest of your remarks are irrelevant until this point is
cleared up.

[1] https://www.umsu.de/trees/#~6a(~3a=a~5a=a)
--
Ben.

[Dan Christensen]

On Monday, April 4, 2022 at 9:09:30 AM UTC-4, Ben Bacarisse wrote:


> In conventional notation, ∀a(a ∈ Ø → f1(a) ∈ x) is true for any function
> f1.

[snip]

In DC Proof, as in most math textbooks, you can either prove the existence of such a function (as in the first part of my proof), or provisionally assume it using an axiom or premise (as in the 2nd part).

Suppose, for example, you have a function f : x --> x. You cannot simply assume that ALL(a):[ a in null => f(a) in x], you have to prove it. To do that, you start with a premise a introducing an new free variable y in the domain of the required function (the null set in this case):

y in null
Premise

Then apply the definition of null to obtain:

~y in null
U Spec

Now you attempt to obtain "f(y) in x", but f(y) was not previously introduced so DC Proof should not allow you to proceed with you argument by vacuous proof.

>
> Unfortunately, if DC Proof is used for teaching, the meanings of ALL(a),
> 'in' and '=>' should match those of conventional mathematics.

What you call "conventional mathematics" might more rightly be called "conventional philosophy." In conventional mathematics, for example, you cannot introduce new free variables by universal specification. Philosophers like to implicitly assume the existence of a non-empty universe (as a handy shortcut AFAICT). Mathematicians do not. A given quantifier may quantify over an empty set (as in empty functions). Even within the same statement, different quantifiers may quantify of different domains. As such, there is no notion in mathematics of an overarching domain of discourse.

> This is
> why I asked for the definition of your notation. I've looked at a
> couple of theorems you've posted which, when translated into
> conventional, were nonsense.
>

Only because you insist on making unwarranted assumptions that cannot be justified in conventional mathematics.

[Ross A. Finlayson]

On Monday, March 28, 2022 at 2:33:33 PM UTC-7, Mostowski Collapse wrote:
> Unfortunately the theorem is not correct.
> You have two vacuous truths, so basically you say:
>
> EXIST(f):ALL(g):[g = f]
>
> You say all functions are the same.
> Just replace the vacuous truth by *T* and simplify the theorem.
>
> LMAO!
> Dan Christensen schrieb am Montag, 28. März 2022 um 23:30:05 UTC+2:
> > The following proof demonstrates how functions, function equality, function spaces and empty functions can be handled in my DC Proof system.

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

> > ********************************************************************
> >
> > THEOREM
> >
> > 1. On every set, there is exists a unique empty function.
> >
> > ALL(x):[Set(x)
> >
> > => EXIST(f):[ALL(a):[a in null => f(a) in x]
> >
> > & ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]
> >
> >
> > 2. The function space (fs) of all functions mapping the empty set to any set x has only a single element.
> >
> > ALL(x):[Set(x)
> >
> > => EXIST(fs):EXIST(f1):[Set(fs) & f1 in fs
> >
> > & [ALL(f):[f in fs <=> ALL(a):[a in null => f(a) in x]] <--- Function space fs
> >
> > & ALL(f2):[f2 in fs => f2=f1]]]]
> >
> > Formal proof: https://dcproof.com/EmptyFunctionsUniqueV2.htm (137 lines)

I mentioned this ten years ago.

[Ben Bacarisse]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> On Monday, April 4, 2022 at 9:09:30 AM UTC-4, Ben Bacarisse wrote:
>
>> In conventional notation, ∀a(a ∈ Ø → f1(a) ∈ x) is true for any function
>> f1.
>
> [snip]

OK. So you don't want to address the problem? That's fine.

The text to wrote just repeats the same problem several times.
If you want to get to the bottom of this, you'd have to engage with what
I wrote. It's still there if you want to talk engage.

--
Ben.

[Ross A. Finlayson]

On Wednesday, March 30, 2022 at 1:33:30 PM UTC-7, Ben Bacarisse wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> > On Monday, March 28, 2022 at 5:33:33 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> >
> >> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> >> > Visit my Math Blog at http://www.dcproof.wordpress.com
> >> > ********************************************************************
> >> >
> >> > THEOREM
> >> >
> >> > 1. On every set, there is exists a unique empty function.
> >> >
> >> > ALL(x):[Set(x)
> >> >
> >> > => EXIST(f):[ALL(a):[a in null => f(a) in x]
> >> >
> >> > & ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]
> >> >
> >> >
> >> > 2. The function space (fs) of all functions mapping the empty set to any set x has only a single element.
> >> >
> >> > ALL(x):[Set(x)
> >> >
> >> > => EXIST(fs):EXIST(f1):[Set(fs) & f1 in fs
> >> >
> >> > & [ALL(f):[f in fs <=> ALL(a):[a in null => f(a) in x]] <--- Function space fs
> >> >
> >> > & ALL(f2):[f2 in fs => f2=f1]]]]
> >> >
> >> > Formal proof: https://dcproof.com/EmptyFunctionsUniqueV2.htm (137 lines)
> >

> >> Unfortunately the theorem is not correct.
> >> You have two vacuous truths, so basically you say:
> >>
> >> EXIST(f):ALL(g):[g = f]
> >

> > Your inexperience with formal logic is showing, Jan Burse. Perhaps you
> > didn't know, but the principle of vacuous proof is a legitimate method
> > of proof.
>
> I am wary of wading into what it obviously a long-standing animosity,
> but I am struck by the fact that you don't seem to see what it is that
> MC is saying. I had the same thought as he, but decided not to comment
> as you had already told me that there is no document explaining your
> notation and, in general, I prefer to comment only what I know what I'm
> commenting on!
>
> However, in most deductions one can replace <vacuous truth> & X with X
> and <vacuous truth> => Y with Y. The vacuous truth part adds nothing.
> In

> ALL(x):[Set(x) =>
> EXIST(f):[
> ALL(a):[a in null => f(a) in x] &
> ALL(g):[
> ALL(a):[a e null => g(a) e x] =>
> g=f
> ]
> ]
> ]

> both ALL(a):[a in null => f(a) in x] and ALL(a):[a e null => g(a) e x]
> appear to be vacuous truths, suggesting that both the conjunction and
> the fourth implication could be simplified:
> ALL(x):[Set(x) =>
> EXIST(f):[
> ALL(g):[
> g=f
> ]
> ]
> ]
> Presumably, in your notation, this sort of simplification is not
> permitted, or the two ALL(a) forms are not, in fact, vacuously true, but
> you do yourself a disservice by not addressing the point.
>
> --
> Ben.

The vacuous satisfaction really depends on whether there is
that the vacuous is satisfaction, or, unsatisfied or unsatisfying,
that the vacuous even exists besides suffices, where variously
the vacuous holds or the vacuous doesn't hold, or, holds not.

As vacated or vacuum, is for cases "vacuous, doesn't hold", or,
"vacuum state, potential field in effect realizes physics".

Usually enough framed "could"....

The extra-ordinary or that "infinity, contains itself", where the
ordinary is "contains at most each other, is contained" makes
for a vacuity, infinitesimals for the infinity instead of empty.

(Which in a closed theory of two words is empty.)

[Ross A. Finlayson]

On Thursday, March 31, 2022 at 6:33:58 PM UTC-7, Dan Christensen wrote:

> > > Again, the principle of vacuous is a legitimate method of proof in mathematics.

> > >
> > >> In
> > >> ALL(x):[Set(x) =>
> > >> EXIST(f):[
> > >> ALL(a):[a in null => f(a) in x] &
> > >> ALL(g):[
> > >> ALL(a):[a e null => g(a) e x] =>
> > >> g=f
> > >> ]
> > >> ]
> > >> ]
> > >

> > > In words, for every set X, there exists a unique function f: { } -->
> > > X. Do you agree with this interpretation? If not, how would you
> > > formally state this sentence?
> > You don't have a definition of your notation, so I can't comment on what
> > is might mean. I am just asking you to clarify just a couple of points
> > about it.
> >
> > In set theory, a function from X to Y is just a particular kind of
> > subset of X x Y. There is only one subset of {} x Y and that's {}.

> > >> both ALL(a):[a in null => f(a) in x] and ALL(a):[a e null => g(a) e x]
> > >> appear to be vacuous truths,
> > >

> > > Agreed.
> > Well that's one. Thanks.

> > >> suggesting that both the conjunction and
> > >> the fourth implication could be simplified:
> > >> ALL(x):[Set(x) =>
> > >> EXIST(f):[
> > >> ALL(g):[
> > >> g=f
> > >> ]
> > >> ]
> > >> ]
> > >

> > > Can you formalize this argument using some form of natural deduction?
> > My question is what is it about your notation and/or system that
> > prevents TRUE & P being replaced by P
> The closest I can come to this is, using my version of natural deduction, I can derive:
>
> 1. Q
> Premise
>
> 2. Q & P
> Premise
>
> 3. P
> Split, 2
>
> 4. Q & P => P
> Conclusion, 2
>
> 5. Q => [Q & P => P]
> Conclusion, 1
> > and TRUE => Q being replaced by Q.
> >
> 1. P
> Premise
>
> 2. P => Q
> Premise
>
> 3. Q
> Detach, 2, 1
>
> 4. P => Q => Q
> Conclusion, 2
>
> 5. P => [P => Q => Q]
> Conclusion, 1
>
> where '=>' is left associative.
>
> I can make some direct replacements within a statement, e.g.
>
> ~~A ---> A
> A=>B ---> ~[A & ~B]
>
> This is nothing new or radical. It is just my formalization of the basic logic that is widely used in mathematics.
>
> Dan

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

The "my version of natural deduction...", agree then what follows
is [...and a course of uninformed after the underdefined that must
always include the abstract closures of the "true" definition before
the "my version of natural deduction"].

I.e. no "DC proof is only forward induction stipulated after terms",
that is just a graph-path in the space of related inferences. For general
terms that are simply defined as constants then "these objects relations
under syllogism, too, forward and mutually conclusive" here is that
the "mutually conclusive" is trivially satisfied by a monolog, but, the
"mutually conclusive", for a logical and mathematical proof,
is part of the entire body, while those closures under constants of
selected inferences, are only as well defined as closing out all the constants
of all the defined terms.

Of course each person has their real definition of terms their
"my version of natural deduction".

So, proofs in mathematics and logic are replete to be complete,
and there are stronger than incomplete theories besides the
"reduced to these terms, in these relations, satisfaction
is discharged as were there no other terms".

Then, there are not so many axiom systems for quite complete
and consistent theories of objects of mathematics numbers and
so on, with of course though that natural quantities are in qualia,
and besides the perfect order and form of geometry.

This then is for the value of things and basically the multivalent,
"the undefined: that is defined".

[Ben Bacarisse]

"Ross A. Finlayson" <ross.fi...@gmail.com> writes:

> The vacuous satisfaction really depends on whether there is
> that the vacuous is satisfaction, or, unsatisfied or unsatisfying,
> that the vacuous even exists besides suffices, where variously
> the vacuous holds or the vacuous doesn't hold, or, holds not.

Can you write that in English?

--
Ben.

[FredJeffries]

The problem seems to me to be that the 'definition' of 'function' being used gives SUFFICIENT conditions, but not NECESSARY conditions.

Could not the problem be resolved by appending something like:
for all b if there exists an a such that f(a) = b then a is an element of the domain of f
?

[Dan Christensen]

On Tuesday, April 5, 2022 at 5:28:49 PM UTC-4, FredJeffries wrote:

> The problem seems to me to be that the 'definition' of 'function' being used gives SUFFICIENT conditions, but not NECESSARY conditions.
>

Don't know it this is what you are looking for, but I was able to prove: Given any sets X and Y, there exists a function f: X --> Y if and only if there exists a graph set mapping X to Y.

ALL(x):ALL(y):[Set(x) & Set(y)

=> [EXIST(f):ALL(a):[a in x => f(a) in y] (There exists f: x --> y)

<=> EXIST(g):[Set'(g) (There exists a graph set g)

& ALL(a):ALL(b):[(a,b) in g => a in x & b in y]

& ALL(a):[a in x => EXIST(b):[b in y & (a,b) in g]]

& ALL(a):ALL(b):ALL(c):[a in x & b in y & c in y => [(a,b) in g & (a,c) in g => b=c]]]]]

https://dcproof.com/FunctionIffGraphSet.htm (109 lines)

[FredJeffries]

On Tuesday, April 5, 2022 at 9:14:24 PM UTC-7, Dan Christensen wrote:
> On Tuesday, April 5, 2022 at 5:28:49 PM UTC-4, FredJeffries wrote:
>
> > The problem seems to me to be that the 'definition' of 'function' being used gives SUFFICIENT conditions, but not NECESSARY conditions.
> >
> Don't know it this is what you are looking for, but I was able to prove: Given any sets X and Y, there exists a function f: X --> Y if and only if there exists a graph set mapping X to Y.
>
> ALL(x):ALL(y):[Set(x) & Set(y)
>
> => [EXIST(f):ALL(a):[a in x => f(a) in y] (There exists f: x --> y)
>
> <=> EXIST(g):[Set'(g) (There exists a graph set g)
>
> & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
>
> & ALL(a):[a in x => EXIST(b):[b in y & (a,b) in g]]
>
> & ALL(a):ALL(b):ALL(c):[a in x & b in y & c in y => [(a,b) in g & (a,c) in g => b=c]]]]]

You are merely repeating the same error: You are saying what happens when you apply f to something that is in its 'domain'. But you nowhere REQUIRE that the something MUST be in the 'domain' in order to apply f to it.

Hence my suggestion (which you snipped):
<quote>

The problem seems to me to be that the 'definition' of 'function' being used gives SUFFICIENT conditions, but not NECESSARY conditions.

Could not the problem be resolved by appending something like:
for all b if there exists an a such that f(a) = b then a is an element of the domain of f

</quote>

[Dan Christensen]

On Friday, April 8, 2022 at 12:39:55 PM UTC-4, FredJeffries wrote:
> On Tuesday, April 5, 2022 at 9:14:24 PM UTC-7, Dan Christensen wrote:
> > On Tuesday, April 5, 2022 at 5:28:49 PM UTC-4, FredJeffries wrote:
> >
> > > The problem seems to me to be that the 'definition' of 'function' being used gives SUFFICIENT conditions, but not NECESSARY conditions.
> > >
> > Don't know it this is what you are looking for, but I was able to prove: Given any sets X and Y, there exists a function f: X --> Y if and only if there exists a graph set mapping X to Y.
> >
> > ALL(x):ALL(y):[Set(x) & Set(y)
> >
> > => [EXIST(f):ALL(a):[a in x => f(a) in y] (There exists f: x --> y)
> >
> > <=> EXIST(g):[Set'(g) (There exists a graph set g)
> >
> > & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
> >
> > & ALL(a):[a in x => EXIST(b):[b in y & (a,b) in g]]
> >
> > & ALL(a):ALL(b):ALL(c):[a in x & b in y & c in y => [(a,b) in g & (a,c) in g => b=c]]]]]

> You are merely repeating the same error: You are saying what happens when you apply f to something that is in its 'domain'. But you nowhere REQUIRE that the something MUST be in the 'domain' in order to apply f to it.
>

Not sure what you are getting at. The statement ALL(a):[a in x => f(a) in y] can only be applied for elements of the function's domain x.

> Hence my suggestion (which you snipped):
> <quote>
> The problem seems to me to be that the 'definition' of 'function' being used gives SUFFICIENT conditions, but not NECESSARY conditions.

Doesn't seem like a problem to me.

> Could not the problem be resolved by appending something like:
> for all b if there exists an a such that f(a) = b then a is an element of the domain of f

Can you give a concrete example of what you are talking about.

[FredJeffries]

On Friday, April 8, 2022 at 11:35:30 AM UTC-7, Dan Christensen wrote:
> On Friday, April 8, 2022 at 12:39:55 PM UTC-4, FredJeffries wrote:
> > On Tuesday, April 5, 2022 at 9:14:24 PM UTC-7, Dan Christensen wrote:
> > > On Tuesday, April 5, 2022 at 5:28:49 PM UTC-4, FredJeffries wrote:
> > >
> > > > The problem seems to me to be that the 'definition' of 'function' being used gives SUFFICIENT conditions, but not NECESSARY conditions.
> > > >
> > > Don't know it this is what you are looking for, but I was able to prove: Given any sets X and Y, there exists a function f: X --> Y if and only if there exists a graph set mapping X to Y.
> > >
> > > ALL(x):ALL(y):[Set(x) & Set(y)
> > >
> > > => [EXIST(f):ALL(a):[a in x => f(a) in y] (There exists f: x --> y)
> > >
> > > <=> EXIST(g):[Set'(g) (There exists a graph set g)
> > >
> > > & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
> > >
> > > & ALL(a):[a in x => EXIST(b):[b in y & (a,b) in g]]
> > >
> > > & ALL(a):ALL(b):ALL(c):[a in x & b in y & c in y => [(a,b) in g & (a,c) in g => b=c]]]]]
>
> > You are merely repeating the same error: You are saying what happens when you apply f to something that is in its 'domain'. But you nowhere REQUIRE that the something MUST be in the 'domain' in order to apply f to it.
> >
> Not sure what you are getting at. The statement ALL(a):[a in x => f(a) in y] can only be applied for elements of the function's domain x.

Which of your axioms or definitions says that?

[Dan Christensen]

You simply won't be able to apply the statement ALL(a):[a in x => f(a) in y] to infer anything about f for elements not in x.

[FredJeffries]

Concrete examples:

domain of f is {0}
codomain of f is (0)
f(0) = 0
f(1) = 0

domain of g is {0}
codomain of g is {0}
g(0) = 0
g(1) = 1

domain of h is {0}
codomain of h is {0}
h(0) = 0
h(1) = -42

...

[FredJeffries]

'You simply won't be able to' is not a valid logical principle.

Take your own medicine. Give a FORMAL PROOF, using your own previously stated definitions, axioms, and logical principles.

[Mostowski Collapse]

Yet another thing Dan-O-Matik doesn't understand,
namely that the counter examples don't need anything
outside of x. If you take the counter example:

f(0)=0
g(0)=0
f(-1)=-1
g(-1)=1

And if we plug into your axiom:

dom = {0}
cod = {0}

And then prove from your axiom:

f=g

Nothing outside of x is needed. Your axiom will only look at
f(0)=0 and g(0)=0 because we have plugged into the axiom dom={0}
and cod={0}. If we then plug into your axiom:

dom={0,-1}
cod={0,-1,1}

And then prove from your axiom:

~f=g

Nothing outside of x is needed. Your axiom will now look at
f(0)=0, g(0)=0, f(-1)=-1 and g(-1)=1. because we have plugged
into the axiom dom={0,-1} and cod={0,-1,1}.

Your obsession with outside x is complete nuts.

[Ward Matsushita]

Mostowski Collapse wrote:

> Yet another thing Dan-O-Matik doesn't understand,
> namely that the counter examples don't need anything outside of x. If
> you take the counter example:
>
> f(0)=0 g(0)=0 f(-1)=-1 g(-1)=1
>
> And if we plug into your axiom:

🏄‍♀️🌊 you are both stupid. "vaccines" comes from the latin "vaca", which is
"cow" in english.🌊🏄‍♀️

[Dan Christensen]

Nothing useful here...

> domain of f is {0}
> codomain of f is (0)
> f(0) = 0

> f(1) = 0 <--- Contradicts the fact that he domain is {0}.

>
> domain of g is {0}
> codomain of g is {0}
> g(0) = 0

> g(1) = 1 <--- Also contradicts the fact the codomain is { 0 }

>
> domain of h is {0}
> codomain of h is {0}
> h(0) = 0
> h(1) = -42

Do you even understand what domains and codomains of functions are, Jan Burse? Apparently not. Oh, well...

[Dan Christensen]

It works for me. AFAIK it works for most mathematicians as well.

>
> Take your own medicine. Give a FORMAL PROOF, using your own previously stated definitions, axioms, and logical principles.

Gladly, but proof of what exactly? What theorem should I prove (stated on the language of set theory)?

[FredJeffries]

> Do you even understand what domains and codomains of functions are?

We're not talking about domains and codomains of functions in mathematical practice.

We're talking about YOUR 'definitions'. It is YOUR OWN, published 'definitions' that allows these (seeming) sillies.

Give a FORMAL PROOF that these three 'functions' violate YOUR definitions, axioms, logical methods. No appealing to Terrence Tao. No appealing to 'You simply won't be able to'. Just YOUR own tools.

[FredJeffries]

Prove that You simply won't be able to apply the statement ALL(a):[a in x => f(a) in y] to infer anything about f for elements not in x.

Or prove my suggestion for amending your 'definition' (since you think it is unnecessary, it must be provable):

[Dan Christensen]

On Saturday, April 9, 2022 at 11:10:19 AM UTC-4, FredJeffries wrote:

> Prove that You simply won't be able to apply the statement ALL(a):[a in x => f(a) in y] to infer anything about f for elements not in x.
>

Suppose z not in x. We can specify: z in x => f(z) in y.

What can you infer about the truth value of the consequent 'f(z) in y' knowing the antecedent is false. Nothing.

[Mostowski Collapse]

Its not needed for the counter example to your axiom 1.

[Dan Christensen]

On Saturday, April 9, 2022 at 12:33:20 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Samstag, 9. April 2022 um 18:11:53 UTC+2:
> > On Saturday, April 9, 2022 at 11:10:19 AM UTC-4, FredJeffries wrote:
> >
> > > Prove that You simply won't be able to apply the statement ALL(a):[a in x => f(a) in y] to infer anything about f for elements not in x.
> > >
> > Suppose z not in x. We can specify: z in x => f(z) in y.
> >
> > What can you infer about the truth value of the consequent 'f(z) in y' knowing the antecedent is false. Nothing.

> Its not needed for the counter example to your axiom 1.

Pay attention, Jan Burse. Here, we are talking about: ALL(a):[a in x => f(a) in y]

[Mostowski Collapse]

You sure have your blonde moments all the time.
Seems to be a constant state of your psychosis.

The value f(a) for an argument ~(a e x) is not
needed for the counter example to your axiom 1:

1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) &
ALL(a):[a e dom => f(a) e cod] &
ALL(a):[a e dom => g(a) e cod]
=> [f=g <=> ALL(a):[a e dom => f(a)=g(a)]]]
Axiom
https://dcproof.com/EmptyFunctionsUniqueV3.htm

The truth value of these subformulas:

ALL(a):[a e dom => f(a) e cod]
ALL(a):[a e dom => g(a) e cod]
ALL(a):[a e dom => f(a)=g(a)]

Is all only dependent of values f(a)
for an argument (a e dom). Valuse f(a)
for an argument ~(a e dom) are totally

irrelevant. Nevertheless we can derive
f=g & ~f=g for:

f(null)=null
g(null)=one

Do you deny that?

Dan Christensen schrieb:

[Dan Christensen]

On Saturday, April 9, 2022 at 12:55:21 PM UTC-4, Mostowski Collapse wrote:
> You sure have your blonde moments all the time.
> Seems to be a constant state of your psychosis.
>
> The value f(a) for an argument ~(a e x) is not
> needed for the counter example to your axiom 1:
>
> 1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) &
> ALL(a):[a e dom => f(a) e cod] &
> ALL(a):[a e dom => g(a) e cod]
> => [f=g <=> ALL(a):[a e dom => f(a)=g(a)]]]
> Axiom
> https://dcproof.com/EmptyFunctionsUniqueV3.htm
>
> The truth value of these subformulas:
>
> ALL(a):[a e dom => f(a) e cod]
> ALL(a):[a e dom => g(a) e cod]
> ALL(a):[a e dom => f(a)=g(a)]
>
> Is all only dependent of values f(a)
> for an argument (a e dom). Valuse f(a)
> for an argument ~(a e dom) are totally
>
> irrelevant. Nevertheless we can derive
> f=g & ~f=g for:
>
> f(null)=null
> g(null)=one
>

Again, you will need to specify values for the bound variables dom, com, f and g in the definition. What seems to be the problem?

[Mostowski Collapse]

Corr.:

Is all only dependent of values f(a) and g(a)
for an argument (a e dom). Values f(a) or g(a)

for an argument ~(a e dom) are totally irrelevant

Your outside value and dark value talk is only
a decoy. Either you to this consciously, divert
the attention from the counter example to some

other nonsense, or you are indeed that stupid,
a formula analphabeth like culio, that cannot
read his own axiom 1. In either case its a total

shame that you post your nonsense on sci.logic and sci.math.

Dan Christensen schrieb:

[Mostowski Collapse]

Dan-O-Matik even doesn't pretend to not be the idiot he is:

> Again, you will need to specify values for the bound variables dom,
> com, f and g in the definition. What seems to be the problem?

There are nor "the bound" variables you Ultra Moron.
If you have an axiom like:

ALL(_):ALL(_): ....

You can use U Spec with whatever seems fit. You can
also use U Spec multiple times with the same Axiom.
The functions f and g, I gave them already:

f(null)=null
g(null)=one

Its extremly trivial to derive f=g and ~f=g. I will
not do your homework. You need to learn

something, otherwise you post the same nonsense
here for the next 10 years.

Mostowski Collapse schrieb:

[Dan Christensen]

On Saturday, April 9, 2022 at 1:04:31 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> Dan-O-Matik even doesn't pretend to not be the idiot he is:

> >>> The value f(a) for an argument ~(a e x) is not
> >>> needed for the counter example to your axiom 1:
> >>>
> >>> 1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) &
> >>> ALL(a):[a e dom => f(a) e cod] &
> >>> ALL(a):[a e dom => g(a) e cod]
> >>> => [f=g <=> ALL(a):[a e dom => f(a)=g(a)]]]
> >>> Axiom
> >>> https://dcproof.com/EmptyFunctionsUniqueV3.htm
> >>>
> >>> The truth value of these subformulas:
> >>>
> >>> ALL(a):[a e dom => f(a) e cod]
> >>> ALL(a):[a e dom => g(a) e cod]
> >>> ALL(a):[a e dom => f(a)=g(a)]
> >>>
> >>> Is all only dependent of values f(a)
> >>> for an argument (a e dom). Valuse f(a)
> >>> for an argument ~(a e dom) are totally
> >>>
> >>> irrelevant. Nevertheless we can derive
> >>> f=g & ~f=g for:
> >>>
> >>> f(null)=null
> >>> g(null)=one
> >>>
> >>
> >> Again, you will need to specify values for the bound variables dom,
> >> com, f and g in the definition. What seems to be the problem?
> >>

> > Again, you will need to specify values for the bound variables dom,
> > com, f and g in the definition. What seems to be the problem?
> There are nor "the bound" variables you Ultra Moron.
> If you have an axiom like:
>
> ALL(_):ALL(_): ....
>
> You can use U Spec with whatever seems fit.

I will try to make this easier for you, Jan Burse.

Simply fill in the blanks with what symbols you want and let's see where it takes us:

dom = _____*
cod = _____*
f = _____*
g = _____*

* required data to proceed

> You can
> also use U Spec multiple times with the same Axiom.
> The functions f and g, I gave them already:
>
> f(null)=null
> g(null)=one
>

Just fill in the blanks, Jan Burse.

> Its extremly trivial to derive f=g and ~f=g. I will
> not do your homework.

Ah, a tacit admission of defeat! OK.

[Mostowski Collapse]

You are still the moron like you are always the moron that you are.

I already wrote:

> The functions f and g, I gave them already:
>
> f(null)=null
> g(null)=one

Then I gave you the following hint, since you seem to be too

stupid. I wrote:

"You can also use U Spec multiple times with the same Axiom"

So why should I fill out a form that has only one dom/cod pair?
You are extremly annoyingly stupid crazy idiot.

[Mostowski Collapse]

You can use U Spec multiple times, and then
use your Join inference step that you have in
DC Proof, and then derive:

f=g & ~f=g

In a normal logic student class, you would have long
already failed the student class, an F- mark. But
since we are very patient with idiots like you,

I will keep giving hints.

Mostowski Collapse schrieb:

[Mostowski Collapse]

Here you see an example of using U Spec
multiple times. Its strange that I have to
explain you your DC poop tool.

1 f=f
Axiom

2 g=g
Axiom

3 ALL(x):x=z
Axiom

4 f=z
U Spec, 3

5 g=z
U Spec, 3

6 g=f
Substitute, 4, 5


Mostowski Collapse schrieb:

[Dan Christensen]

On Saturday, April 9, 2022 at 2:48:27 PM UTC-4, Mostowski Collapse wrote:

> Mostowski Collapse schrieb:
> > You are still the moron like you are always the moron that you are.
> > I already wrote:
> >
> >> The functions f and g, I gave them already:
> >>
> >> f(null)=null
> >> g(null)=one
> >
> > Then I gave you the following hint, since you seem to be too
> > stupid. I wrote:
> >
> > "You can also use U Spec multiple times with the same Axiom"
> >
> > So why should I fill out a form that has only one dom/cod pair?
> > You are extremly annoyingly stupid crazy idiot.
> >
> >
> > Dan Christensen schrieb am Samstag, 9. April 2022 um 19:33:04 UTC+2:
> >> dom = _____*
> >> cod = _____*
> >> f = _____*
> >> g = _____*

> You can use U Spec multiple times,

Yup. 4 times in this case, for 2 sets and 2 functions.

> and then
> use your Join inference step that you have in
> DC Proof, and then derive:
>
> f=g & ~f=g
>

Now, there's the tricky part, Jan Burse. Why don't you show readers how it's done? NO??? Not today??? Too busy making money? Oh, well.... (Hee, hee!)

[Mostowski Collapse]

Your case is not my case. My case is a counter example,
which derives:

f=g & ~f=g

For such a counter example, you need to apply U Spec
more than only 4 times.

Good Luck! We are waiting...

[Mostowski Collapse]

Now I gave you again a hint, which you couldn't figure
out by yourself. Asked too much of logic from poor
Dan-O-Matik? Now to answer your question:

> Why don't you show readers how it's done?

You have to solve the homework by yourself,
because you need to learn something, otherwise
you continue posting your DC poop nonsense here

on sci.math and sci.logic for the next 10 years,
judging from the bone head you are...

LMAO!

[Dan Christensen]

> Your case is not my case. My case is a counter example,
> which derives:
>
> f=g & ~f=g
>

Only in the Jan Burse Math Fantasyland. Alas, not in the real world.

> For such a counter example, you need to apply U Spec
> more than only 4 times.
>

HA, HA, HA!!!

[Mostowski Collapse]

So you give up, making your homework. You
know what this means, F- in logic class.

I give a solution, if you state here that you
are not able to derive trivial proof.

LoL

[Mostowski Collapse]

Ok, here is the first part, its called idiot.html.
Its the proof of f=g. Do you want me to post also
idiot2.html, the proof of ~f=g, for the same functions

f(null)=null
g(null)=one

, or can you do it by yourself?


1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a ε dom
=> f(a) ε dom] & ALL(a):[a ε dom => g(a) ε dom] => [f=g <=> ALL(a):[a ε
dom => f(a)=g(a)]]]
Axiom

2 Set(null)
Axiom

3 ALL(a):~a ε null
Axiom

4 f(null)=null
Axiom

5 g(null)=one
Axiom

6 ~ALL(a):[a ε null => f(a) ε null]
Premise

7 ~~EXIST(a):~[a ε null => f(a) ε null]
Quant, 6

8 EXIST(a):~[a ε null => f(a) ε null]
Rem DNeg, 7

9 ~[b ε null => f(b) ε null]
E Spec, 8

10 ~~[b ε null & ~f(b) ε null]
Imply-And, 9

11 b ε null & ~f(b) ε null
Rem DNeg, 10

12 ~b ε null
U Spec, 3

13 b ε null
Split, 11

14 ~f(b) ε null
Split, 11

15 ~b ε null & b ε null
Join, 12, 13

16 ~~ALL(a):[a ε null => f(a) ε null]
Conclusion, 6

17 ALL(a):[a ε null => f(a) ε null]
Rem DNeg, 16

18 ~ALL(a):[a ε null => g(a) ε null]
Premise

19 ~~EXIST(a):~[a ε null => g(a) ε null]
Quant, 18

20 EXIST(a):~[a ε null => g(a) ε null]
Rem DNeg, 19

21 ~[c ε null => g(c) ε null]
E Spec, 20

22 ~~[c ε null & ~g(c) ε null]
Imply-And, 21

23 c ε null & ~g(c) ε null
Rem DNeg, 22

24 ~c ε null
U Spec, 3

25 c ε null
Split, 23

26 ~g(c) ε null
Split, 23

27 ~c ε null & c ε null
Join, 24, 25

28 ~~ALL(a):[a ε null => g(a) ε null]
Conclusion, 18

29 ALL(a):[a ε null => g(a) ε null]
Rem DNeg, 28

30 Set(null) & Set(null)
Join, 2, 2

31 Set(null) & Set(null)
& ALL(a):[a ε null => f(a) ε null]
Join, 30, 17

32 Set(null) & Set(null)
& ALL(a):[a ε null => f(a) ε null]
& ALL(a):[a ε null => g(a) ε null]
Join, 31, 29

33 ALL(cod):ALL(f):ALL(g):[Set(null) & Set(cod) & ALL(a):[a ε null =>
f(a) ε null] & ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε
null => f(a)=g(a)]]]
U Spec, 1

34 ALL(f):ALL(g):[Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε
null] & ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null =>
f(a)=g(a)]]]
U Spec, 33

35 ALL(g):[Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε null] &
ALL(a):[a ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null =>
f(a)=g(a)]]]
U Spec, 34

36 Set(null) & Set(null) & ALL(a):[a ε null => f(a) ε null] & ALL(a):[a
ε null => g(a) ε null] => [f=g <=> ALL(a):[a ε null => f(a)=g(a)]]
U Spec, 35

37 f=g <=> ALL(a):[a ε null => f(a)=g(a)]
Detach, 36, 32

38 ~ALL(a):[a ε null => f(a)=g(a)]
Premise

39 ~~EXIST(a):~[a ε null => f(a)=g(a)]
Quant, 38

40 EXIST(a):~[a ε null => f(a)=g(a)]
Rem DNeg, 39

41 ~[d ε null => f(d)=g(d)]
E Spec, 40

42 ~~[d ε null & ~f(d)=g(d)]
Imply-And, 41

43 d ε null & ~f(d)=g(d)
Rem DNeg, 42

44 ~d ε null
U Spec, 3

45 d ε null
Split, 43

46 ~f(d)=g(d)
Split, 43

47 ~d ε null & d ε null
Join, 44, 45

48 ~~ALL(a):[a ε null => f(a)=g(a)]
Conclusion, 38

49 ALL(a):[a ε null => f(a)=g(a)]
Rem DNeg, 48

50 [f=g => ALL(a):[a ε null => f(a)=g(a)]]
& [ALL(a):[a ε null => f(a)=g(a)] => f=g]
Iff-And, 37

51 f=g => ALL(a):[a ε null => f(a)=g(a)]
Split, 50

52 ALL(a):[a ε null => f(a)=g(a)] => f=g
Split, 50

53 f=g
Detach, 52, 49

Mostowski Collapse schrieb:

[Dan Christensen]

A valiant effort!

To prove ~f=g, however, you must prove: EXIST(a):[a in null & ~f(a)=g(a)]

Impossible.

[Mostowski Collapse]

Thats your fallacy. I can use U Spec with another
domain. When will you learn? Do you really want
me to publish idiot2.html, or could you maybe

save us from such an embarrassment?

I already wrote:

Mostowski Collapse schrieb am Samstag, 9. April 2022 um 21:59:37 UTC+2:
> Your case is not my case. My case is a counter example,
> which derives:
>
> f=g & ~f=g
>

> For such a counter example, you need to apply U Spec
> more than only 4 times.
>

> Good Luck! We are waiting...

https://groups.google.com/g/sci.math/c/on3M3w_8t6Q/m/ahvG9MF1BQAJ

I wrote:

YOU NEED TO APPLY U SPEC MORE THAN ONLY 4 TIMES

[Mostowski Collapse]

I mean, you cannot say that I didn't warn you. I tried everything
to explain you how ALL(_) works, but you seem to be
infinitely stubborn. Repeating the same fallacy again and

again, and diverting into some outside domain nonsense.
Whereby on the other hand I warned you and showed you
how simple the quest is:

Mostowski Collapse schrieb am Samstag, 9. April 2022 um 20:55:44 UTC+2:
> Here you see an example of using U Spec
> multiple times. Its strange that I have to
> explain you your DC poop tool.
>
> 1 f=f
> Axiom
>
> 2 g=g
> Axiom
>
> 3 ALL(x):x=z
> Axiom
>
> 4 f=z
> U Spec, 3
>
> 5 g=z
> U Spec, 3
>
> 6 g=f
> Substitute, 4, 5
>

> The rest of proving f=g & ~f=g from your Axiom 1
> for the f and g I gave is a walk in the park.
>
> It surely not a walk on the moon.
https://groups.google.com/g/sci.logic/c/CXzwX-hyWj0/m/RYDiKMjwCAAJ

But once a bone head, always a bone head. You really
want to force me to show you idiot2.html as well?

[Mostowski Collapse]

Here is a file domex.html, that shows as an example how you
can prove some ALL(a):[a e dom => f(a) e cod], without
having it as an axiom:

1 f(null)=null
Axiom

2 ALL(a):[a ε one <=> a=null]
Axiom

3 ~ALL(a):[a ε one => f(a) ε one]
Premise

4 ~~EXIST(a):~[a ε one => f(a) ε one]
Quant, 3

5 EXIST(a):~[a ε one => f(a) ε one]
Rem DNeg, 4

6 ~[b ε one => f(b) ε one]
E Spec, 5

7 ~~[b ε one & ~f(b) ε one]
Imply-And, 6

8 b ε one & ~f(b) ε one
Rem DNeg, 7

9 b ε one <=> b=null
U Spec, 2

10 [b ε one => b=null] & [b=null => b ε one]
Iff-And, 9

11 b ε one => b=null
Split, 10

12 b=null => b ε one
Split, 10

13 b ε one
Split, 8

14 ~f(b) ε one
Split, 8

15 b=null
Detach, 11, 13

16 ~f(null) ε one
Substitute, 15, 14

17 ~null ε one
Substitute, 1, 16

18 null ε one <=> null=null
U Spec, 2

19 [null ε one => null=null] & [null=null => null ε one]
Iff-And, 18

20 null ε one => null=null
Split, 19

21 null=null => null ε one
Split, 19

22 null=null
Reflex

23 null ε one
Detach, 21, 22

24 ~null ε one & null ε one
Join, 17, 23

25 ~~ALL(a):[a ε one => f(a) ε one]
Conclusion, 3

26 ALL(a):[a ε one => f(a) ε one]
Rem DNeg, 25

Hope this helps...

[Dan Christensen]

On Saturday, April 9, 2022 at 6:33:56 PM UTC-4, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Samstag, 9. April 2022 um 21:59:37 UTC+2:
> > Your case is not my case. My case is a counter example,
> > which derives:
> >
> > f=g & ~f=g
> >
> > For such a counter example, you need to apply U Spec
> > more than only 4 times.
> >
> > Good Luck! We are waiting...
> https://groups.google.com/g/sci.math/c/on3M3w_8t6Q/m/ahvG9MF1BQAJ
>
> I wrote:
>
> YOU NEED TO APPLY U SPEC MORE THAN ONLY 4 TIMES
> Dan Christensen schrieb am Sonntag, 10. April 2022 um 00:29:37 UTC+2:
> > A valiant effort!
> >
> > To prove ~f=g, however, you must prove: EXIST(a):[a in null & ~f(a)=g(a)]
> >
> > Impossible.

> Thats your fallacy.

I guess you haven't fully learned your lesson yet, but you seem to be getting there. Keep at it!

[Mostowski Collapse]

For the counter example, where we already proved
in the file idiot.html that f=g:

f(null)=null
g(null)=one

In a a file idiot2.html, you only need to set one={null}
and two={null,one} and then prove:

ALL(a):[a e one => f(a) e two]
ALL(a):[a e one => g(a) e two]
~ALL(a):[a e one => f(a)=g(a)]

You then get ~f=g. Joining you get f=g & ~f=g.
We are waiting Dan-O-Matik. Too difficult for DC poop?