The new release of DC Proof 2.0 freeware, dated today, has a revised Function Axiom. The Functions Spaces axiom has been withdrawn as it can be show that every set X and Y, there exists a set of graphs (ordered pairs), each of which corresponds a function mapping X to Y.

ALL(x):ALL(y):[Set(x) & Set(y)
=> EXIST(graphs):[Set(graphs)
& ALL(g):[g in graphs
<=> 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]]]]

& ALL(g):[g in graphs
=> EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in y
=> [fun(a1)=b <=> (a1,b) in g]]]]]

https://www.dcproof.com/FunctionGraphSets.htm (98 lines)

Dan

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

Still bollocks.
How many funs are there if x={0} and y={0}.
The same many as gs?

Dan Christensen schrieb am Dienstag, 25. Januar 2022 um 18:36:08 UTC+1:
> The new release of DC Proof 2.0 freeware, dated today, has a revised Function Axiom. The Functions Spaces axiom has been withdrawn as it can be show that every set X and Y, there exists a set of graphs (ordered pairs), each of which corresponds a function mapping X to Y.
>
> ALL(x):ALL(y):[Set(x) & Set(y)
> => EXIST(graphs):[Set(graphs)
> & ALL(g):[g in graphs
> <=> 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]]]]
>
> & ALL(g):[g in graphs
> => EXIST(fun):ALL(a1):ALL(b):[a1 in x & b in y
> => [fun(a1)=b <=> (a1,b) in g]]]]]
>
> https://www.dcproof.com/FunctionGraphSets.htm (98 lines)
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

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

On Tuesday, January 25, 2022 at 8:40:38 PM UTC-5, Mostowski Collapse wrote:

> How many funs are there if x={0} and y={0}.
> The same many as gs?

> Dan Christensen schrieb am Dienstag, 25. Januar 2022 um 18:36:08 UTC+1:
> > The new release of DC Proof 2.0 freeware, dated today, has a revised Function Axiom. The Functions Spaces axiom has been withdrawn as it can be show that every set X and Y, there exists a set of graphs (ordered pairs), each of which corresponds a function mapping X to Y.
....

Dan Christensen wrote:

> The new release of DC Proof 2.0 freeware, dated today, has a revised
> Function Axiom. The Functions Spaces axiom has been withdrawn as it can
> be show that every set X and Y, there exists a set of graphs (ordered
> pairs),

yes, sure, absolutely. But this trucker convoy has to start
*NOT_singing*, protesting, wherever they go. They have to *ARREST* the
*corrupt_government*, the *mass_murderers*, *ARREST* the directly
complicit *national_media*, the *TV* etc,

THEN they can start singing. Otherwise, NOTHING at all will happen. And
most probably, *extermination_covid_19_camps*

TRUCKERS CONVOY FOR FREEDOM AND AGAINST DICTATOR JUSTIN TRUDEAU AND COVID
TYRANNY https://www.bitchute.com/video/cFEDROcXQcDe/

it wasn't clear for me how to circumvent the
new restrictions of (forall) that are already present for
a while in DC Proof. But in the end it was very easy.

From Wolfgang Schartz proof I saw we needed to substitute
f(c) in (forall), but DC Proof will not allow to substitute
f(c) in (forall) unless there is also some f(c) e S:

(¬EcN ∧ ∀a∀b(f(a)=b ↔ (EaN ∧ (EbN ∧ a=b)))) → f(c)=c is valid.
https://www.umsu.de/trees/#~3EcN~1~6a~6b%28f%28a%29=b~4EaN~1EbN~1a=b%29~5f%28c%29=c

So how circumvent the problem? Well just assume
there exists some d with f(c)=d and then try something.
Ok I didn't arrive at f(c)=c as planned, but this here

could remove the new block in (forall):

16 EXIST(d):f(c)=d
Premise

17 f(c)=e
E Spec, 16

18 ALL(b):[f(c)=b <=> c ε n & b ε n & c=b]
U Spec, 3

19 f(c)=e <=> c ε n & e ε n & c=e
U Spec, 18

Lessons learnt? Dont tweak (forall) without
tweaking its dual, the (exists).

LoL

Another lesson could be, FOL function symbols are
not partial functions. They are total functions.

It needs a little bit more than only tweaking (forall)
in a ad-hoc manner to make them partial.

See for example:

Definedness, Dedicated to Alonzo Church
Solomon Feferman - 1995
https://math.stanford.edu/~feferman/papers/definedness.pdf

The paper is a little sloppy in its second part,
it has also its bugs in my opinion.

