How can we figure out what is more clumsy, a definition:

Surjective(_) <=>

Or a definition as follows:

Surjective(_,_,_) <=>

Lets make an empirical study, prove this both ways with
Surjective(_) and Surjective(_,_,_) (and analogue for injective):

Let A and B be sets and f : A → B an injective function. Suppose
that A is non-empty. Then there exists a surjection g : B → A

Which proof is less clumsy?

Somehow I think defining:

Injective(_) <=> ...

Is less clumsy, because we can first prove:

Let A and B be sets and f : A → B a function. Suppose
that A is non-empty. Then there exists a surjection g : B → A

And then this is only a corollary:

Let A and B be sets and f : A → B an injective function. Suppose
that A is non-empty. Then there exists a surjection g : B → A

Maybe its a trick question?

Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
> How can we figure out what is more clumsy, a definition:
>
> Surjective(_) <=>
>
> Or a definition as follows:
>
> Surjective(_,_,_) <=>
>
> Lets make an empirical study, prove this both ways with
> Surjective(_) and Surjective(_,_,_) (and analogue for injective):
>
> Let A and B be sets and f : A → B an injective function. Suppose
> that A is non-empty. Then there exists a surjection g : B → A
>
> Which proof is less clumsy?

Oops my bad, injectivity is needed. Oki Doki.

Mostowski Collapse schrieb am Montag, 22. August 2022 um 01:22:51 UTC+2:
> Somehow I think defining:
>
> Injective(_) <=> ...
>
> Is less clumsy, because we can first prove:
>
> Let A and B be sets and f : A → B a function. Suppose
> that A is non-empty. Then there exists a surjection g : B → A
> And then this is only a corollary:
> Let A and B be sets and f : A → B an injective function. Suppose
> that A is non-empty. Then there exists a surjection g : B → A
> Maybe its a trick question?
> Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
> > How can we figure out what is more clumsy, a definition:
> >
> > Surjective(_) <=>
> >
> > Or a definition as follows:
> >
> > Surjective(_,_,_) <=>
> >
> > Lets make an empirical study, prove this both ways with
> > Surjective(_) and Surjective(_,_,_) (and analogue for injective):
> >
> > Let A and B be sets and f : A → B an injective function. Suppose
> > that A is non-empty. Then there exists a surjection g : B → A
> >
> > Which proof is less clumsy?

On Sunday, August 21, 2022 at 6:03:52 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> How can we figure out what is more clumsy, a definition:
>
> Surjective(_) <=>
>

Should be: ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> [ALL(a):[a in cod => EXIST(b): [b in dom & f(b)=a]]]]

It is a purely optional abbreviation to improve readability, but somehow it causes Jan Burse's brain to explode.

> Or a definition as follows:
>
> Surjective(_,_,_) <=>
>
> Lets make an empirical study, prove this both ways with
> Surjective(_) and Surjective(_,_,_) (and analogue for injective):
>
> Let A and B be sets and f : A → B an injective function. Suppose
> that A is non-empty. Then there exists a surjection g : B → A
>
> Which proof is less clumsy?

Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.

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, August 21, 2022 at 9:11:30 PM UTC-4, Dan Christensen wrote:
> On Sunday, August 21, 2022 at 6:03:52 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> > How can we figure out what is more clumsy, a definition:
> >
> > Surjective(_) <=>
> >
> Should be: ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> [ALL(a):[a in cod => EXIST(b): [b in dom & f(b)=a]]]]
>
> It is a purely optional abbreviation to improve readability, but somehow it causes Jan Burse's brain to explode.
> > Or a definition as follows:
> >
> > Surjective(_,_,_) <=>
> >
> > Lets make an empirical study, prove this both ways with
> > Surjective(_) and Surjective(_,_,_) (and analogue for injective):
> >
> > Let A and B be sets and f : A → B an injective function. Suppose
> > that A is non-empty. Then there exists a surjection g : B → A
> >
> > Which proof is less clumsy?
> Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
>

BTW I have given my optional abbreviation here. Could you list your required axioms/definitions here, so that readers can compare, Jan Burse?

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

On Monday, August 22, 2022 at 4:10:21 AM UTC+2, Dan Christensen wrote:
>
> ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> [ALL(a):[a in cod => EXIST(b): [b in dom & f(b)=a]]]]
>
> It is a purely optional abbreviation

Just nonsense.

It seems to me that you just want to express

f[A] = B

with your idiotic "Surjective(f,A,B)". Though *I* would prefere to add the condition A c dom(f) in this connection.

Hence, the term "Surjective" is rather misleading here.

On Monday, August 22, 2022 at 4:55:18 AM UTC+2, Fritz Feldhase wrote:
> On Monday, August 22, 2022 at 4:10:21 AM UTC+2, Dan Christensen wrote:
> >
> > ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> [ALL(a):[a in cod => EXIST(b): [b in dom & f(b)=a]]]]
> >
> > It is a purely optional abbreviation
> >
> Just nonsense.
>
> It seems to me that you just want to express
>
> f[A] = B
>
> with your idiotic "Surjective(f,A,B)".

Right. As we can see here:

"Definition 3.3.17 [slightly altered]: A function f: X --> Y is /surjective/ iff f[X] = Y, i.e., for every y ∈ Y, there exists an x ∈ X such that f(x) = y."

Here Tao mentions that

f[X] = Y

"means the same" as

for every y ∈ Y, there exists an x ∈ X such that f(x) = y

[at least in the given context].

Hint: A function f is surjective iff f[dom(f)] = cod(f).

