The inventor of DC Proof recently proved, fn denotes
the function space N --> N:

162 ALL(f):[f e fn
<=> ALL(a):[a e n => f(a) e n]
& [Set'(f)
& ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
& ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]]
https://dcproof.com/FunctionsNtoN.htm

But what is the domain of discourse of function quantifiers
ALL(f) in DC Proof? Can he also prove:

EXIST(f):[f e fn] ?

If yes, what kind of function f : N --> N is such a function,
when we can also prove EXIST(x):[f(f)=x] in DC Proof.

The later I guess only is possible in the bombastic function
spaces of DC Proof, doesn't it imply f e n. I wouldn't know that

this is possible for text book f : N --> N.

On Wednesday, July 7, 2021 at 3:37:06 AM UTC-4, Mostowski Collapse wrote:
> The inventor of DC Proof recently proved, fn denotes
> the function space N --> N:
>
> 162 ALL(f):[f e fn
> <=> ALL(a):[a e n => f(a) e n]
> & [Set'(f)
> & ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
> & ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]]
> https://dcproof.com/FunctionsNtoN.htm
>
> But what is the domain of discourse of function quantifiers
> ALL(f) in DC Proof?

As in most math textbooks, there is no notion of a overarching "domain of discourse" in DC Proof.

> Can he also prove:
>
> EXIST(f):[f e fn] ?
>

The set f= {(a,b) in n^2: a=b} should do nicely.

> If yes, what kind of function f : N --> N is such a function,

It would be the identity function f(x)=x.

> when we can also prove EXIST(x):[f(f)=x] in DC Proof.
>

I doubt you can construct such a function on N, but you can give it try. You would probably have to introduce some wonky axiom, but note that DC Proof does not check axioms introduced by the user for consistency. You could even introduce A & ~A as an axiom just to see what happens.

Dan

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

On Wednesday, July 7, 2021 at 3:37:06 AM UTC-4, Mostowski Collapse wrote:
> The inventor of DC Proof recently proved, fn denotes
> the function space N --> N:
>
> 162 ALL(f):[f e fn
> <=> ALL(a):[a e n => f(a) e n]
> & [Set'(f)
> & ALL(a1):ALL(b):[(a1,b) e f => a1 e n & b e n]
> & ALL(a1):ALL(b):[a1 e n & b e n => [f(a1)=b <=> (a1,b) e f]]]]
> https://dcproof.com/FunctionsNtoN.htm
>
> But what is the domain of discourse of function quantifiers
> ALL(f) in DC Proof?

As in most math textbooks, there is no notion of a overarching "domain of discourse" in DC Proof.

Note that on line 19, I define fn as follows:

ALL(a):[a in fn <=> a in pn2 & ALL(b):[b in n => EXIST(c):[c in n & (b,c) in a & ALL(d):[d in n => [(b,d) in a => d=c]]]]]

> Can he also prove:
>
> EXIST(f):[f e fn] ?
>

On line 19, I define fn as follows:

ALL(a):[a in fn <=> a in pn2 & ALL(b):[b in n => EXIST(c):[c in n & (b,c) in a & ALL(d):[d in n => [(b,d) in a => d=c]]]]]

The set f= {(a,b) in n^2: a=b} should do nicely as an example.

> If yes, what kind of function f : N --> N is such a function,

It would be the identity function f(x)=x.

> when we can also prove EXIST(x):[f(f)=x] in DC Proof.
>

I doubt you can construct such a function on N, but you can give it try. You would probably have to introduce some wonky axiom, but note that DC Proof does not check axioms introduced by the user for consistency. You could even introduce A & ~A as an axiom just to see what happens.

Dan

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