What if I had defined g(x) as follows:

g(x) = 1 / (|x| / x)

Can you show:

g(x) = f'(x) where f(x) = |x|

LoL

Mostowski Collapse schrieb am Donnerstag, 10. Februar 2022 um 21:11:22 UTC+1:
> I mean why can I not prove in DC poop:
>
> g(0) - g(0) ≠ 0
>
> Highschool math will tell me, when g(0)
> is undefined, then undefined - undefined is
> undefined and undefined is not zero.
> Dan Christensen schrieb am Donnerstag, 10. Februar 2022 um 21:01:43 UTC+1:
> > On Thursday, February 10, 2022 at 2:53:29 PM UTC-5, Mostowski Collapse wrote:
> > > And why can I prove in DC poop:
> > >
> > > g(0) - g(0) = 0
> > >
> > Let's see your proof.
> >
> > Dan

On Thursday, February 10, 2022 at 3:11:22 PM UTC-5, Mostowski Collapse wrote:
> I mean why can I not prove in DC poop:
>
> g(0) - g(0) ≠ 0
>
> Highschool math will tell me, when g(0)
> is undefined, then undefined - undefined is
> undefined and undefined is not zero.

You mean, you have something like:

1. 0 in n
Axiom

2. ALL(a):ALL(b):ALL(c):[a in n & b in n & c in n => [a-b=c <=> a=c+b]]
Axiom

3. ALL(a):[a in n & ~a=0 => g(a) in n]
Axiom

4. 0 in n & ~0=0 => g(0) in n
U Spec, 3

And you want to specify a=g(0), b=g(0), and c=0 in (2)?

The trouble is, you won't be able to prove that g(0) in n. As such, g(0) is undefined and you won't be able to apply (2).

Dan

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

You dont need ZFC for Highschool mathematics.
All that is needed is:

0 ≠ 1

Then by Russells Definite Descriptions, this
here is provable:

~∃z /(0,0,z)

Dan Christensen schrieb am Donnerstag, 10. Februar 2022 um 21:56:56 UTC+1:
> On Thursday, February 10, 2022 at 3:11:22 PM UTC-5, Mostowski Collapse wrote:
> > I mean why can I not prove in DC poop:
> >
> > g(0) - g(0) ≠ 0
> >
> > Highschool math will tell me, when g(0)
> > is undefined, then undefined - undefined is
> > undefined and undefined is not zero.
> You mean, you have something like:
>
> 1. 0 in n
> Axiom
>
> 2. ALL(a):ALL(b):ALL(c):[a in n & b in n & c in n => [a-b=c <=> a=c+b]]
> Axiom
>
> 3. ALL(a):[a in n & ~a=0 => g(a) in n]
> Axiom
>
> 4. 0 in n & ~0=0 => g(0) in n
> U Spec, 3
>
> And you want to specify a=g(0), b=g(0), and c=0 in (2)?
>
> The trouble is, you won't be able to prove that g(0) in n. As such, g(0) is undefined and you won't be able to apply (2).
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Friday, February 11, 2022 at 2:23:40 AM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Donnerstag, 10. Februar 2022 um 21:56:56 UTC+1:
> > On Thursday, February 10, 2022 at 3:11:22 PM UTC-5, Mostowski Collapse wrote:
> > > I mean why can I not prove in DC poop:
> > >
> > > g(0) - g(0) ≠ 0
> > >
> > > Highschool math will tell me, when g(0)
> > > is undefined, then undefined - undefined is
> > > undefined and undefined is not zero.
> > You mean, you have something like:
> >
> > 1. 0 in n
> > Axiom
> >
> > 2. ALL(a):ALL(b):ALL(c):[a in n & b in n & c in n => [a-b=c <=> a=c+b]]
> > Axiom
> >
> > 3. ALL(a):[a in n & ~a=0 => g(a) in n]
> > Axiom
> >
> > 4. 0 in n & ~0=0 => g(0) in n
> > U Spec, 3
> >
> > And you want to specify a=g(0), b=g(0), and c=0 in (2)?
> >
> > The trouble is, you won't be able to prove that g(0) in n. As such, g(0) is undefined and you won't be able to apply (2).