On Sunday, August 21, 2022 at 10:55:18 PM UTC-4, Fritz Feldhase wrote:
> On Monday, August 22, 2022 at 4:10:21 AM UTC+2, Dan Christensen wrote:
> >
> > ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> [ALL(a):[a in cod => EXIST(b): [b in dom & f(b)=a]]]]
> >
> > It is a purely optional abbreviation

> Just nonsense.

[snip]

You seem to be grasping at straws here, Fritz. There is nothing in set theory the requires a formal definition of the word "surjective." Instead of saying the function f mapping set X to set Y is "surjective," we can as easily say that it is such that ALL(a):[a in Y => EXIST(b):[b in X & f(b)=a]] without introducing any new terminology.

Dan

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

On Monday, August 22, 2022 at 5:57:53 AM UTC+2, Dan Christensen wrote:
> On Sunday, August 21, 2022 at 10:55:18 PM UTC-4, Fritz Feldhase wrote:
> > On Monday, August 22, 2022 at 4:10:21 AM UTC+2, Dan Christensen wrote:
> > >
> > > ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> [ALL(a):[a in cod => EXIST(b): [b in dom & f(b)=a]]]]
> > >
> > > It is a purely optional abbreviation
> >
> > Just nonsense.

Hint: It seems to me that you just want to express

f[A] = B

with your idiotic "Surjective(f,A,B)".

Seems that this idiotic idea was triggered by the following definition:

"Definition 3.3.17 [slightly altered]: A function f: X --> Y is /surjective/ iff f[X] = Y, i.e., for every y ∈ Y, there exists an x ∈ X such that f(x) = y."

Here Tao mentions that

f[X] = Y

"means the same" as

for every y ∈ Y, there exists an x ∈ X such that f(x) = y

[at least in the given context].

Tao's definition for /surjective/ may be formalized the following way:

AfAXAY: f:X --> Y -> (surjective(f) <-> f[X] = Y).

So we MIGHT use your "abbreviation" to write:

AfAXAY: f:X --> Y -> (surjective(f) <-> surjective(f,X,Y)) ,

which would be rather idiotic! Especially, since the notion f[.] is heavily used in math and has a distinctive meaning (i. e. is a common idiom).

Could you point out a SINGLE source (textbook, internet source, etc.) where a/the predicat

surjective(f,X,Y)

was introduced for "abbreviating"

for every y ∈ Y, there exists an x ∈ X such that f(x) = y..

?

No? Any idea why not?

On Monday, August 22, 2022 at 12:25:37 AM UTC-4, Fritz Feldhase wrote:

[snip]

>
> Could you point out a SINGLE source (textbook, internet source, etc.) where a/the predicat
>
> surjective(f,X,Y)
>

Proofs in mathematical textbooks are overwhelmingly informal proofs. I don't recall any that formally define a "surjective" predicate with ANY number of arguments. DC Proof, like any proof-checking software however, must deal strictly with formal proofs. If you want to formally define a "surjective" predicate with only only predicate, DC Proof can accommodate that. In my proofs, I prefer a simple abbreviation of 3 arguments with no restrictions. Note that this and other similar abbreviations are not built into DC Proof.. They must be introduced by users are the beginning of their proofs using the Axiom Rule available on the Logic menu.

Dan

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

Well there is no "should be" you moron. There is only a "could be".
There "could be":

Surjective(_) <=> ....

Or there "could be":

Surjective(_,_,_) <=> ....

The by the scientific method of empirical investigation:
"Empirical research is research using empirical evidence.
It is also a way of gaining knowledge by means of direct
and indirect observation or experience."
https://de.wikipedia.org/wiki/Empirie

We have to find out what is more "clumsy".

Whats wrong with you? Never done science in your life?

P.S.: I have already a working definition for Dan O Matiks
"clumsy". "clumsy" is a new unit introduced by Dan Christensen.
Its the number of belgian waffles a mathematician eats,

while doing a proof. More belgian waffles more clumsy.

Dan Christensen schrieb am Montag, 22. August 2022 um 03:11:30 UTC+2:
> On Sunday, August 21, 2022 at 6:03:52 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> > How can we figure out what is more clumsy, a definition:
> >
> > Surjective(_) <=>
> >
> Should be: ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> [ALL(a):[a in cod => EXIST(b): [b in dom & f(b)=a]]]]
>
> It is a purely optional abbreviation to improve readability, but somehow it causes Jan Burse's brain to explode.
> > Or a definition as follows:
> >
> > Surjective(_,_,_) <=>
> >
> > Lets make an empirical study, prove this both ways with
> > Surjective(_) and Surjective(_,_,_) (and analogue for injective):
> >
> > Let A and B be sets and f : A → B an injective function. Suppose
> > that A is non-empty. Then there exists a surjection g : B → A
> >
> > Which proof is less clumsy?
> Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

A.D. de Groot's empirical cycle:

- Observation: The observation of a phenomenon
and inquiry concerning its causes.
- Induction: The formulation of hypotheses - generalized
explanations for the phenomenon.
- Deduction: The formulation of experiments that will test
the hypotheses (i.e. confirm them if true, refute them if false).
- Testing: The procedures by which the hypotheses are
tested and data are collected.
- Evaluation: The interpretation of the data and the formulation
of a theory - an abductive argument that presents the results
of the experiment as the most reasonable explanation for the phenomenon.
https://en.wikipedia.org/wiki/Empirical_research#Empirical_cycle

