DC poop is heavily challenged by beginner math

[Mostowski Collapse]

We find this funny blooper, through "simplification" of math:

Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 06:07:30 UTC+1:
> F is a functional predicate:
> 1 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]]]
> Axiom
https://groups.google.com/g/sci.logic/c/IOI8huqNaBU/m/uCo-Mz4ABwAJ

Lets see whether this is correct. Take a function F : {0} -> {0},
it should be undefined outside of the domain {0}. So we should
be able to prove the following:

1≠0 => ~F(1,0)

Can we prove it? Lets use the tree tool to find a counter model,
and show that we cannot prove it. So Dan-O-Matik "simplification"
puntched a hole into what we understand by the notion F : X -> Y:

∀a(a=z → ∃b(b=z ∧ ∀c(c=z → (Fac → c=b)))) → (¬o=z → ¬Foz) is invalid.
Countermodel:
Domain: { 0, 1 }
z: 0
o: 1
F: { (1,0) }

What Dan-O-Matik posted is simply an incorrect axiom.

[Dan Christensen]

On Thursday, December 2, 2021 at 8:08:01 AM UTC-5, Mostowski Collapse wrote:
> We find this funny blooper, through "simplification" of math:
>
> Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 06:07:30 UTC+1:
> > F is a functional predicate:
> > 1 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]]]
> > Axiom
> https://groups.google.com/g/sci.logic/c/IOI8huqNaBU/m/uCo-Mz4ABwAJ
>
> Lets see whether this is correct. Take a function F : {0} -> {0},
> it should be undefined outside of the domain {0}. So we should
> be able to prove the following:
>
> 1≠0 => ~F(1,0)
>

Nope. But if you think you can prove it, this should get you started:

1 ALL(a):[P(a) <=> a=0]
Axiom

2 ~1=0
Axiom

3 P(0) <=> 0=0
U Spec, 1

4 [P(0) => 0=0] & [0=0 => P(0)]
Iff-And, 3

5 0=0 => P(0)
Split, 4

6 0=0
Reflex

7 P(0)
Detach, 5, 6

8 P(1) <=> 1=0
U Spec, 1

9 [P(1) => 1=0] & [1=0 => P(1)]
Iff-And, 8

10 P(1) => 1=0
Split, 9

11 ~1=0 => ~P(1)
Contra, 10

12 ~P(1)
Detach, 11, 2

13 ALL(a):[P(a) => EXIST(b):[P(b) & ALL(c):[P(c) => [F(a,c) => c=b]]]]
Premise

14 P(1) => EXIST(b):[P(b) & ALL(c):[P(c) => [F(1,c) => c=b]]]
U Spec, 13

Now what? Since the antecedent P(1) is false, the truth value of the consequent is indeterminate, i.e. it could be either true or false. (See the truth table for logical implication.) We can say that F is UNDEFINED if the argument is not 0.

Dan

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

[Mostowski Collapse]

Well if the domain is {0} and the codomain is {0}, then
the only function is F = {(0,0)}. Or equivalently:

ALL(x):ALL(y):(F(x,y) <=> x=0 /\ y= 0).

Its easy to see that now this here follows:

1≠0 => ~F(1,0)

You can also try the tree tool,
I using z for zero 0, and o for one 1:

∀x∀y(Fxy ↔ (x=z ∧ y=z)) → (¬o=z → ¬Foz) is valid.
https://www.umsu.de/trees

[Mostowski Collapse]

Conclusion, your definition of F : P -> Q is botched.
It already fails for P=Q={0}. Since it cannot be used
to derive 1≠0 => ~F(1,0) .

Try a better definition of F : P -> Q. A definition that is
mathematically correct, and that would express that
dom(F)=P and ran(F) subset Q.

And not ran(F|P) subset Q as you do. A mathematical
correct definition is found in this booklet:

Basic Set Theory - Azriel Levy
https://www.amazon.de/dp/0486420795

The booklet is only 20 bucks or so.

[Dan Christensen]