> You dont need ZFC for Highschool mathematics.

Huh???

> All that is needed is:
>
> 0 ≠ 1
>
> Then by Russells Definite Descriptions, this
> here is provable:
>
> ~∃z /(0,0,z)

Utter nonsense! Get back to us when you sober up, Jan Burse.

Dan

On Friday, February 11, 2022 at 2:23:40 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 10. Februar 2022 um 21:56:56 UTC+1:
> > On Thursday, February 10, 2022 at 3:11:22 PM UTC-5, Mostowski Collapse wrote:
> > > I mean why can I not prove in DC poop:
> > >
> > > g(0) - g(0) ≠ 0
> > >
> > > Highschool math will tell me, when g(0)
> > > is undefined, then undefined - undefined is
> > > undefined and undefined is not zero.
> > You mean, you have something like:
> >
> > 1. 0 in n
> > Axiom
> >
> > 2. ALL(a):ALL(b):ALL(c):[a in n & b in n & c in n => [a-b=c <=> a=c+b]]
> > Axiom
> >
> > 3. ALL(a):[a in n & ~a=0 => g(a) in n]
> > Axiom
> >
> > 4. 0 in n & ~0=0 => g(0) in n
> > U Spec, 3
> >
> > And you want to specify a=g(0), b=g(0), and c=0 in (2)?
> >
> > The trouble is, you won't be able to prove that g(0) in n. As such, g(0) is undefined and you won't be able to apply (2).

> You dont need ZFC for Highschool mathematics.
> All that is needed is:
>
> 0 ≠ 1
>
> Then by Russells Definite Descriptions, this
> here is provable:
>
> ~∃z /(0,0,z)

Utter nonsense. Guessing at what you MIGHT be getting at, consider the following proof:

1. 0 in n
Axiom

2. 1 in n
Axiom

3. ~1=0
Axiom

Define: f

4. ALL(a):[a in n => f(a) in n]
Axiom

5. f(0)=1
Axiom

Define: g

6. ALL(a):[a in n & ~a=0 => g(a) in n]
Axiom

7. g(1)=0
Axiom

8. f(g(1))=1
Substitute, 7, 5

9. ~f(g(1))=0
Substitute, 8, 3

Suppose...

10. x in n & ~x=0
Premise

11. x in n & ~x=0 => g(x) in n
U Spec, 6

12. g(x) in n
Detach, 11, 10

13. g(x) in n => f(g(x)) in n
U Spec, 4, 12

14. f(g(x)) in n
Detach, 13, 12

Define: f(g(a))

15. ALL(a):[a in n & ~a=0 => f(g(a)) in n]
Conclusion, 10

Specifying a=0, we see from the definition of f(g(a)) that f(g(0)) is undefined since ~0=0 is always false:

16. 0 in n & ~0=0 => f(g(0)) in n
U Spec, 15

Dan

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

About sober, what does ~0=0 mean? Isn't this
false? So that the implication is vacously true?

And why did you prove something with f o g?
I mentioned 0=\=1 because of zero divided by zero.

Dan Christensen schrieb am Freitag, 11. Februar 2022 um 22:25:27 UTC+1:
> 16. 0 in n & ~0=0 => f(g(0)) in n
> U Spec, 15

On Friday, February 11, 2022 at 6:59:16 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 11. Februar 2022 um 22:25:27 UTC+1:
> > 16. 0 in n & ~0=0 => f(g(0)) in n
> > U Spec, 15

> About sober, what does ~0=0 mean?

It means 0 is not equal to 0.

> Isn't this
> false?

If 0 is found in an active statement in a proof, then you can infer that 0=0.

> So that the implication is vacously true?

Once you have 0=0, you can prove ~0=0 => P for any proposition P. Of course, you won't be able to infer that P is true because the antecedent is false, but the implication ~0=0 => P would itself be true (vacuously so).

>
> And why did you prove something with f o g?

I thought you MIGHT find it useful as a simple example.

> I mentioned 0=\=1 because of zero divided by zero.

This makes no sense. Forget it.