Dan Christensen formulated the hypothesis Surjective(_,_,_) is less clumsy.
But is this really true? Does a mathematician that uses Surjective(_,_,_)
consume less belgian waffles than a mathematician that uses Surjective(_)?

BTW: His hypothesis is from here:
Dan Christensen schrieb am Mittwoch, 17. August 2022 um 20:27:51 UTC+2:
> I have tried various definitions of a surjectivity abbreviation including
your suggestion to restrict its application using the Function(f,x,y) signature,
but found it needlessly cumbersome.
https://groups.google.com/g/sci.logic/c/QSfRj2g1ur8/m/fFHeqEU7AQAJ

Where are his "trials" documented?

Mostowski Collapse schrieb am Montag, 22. August 2022 um 11:44:44 UTC+2:
> Well there is no "should be" you moron. There is only a "could be".
> There "could be":
>
> Surjective(_) <=> ....
>
> Or there "could be":
>
> Surjective(_,_,_) <=> ....
>
> The by the scientific method of empirical investigation:
> "Empirical research is research using empirical evidence.
> It is also a way of gaining knowledge by means of direct
> and indirect observation or experience."
> https://de.wikipedia.org/wiki/Empirie
>
> We have to find out what is more "clumsy".
>
> Whats wrong with you? Never done science in your life?
>
> P.S.: I have already a working definition for Dan O Matiks
> "clumsy". "clumsy" is a new unit introduced by Dan Christensen.
> Its the number of belgian waffles a mathematician eats,
>
> while doing a proof. More belgian waffles more clumsy.
> Dan Christensen schrieb am Montag, 22. August 2022 um 03:11:30 UTC+2:
> > On Sunday, August 21, 2022 at 6:03:52 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> > > How can we figure out what is more clumsy, a definition:
> > >
> > > Surjective(_) <=>
> > >
> > Should be: ALL(f):ALL(dom):ALL(cod):[Surjective(f,dom,cod) <=> [ALL(a):[a in cod => EXIST(b): [b in dom & f(b)=a]]]]
> >
> > It is a purely optional abbreviation to improve readability, but somehow it causes Jan Burse's brain to explode.
> > > Or a definition as follows:
> > >
> > > Surjective(_,_,_) <=>
> > >
> > > Lets make an empirical study, prove this both ways with
> > > Surjective(_) and Surjective(_,_,_) (and analogue for injective):
> > >
> > > Let A and B be sets and f : A → B an injective function. Suppose
> > > that A is non-empty. Then there exists a surjection g : B → A
> > >
> > > Which proof is less clumsy?
> > Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Monday, August 22, 2022 at 7:04:39 AM UTC+2, Dan Christensen wrote:
> On Monday, August 22, 2022 at 12:25:37 AM UTC-4, Fritz Feldhase wrote:

> > surjective(f,X,Y)

The following might be a reasonable definition:

surjective(f,X,Y) :<-> function(f,X,Y) & f[X] = Y.

In math lingo (usually):

f: X -->> Y :<-> f: X --> Y & f[X] = Y.

"f is an surjective function from X into Y"
("f is a function from X onto Y")

On Monday, August 22, 2022 at 5:44:44 AM UTC-4, Mostowski Collapse wrote:
[snip]

> > Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
> >

[snip abuse]

> There "could be":
>
> Surjective(_) <=> ....
>
> Or there "could be":
>
> Surjective(_,_,_) <=> ....
>

Or there could be no predicates whatsoever, e.g.

ALL(f):[ALL(a):[a in {0} => f(a) in {0}]
=> ALL(a):[a in {0} => EXIST(b):[b in {0} & f(b)=a]]] <----- f is surjective

ALL(g):[ALL(a):[a in {0} => g(a) in {0,1}] & g(0)=0
=> ~ALL(a):[a in {0,1} => EXIST(b):[b in {0} & g(b)=a]]] <----- g is not surjective

Your "system" should be able handle these as well.

> The by the scientific method of empirical investigation:
> "Empirical research is research using empirical evidence.
> It is also a way of gaining knowledge by means of direct
> and indirect observation or experience."
> https://de.wikipedia.org/wiki/Empirie
>
[snip abuse]

Scientific method???

Quit making excuses, Jan Burse. Let's see the full set of your axioms/definitions for Surjective(_), dom(_), cod(_), etc. and some proofs using them, say the equivalent of those above.

Dan

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

On Monday, August 22, 2022 at 11:01:50 AM UTC-4, Dan Christensen wrote:
> On Monday, August 22, 2022 at 5:44:44 AM UTC-4, Mostowski Collapse wrote:
>
> [snip]
> > > Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
> > >
> [snip abuse]
> > There "could be":
> >
> > Surjective(_) <=> ....
> >
> > Or there "could be":
> >
> > Surjective(_,_,_) <=> ....
> >
> Or there could be no predicates whatsoever, e.g.
>
> ALL(f):[ALL(a):[a in {0} => f(a) in {0}]
> => ALL(a):[a in {0} => EXIST(b):[b in {0} & f(b)=a]]] <----- f is surjective
>

PROOF

1. ALL(a):[a in x <=> a=0]
Axiom

Suppose...

2. ALL(a):[a in x => f(a) in x]
Premise

Prove: ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]

Suppose...

3. t in x
Premise

Apply definition of x

4. t in x <=> t=0
U Spec, 1

5. [t in x => t=0] & [t=0 => t in x]
Iff-And, 4

6. t in x => t=0
Split, 5

7. t=0
Detach, 6, 3