On Thursday, December 2, 2021 at 6:33:16 PM UTC-5, Mostowski Collapse wrote:
> Conclusion, your definition of F : P -> Q is botched.
> It already fails for P=Q={0}. Since it cannot be used
> to derive 1≠0 => ~F(1,0) .
>

See my reply to your identical posting here just now.

[Mostowski Collapse]

Dan-O-Matik halucinated his own little crazy world:
> Given s0={0}, f:s0-->s0 and ~1=0, we have: f(0)=0 and f(1) is indeterminate (undefined)
> Formal Proof: https://www.dcproof.com/FunctionUndefined.htm (23 lines)

This is not correct mathematics. If you say f : X -> Y, you
want the domain of f to be determined to be X.
If you have for f : {0} -> {0}, f(1) inderminate, then dom(f)

can be either {0} or {0,1}. You need to have f(1) undefined,
so that the domain is always {0}. You can check any standard
reference in mathematics, for example:

Basic Set Theory - Azriel Levy
https://www.amazon.de/dp/0486420795

The booklet is only 20 bucks or so.

[Mostowski Collapse]

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

Obviously these theorems neither talk about empty functions,
nor do they consist generally valid statements. The statements
cannot be generally valid, since there are mathematical models

where we have at least two functions, like in trigonometry,
one has sinus and cosinus, i.e. sin and cos, and sin =\= cos.
Both formulas EXIST(f):[ALL(g):[g=f]] and ALL(f1):ALL(f2):[f1=f2]]

are not satisfied when there at least two functions.

So whats going wrong in DC poop.

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

[Ross A. Finlayson]

But if you model a set in all relation isn't one outside,
the set or the relation, in the theory of either?


Set relation theory.

Function theory and set theory are two different things,
i.e. what in set theory "is a Cartesian model of a function
according to the existence and there are usual models of
at least indicator presence in all the discrete Cartesian,
so that existence proofs are so easy in terms of functions",
here is for variously theory: set theory, part theory, function
theory, type theory, category theory, ....

When you write "f subset domain cross co-domain", even those
don't define all function besides that you made for "defined" in
function.

Of course this is where a special function the line-drawing between
zero and one rests right between set theory and function theory,
though a function not having necessarily a Cartesian model.

(In set theory.)

For whatever the strength of a set theory is and whatever strength
is, there is an object that is a model of each, under the "equi-interpretable",
in terms of the theories being and having a model, this is a ubiquitous
theory with various primary elements like set theory's, category theory,
relations and other theories in terms, and besides what's categorical as
geometry, though that geometry definitely has the continuous, which in
terms is not so much a usual matter of words, plural.


Existence proofs are often by allusion. (And exclusion.)

Then the point of theory and statement is the strength,
here the point is that DC proof is arbitrarily weak, according
to that following adherence admits the validity of inference,
when in reality it is for example a case of slippery-slope.

The "slippery slope" is an example from logic, it's that the
approach makes back-pedaling, or otherwise admits a reason
to admit a reason to admit a reason that under terms makes
sense as an approach, but doesn't work as an approach.
(To reaching soundness, for decision, and in validities.)

[Mostowski Collapse]

I wonder why Dan-O-Matik is so slow in grasping Function
Spaces from Set Theory. Maybe he is ruSSian?

Reagan tells Soviet jokes
"There's a ten-year wait, and you go through quite a
process when you are ready to buy, and then you put
up the money in advance. And this happened to a fella.
And this is their story that they tell, their joke... that this
man, he laid down his money. And then the fella who
was in charge tells him, "Okay, come back in ten years
and get your car." And he said, "Morning or afternoon?"
And ... and the fella behind the cars said, "Well, ten years
from now what difference does it make?" And he said,
"Well, the plumber is coming in the morning."
https://www.youtube.com/watch?v=mN3z3eSVG7A

> Set relation theory.

[Ross A. Finlayson]

On Sunday, April 3, 2022 at 5:05:18 PM UTC-7, Mostowski Collapse wrote:

Optimized Regular Data Structures?

Optimized regular data structures?