Dan

(Correction)

On Friday, February 11, 2022 at 6:59:16 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 11. Februar 2022 um 22:25:27 UTC+1:
> > 16. 0 in n & ~0=0 => f(g(0)) in n
> > U Spec, 15

> About sober, what does ~0=0 mean? Isn't this
> false?

Yes. And since the antecedent is false, we cannot infer that f(g(0)) in n is true, or that it is false. In this case, f(g(0)) in n is simply UNDEFINED..

Here is the truth table for A=>B:

A B A=>B
T T T
T F F
F T T <---
F F T <---

Notice that, from lines 3 and 4, the antecedent A is false, but the implication A=>B is true, and that the consequent B could be EITHER true (line 3) OR false (line 4).

> So that the implication is vacously true?
>

Yes, but we cannot use to infer the truth value of the consequent. (See truth table above)

> And why did you prove something with f o g?

I thought it was a simpler example that would help you understand.

It seem to me that your example was needlessly complicated by having to introduce the definition of subtraction and the + operator. IIUC you had a function g: N\{0} --> N and a wonky composition of g with subtraction on N, namely f(x) = g(x)-g(x). In your example, f(0) would be undefined since g(0) is undefined.

> I mentioned 0=\=1 because of zero divided by zero.

I needed ~1=0 on line 3 to indicate the existence of at least two distinct elements in n, namely 0 and 1.

Dan

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

Newest low in Dan-O-Matiks logic capabilities.
He doesn't see that Vacuous Truth means that

ALL(a):[a e null => Q]

Is logically equivalent to TRUE, i.e.

P v ~P

He is slower than the Snake Gary in Sponge Bob.

Gary the Snail's Most SAVAGE Moments!
https://www.youtube.com/watch?v=HvBgdUXis5Y

Dan Christensen schrieb am Samstag, 12. Februar 2022 um 06:45:59 UTC+1:
> I am stupid and I know it

On Wednesday, March 30, 2022 at 1:15:52 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> Newest low in Dan-O-Matiks logic capabilities.
> He doesn't see that Vacuous Truth means that
>
> ALL(a):[a e null => Q]
>
> Is logically equivalent to TRUE, i.e.
>
> P v ~P
>

Poor Jan Burse has never been the same since he found out that you can't make inferences about a function outside of its domain. His "dark elements" keep haunting him day and night.

BTW, vacuous truth is easily handled in DC Proof. Poor Jan Burse just can't seem to get the hang of it. Oh, well...

Dan

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

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.

Dan Christensen schrieb am Mittwoch, 30. März 2022 um 19:32:38 UTC+2:
> On Wednesday, March 30, 2022 at 1:15:52 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > Newest low in Dan-O-Matiks logic capabilities.
> > He doesn't see that Vacuous Truth means that
> >
> > ALL(a):[a e null => Q]
> >
> > Is logically equivalent to TRUE, i.e.
> >
> > P v ~P
> >
> Poor Jan Burse has never been the same since he found out that you can't make inferences about a function outside of its domain. His "dark elements" keep haunting him day and night.
>
> BTW, vacuous truth is easily handled in DC Proof. Poor Jan Burse just can't seem to get the hang of it. Oh, well...
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

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

Its then trivial to see that what 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]]]
https://dcproof.com/EmptyFunctionsUniqueV2.htm

Is logical equivalent to:
EXIST(f):[ALL(g):[g=f]]]

But such a Theorem is obviously incorrect. Since there
is more then one function possible in mathematics, for
example the functions sinus sin() and cosinus cos(),

which have sin=\=cos, so your theorem is nonsense.
When you can prove an incorrect theorem in DC poop,
this means DC poop is inconsistent.