8. 0 in x
Substitute, 7, 3

9. t in x => f(t) in x
U Spec, 2

10. f(t) in x
Detach, 9, 3

Apply definition of x

11. f(t) in x <=> f(t)=0
U Spec, 1, 10

12. [f(t) in x => f(t)=0] & [f(t)=0 => f(t) in x]
Iff-And, 11

13. f(t) in x => f(t)=0
Split, 12

14. f(t)=0
Detach, 13, 10

Substituting...

15. f(0)=0
Substitute, 7, 14

16. f(0)=t
Substitute, 7, 15

17. 0 in x & f(0)=t
Join, 8, 16

18. EXIST(b):[b in x & f(b)=t]
E Gen, 17

f is surjective
As Required:

19. ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
Conclusion, 3

As Required:

20. ALL(f):[ALL(a):[a in x => f(a) in x]
=> ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]]
Conclusion, 2

> ALL(g):[ALL(a):[a in {0} => g(a) in {0,1}] & g(0)=0
> => ~ALL(a):[a in {0,1} => EXIST(b):[b in {0} & g(b)=a]]] <----- g is not surjective
>
> Your "system" should be able handle these as well.
> > The by the scientific method of empirical investigation:
> > "Empirical research is research using empirical evidence.
> > It is also a way of gaining knowledge by means of direct
> > and indirect observation or experience."
> > https://de.wikipedia.org/wiki/Empirie
> >
> [snip abuse]
>
> Scientific method???
>
> Quit making excuses, Jan Burse. Let's see the full set of your axioms/definitions for Surjective(_), dom(_), cod(_), etc. and some proofs using them, say the equivalent of those above.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Holy cow! What is this guy smoking? Tibet, Afghanistan, ...?

Its not the theorem we want. You have as an axiom:

1. ALL(a):[a in x <=> a=0]
Axiom

Which says a = {0}. But the theorem would have maybe:

1. EXIST(a):[a in x]
Axiom

Better have it in the conclusion though. The challenge is:

Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
> Let A and B be sets and f : A → B an injective function. Suppose
> that **A is non-empty**. Then there exists a surjection g : B → A
https://groups.google.com/g/sci.math/c/T7OzU-PmpEg/m/hLscRJOtAwAJ

Dan Christensen schrieb am Montag, 22. August 2022 um 17:42:36 UTC+2:
> On Monday, August 22, 2022 at 11:01:50 AM UTC-4, Dan Christensen wrote:
> > On Monday, August 22, 2022 at 5:44:44 AM UTC-4, Mostowski Collapse wrote:
> >
> > [snip]
> > > > Why don't you do a couple of proofs for us testing each alternative.. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
> > > >
> > [snip abuse]
> > > There "could be":
> > >
> > > Surjective(_) <=> ....
> > >
> > > Or there "could be":
> > >
> > > Surjective(_,_,_) <=> ....
> > >
> > Or there could be no predicates whatsoever, e.g.
> >
> > ALL(f):[ALL(a):[a in {0} => f(a) in {0}]
> > => ALL(a):[a in {0} => EXIST(b):[b in {0} & f(b)=a]]] <----- f is surjective
> >
> PROOF
>
> 1. ALL(a):[a in x <=> a=0]
> Axiom
>
> Suppose...
>
> 2. ALL(a):[a in x => f(a) in x]
> Premise
>
>
> Prove: ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
>
> Suppose...
>
> 3. t in x
> Premise
>
> Apply definition of x
>
> 4. t in x <=> t=0
> U Spec, 1
>
> 5. [t in x => t=0] & [t=0 => t in x]
> Iff-And, 4
>
> 6. t in x => t=0
> Split, 5
>
> 7. t=0
> Detach, 6, 3
>
> 8. 0 in x
> Substitute, 7, 3
>
> 9. t in x => f(t) in x
> U Spec, 2
>
> 10. f(t) in x
> Detach, 9, 3
>
> Apply definition of x
>
> 11. f(t) in x <=> f(t)=0
> U Spec, 1, 10
>
> 12. [f(t) in x => f(t)=0] & [f(t)=0 => f(t) in x]
> Iff-And, 11
>
> 13. f(t) in x => f(t)=0
> Split, 12
>
> 14. f(t)=0
> Detach, 13, 10
>
> Substituting...
>
> 15. f(0)=0
> Substitute, 7, 14
>
> 16. f(0)=t
> Substitute, 7, 15
>
> 17. 0 in x & f(0)=t
> Join, 8, 16
>
> 18. EXIST(b):[b in x & f(b)=t]
> E Gen, 17
>
> f is surjective
>
> As Required:
>
> 19. ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
> Conclusion, 3
>
> As Required:
>
> 20. ALL(f):[ALL(a):[a in x => f(a) in x]
> => ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]]
> Conclusion, 2
> > ALL(g):[ALL(a):[a in {0} => g(a) in {0,1}] & g(0)=0
> > => ~ALL(a):[a in {0,1} => EXIST(b):[b in {0} & g(b)=a]]] <----- g is not surjective
> >
> > Your "system" should be able handle these as well.
> > > The by the scientific method of empirical investigation:
> > > "Empirical research is research using empirical evidence.
> > > It is also a way of gaining knowledge by means of direct
> > > and indirect observation or experience."
> > > https://de.wikipedia.org/wiki/Empirie
> > >
> > [snip abuse]
> >
> > Scientific method???
> >
> > Quit making excuses, Jan Burse. Let's see the full set of your axioms/definitions for Surjective(_), dom(_), cod(_), etc. and some proofs using them, say the equivalent of those above.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Corr.:
Which says x = {0}. But the theorem would have maybe:

Mostowski Collapse schrieb am Montag, 22. August 2022 um 19:22:18 UTC+2:
> Holy cow! What is this guy smoking? Tibet, Afghanistan, ...?
>
> Its not the theorem we want. You have as an axiom:
> 1. ALL(a):[a in x <=> a=0]
> Axiom
> Which says a = {0}. But the theorem would have maybe:
>
> 1. EXIST(a):[a in x]
> Axiom
>
> Better have it in the conclusion though. The challenge is:
> Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
> > Let A and B be sets and f : A → B an injective function. Suppose
> > that **A is non-empty**. Then there exists a surjection g : B → A
> https://groups.google.com/g/sci.math/c/T7OzU-PmpEg/m/hLscRJOtAwAJ
> Dan Christensen schrieb am Montag, 22. August 2022 um 17:42:36 UTC+2:
> > On Monday, August 22, 2022 at 11:01:50 AM UTC-4, Dan Christensen wrote:
> > > On Monday, August 22, 2022 at 5:44:44 AM UTC-4, Mostowski Collapse wrote:
> > >
> > > [snip]
> > > > > Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
> > > > >
> > > [snip abuse]
> > > > There "could be":
> > > >
> > > > Surjective(_) <=> ....
> > > >
> > > > Or there "could be":
> > > >
> > > > Surjective(_,_,_) <=> ....
> > > >
> > > Or there could be no predicates whatsoever, e.g.
> > >
> > > ALL(f):[ALL(a):[a in {0} => f(a) in {0}]
> > > => ALL(a):[a in {0} => EXIST(b):[b in {0} & f(b)=a]]] <----- f is surjective
> > >
> > PROOF
> >
> > 1. ALL(a):[a in x <=> a=0]
> > Axiom
> >
> > Suppose...
> >
> > 2. ALL(a):[a in x => f(a) in x]
> > Premise
> >
> >
> > Prove: ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
> >
> > Suppose...
> >
> > 3. t in x
> > Premise
> >
> > Apply definition of x
> >
> > 4. t in x <=> t=0
> > U Spec, 1
> >
> > 5. [t in x => t=0] & [t=0 => t in x]
> > Iff-And, 4
> >
> > 6. t in x => t=0
> > Split, 5
> >
> > 7. t=0
> > Detach, 6, 3
> >
> > 8. 0 in x
> > Substitute, 7, 3
> >
> > 9. t in x => f(t) in x
> > U Spec, 2
> >
> > 10. f(t) in x
> > Detach, 9, 3
> >
> > Apply definition of x
> >
> > 11. f(t) in x <=> f(t)=0
> > U Spec, 1, 10
> >
> > 12. [f(t) in x => f(t)=0] & [f(t)=0 => f(t) in x]
> > Iff-And, 11
> >
> > 13. f(t) in x => f(t)=0
> > Split, 12
> >
> > 14. f(t)=0
> > Detach, 13, 10
> >
> > Substituting...
> >
> > 15. f(0)=0
> > Substitute, 7, 14
> >
> > 16. f(0)=t
> > Substitute, 7, 15
> >
> > 17. 0 in x & f(0)=t
> > Join, 8, 16
> >
> > 18. EXIST(b):[b in x & f(b)=t]
> > E Gen, 17
> >
> > f is surjective
> >
> > As Required:
> >
> > 19. ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
> > Conclusion, 3
> >
> > As Required:
> >
> > 20. ALL(f):[ALL(a):[a in x => f(a) in x]
> > => ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]]
> > Conclusion, 2
> > > ALL(g):[ALL(a):[a in {0} => g(a) in {0,1}] & g(0)=0
> > > => ~ALL(a):[a in {0,1} => EXIST(b):[b in {0} & g(b)=a]]] <----- g is not surjective
> > >
> > > Your "system" should be able handle these as well.
> > > > The by the scientific method of empirical investigation:
> > > > "Empirical research is research using empirical evidence.
> > > > It is also a way of gaining knowledge by means of direct
> > > > and indirect observation or experience."
> > > > https://de.wikipedia.org/wiki/Empirie
> > > >
> > > [snip abuse]
> > >
> > > Scientific method???
> > >
> > > Quit making excuses, Jan Burse. Let's see the full set of your axioms/definitions for Surjective(_), dom(_), cod(_), etc. and some proofs using them, say the equivalent of those above.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

What is the condition **A is non-empty** good for in the theorem?

BTW: The theorem is proposition 1.1 here (applied to classical logic):

Cantor-Bernstein implies Excluded Middle
Pierre Pradic, Chad E. Brown - August 16, 2022
https://arxiv.org/pdf/1904.09193.pdf

Mostowski Collapse schrieb am Montag, 22. August 2022 um 19:23:28 UTC+2:
> Corr.:
> Which says x = {0}. But the theorem would have maybe:
> Mostowski Collapse schrieb am Montag, 22. August 2022 um 19:22:18 UTC+2:
> > Holy cow! What is this guy smoking? Tibet, Afghanistan, ...?
> >
> > Its not the theorem we want. You have as an axiom:
> > 1. ALL(a):[a in x <=> a=0]
> > Axiom
> > Which says a = {0}. But the theorem would have maybe:
> >
> > 1. EXIST(a):[a in x]
> > Axiom
> >
> > Better have it in the conclusion though. The challenge is:
> > Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
> > > Let A and B be sets and f : A → B an injective function. Suppose
> > > that **A is non-empty**. Then there exists a surjection g : B → A
> > https://groups.google.com/g/sci.math/c/T7OzU-PmpEg/m/hLscRJOtAwAJ

