Equivalent in DC Proof of the ZFC Axiom Schema of Replacement

[Dan Christensen]

Some interest has been expressed here in a DC Proof equivalent of the ZFC Axiom Schema of Replacement. Here is my suggestion:

ALL(a):[Set(a) & ALL(b):[b in a => EXIST(c):ALL(d):[P(b,d) <=> d=c]]

=> EXIST(b):[Set(b) & ALL(c):[c in b <=> EXIST(d):[d in a & P(d,c)]]]]

where P is a binary predicate (a functional relation). This statement can introduced as an axiom at the beginning of a proof using the Create Axiom option on the Logic menu on the main screen of DC Proof.

Comments?

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]

Try it with this challenge:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

If you remove the s≠0 spice you can show that the
axiom of replacement implies the axiom of collection.

Do you know whether DC Proof stays consistent
when you add this axiom schema? Usually you

need a side condition that b doesn't occur in P().

See also:
but B is not free in ϕ.
https://en.wikipedia.org/wiki/Axiom_schema_of_replacement

[Dan Christensen]

On Friday, November 26, 2021 at 2:47:15 PM UTC-5, Mostowski Collapse wrote:
> Try it with this challenge:
>

> > s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

THEOREM

Suppose x is a non-empty set, and P is a functional relation with domain x and unspecified codomain and range. Apply the Replacement Axiom to construct the range of P over x. Then that range is non-empty.

ALL(x):[Set(x) & EXIST(a):a in x

=> [ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]

=> EXIST(y):[Set(y) & ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]]

& EXIST(a):a in y]]]


Axiom of Replacement (after ZFC)

1 ALL(a):[Set(a) & ALL(b):[b in a => EXIST(c):ALL(d):[P(b,d) <=> d=c]]

=> EXIST(b):[Set(b) & ALL(c):[c in b <=> EXIST(d):[d in a & P(d,c)]]]]

Axiom


PROOF

Let x be a non-empty set

2 Set(x) & EXIST(a):a in x
Premise

Let P be a functional relation with domain x

3 ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]
Premise

Apply Replacement Axiom

4 Set(x) & ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]
=> EXIST(b):[Set(b) & ALL(c):[c in b <=> EXIST(d):[d in x & P(d,c)]]]
U Spec, 1

5 Set(x)
Split, 2

6 EXIST(a):a in x
Split, 2

7 Set(x)
& ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]
Join, 5, 3

8 EXIST(b):[Set(b) & ALL(c):[c in b <=> EXIST(d):[d in x & P(d,c)]]]
Detach, 4, 7

Define: y (The range of P over x)

9 Set(y) & ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]]
E Spec, 8

10 Set(y)
Split, 9

11 ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]]
Split, 9

12 x0 in x
E Spec, 6

Apply functionality of P

13 x0 in x => EXIST(c):ALL(d):[P(x0,d) <=> d=c]
U Spec, 3

14 EXIST(c):ALL(d):[P(x0,d) <=> d=c]
Detach, 13, 12

Define: y0 (The image of x0 under P)

15 ALL(d):[P(x0,d) <=> d=y0]
E Spec, 14

Apply definition of y

16 y0 in y <=> EXIST(d):[d in x & P(d,y0)]
U Spec, 11

17 [y0 in y => EXIST(d):[d in x & P(d,y0)]]
& [EXIST(d):[d in x & P(d,y0)] => y0 in y]
Iff-And, 16

18 y0 in y => EXIST(d):[d in x & P(d,y0)]
Split, 17

Sufficient: For y0 in y

19 EXIST(d):[d in x & P(d,y0)] => y0 in y
Split, 17

Apply definition of y0

20 P(x0,y0) <=> y0=y0
U Spec, 15

21 [P(x0,y0) => y0=y0] & [y0=y0 => P(x0,y0)]
Iff-And, 20

22 y0=y0 => P(x0,y0)
Split, 21

23 y0=y0
Reflex

24 P(x0,y0)
Detach, 22, 23

Joining results...

25 x0 in x & P(x0,y0)
Join, 12, 24

26 EXIST(d):[d in x & P(d,y0)]
E Gen, 25

27 y0 in y
Detach, 19, 26

28 EXIST(a):a in y
E Gen, 27

29 Set(y) & ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]]
& EXIST(a):a in y
Join, 9, 28

As Required:

30 ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]
=> EXIST(y):[Set(y) & ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]]
& EXIST(a):a in y]
Conclusion, 3

As Required:

31 ALL(x):[Set(x) & EXIST(a):a in x
=> [ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]
=> EXIST(y):[Set(y) & ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]]
& EXIST(a):a in y]]]
Conclusion, 2

[Mostowski Collapse]

And how about this, still unsolved in DC poop:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:

> Or formally, s≠0 stands for EXIST(c):[c e s]:

> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

ZFC does not require ϕ to be a user predicate prime formula P(b,d),
it can be any formula. As long as you can prove the precondition,
that the formula is functional.

You didn't read past the first paragraph of wiki?
The next paragraph says formula ϕ:

"Because it is impossible to quantify over definable functions in
first-order logic, one instance of the schema is included for each
**formula ϕ** in the language of set theory with free variables among
w 1 , … , w n , A , x , y"
https://en.wikipedia.org/wiki/Axiom_schema_of_replacement#Statement

[Mostowski Collapse]

Also what the heck, where does <=> come from?

31 ALL(x):[Set(x) & EXIST(a):a in x
=> [ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]

=> EXIST(y):[Set(y) & ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]] /** here **/

& EXIST(a):a in y]]]

Do you see any <=> in my problem?

[Dan Christensen]

> ZFC does not require ϕ to be a user predicate prime formula P(b,d),

A predicate works just fine.

> it can be any formula. As long as you can prove the precondition,
> that the formula is functional.
>

The precondition ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]] works. This is from an axiom schema, a single instance.

[Dan Christensen]

On Friday, November 26, 2021 at 5:03:23 PM UTC-5, Mostowski Collapse wrote:
> Also what the heck, where does <=> come from?
> 31 ALL(x):[Set(x) & EXIST(a):a in x
> => [ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]
> => EXIST(y):[Set(y) & ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]] /** here **/
> & EXIST(a):a in y]]]
> Do you see any <=> in my problem?

I have seen it both ways at Wiki (=> and <=>). If you want to use the other version, go right ahead.

[Mostowski Collapse]

Since he bought a hammock for his office,
he doesn't do much math recently. Zzz Zzz

My theorem doen't work with <=>:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

For example if f(0)=1, f(1)=2, f(2)=0 and a = {0,1}.

[Mostowski Collapse]

Corr.:
For example if f(0)=1, f(1)=2, f(2)=1 and a = {0,1}.

I guess this tool will find a counter model for <=>:
https://www.umsu.de/trees/

Didn't try yet. Should I try?

[Mostowski Collapse]

Woa, cool, the tree tool found some counter model.

Here what the problem is with => that can be proved:

Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 08:41:20 UTC+1:
> Here is a tableaux proof of the theorem in FOL+ZF, using Exy for x e y:
> ∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is valid.
> https://www.umsu.de/trees
> The LHS is an instance of the axiom schema of replacement from ZF.
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/mU9GF5PiBAAJ

And here what Dan-O-Matik thinks can be proved with <=>, but it cant:

∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza ↔ ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is invalid.
Countermodel:
Domain: { 0, 1 }
f: { (0,0) }
E: { (0,1) }

Now the problem is that the counter model is not a set
model. Elements from the domain of discourse are simply
numbered, and some E relation is invented.

Hm. 0={} and 1={{}}, it would actually be a smaller counter
model than the one I had in mind. Pitty the tool doesn't show
a counter model justification.

So why is ALL(x):[x e a => f(x) e b] and ALL(x):[x e a <=> f(x) e b]
not the same? Can you imagine?

What we know for sure is that the <=> formula is not
provable from the particular axiom schema of replacement
instance, and if at all, would need more axioms.

But I think it is not provable at all in ZFC. Since there are
functions which are not injective. If you it a value where the
function is not injective the <= direction can fail,

since the preimage of the image might fall out of the set a.

[Dan Christensen]

On Tuesday, November 30, 2021 at 2:50:40 PM UTC-5, Mostowski Collapse wrote:
> Woa, cool, the tree tool found some counter model.
>
> Here what the problem is with => that can be proved:
>
> Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 08:41:20 UTC+1:
> > Here is a tableaux proof of the theorem in FOL+ZF, using Exy for x e y:
> > ∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is valid.
> > https://www.umsu.de/trees
> > The LHS is an instance of the axiom schema of replacement from ZF.
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/mU9GF5PiBAAJ
>
> And here what Dan-O-Matik thinks can be proved with <=>, but it cant:
>
> ∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza ↔ ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b)))

Doesn't look much like:

ALL(a):[Set(a) & ALL(b):[b in a => EXIST(c):ALL(d):[P(b,d) <=> d=c]]
=> EXIST(b):[Set(b) & ALL(c):[c in b <=> EXIST(d):[d in a & P(d,c)]]]]

=>ALL(x):[Set(x)

& EXIST(a):a in x
=> [ALL(b):[b in x => EXIST(c):ALL(d):[P(b,d) <=> d=c]]
=> EXIST(y):[Set(y) & ALL(c):[c in y <=> EXIST(d):[d in x & P(d,c)]]

& EXIST(a):a in y]]]

Keep trying, Jan Burse.

[Mostowski Collapse]

I agree, what you prove so far isn't what was asked.
Well the challenge was to prove:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

It is still not proved by DC Proof. And when you replace the second
(=>) by (<=>) you get something that isn't provable.

[Dan Christensen]

On Tuesday, November 30, 2021 at 4:51:45 PM UTC-5, Mostowski Collapse wrote:
> I agree, what you prove so far isn't what was asked.
> Well the challenge was to prove:
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> It is still not proved by DC Proof. And when you replace the second
> (=>) by (<=>) you get something that isn't provable.

It's a biconditional, Jan Burse. Check it out:

https://en.wikipedia.org/wiki/Axiom_schema_of_replacement
https://proofwiki.org/wiki/Axiom:Axiom_of_Replacement

Dan

[Dan Christensen]

Maybe there is a bug in The Proof Tree Generator and it has gone into an infinite loop, but this has been running for hours:

∀a((Sa ∧ ∀b(Eba → ∃c∀d(Pbd ↔ d=c))) → (∃b(Sb ∧ ∀c(Ecb ↔ ∃d(Eda ∧ Pdc))))) → ∀x((Sx ∧ ∃aEax) → (∀b(Ebx → ∃c∀d(Pbd ↔ d=c)) → ∃y(Sy ∧ (∀c(Ecy ↔ ∃d(Edx ∧ Pdc)) ∧ ∃aEay))))

[Dan Christensen]

So far: "step 141411 alternative 8690, 79 nodes, model size 2"

[Dan Christensen]

Currently: "step 144785 alternative 8880, 77 nodes, model size 2"

[Dan Christensen]

Jan, maybe you can try it on your computer. I had made several failed ("invalid") attempts prior to starting this one. Maybe a field got corrupted causing an infinite loop? I don't want to start over at this point (still going).

[Dan Christensen]

Stopped it after about 12 hours.

Output: "step 159960 alternative 9895, 83 nodes, model size 2"

Obviously TPG cannot handle a statement of this size. It took maybe 10 minutes to do it manually in DC Proof.

[Dan Christensen]

Trying it without the "is a set" predicate S.

[Jim Burns]

I think that you're working with, from wikipedia,
∀A([∀x∈A,∃!y,ϕ(x,y,A)] ⟹ ∃B∀y[y∈B ⇔ ∃x∈A,ϕ(x,y,A)])

or, as I'd rather see it,
∀A( ∀x∈A,∃!y = ϕ(x,A) ⟹ ∃B = { ϕ(x,A) | x∈A } )

Making it Proof-Tree-compatible, I get
∀a(
( ∀x(Exa→∃y( Pxy∧∀u(Pxu→u=y) )) )
→∃b
∀y(Eyb ↔ ∃x(Exa∧Pxy))
)

or
∀a((∀x(Exa→∃y(Pxy∧∀u(Pxu→u=y))))→∃b∀y(Eyb↔∃x(Exa∧Pxy)))

With this, Proof Tree gives me pretty much an instant response.
Neither this nor its negation are valid, and counter-models
are given.

Since this is intended to be an axiom, this is a
desirable state of affairs. The point of asserting
∀a((∀x(Exa→∃y(Pxy∧∀u(Pxu→u=y))))→∃b∀y(Eyb↔∃x(Exa∧Pxy)))
would be to distinguish certain models as a topic of
discussion. If the assertion was true for all or (horrors)
false for all, there'd be no point in asserting it.

I'm curious why you're doing things the way you are.
∃c∀d(Pbd ↔ d=c)
is supposed to be
∃!c(Pbc)

Isn't it?
Why that and not
∃c(Pbc∧∀d(Pbd→d=c))

Why did you add assertions about set-hood
and non-emptiness?

A stylistic suggestion:
Why not use names a,b,c,... for sets
and names u,v,x,y,z,... as elements?

Also: PLEASE use more whitespace, to assist
non-mechanical parsers (eg, H.sapiens).

[Dan Christensen]

The purpose of this whole exercise was to demonstrate how one might implement an axiom of replacement (from ZFC) in my DC Proof program and to demonstrate its application with some trivial proof, e.g. if the domain is non-empty, then so is the codomain.

The only quantifiers supported in DC Proof are the usual universal and existential quantifiers, ALL( ) and EXIST( ). It supporters functional notation, but f(x) must be declared to be an element of a set, not just an arbitrary operator. This avoids some bizarre results.

> Why that and not
> ∃c(Pbc∧∀d(Pbd→d=c))
>

That would work, too.

> Why did you add assertions about set-hood
> and non-emptiness?
>

The trivial theorem was Jan's choice. It's strange how it gives The Tree Proof Generator such a hard time.

> A stylistic suggestion:
> Why not use names a,b,c,... for sets
> and names u,v,x,y,z,... as elements?
>

I usually try to use a-k for variables nd

> Also: PLEASE use more whitespace, to assist
> non-mechanical parsers (eg, H.sapiens).

Stupidly, Google Groups recently automatically eliminated "extraneous" spaces in postings. It makes the text version of my proofs look like hell. The HTML version of my proofs are much more readable with lots of whitespace and different colours and sizes of fonts. If the proof is not too long, I thought readers an be more likely to read inline proofs to facilitate comments rather than click on a link. It also takes some time to upload the HTML to my website.

[Jim Burns]

On 12/1/2021 5:06 PM, Dan Christensen wrote:
> On Wednesday, December 1, 2021 at 3:13:39 PM UTC-5,
> Jim Burns wrote:

>> I'm curious why you're doing things the way you are.
>> ∃c∀d(Pbd ↔ d=c)
>> is supposed to be
>> ∃!c(Pbc)
>>
>> Isn't it?
>
> The purpose of this whole exercise was to demonstrate how
> one might implement an axiom of replacement (from ZFC)
> in my DC Proof program and to demonstrate its application
> with some trivial proof, e.g. if the domain is non-empty,
> then so is the codomain.
>
> The only quantifiers supported in DC Proof are the usual
> universal and existential quantifiers, ALL( ) and EXIST( ).
> It supporters functional notation, but f(x) must be
> declared to be an element of a set, not just an arbitrary
> operator. This avoids some bizarre results.

Declaring the value of f(x) to be an element of a set
_before_ one uses Replacement seems to defeat the purpose
of Replacement -- declaring not-otherwise-declared sets
to exist.

My understanding is that using Replacement &Co. avoids
the bizarre results. I refer to the Replacement-that-
-declares-new-sets Replacement.

[Mostowski Collapse]

You are confusing the axiom with what I want to prove.
What I want to prove has no <=>. It has only =>.
You know proofs start with axioms and then end with
what one wants to prove. Then one can say Heureka, Q.E.D.

There is still no Heureka, Q.E.D. for my ALL(a):[a≠0 =>
EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]. But it is clearly
beginner math. Isn't DC Proof a beginner tool? And isn't
set theory what beginners should learn?

[Mostowski Collapse]

Beginners should learn notions such as "surjective" and
"injective", how do you define these without set theory?

That ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]
isn't provable has also to do with beginner notions.

[Jim Burns]

On 12/1/2021 5:06 PM, Dan Christensen wrote:

> On Wednesday, December 1, 2021 at 3:13:39 PM UTC-5,
> Jim Burns wrote:

>> ∃c∀d(Pbd ↔ d=c)
>> is supposed to be
>> ∃!c(Pbc)
>>
>> Isn't it?

>> Why that and not
>> ∃c(Pbc∧∀d(Pbd→d=c))
>
> That would work, too.

It needs saying, I think, because I thought it
might be otherwise;

∃c∀d(Pbd ↔ d=c) and ∃c(Pbc ∧ ∀d(Pbd → d=c))
are equivalent.

I popped
∃c∀d(Pbd↔d=c)↔∃c(Pbc∧∀d(Pbd→d=c))
into the Tree Proof Generator, and it came up "valid".
It's a nice little proof, 40 steps, 7 branches.

[Dan Christensen]

My understanding of the axiom of replacement in ZFC is that, given any set and functional predicate on that set (the domain set), we can infer the existence of a range set of the function.

[Dan Christensen]

On Wednesday, December 1, 2021 at 7:31:05 PM UTC-5, Mostowski Collapse wrote:
> You are confusing the axiom with what I want to prove.

No, I provided a ZFC-like axiom with which to prove what you requested. It's a trivial, 10 minute exercise in DC Proof, but it seems to be an intractable problem for the TPG. It went on for several hours without finding a proof or countermodel. Very interesting.

[Dan Christensen]

On Wednesday, December 1, 2021 at 7:33:25 PM UTC-5, Mostowski Collapse wrote:
> Beginners should learn notions such as "surjective" and
> "injective", how do you define these without set theory?
>

F is a functional predicate:

1 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]]]
Axiom

F is an injective predicate:

2 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]]]
& ALL(a):ALL(b):ALL(c):[P(a) & P(b) & Q(c) => [F(a,c) & F(b,c) => a=b]]
Axiom

F is an surjective predicate:

3 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]]]
& ALL(a):[Q(a) => EXIST(b):[P(b) & F(b,a)]]
Axiom

> That ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]

I have already proven here that, given a function with a non-empty domain set, it will have a non-empty range set if that's what you mean.

[Mostowski Collapse]

Its indeed a nice tool, it can proove what DC poop
didn't demonstrate yet, namely my problem
ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]].

Try this:

Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 08:41:20 UTC+1:
> Here is a tableaux proof of the theorem in FOL+ZF, using Exy for x e y:
> ∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is valid.
> https://www.umsu.de/trees
> The LHS is an instance of the axiom schema of replacement from ZF.
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/mU9GF5PiBAAJ

[Mostowski Collapse]

There is a third option for ∃!x A(x), split it
up into two independent verifications:

/* existence */
∃xA(x)
/* uniqueness */
∀x∀y(A(x) & A(y) → x = y)

For my problem, ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
we would need to verify ∀y∃!x f(y)=x, we would then be licenced
to deploy the axiom schema of replacement.

So far on 25. November 2021 I did not do this verification. But we
can also do this verification quickly with the tree tool. Namely
here, we can indeed verify the two:

/* existence */
∀y∃xf(y)=x is valid.
https://www.umsu.de/trees

/* uniqueness */
∀y∀x∀z((f(y)=x ∧ f(y)=z) → x=z) is valid.
https://www.umsu.de/trees

[Mostowski Collapse]

Q and P are not sets. But the classical surjective and injective
works with set like domains and codomains.

See wikipedia:
Given a function f : X → Y
https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection

> I have already proven here that, given a function

No you didn't prove given a function f, you proved given
a predicate P, which is functional, inside a logic calculus.
My problem addresses FOL function symbols f : V -> V,