Mostowski Collapse schrieb am Mittwoch, 30. März 2022 um 21:08:57 UTC+2:
> 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.
> Dan Christensen schrieb am Mittwoch, 30. März 2022 um 19:32:38 UTC+2:
> > On Wednesday, March 30, 2022 at 1:15:52 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > > Newest low in Dan-O-Matiks logic capabilities.
> > > He doesn't see that Vacuous Truth means that
> > >
> > > ALL(a):[a e null => Q]
> > >
> > > Is logically equivalent to TRUE, i.e.
> > >
> > > P v ~P
> > >
> > Poor Jan Burse has never been the same since he found out that you can't make inferences about a function outside of its domain. His "dark elements" keep haunting him day and night.
> >
> > BTW, vacuous truth is easily handled in DC Proof. Poor Jan Burse just can't seem to get the hang of it. Oh, well...
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

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.
https://www.umsu.de/trees/#%28P~5%28Q~5R%29%29~4%28P~1Q~5R%29

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

Propositional Logic is like Rubiks Cube. Some can do
it very quick, some are not that quick.

Dan-O-Matik on the other hand doesn't master propositional
logic at all, otherwise he would post one nonsense

after the other, without seeing that some of axioms
or axiom schemas are buggy.

Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:05:04 UTC+2:
> 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.
> https://www.umsu.de/trees/#%28P~5%28Q~5R%29%29~4%28P~1Q~5R%29
>
> 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

Corr.:
Dan-O-Matik on the other hand doesn't master propositional
logic at all, otherwise he wouldn't post one nonsense

Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:17:26 UTC+2:
> Propositional Logic is like Rubiks Cube. Some can do
> it very quick, some are not that quick.
>
> Dan-O-Matik on the other hand doesn't master propositional
> logic at all, otherwise he would post one nonsense
>
> after the other, without seeing that some of axioms
> or axiom schemas are buggy.
> Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:05:04 UTC+2:
> > 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.
> > https://www.umsu.de/trees/#%28P~5%28Q~5R%29%29~4%28P~1Q~5R%29
> >
> > 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

So Dan-O-Matik doesn't know this meta rule of replacement,
which can be meta derived in natural deduction(*)?

P <=> Q
--------------------
A(P) <=> A(Q)

This is left as an exercise. Or lookup W. V. Quine Mathematical Logic,
you find this rule also mentioned.

Mathematical Logic Revised Edition W. V. Quine
$40.00 - ISBN 9780674554511 - 11/16/1982 - 364 pages
https://www.hup.harvard.edu/catalog.php?isbn=9780674554511

(*) BTW: it works in any complete calculus, this meta
theorem. Need not be only natural deduction, can be
also another calculus.

Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:18:31 UTC+2:
> Corr.:
> Dan-O-Matik on the other hand doesn't master propositional
> logic at all, otherwise he wouldn't post one nonsense
> Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:17:26 UTC+2:
> > Propositional Logic is like Rubiks Cube. Some can do
> > it very quick, some are not that quick.
> >
> > Dan-O-Matik on the other hand doesn't master propositional
> > logic at all, otherwise he would post one nonsense
> >
> > after the other, without seeing that some of axioms
> > or axiom schemas are buggy.
> > Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:05:04 UTC+2:
> > > 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.
> > > https://www.umsu.de/trees/#%28P~5%28Q~5R%29%29~4%28P~1Q~5R%29
> > >
> > > 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

Here is a proof by induction, over the implicative fragment:

Base Case:
A(P) = P, A(Q) = Q, trivial (P <=> Q) / (P <=> Q)
A(P) = R, A(Q) = R, trivial (P <=> Q) / (R <=> R)

Inductive Step:
A(P) = (A1(P) => A2(P)), A(Q) = (A1(Q) => A2(Q)),
By induction hypothessis we have:
(P <=> Q) / (A1(P) <=> A1(Q))
(P <=> Q) / (A2(P) <=> A2(Q))
All we have to show that we can now create a proof
in the calculus of choice:

A1(P) <=> A1(Q) A2(P) <=> A2(Q)
--------------------------------------------------------------------------
(A1(P) => A2(P)) <=> (A1(Q) => A2(Q))