[Ross A. Finlayson]

chip set

CPU and packaging

RAM
queues (buffers)

graphics/video <-> direct to port

networking <-> interface to port

USB and connectivity <-> "USB micro-bus"

port <-> bus

port protocols
bus protocols

Device model and the simple


It is one thing to "show your work", the other to, show "the" work.

[Ross A. Finlayson]

On Monday, April 4, 2022 at 8:22:51 AM UTC-7, Ross A. Finlayson wrote:

Then it's like, if you're not going to bother to read these books, you can sit and listen to someone read them to you.

Then I'd probably imagine employing myself as an otherwise dumb stage-reader.

Basically for providing an audio reader, is to make what results after report, what as one would expect from reading, the results of content of reading.

Using my own voice samples and along those lines, is for resulting that recognition begins, about audio, samples.

Tone samples <-> Note samples
Noise reduction <-> Sound

Here the point is to employ the software or audio registers, or also as what are the employment of the board interface, what results that the chips together with the processors, activates software that via a concise vocal dictionary, outputs a reading audio format, that for a given corpus reads it.

Audio, CD Audio, and digital audio

Output and audio
source and sampling, "url"
"ad-hoc URL, points through URL handler"

(audio/...)

"Samples are simple files"
"Tone gets four samples"

4-sample tone
8-sample tone
...

(3, 5, 7, notes and octave tone)

"This sample is the audio output format"

"These samples, are used to compute alternate input formats, the audio output format"

"This usual playback indicator of the usual playback to an output, picks a tone"
"given a source, tone is expected to indicate potential"
(potential standing down from standing sustain)

Tones, range, and speed
Chords

Digital audio, and, "Wave", format

Audio encoding and usual speech-organized codecs
Audio encoding and usual sound-organized codecs

Tone and beat removal
Tone and Beat

Sound, tone, and aspiration

sibilant beats and power beats

sound and noise reduction

words and phonetics

words and the spoken word
matters of dialect
intentions if correct

[Mostowski Collapse]

My counter model is easy to prove. The first proof you need
to do, is to prove some properties about these functions:

f(x) = x, is a line
https://www.wolframalpha.com/input?i=y+%3D+x

g(x) = abs(x), is two half lines
https://www.wolframalpha.com/input?i=y+%3D+abs%28x%29

You should be able to prove, for dom = [0,oo) ⊆ R and cod = R:

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

And you should be able to prove:

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

Using this axiom:

"If two functions differs at some argument, then they differ"
ALL(f):ALL(g):[EXIST(a):[f(a)=/=g(a)] => f=/=g]

[Dan Christensen]

Only if, as you seem to believe, there exists x in R+ such that x =/= |x|. One of those "dark elements" of yours, Jan Burse? (HA, HA, HA!!!)

Dan

[Mostowski Collapse]

STUDENTS BEWARE: Dan-O-Matik, the only Ultra Moron on
this planet who doesn't understand how ALL(_) quantifier
works. If you state an axiom such as:

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

It MUST be satisfied by ALL possible combinations
of f, g, dom and cod, not only those that Dan-O-Matik has
in mind. It must be the full cross product.

If you want something else than a full cross product,
you musts stated this explicitly, like for example:

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

If you do not have functions like dom(_) and cod(_)
that retrieve the dom and cod of a function and
if you don't state the FUNCTIONAL DEPENDENCIES

such as d = dom(f) & c = cod(f) & d = dom(g) & c = cod(g),
then your axiom becomes pure nonsense.

[Mostowski Collapse]

Since the author collective Nicolas Bourbaki, which
introduced notions such as surjective, injective, bijective
to mathematics, the function concept Terrence Tao

is refering to is a triple:

f = <F, X, Y>

You can easily retrieve dom and cod from f, by using
the projections of the triple:

/* Projection on First Component of the Triple */
graph(f) = π_1(f) = F

/* Projection on the Second Component of the Triple */
dom(f) = π_2(f) = X

/* Projection on the Third Component of the Triple */
cod(f) = π_3(f) = Y