and not predicates P, which are functional. You might
"think" in your mind that they are the same. But I want
to "see" something working on the computer.

I don't want to do Dan-O-Matik jumping to conclusions,
if it works for this then it works also for this. You already
wrongly claimed that my theorem works for "<=>".

But my theorem cannot be proved if you replace the
second "=>" by "<=>". I want to do exact science and not
some WM handwaving. Dan-O-Matik has become the

second WM, only with extra steps by his DC poop.

[Dan Christensen]

On Thursday, December 2, 2021 at 7:32:29 AM UTC-5, Mostowski Collapse wrote:

> second WM, only with extra steps by his DC poop.
> Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 06:07:30 UTC+1:
> > On Wednesday, December 1, 2021 at 7:33:25 PM UTC-5, Mostowski Collapse wrote:
> > > Beginners should learn notions such as "surjective" and
> > > "injective", how do you define these without set theory?
> > >
> > F is a functional predicate:
> >
> > 1 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]]]
> > Axiom
> >
> > F is an injective predicate:
> >
> > 2 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]]]
> > & ALL(a):ALL(b):ALL(c):[P(a) & P(b) & Q(c) => [F(a,c) & F(b,c) => a=b]]
> > Axiom
> >
> > F is an surjective predicate:
> >
> > 3 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]]]
> > & ALL(a):[Q(a) => EXIST(b):[P(b) & F(b,a)]]
> > Axiom
> > > That ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]
> > I have already proven here that, given a function with a non-empty domain set, it will have a non-empty range set if that's what you mean.

> Q and P are not sets. But the classical surjective and injective
> works with set like domains and codomains.
>

As we can see here, it also works in first-order predicate logic. Set theory, however, allows you to quantify over functions, FOPL does not.

> See wikipedia:
> Given a function f : X → Y
> https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection

> > I have already proven here that, given a function

> No you didn't prove given a function f, you proved given
> a predicate P, which is functional, inside a logic calculus.

P, in that case, was a functional predicate. If you assumed or proven the existence of the required domain and codomain sets, the corresponding set-theoretic function can be easily constructed.

> My problem addresses FOL function symbols f : V -> V,
>
> and not predicates P, which are functional.

Your "universal set" V is problematic in set theory. IIUC it requires additional axioms (in addition to ZFC) to formally obtain the required results.

You might
> "think" in your mind that they are the same. But I want
> to "see" something working on the computer.
>
> I don't want to do Dan-O-Matik jumping to conclusions,
> if it works for this then it works also for this. You already
> wrongly claimed that my theorem works for "<=>".
>

You are grasping at straws here, Jan Burse. In ZFC, the replacement axiom uses a biconditional to define what might be called the range set of the given function. Deal with it.

Perhaps, you didn't know, but every set is a superset of itself. And if A <=> B, then A => B. I hope this helps.

[Mostowski Collapse]

Dan-O-Matik halucinated:

> Your "universal set" V is problematic in set theory. IIUC it requires
additional axioms (in addition to ZFC) to formally obtain the required
results.

I am not using some universal set. I am using
a predicate like you did here, which is BTW wrong:

>>> F is a functional predicate: >>> 1 ALL(a):[P(a) => EXIST(b):[Q(b) & ALL(c):[Q(c) => [F(a,c) => c=b]]
>>> Axiom

Just use for P and Q, this V, with the following
definition:

ALL(a):(V(a) <=> a=a)

[Mostowski Collapse]

Now you can prove for every function symbol f from FOL,
that f is functional f : V -> V, where V is the universal class:

ALL(a):[V(a) => EXIST(b):[V(b) & ALL(c):[V(c) => [f(a)=c => c=b]]

Thats an easy exercise, which even the tree tool can
automaticaly manage. See for yourself:

∀a(Va ↔ a=a) → ∀a(Va → ∃b(Vb ∧ ∀c(Vc → (f(a)=c → c=b)))) is valid.
https://www.umsu.de/trees

Mostowski Collapse schrieb:

[Mostowski Collapse]

But you need a better definition of functional, so that
this blooper doesn't happen, from F : {0} -> {0} to
not be able to prove 1<>0 => ~F(1,0).

DC poop is heavily challenged by beginner math
https://groups.google.com/g/sci.logic/c/170wZq-W9Dw/m/leO8xnYaBwAJ

I dont mind when for F : X -> Y the X and Y are also allowed to
be classes. Your axiom didn't exclude classes. But it has another
bug, the aforementioned blooper.

My original questions was can we defined notions such
as injective and surjective without set theory? What is the
answer exactly now?

When I introduce my original image question, you cited
Wikipedia, and somehow insisted on set-like functions.
Now you have a "function" axiom where nothing

is required to be set like. Howdy how! The DC poop
world seem to be very fickle.

[Dan Christensen]

On Thursday, December 2, 2021 at 3:02:39 PM UTC-5, Mostowski Collapse wrote:
> But you need a better definition of functional, so that
> this blooper doesn't happen, from F : {0} -> {0} to
> not be able to prove 1<>0 => ~F(1,0).
>

Wrong again, Jan Burse. As we see here, there is more to a function that a set of ordered pairs.

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)

[Mostowski Collapse]

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

[Mostowski Collapse]

Try proving this here:

| n->2 | = 2^n

With your wonky definitions.

For example there are two functions f : {0} -> {0,1}, 4 functions
f : {0,1} -> {0,1}, 8 functions f : {0,1,2} -> {0,1}, etc...

[Mostowski Collapse]

You find it also in your beloved Wikipedia:

Given two sets S and T, the set of all functions from T to S is denoted S^T.
This fits in with the exponentiation of cardinal numbers, in the sense
that |S^T| = |S|^|T|, where |X| is the cardinality of X.
https://en.wikipedia.org/wiki/Exponentiation#Sets_as_exponents

Would work with your wonky definition.

[Mostowski Collapse]

Corr.:
Would never work with your wonky definition.
Thats just utter garbage what you are producing here.

[Dan Christensen]

On Friday, December 3, 2021 at 3:36:55 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 3. Dezember 2021 um 06:40:27 UTC+1:
> > On Thursday, December 2, 2021 at 3:02:39 PM UTC-5, Mostowski Collapse wrote:
> > > But you need a better definition of functional, so that
> > > this blooper doesn't happen, from F : {0} -> {0} to
> > > not be able to prove 1<>0 => ~F(1,0).
> > >
> > Wrong again, Jan Burse. As we see here, there is more to a function that a set of ordered pairs.
> >
> > 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.
>

Actually, X and Y can be arbitrary sets with no other logical connection.

> 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,
>

f is defined as follows:

ALL(a):[a in s0 => f(a) in s0] (line 2)

where ALL(a):[a in s0 <=> a=0] (line 1) and ~1=0 (line 3)

f(x) is undefined for any x not in s0. s0 is both the domain and codomain is this case.

[Mostowski Collapse]

We are talking about F, a two place predicate, and not a
function symbol f. You can anyway not coerce a function
symbol f from FOL into f : X -> Y, because

it is f : V -> V. Whats wrong with you? For every function
symbol you can prove:

ALL(x):EXIST(y):f(x)=y

So dom(f) = V. Your axiom doesn't change that. The above
is still provable. You cannot downgrade a function symbol
from f : V -> V to a smaller domain X , such that f : X -> Y.

Thats impossible.

[Mostowski Collapse]

In FOL all function n-ary symbols f are interpreted
as f : V^n -> V, there is no way to change that.

On the other hand n-ary predicates P are interpreted
as P ⊆ V^n, so when you view a predicate as

function, you can have arguments missing.

[Mostowski Collapse]

But this here:

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

Is not a definition for F : P -> Q. Because it does not
allow to deduce dom(F) = P. You cannot prove from it:

ALL(x):[~x e P => ~EXIST(y):F(x,y)]

Now I kind of told you already the solution how to define
F : P -> Q correctly. But you might also look it up here:

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

The booklet is only 20 bucks or so.

[Daniel Pehoushek]

sigmund freud said
only fags really care
sigmund really cared
freud was a fag

daniel

[Dan Christensen]

On Friday, December 3, 2021 at 1:40:18 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 3. Dezember 2021 um 16:09:27 UTC+1:
> > On Friday, December 3, 2021 at 3:36:55 AM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Freitag, 3. Dezember 2021 um 06:40:27 UTC+1:
> > > > On Thursday, December 2, 2021 at 3:02:39 PM UTC-5, Mostowski Collapse wrote:
> > > > > But you need a better definition of functional, so that
> > > > > this blooper doesn't happen, from F : {0} -> {0} to
> > > > > not be able to prove 1<>0 => ~F(1,0).
> > > > >
> > > > Wrong again, Jan Burse. As we see here, there is more to a function that a set of ordered pairs.
> > > >
> > > > 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.
> > >
> > Actually, X and Y can be arbitrary sets with no other logical connection.
> > > 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,
> > >
> > f is defined as follows:
> >
> > ALL(a):[a in s0 => f(a) in s0] (line 2)
> >
> > where ALL(a):[a in s0 <=> a=0] (line 1) and ~1=0 (line 3)
> >
> > f(x) is undefined for any x not in s0. s0 is both the domain and codomain is this case.

> We are talking about F, a two place predicate, and not a
> function symbol f.

I will upload a functional predicate version in a day or two. It follows the set-theoretic proof very closely.

> You can anyway not coerce a function
> symbol f from FOL into f : X -> Y, because
>
> it is f : V -> V. Whats wrong with you? For every function
> symbol you can prove:
>
> ALL(x):EXIST(y):f(x)=y
>

Not in the vast majority of math textbooks where every function must always have domain and codomain sets specified. Deal with it, Jan Burse.

[Dan Christensen]

On Saturday, December 4, 2021 at 12:27:55 AM UTC-5, Dan Christensen wrote:
> On Friday, December 3, 2021 at 1:40:18 PM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Freitag, 3. Dezember 2021 um 16:09:27 UTC+1:
> > > On Friday, December 3, 2021 at 3:36:55 AM UTC-5, Mostowski Collapse wrote:
> > >
> > > > Dan Christensen schrieb am Freitag, 3. Dezember 2021 um 06:40:27 UTC+1:
> > > > > On Thursday, December 2, 2021 at 3:02:39 PM UTC-5, Mostowski Collapse wrote:
> > > > > > But you need a better definition of functional, so that
> > > > > > this blooper doesn't happen, from F : {0} -> {0} to
> > > > > > not be able to prove 1<>0 => ~F(1,0).
> > > > > >
> > > > > Wrong again, Jan Burse. As we see here, there is more to a function that a set of ordered pairs.
> > > > >
> > > > > 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.
> > > >
> > > Actually, X and Y can be arbitrary sets with no other logical connection.
> > > > 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,
> > > >
> > > f is defined as follows:
> > >
> > > ALL(a):[a in s0 => f(a) in s0] (line 2)
> > >
> > > where ALL(a):[a in s0 <=> a=0] (line 1) and ~1=0 (line 3)
> > >
> > > f(x) is undefined for any x not in s0. s0 is both the domain and codomain is this case.
> > We are talking about F, a two place predicate, and not a
> > function symbol f.
> I will upload a functional predicate version in a day or two. It follows the set-theoretic proof very closely.

https://www.dcproof.com/FunctionUndefinedV2.htm

[Mostowski Collapse]

Dang your stupid, the link says:
> Can we determine a truth value for, say, F(1,0)? No, not from the above assumptions (lines 1-3).
https://www.dcproof.com/FunctionUndefinedV2.htm

Thats the bug in your definition. For the wikipedia definition, ~F(1,0)
already follows from F ⊆ {0} x {0}. Even a blind mole can prove that:

/* using 0=z and 1=o */
(∀a∀b(Fab → (a=z ∧ b=z)) ∧ ¬o=z) → ¬Foz is valid.
https://www.umsu.de/trees

The wikipedia definition is here:
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

[Mostowski Collapse]

Since you don't get it Dan-O-Matik, this reminds me of:
"This dog is like Texas, he just dont know when to stop"

Looney Tunes | Foghorn Leghorn on the Farm
https://youtu.be/kF6qUh3T9KE?t=390

[Dan Christensen]

On Saturday, December 4, 2021 at 7:38:17 PM UTC-5, Mostowski Collapse wrote:
> Dang your stupid, the link says:
> > Can we determine a truth value for, say, F(1,0)? No, not from the above assumptions (lines 1-3).
> https://www.dcproof.com/FunctionUndefinedV2.htm
>
> Thats the bug in your definition. For the wikipedia definition, ~F(1,0)
> already follows from F ⊆ {0} x {0}.

Can you formally prove that f(0)=1 is false given: For all real, non-zero x and real y, we have f(x)=y <=> x*y=1?

[Dan Christensen]

On Saturday, December 4, 2021 at 8:55:11 PM UTC-5, Dan Christensen wrote:
> On Saturday, December 4, 2021 at 7:38:17 PM UTC-5, Mostowski Collapse wrote:
> > Dang your stupid, the link says:
> > > Can we determine a truth value for, say, F(1,0)? No, not from the above assumptions (lines 1-3).
> > https://www.dcproof.com/FunctionUndefinedV2.htm
> >
> > Thats the bug in your definition. For the wikipedia definition, ~F(1,0)
> > already follows from F ⊆ {0} x {0}.

> Can you formally prove that f(0)=1 is false given: For all real, non-zero x and real y, we have f(x)=y <=> x*y=1?

Or given equivalently: For all real x and y, if x=/=0 then we have f(x)=y <=> x*y=1

Might be easier.

[Dan Christensen]

On Saturday, December 4, 2021 at 7:38:17 PM UTC-5, Mostowski Collapse wrote:
> Dang your stupid, the link says:
> > Can we determine a truth value for, say, F(1,0)? No, not from the above assumptions (lines 1-3).
> https://www.dcproof.com/FunctionUndefinedV2.htm
>
> Thats the bug in your definition. For the wikipedia definition, ~F(1,0)
> already follows from F ⊆ {0} x {0}.

It seems you don't care to distinguish a proposition being false from it being unprovable. From basic logic, if A is false and A => B, we cannot determine a truth value for B without further information.

[Mostowski Collapse]

You can make another experiment to show that your
definition is nonsense. There is only one function F : {0} -> {0}.
So if Def(F) expresses F : {0} -> {0}, then this here should

be provable:

(**) Def(F) & Def(G) => F = G

Can you prove it with your definition?

Or more precisely can you prove from this 3 axioms:

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

(2) ALL(a):[S(a) => EXIST(b):[S(b) & F(a,b) & ALL(c):[S(c) => [F(a,c) => c=b]]]]

(3) ALL(a):[S(a) => EXIST(b):[S(b) & G(a,b) & ALL(c):[S(c) => [G(a,c) => c=b]]]]

That this follows theorem follows:

ALL(a):ALL(b):[F(a,b) <=> G(a,b)] ?

[Mostowski Collapse]

You cannot prove with your chimpansee definition:

(**) Def(F) & Def(G) => F = G

Here is a counter model:

∀a(a=z → ∃b(b=z ∧ (Fab ∧ ∀c(c=z → (Fac → c=b))))) ∧
∀a(a=z → ∃b(b=z ∧ (Gab ∧ ∀c(c=z → (Gac → c=b)))))
does not entail
∀a∀b(Fab ↔ Gab).
https://www.umsu.de/trees

Countermodel:
Domain: { 0, 1 }
z: 0
F: { (0,0), (1,0) }
G: { (0,0), (1,1) }

But a graph for any F : {0} -> {0} looks always the same:

Dom Co-Dom
( ) ( )
( 0-)---------(>0 )
( ) ( )

So we want a definition in math, like the one on Wikipedia,
that results in something welldefined, and not a chimpansee definition.

https://en.wikipedia.org/wiki/Well-defined_expression

[Dan Christensen]

On Saturday, December 4, 2021 at 10:48:44 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 5. Dezember 2021 um 03:57:56 UTC+1:
> > On Saturday, December 4, 2021 at 7:38:17 PM UTC-5, Mostowski Collapse wrote:
> > > Dang your stupid, the link says:
> > > > Can we determine a truth value for, say, F(1,0)? No, not from the above assumptions (lines 1-3).
> > > https://www.dcproof.com/FunctionUndefinedV2.htm
> > >
> > > Thats the bug in your definition. For the wikipedia definition, ~F(1,0)
> > > already follows from F ⊆ {0} x {0}.
> > It seems you don't care to distinguish a proposition being false from it being unprovable. From basic logic, if A is false and A => B, we cannot determine a truth value for B without further information.

> You can make another experiment to show that your
> definition is nonsense. There is only one function F : {0} -> {0}.
> So if Def(F) expresses F : {0} -> {0}, then this here should
>
> be provable:
>
> (**) Def(F) & Def(G) => F = G
>
> Can you prove it with your definition?
>
> Or more precisely can you prove from this 3 axioms:
>
> (1) ALL(a):[S(a) <=> a=0]
>
> (2) ALL(a):[S(a) => EXIST(b):[S(b) & F(a,b) & ALL(c):[S(c) => [F(a,c) => c=b]]]]
>
> (3) ALL(a):[S(a) => EXIST(b):[S(b) & G(a,b) & ALL(c):[S(c) => [G(a,c) => c=b]]]]
>
> That this follows theorem follows:
>
> ALL(a):ALL(b):[F(a,b) <=> G(a,b)] ?

No, it follows trivially that ALL(a):ALL(b):[S(a) & S(b) => [F(a,b) <=> G(a,b)]]. (Will post proof if requested.)

[Dan Christensen]

On Saturday, December 4, 2021 at 10:59:33 PM UTC-5, Mostowski Collapse wrote:
> You cannot prove with your chimpansee definition:
> (**) Def(F) & Def(G) => F = G
> Here is a counter model:
>
> ∀a(a=z → ∃b(b=z ∧ (Fab ∧ ∀c(c=z → (Fac → c=b))))) ∧
> ∀a(a=z → ∃b(b=z ∧ (Gab ∧ ∀c(c=z → (Gac → c=b)))))

You want:

∀a(Sa↔a=z)∧
∀a(Sa→∃b(Sb∧Fab∧∀c(Sc→(Fac→c=b))))∧
∀a(Sa→∃b(Sb∧Gab∧∀c(Sc→(Gac→c=b))))→
∀a∀b(Sa∧Sb→(Fab↔Gab))

(Caused TPG to blow up again! WTF)

[Mostowski Collapse]

No, I wrote

F = G

I didn't write:

F|S^2 = G|S^2

Naked Gun - Epic Facepalm [1080p]
https://www.youtube.com/watch?v=ahrBOvz1jzA

[Mostowski Collapse]

Your S doesn't change anything, still not provable:

∀a(Sa ↔ a=z) ∧
(∀a(Sa → ∃b(Sb ∧ (Fab ∧ ∀c(Sc → (Fac → c=b))))) ∧
∀a(Sa → ∃b(Sb ∧ (Gab ∧ ∀c(Sc → (Gac → c=b))))))

does not entail
∀a∀b(Fab ↔ Gab).

https://www.umsu.de/trees/#~6a%28Sa~4a=z%29~1~6a%28Sa~5~7b%28Sb~1%28Fab~1~6c%28Sc~5%28Fac~5c=b%29%29%29%29%29~1~6a%28Sa~5~7b%28Sb~1%28Gab~1~6c%28Sc~5%28Gac~5c=b%29%29%29%29%29|=~6a~6b%28Fab~4Gab%29

Domain: { 0, 1 }
z: 0
F: { (0,0), (1,0) }
G: { (0,0), (1,1) }

S: { 0 }

[Mostowski Collapse]

LoL, the full facepalm:

Prologue to the Facepalm
https://www.youtube.com/watch?v=wjLgekyOZA0