Which should be possible:

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

Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 19:04:26 UTC+2:
> So Dan-O-Matik doesn't know this meta rule of replacement,
> which can be meta derived in natural deduction(*)?
>
> P <=> Q
> --------------------
> A(P) <=> A(Q)
>
> This is left as an exercise. Or lookup W. V. Quine Mathematical Logic,
> you find this rule also mentioned.
>
> Mathematical Logic Revised Edition W. V. Quine
> $40.00 - ISBN 9780674554511 - 11/16/1982 - 364 pages
> https://www.hup.harvard.edu/catalog.php?isbn=9780674554511
>
> (*) BTW: it works in any complete calculus, this meta
> theorem. Need not be only natural deduction, can be
> also another calculus.
> Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:18:31 UTC+2:
> > Corr.:
> > Dan-O-Matik on the other hand doesn't master propositional
> > logic at all, otherwise he wouldn't post one nonsense
> > Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:17:26 UTC+2:
> > > Propositional Logic is like Rubiks Cube. Some can do
> > > it very quick, some are not that quick.
> > >
> > > Dan-O-Matik on the other hand doesn't master propositional
> > > logic at all, otherwise he would post one nonsense
> > >
> > > after the other, without seeing that some of axioms
> > > or axiom schemas are buggy.
> > > Mostowski Collapse schrieb am Sonntag, 3. April 2022 um 01:05:04 UTC+2:
> > > > 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.
> > > > https://www.umsu.de/trees/#%28P~5%28Q~5R%29%29~4%28P~1Q~5R%29
> > > >
> > > > 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

On Sunday, April 3, 2022 at 1:16:15 PM UTC-4, Mostowski Collapse wrote:
> Here is a proof by induction, over the implicative fragment:
>
> Base Case:
> A(P) = P, A(Q) = Q, trivial (P <=> Q) / (P <=> Q)
> A(P) = R, A(Q) = R, trivial (P <=> Q) / (R <=> R)
>
> Inductive Step:
> A(P) = (A1(P) => A2(P)), A(Q) = (A1(Q) => A2(Q)),
> By induction hypothessis we have:
> (P <=> Q) / (A1(P) <=> A1(Q))
> (P <=> Q) / (A2(P) <=> A2(Q))
> All we have to show that we can now create a proof
> in the calculus of choice:
>
> A1(P) <=> A1(Q) A2(P) <=> A2(Q)
> --------------------------------------------------------------------------
> (A1(P) => A2(P)) <=> (A1(Q) => A2(Q))
>
> Which should be possible:
>
> ((P↔Q) ∧ (R↔S)) → ((P→R) ↔ (Q→S)) is valid.
> https://www.umsu.de/trees/#%28P~4Q%29~1%28R~4S%29~5%28%28P~5R%29~4%28Q~5S%29%29

Pay attention, Jan Burse! Recall that your assignment was to formally prove using some form of natural deduction that:

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) e x] => f1=f2]]
=> ALL(x):[Set(x) =>ALL(f1): ALL(f2):[f1=f2]]

I take it, you were unable to do so. Oh, well...

Dan

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

Hey Uber Moron, you prove the same way like the other
formula. You can even derive a stronger statement,
which shows the full extend of your nonsense claim:

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

Its extremly easy, even my grandmother can do it.

The used rules of replacement are:

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

The used replacement steps are:

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) e x] => f1=f2]]

Apply 1) to get:

ALL(x):[Set(x)
=> EXIST(f):(R∨¬R)
& ALL(f1):ALL(f2):[ALL(a):[a in null => f1(a) in x] & ALL(a):[a in null => f2(a) e x] => f1=f2]]

Apply 1) to get:

ALL(x):[Set(x)
=> EXIST(f):(R∨¬R)
& ALL(f1):ALL(f2):[(R∨¬R) & ALL(a):[a in null => f2(a) e x] => f1=f2]]

Apply 1) to get:

ALL(x):[Set(x)
=> EXIST(f):(R∨¬R)
& ALL(f1):ALL(f2):[(R∨¬R) & (R∨¬R) => f1=f2]]

Apply 2) to get:

ALL(x):[Set(x)
=> EXIST(f):(R∨¬R)
& ALL(f1):ALL(f2):[(R∨¬R) => f1=f2]]

Apply 3) to get:

ALL(x):[Set(x)
=> EXIST(f):(R∨¬R)
& ALL(f1):ALL(f2):[f1=f2]]

Apply EXIST(v):A when v not in A is the same as A:

ALL(x):[Set(x)
=> (R∨¬R)
& ALL(f1):ALL(f2):[f1=f2]]

Apply 2) to get:

ALL(x):[Set(x)
=> ALL(f1):ALL(f2):[f1=f2]]

Apply the Forall Instantiation rule of Natural Deduction:

[Set(null)
=> ALL(f1):ALL(f2):[f1=f2]]

Apply Modus Ponens of Natural Deduction with your Set(null) Axiom:

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

Dan Christensen schrieb am Sonntag, 3. April 2022 um 20:15:21 UTC+2:
> 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) e x] => f1=f2]]
> => ALL(x):[Set(x) =>ALL(f1): ALL(f2):[f1=f2]]

My previous reply here still applies. Deal with it Jan Burse. We are STILL waiting for that FORMAL proof. Maybe you need to familiarize yourself with what is meant by formal proof. See https://en.wikipedia.org/wiki/Formal_system

Dan

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

On Sunday, April 3, 2022 at 5:20:48 PM UTC-4, Mostowski Collapse wrote:
> Hey Uber Moron, you prove the same way like the other
> formula. You can even derive a stronger statement,
> which shows the full extend of your nonsense claim: ...

I showed a formal proof. Only you cannot grasp it.

LoL

Dan Christensen schrieb am Montag, 4. April 2022 um 00:30:04 UTC+2:
> My previous reply here still applies. Deal with it Jan Burse. We are STILL waiting for that FORMAL proof. Maybe you need to familiarize yourself with what is meant by formal proof. See https://en.wikipedia.org/wiki/Formal_system
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
> On Sunday, April 3, 2022 at 5:20:48 PM UTC-4, Mostowski Collapse wrote:
> > Hey Uber Moron, you prove the same way like the other
> > formula. You can even derive a stronger statement,
> > which shows the full extend of your nonsense claim: ...

On Sunday, April 3, 2022 at 7:44:12 PM UTC-4, Mostowski Collapse wrote:
> I showed a formal proof. Only you cannot grasp it.
>

You listed several claims, each without a formal proof.

Dan

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

No I listed step by step proofs.

We have now reduced two proofs from here:
https://dcproof.com/EmptyFunctionsUniqueV2.htm

To utter nonsense:

What Dan-O-Matik calls: "On every set, there is exists a unique empty function (lines 1-91)"
EXIST(f):ALL(g):[g=f]
https://groups.google.com/g/sci.logic/c/qdh5sCBDPJo/m/T8HochqvCAAJ

What Dan-O-Matik calls: "The function space (fs) of all functions mapping the empty set to any set x has only a single element (lines 92-137)"
ALL(f1):ALL(f2):[f1=f2]]
https://groups.google.com/g/sci.logic/c/3CrCpBI8I2E/m/jGjj7n69CAAJ

Your are only incapable to grasp it.

Dan Christensen schrieb am Montag, 4. April 2022 um 03:45:17 UTC+2:
> On Sunday, April 3, 2022 at 7:44:12 PM UTC-4, Mostowski Collapse wrote:
> > I showed a formal proof. Only you cannot grasp it.
> >
> You listed several claims, each without a formal proof.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan-O-Matik braught up:
> non-negative real number x such the x =/= |x|.

Can we agree about the following new axiom for DC Proof?

ALL(f):ALL(g):[EXIST(a):[f(a)=/=g(a)] => f=/=g]

On Monday, April 4, 2022 at 2:54:02 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> No I listed step by step proofs.
>

Some "steps!" You really don't have clue, do you, Jan Burse?

> We have now reduced two proofs from here:
> https://dcproof.com/EmptyFunctionsUniqueV2.htm
>
> To utter nonsense:
>

Only in your wet dreams, Jan Burse.

You are the one claiming that x =/= |x| for some non-negative real x. And that we can make inferences about a function outside of its domain of definition--your "dark elements."

You should team up with WM and AP as a junior partner. Dark elements meets dark numbers meets one atom universe. They have been pushing shit like this for decades here. The sci.math Dream Team. (HA, HA, HA!)

Dan