On Monday, August 22, 2022 at 1:22:18 PM UTC-4, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:

> > > > > Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
> > > > >
> > > [snip abuse]
> > > > There "could be":
> > > >
> > > > Surjective(_) <=> ....
> > > >
> > > > Or there "could be":
> > > >
> > > > Surjective(_,_,_) <=> ....
> > > >
> > > Or there could be no predicates whatsoever, e.g. <-------------------- See here
> > >
> > > ALL(f):[ALL(a):[a in {0} => f(a) in {0}]
> > > => ALL(a):[a in {0} => EXIST(b):[b in {0} & f(b)=a]]] <----- f is surjective
> > >
> > PROOF
> >
> > 1. ALL(a):[a in x <=> a=0]
> > Axiom
> >
> > Suppose...
> >
> > 2. ALL(a):[a in x => f(a) in x]
> > Premise
> >
> >
> > Prove: ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
> >
> > Suppose...
> >
> > 3. t in x
> > Premise
> >
> > Apply definition of x
> >
> > 4. t in x <=> t=0
> > U Spec, 1
> >
> > 5. [t in x => t=0] & [t=0 => t in x]
> > Iff-And, 4
> >
> > 6. t in x => t=0
> > Split, 5
> >
> > 7. t=0
> > Detach, 6, 3
> >
> > 8. 0 in x
> > Substitute, 7, 3
> >
> > 9. t in x => f(t) in x
> > U Spec, 2
> >
> > 10. f(t) in x
> > Detach, 9, 3
> >
> > Apply definition of x
> >
> > 11. f(t) in x <=> f(t)=0
> > U Spec, 1, 10
> >
> > 12. [f(t) in x => f(t)=0] & [f(t)=0 => f(t) in x]
> > Iff-And, 11
> >
> > 13. f(t) in x => f(t)=0
> > Split, 12
> >
> > 14. f(t)=0
> > Detach, 13, 10
> >
> > Substituting...
> >
> > 15. f(0)=0
> > Substitute, 7, 14
> >
> > 16. f(0)=t
> > Substitute, 7, 15
> >
> > 17. 0 in x & f(0)=t
> > Join, 8, 16
> >
> > 18. EXIST(b):[b in x & f(b)=t]
> > E Gen, 17
> >
> > f is surjective
> >
> > As Required:
> >
> > 19. ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
> > Conclusion, 3
> >
> > As Required:
> >
> > 20. ALL(f):[ALL(a):[a in x => f(a) in x]
> > => ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]]
> > Conclusion, 2

[snip abuse]

>
> Its not the theorem we want.

Pay attention, Jan Burse! This is just an a very simple example of how to prove a function is surjective without defining ANY predicate, unary or otherwise (an example you yourself recently put forth here) . Deal with it. Now, get busy with your formal proofs demonstrating how to use your wonky unary Surjective predicate.

Dan

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

Stop bull shitting, and posting false excuses.

Its an irrelevant example, it doesn't prove this theorem:

Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
> Let A and B be sets and f : A → B an injective function. Suppose
> that **A is non-empty**. Then there exists a surjection g : B → A
https://groups.google.com/g/sci.math/c/T7OzU-PmpEg/m/hLscRJOtAwAJ

And besides that it doesn't use this requirement:

> How can we figure out what is more clumsy, a definition:
> Surjective(_) <=>
> Or a definition as follows:
> Surjective(_,_,_) <=>

You are wasting everybodies time...

Dan Christensen schrieb am Montag, 22. August 2022 um 19:39:30 UTC+2:
> On Monday, August 22, 2022 at 1:22:18 PM UTC-4, Mostowski Collapse wrote:
>
> > Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
>
> > > > > > Why don't you do a couple of proofs for us testing each alternative. You can use the Axiom Rule on the Logic menu in DC Proof to create your own axioms for Surjective(_), dom(_), cod(_) and whatever else you might need.
> > > > > >
> > > > [snip abuse]
> > > > > There "could be":
> > > > >
> > > > > Surjective(_) <=> ....
> > > > >
> > > > > Or there "could be":
> > > > >
> > > > > Surjective(_,_,_) <=> ....
> > > > >
> > > > Or there could be no predicates whatsoever, e.g. <-------------------- See here
> > > >
> > > > ALL(f):[ALL(a):[a in {0} => f(a) in {0}]
> > > > => ALL(a):[a in {0} => EXIST(b):[b in {0} & f(b)=a]]] <----- f is surjective
> > > >
> > > PROOF
> > >
> > > 1. ALL(a):[a in x <=> a=0]
> > > Axiom
> > >
> > > Suppose...
> > >
> > > 2. ALL(a):[a in x => f(a) in x]
> > > Premise
> > >
> > >
> > > Prove: ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
> > >
> > > Suppose...
> > >
> > > 3. t in x
> > > Premise
> > >
> > > Apply definition of x
> > >
> > > 4. t in x <=> t=0
> > > U Spec, 1
> > >
> > > 5. [t in x => t=0] & [t=0 => t in x]
> > > Iff-And, 4
> > >
> > > 6. t in x => t=0
> > > Split, 5
> > >
> > > 7. t=0
> > > Detach, 6, 3
> > >
> > > 8. 0 in x
> > > Substitute, 7, 3
> > >
> > > 9. t in x => f(t) in x
> > > U Spec, 2
> > >
> > > 10. f(t) in x
> > > Detach, 9, 3
> > >
> > > Apply definition of x
> > >
> > > 11. f(t) in x <=> f(t)=0
> > > U Spec, 1, 10
> > >
> > > 12. [f(t) in x => f(t)=0] & [f(t)=0 => f(t) in x]
> > > Iff-And, 11
> > >
> > > 13. f(t) in x => f(t)=0
> > > Split, 12
> > >
> > > 14. f(t)=0
> > > Detach, 13, 10
> > >
> > > Substituting...
> > >
> > > 15. f(0)=0
> > > Substitute, 7, 14
> > >
> > > 16. f(0)=t
> > > Substitute, 7, 15
> > >
> > > 17. 0 in x & f(0)=t
> > > Join, 8, 16
> > >
> > > 18. EXIST(b):[b in x & f(b)=t]
> > > E Gen, 17
> > >
> > > f is surjective
> > >
> > > As Required:
> > >
> > > 19. ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]
> > > Conclusion, 3
> > >
> > > As Required:
> > >
> > > 20. ALL(f):[ALL(a):[a in x => f(a) in x]
> > > => ALL(a):[a in x => EXIST(b):[b in x & f(b)=a]]]
> > > Conclusion, 2
> [snip abuse]
> >
> > Its not the theorem we want.
> Pay attention, Jan Burse! This is just an a very simple example of how to prove a function is surjective without defining ANY predicate, unary or otherwise (an example you yourself recently put forth here) . Deal with it. Now, get busy with your formal proofs demonstrating how to use your wonky unary Surjective predicate.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Where do you even see {0} ?
Did you misunderstand this phrase:

**A is non-empty**

LoL

Mostowski Collapse schrieb am Montag, 22. August 2022 um 19:53:34 UTC+2:
> Stop bull shitting, and posting false excuses.
>
> Its an irrelevant example, it doesn't prove this theorem:
> Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
> > Let A and B be sets and f : A → B an injective function. Suppose
> > that **A is non-empty**. Then there exists a surjection g : B → A
> https://groups.google.com/g/sci.math/c/T7OzU-PmpEg/m/hLscRJOtAwAJ
> And besides that it doesn't use this requirement:
> > How can we figure out what is more clumsy, a definition:
> > Surjective(_) <=>
> > Or a definition as follows:
> > Surjective(_,_,_) <=>
> You are wasting everybodies time...
> Dan Christensen schrieb am Montag, 22. August 2022 um 19:39:30 UTC+2:
> > On Monday, August 22, 2022 at 1:22:18 PM UTC-4, Mostowski Collapse wrote:
> >
> > > Mostowski Collapse schrieb am Montag, 22. August 2022 um 00:03:52 UTC+2:
> > > Its not the theorem we want.
> > Pay attention, Jan Burse! This is just an a very simple example of how to prove a function is surjective without defining ANY predicate, unary or otherwise (an example you yourself recently put forth here) .

On Sunday, August 21, 2022 at 6:03:52 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:

>
> Let A and B be sets and f : A → B an injective function. Suppose
> that A is non-empty. Then there exists a surjection g : B → A
>

Posted here several weeks ago:

THEOREM

ALL(a):ALL(b):ALL(f1):[Set(a)

& EXIST(c):c in a & Set(b) <----- non-empty set

& ALL(c):[c in a => f1(c) in b] <----- function f1: a --> b

& ALL(c):ALL(d):[c in a & d in a => [f1(c)=f1(d) => c=d]] <----- f1 is injective

=> EXIST(f2):[ALL(c):[c in b => f2(c) in a] <----- function f2: b --> a

& ALL(c):[c in a => EXIST(d):[d in b & f2(d) in a]]]] <----- f2 is surjective

The proof makes use the following axioms of set theory and no others:

1. Cartesian Product Axiom
2. Subset Axiom
3. Function Axiom

No additional axioms, definitions, previous results or references to cardinalities were required.

https://dcproof.com/SurjectionFromInjection.htm (381 lines)

What have you got, Jan Burse?

Dan

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

That you didn't solve the task is also seen in the comments of
the form <----- f1 is injective, and <----- f2 is surjective, but the
task was totally different.

You should have predicates Surjective and Injective. Mostlikely
they will have the same number of proof lines, since they will
have the same number of quantifiers.

Surjective(_) will have some quantifiers after <=>:

ALL(f):[Surjective(_) <=> EXIST(dom):EXIST(cod): .... ]

Surjective(_,_,_) will have some quantifiers before <=>:

ALL(f):ALL(f):ALL(f):[Surjective(_,_,_) <=> .... ]

If every quajtifiers needs some proof step, they could
need the same number of proof steps. But Dan Christensen
said Surjective(_,_,_) is less clumsy. Can you empirically

show us that this is the case?

BTW: His less clumsy hypothesis is from here:
Dan Christensen schrieb am Mittwoch, 17. August 2022 um 20:27:51 UTC+2:
> I have tried various definitions of a surjectivity abbreviation including
your suggestion to restrict its application using the Function(f,x,y) signature,
but found it needlessly cumbersome.
https://groups.google.com/g/sci.logic/c/QSfRj2g1ur8/m/fFHeqEU7AQAJ

Where are his "trials" documented?
I still don't see some "trials".