Since for example you have now cod(_) available for
a function f in this framework, you can also uniquely
talk about "the surjectivity" of a function f. Which would
be defined as follows:

/* informally */
f surjective :<=> ALL(y):[y e Y => EXIST(x):[x e X & f(x) = y]]

/* formall */
f surjective :<=> ALL(y):[y e π_3(f) => EXIST(x):x e π_2(f) & <x,y> e π_1(f)]]

On the other hand the Dan-O-Matik nonsense ALL(a):[a e dom =>
f(a) e cod] is ambigious. Take the functions f : R -> R, f(x) = abs(x),
is it ALL(a):[a e R -> abs(a) e R] or is it ALL(a):[a e R => abs(a) e R+]

/* Dan-O-Matik Nonsense is a Ambigious */
Do we have?
ALL(a):[a e R -> abs(a) e R]
Or do we have?
ALL(a):[a e R => abs(a) e R+]

both would work. Its just nonsense. There is reason that all
mathematicians nowadays basically work in the Nicolas Bourbaki
framework, even Terrence Tao , although

Dan-O-Matik cannot grasp it.

[Dan Christensen]

On Thursday, April 7, 2022 at 5:04:54 AM UTC-4, Mostowski Collapse wrote:
> Since the author collective Nicolas Bourbaki, which
> introduced notions such as surjective, injective, bijective
> to mathematics, the function concept Terrence Tao
>

...

See my reply in the thread "Equality of Functions: Big Controversy" at sci.math

Dan

[Mostowski Collapse]

I have never seen an intelligent reply by Dan-O-Matik. He is
obsessed with some outside values and dark matter.
And ingnores basic facts such as that this here:

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

is ambigious. Namely:

Covariance in cod:
cod ⊆ cod' & ALL(a):[a e dom => f(a) e cod] => ALL(a):[a e dom => f(a) e cod']

Contravariance in dom:
dom ⊆ dom' & ALL(a):[a e dom' => f(a) e cod] => ALL(a):[a e dom => f(a) e cod]

See also:
https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29#Function_types

Examples:

ALL(a):[a e Animal => f(a) e Cat] => ALL(a):[a e Animal => f(a) e Animal]

ALL(a):[a e Animal => f(a) e Cat] => ALL(a):[a e Cat=> f(a) e Cat]

[Dan Christensen]

On Friday, April 8, 2022 at 7:58:55 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> I have never seen an intelligent reply by Dan-O-Matik. He is
> obsessed with some outside values and dark matter.

Bullshit.

> And ingnores basic facts such as that this here:
> ALL(a):[a e dom => f(a) e cod]
> is ambigious. Namely:
>

Nothing ambiguous about it. You are just pissed of that it does allow for your "dark elements." Get a life, Jan Burse.

> Covariance in cod:
> cod ⊆ cod' & ALL(a):[a e dom => f(a) e cod] => ALL(a):[a e dom => f(a) e cod']
>

If x is an element of set y, then it is also a set of any superset of y. Nothing "ambiguous" about it.

> Contravariance in dom:
> dom ⊆ dom' & ALL(a):[a e dom' => f(a) e cod] => ALL(a):[a e dom => f(a) e cod]
>

Only Jan Burse could think there was anything "ambiguous" about this either. Oh, well...

[Ross A. Finlayson]

How do you model ambiguity then?

[Mostowski Collapse]

Can you prove in DC Poop from:

2 Set(null)
Axiom
3 ALL(a):~a e null
Axiom
https://dcproof.com/EmptyFunctionsUniqueV3.htm

And:

6 Set(one)
Axiom
7 ALL(a):[a e one <=> a = null]
Axiom

That there is the a union of null and one, lets call
it two, such that:

Set(two)

ALL(a):[a e two <=> a = null | a = one]

Does DC poop allow performing set union? Like
in normal set theory?

[Mostowski Collapse]

One more question about DC poop, can
you also prove:

one =/= null

Because null is empty and one is non-empty.
Usually this is called set extensionality?