Mostowski Collapse schrieb am Samstag, 29. Januar 2022 um 00:56:03 UTC+1:
> it wasn't clear for me how to circumvent the
> new restrictions of (forall) that are already present for
> a while in DC Proof. But in the end it was very easy.
>
> From Wolfgang Schartz proof I saw we needed to substitute
> f(c) in (forall), but DC Proof will not allow to substitute
> f(c) in (forall) unless there is also some f(c) e S:
>
> (¬EcN ∧ ∀a∀b(f(a)=b ↔ (EaN ∧ (EbN ∧ a=b)))) → f(c)=c is valid.
> https://www.umsu.de/trees/#~3EcN~1~6a~6b%28f%28a%29=b~4EaN~1EbN~1a=b%29~5f%28c%29=c
>
> So how circumvent the problem? Well just assume
> there exists some d with f(c)=d and then try something.
> Ok I didn't arrive at f(c)=c as planned, but this here
>
> could remove the new block in (forall):
>
> 16 EXIST(d):f(c)=d
> Premise
>
> 17 f(c)=e
> E Spec, 16
>
> 18 ALL(b):[f(c)=b <=> c ε n & b ε n & c=b]
> U Spec, 3
>
> 19 f(c)=e <=> c ε n & e ε n & c=e
> U Spec, 18
>
> Lessons learnt? Dont tweak (forall) without
> tweaking its dual, the (exists).
>
> LoL

On Friday, January 28, 2022 at 6:56:03 PM UTC-5, Mostowski Collapse wrote:
> it wasn't clear for me how to circumvent the
> new restrictions of (forall) that are already present for
> a while in DC Proof. But in the end it was very easy.
>
> From Wolfgang Schartz proof I saw we needed to substitute
> f(c) in (forall), but DC Proof will not allow to substitute
> f(c) in (forall) unless there is also some f(c) e S:
>
> (¬EcN ∧ ∀a∀b(f(a)=b ↔ (EaN ∧ (EbN ∧ a=b)))) → f(c)=c is valid.
> https://www.umsu.de/trees/#~3EcN~1~6a~6b%28f%28a%29=b~4EaN~1EbN~1a=b%29~5f%28c%29=c
>
> So how circumvent the problem? Well just assume
> there exists some d with f(c)=d and then try something.
> Ok I didn't arrive at f(c)=c as planned, but this here
>
> could remove the new block in (forall):
>
> 16 EXIST(d):f(c)=d
> Premise
>
> 17 f(c)=e
> E Spec, 16
>
> 18 ALL(b):[f(c)=b <=> c ε n & b ε n & c=b]
> U Spec, 3
>
> 19 f(c)=e <=> c ε n & e ε n & c=e
> U Spec, 18
>
> Lessons learnt?

You can introduce any premise or axiom you like, as long as it is syntactically correct. They can even be self-contradictory. There is no filter for wonky premises or axioms in DC Proof (e.g. your lines 3, 4 and 16). As you can see, it didn't pay off for you in the end here. You just end up looking ridiculous. (Hee, hee!)

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, January 28, 2022 at 7:01:37 PM UTC-5, Mostowski Collapse wrote:
> Another lesson could be, FOL function symbols are
> not partial functions. They are total functions.
>

That's too bad. You may need partial functions, too. (If a partial function is defined for some element of its domain, it's image must be unique.) You may also need different functions with different domains even within a single statement in a proof. You may also need to quantify over functions. All weak points for standard FOL, I'm afraid.

Dan

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

The proper math textbook definition is:

ALL(a):ALL(b):[(a,b) e f <=> a in N & b in N & a=b]

This the proper definition of f : N -> N and identity function.
It doesn't lead to an inconsistency, and you can prove:

EXISTUNIQUE(f):ALL(a):ALL(b):[(a,b) e f <=> a in N & b in N & a=b]

Because its a simple comprehension.

Dan Christensen schrieb am Samstag, 29. Januar 2022 um 06:56:22 UTC+1:
> On Friday, January 28, 2022 at 7:01:37 PM UTC-5, Mostowski Collapse wrote:
> > Another lesson could be, FOL function symbols are
> > not partial functions. They are total functions.
> >
> That's too bad. You may need partial functions, too. (If a partial function is defined for some element of its domain, it's image must be unique.) You may also need different functions with different domains even within a single statement in a proof. You may also need to quantify over functions. All weak points for standard FOL, I'm afraid.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com.

On Saturday, January 29, 2022 at 7:37:09 AM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> The proper math textbook definition is:
>
> ALL(a):ALL(b):[(a,b) e f <=> a in N & b in N & a=b]
>

You are a shameless liar, Jan Burse.

See my reply just now to your posting on this topic in another thread at sci.math.

Dan

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

The problem is, you cannot prove:

EXISTUNIQUE(f):ALL(a): ALL(b): [a in N & b in N => [ f(a)=b <=> a=b ]]

Same, you cannot prove:

EXISTUNIQUE(f):ALL(a): [a in N => f(a)=a]

So they are not valid definitions of f : N -> N identity function.
Because there is only one such functions, and not many.

Dan Christensen schrieb am Samstag, 29. Januar 2022 um 15:10:29 UTC+1:
> On Saturday, January 29, 2022 at 7:37:09 AM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> > The proper math textbook definition is:
> >
> > ALL(a):ALL(b):[(a,b) e f <=> a in N & b in N & a=b]
> >
> You are a shameless liar, Jan Burse.
>
> See my reply just now to your posting on this topic in another thread at sci.math.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com