Dan Christensen schrieb am Dienstag, 23. August 2022 um 05:07:26 UTC+2:
> On Sunday, August 21, 2022 at 6:03:52 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
>
> >
> > Let A and B be sets and f : A → B an injective function. Suppose
> > that A is non-empty. Then there exists a surjection g : B → A
> >
> Posted here several weeks ago:
>
> THEOREM
>
> ALL(a):ALL(b):ALL(f1):[Set(a)
>
> & EXIST(c):c in a & Set(b) <----- non-empty set
>
> & ALL(c):[c in a => f1(c) in b] <----- function f1: a --> b
>
> & ALL(c):ALL(d):[c in a & d in a => [f1(c)=f1(d) => c=d]] <----- f1 is injective
>
> => EXIST(f2):[ALL(c):[c in b => f2(c) in a] <----- function f2: b --> a
>
> & ALL(c):[c in a => EXIST(d):[d in b & f2(d) in a]]]] <----- f2 is surjective
>
> The proof makes use the following axioms of set theory and no others:
>
> 1. Cartesian Product Axiom
> 2. Subset Axiom
> 3. Function Axiom
>
> No additional axioms, definitions, previous results or references to cardinalities were required.
>
> https://dcproof.com/SurjectionFromInjection.htm (381 lines)
>
> What have you got, Jan Burse?
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Also dcproof17.exe has the same old bug, its unusable.
This bug was reported on sci.logic or sci.math in the past.

Try entering an axiom:

ALL(x):ALL(y):[P((x,y)) <=> Q]

It will show you:

1 ALL(x):ALL(y):[P(x,y) <=> Q]
Axiom

Mostowski Collapse schrieb am Dienstag, 23. August 2022 um 12:16:44 UTC+2:
> That you didn't solve the task is also seen in the comments of
> the form <----- f1 is injective, and <----- f2 is surjective, but the
> task was totally different.
>
> You should have predicates Surjective and Injective. Mostlikely
> they will have the same number of proof lines, since they will
> have the same number of quantifiers.
>
> Surjective(_) will have some quantifiers after <=>:
>
> ALL(f):[Surjective(_) <=> EXIST(dom):EXIST(cod): .... ]
>
> Surjective(_,_,_) will have some quantifiers before <=>:
>
> ALL(f):ALL(f):ALL(f):[Surjective(_,_,_) <=> .... ]
>
> If every quajtifiers needs some proof step, they could
> need the same number of proof steps. But Dan Christensen
> said Surjective(_,_,_) is less clumsy. Can you empirically
>
> show us that this is the case?
>
> BTW: His less clumsy hypothesis is from here:
> Dan Christensen schrieb am Mittwoch, 17. August 2022 um 20:27:51 UTC+2:
> > I have tried various definitions of a surjectivity abbreviation including
> your suggestion to restrict its application using the Function(f,x,y) signature,
> but found it needlessly cumbersome.
> https://groups.google.com/g/sci.logic/c/QSfRj2g1ur8/m/fFHeqEU7AQAJ
>
> Where are his "trials" documented?
> I still don't see some "trials".
> Dan Christensen schrieb am Dienstag, 23. August 2022 um 05:07:26 UTC+2:
> > On Sunday, August 21, 2022 at 6:03:52 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> >
> > >
> > > Let A and B be sets and f : A → B an injective function. Suppose
> > > that A is non-empty. Then there exists a surjection g : B → A
> > >
> > Posted here several weeks ago:
> >
> > THEOREM
> >
> > ALL(a):ALL(b):ALL(f1):[Set(a)
> >
> > & EXIST(c):c in a & Set(b) <----- non-empty set
> >
> > & ALL(c):[c in a => f1(c) in b] <----- function f1: a --> b
> >
> > & ALL(c):ALL(d):[c in a & d in a => [f1(c)=f1(d) => c=d]] <----- f1 is injective
> >
> > => EXIST(f2):[ALL(c):[c in b => f2(c) in a] <----- function f2: b --> a
> >
> > & ALL(c):[c in a => EXIST(d):[d in b & f2(d) in a]]]] <----- f2 is surjective
> >
> > The proof makes use the following axioms of set theory and no others:
> >
> > 1. Cartesian Product Axiom
> > 2. Subset Axiom
> > 3. Function Axiom
> >
> > No additional axioms, definitions, previous results or references to cardinalities were required.
> >
> > https://dcproof.com/SurjectionFromInjection.htm (381 lines)
> >
> > What have you got, Jan Burse?
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, August 23, 2022 at 6:16:44 AM UTC-4, Mostowski Collapse (Jan Burse) wrote:
[snip]

> You should have predicates Surjective and Injective.

Strictly speaking, we see here that they are unnecessary. Optionally, for readability, you might define the predicates Injective and Surjective at the beginning of a proof as follows:

1. ALL(f):ALL(x):ALL(y):[Injective(f,x,y) <=> ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]]
Axiom

2. ALL(f):ALL(x):ALL(y):[Surjective(f,x,y) <=> ALL(a):[a in y => EXIST(b):[b in x & f(b)=a]]]
Axiom

Then, using my proof, you could prove:

ALL(a):ALL(b):ALL(f1):[Set(a)

& EXIST(c):c in a

& Set(b)

& ALL(c):[c in a => f1(c) in b]

& Injective(f1,a,b) <----- New

=> EXIST(f2):[ALL(c):[c in b => f2(c) in a]

& Surjective(f2,b,a) ]]] <----- New

It would only take a few extra lines at the beginning and end of the proof. Most of the proof could remain unchanged. How about it, Jan Burse? You seem to have a lot of time on your hands.

Dan

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