It seems there are ways to do things without set theory,
You find here an example:

Example 2.2. The sentence
states that every function has a range and is provable in NK2.
https://www.dmg.tuwien.ac.at/hetzl/teaching/hol.20190125.pdf

But you need lambda expressions. Actually lambda
expressions about predications. The PM called these

fictitious object:
https://en.wikipedia.org/wiki/Principia_Mathematica#Introduction_to_the_notation_of_the_theory_of_classes_and_relations

So what is the DC Proof, plain set theory nevertheless?

Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 09:35:46 UTC+1:
> Why don't you show the proof?
> Does it use bizzarro set theory?
> Dan Christensen schrieb am Sonntag, 26. Dezember 2021 um 22:09:01 UTC+1:
> > On Sunday, December 26, 2021 at 10:23:12 AM UTC-5, Dan Christensen wrote:
> > > On Sunday, December 26, 2021 at 5:04:17 AM UTC-5, Mostowski Collapse wrote:
> > > > So you cannot show existence of g?
> > > >
> > > See the proof of "Existence of Inverse Function Lemma" at the above link. It proves the existence of the inverse of a bijection.
> > > Dan
> > >
> > Just now completed a proof (138 lines) of the following:
> >
> > ALL(x):ALL(y):ALL(f):[Set(x)
> > & Set(y)
> > & ALL(c):[c in x => f(c) in y]
> > & ALL(c):ALL(d):[c in x & d in x => [f(c)=f(d) => c=d]]
> >
> > => EXIST(rf):EXIST(g):[Set(rf) & ALL(b):[b in rf <=> b in y & EXIST(c):[c in x & f(c)=b]]
> > & ALL(a):[a in rf => g(a) in x]
> > & ALL(a):[a in rf => f(g(a))=a]]]
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

Ha Ha, Dan-O-Matik is quite desperate, he now
denies valid proofs in mathematics:

Dan Christensen schrieb am Freitag, 31. Dezember 2021 um 16:41:43 UTC+1:
> Some universal function-like f just pops into existence,
a consequence of ANY theorem??? Maybe in philosophy class.
Not in math. Sorry. Likewise, (4) and (5).
https://groups.google.com/g/sci.math/c/Wr4n-Hb4b98/m/AjdUTKPeAgAJ

But there is nothing invalid in this proof:

1. f(a)=f(a) ⊢ f(a)=f(a) (ax)
2. f(a)=f(a) ⊢ ∃yf(a)=y (R∃)
3. ∀zz=z ⊢ ∃yf(a)=y (L∀)
4. ∀zz=z ⊢ ∀x∃yf(x)=y (R∀)
5. ⊢ ∀zz=z ⇒ ∀x∃yf(x)=y (R⇒)

http://www.xlog.ch/izytab/moblet/en/docs/18_live/40_bin2021/paste07/package..html

Used inference rules, besides reflexivity of equality:

https://en.wikipedia.org/wiki/Sequent_calculus#Inference_rules

Can this be proved in DC Proof?

ALL(x):[P(x)=>ALL(y):[P(y) & P(f(y))]]

Here is a LK calculus proof:

?- prove0((![X='x']:p(X) => ![Y='y']:(p(Y) & p(f(Y)))), 1).

1. p(a) ⊢ p(a) (ax)
2. ∀xp(x) ⊢ p(a) (L∀)
3. p(f(a)) ⊢ p(f(a)) (ax)
4. ∀xp(x) ⊢ p(f(a)) (L∀)
5. ∀xp(x) ⊢ p(a) ∧ p(f(a)) (R∧, 2)
6. ∀xp(x) ⊢ ∀y(p(y) ∧ p(f(y))) (R∀)
7. ⊢ ∀xp(x) ⇒ ∀y(p(y) ∧ p(f(y))) (R⇒)

http://www.xlog.ch/izytab/moblet/en/docs/18_live/40_bin2021/paste07/package..html

Adapted from an example for another proof method:
https://en.wikipedia.org/wiki/Method_of_analytic_tableaux#First-order_tableau_with_unification

Corr.: Typo

ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]

Mostowski Collapse schrieb am Sonntag, 2. Januar 2022 um 20:18:53 UTC+1:
> Can this be proved in DC Proof?
>
> ALL(x):[P(x)=>ALL(y):[P(y) & P(f(y))]]
>
> Here is a LK calculus proof:
>
> ?- prove0((![X='x']:p(X) => ![Y='y']:(p(Y) & p(f(Y)))), 1).
>
> 1. p(a) ⊢ p(a) (ax)
> 2. ∀xp(x) ⊢ p(a) (L∀)
> 3. p(f(a)) ⊢ p(f(a)) (ax)
> 4. ∀xp(x) ⊢ p(f(a)) (L∀)
> 5. ∀xp(x) ⊢ p(a) ∧ p(f(a)) (R∧, 2)
> 6. ∀xp(x) ⊢ ∀y(p(y) ∧ p(f(y))) (R∀)
> 7. ⊢ ∀xp(x) ⇒ ∀y(p(y) ∧ p(f(y))) (R⇒)
>
> http://www.xlog.ch/izytab/moblet/en/docs/18_live/40_bin2021/paste07/package.html
>
> Adapted from an example for another proof method:
> https://en.wikipedia.org/wiki/Method_of_analytic_tableaux#First-order_tableau_with_unification

Mostowski Collapse wrote:

> Can this be proved in DC Proof?
>
> ALL(x):[P(x)=>ALL(y):[P(y) & P(f(y))]]

APPOLLO 11 THE REAL MOON LANDING
https://seed125.bitchute.com/x4t2DPNQVTsV/S120GRdJlfKH.mp4

The next challenge is to become cyborgs:

"I Tried To Warn You" | Elon Musk's Last Warning (2022)
https://www.youtube.com/watch?v=AQNBO6WbQo8

Scot Dino schrieb:
> Mostowski Collapse wrote:
>
>> Can this be proved in DC Proof?
>>
>> ALL(x):[P(x)=>ALL(y):[P(y) & P(f(y))]]
>
> APPOLLO 11 THE REAL MOON LANDING
> https://seed125.bitchute.com/x4t2DPNQVTsV/S120GRdJlfKH.mp4
>

On Sunday, January 2, 2022 at 3:34:51 PM UTC-8, Mostowski Collapse wrote:
> The next challenge is to become cyborgs:
>
> "I Tried To Warn You" | Elon Musk's Last Warning (2022)
> https://www.youtube.com/watch?v=AQNBO6WbQo8
>
> Scot Dino schrieb:
> > Mostowski Collapse wrote:
> >
> >> Can this be proved in DC Proof?
> >>
> >> ALL(x):[P(x)=>ALL(y):[P(y) & P(f(y))]]
> >
> > APPOLLO 11 THE REAL MOON LANDING
> > https://seed125.bitchute.com/x4t2DPNQVTsV/S120GRdJlfKH.mp4
> >

Glorified calculators can't program the human brain.

These calculators are quite good in controlling
robots. I guess cars are all now manifactured

by robots. So where are the jobs in the future?

mitchr...@gmail.com schrieb am Montag, 3. Januar 2022 um 01:00:23 UTC+1:
> On Sunday, January 2, 2022 at 3:34:51 PM UTC-8, Mostowski Collapse wrote:
> > The next challenge is to become cyborgs:
> >
> > "I Tried To Warn You" | Elon Musk's Last Warning (2022)
> > https://www.youtube.com/watch?v=AQNBO6WbQo8
> >
> > Scot Dino schrieb:
> > > Mostowski Collapse wrote:
> > >
> > >> Can this be proved in DC Proof?
> > >>
> > >> ALL(x):[P(x)=>ALL(y):[P(y) & P(f(y))]]
> > >
> > > APPOLLO 11 THE REAL MOON LANDING
> > > https://seed125.bitchute.com/x4t2DPNQVTsV/S120GRdJlfKH.mp4
> > >
> Glorified calculators can't program the human brain.

On Sunday, January 2, 2022 at 2:20:35 PM UTC-5, Mostowski Collapse wrote:

> > Can this be proved in DC Proof?
> >
> > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] (Corr.)
> >

Yes, but you have to make the domain of discourse explicit. In mathematics, it can't just be lurking unseen in the shadows.

Define: f on the domain of discourse u

1. ALL(a):[a in u => f(a) in u]
(Axiom)
Prove: ALL(a):[a in u => P(a)]
=> ALL(a):[a in u => P(a) & P(f(a))]
Suppose...

2. ALL(a):[a in u => P(a)]
(Premise)

Prove: ALL(a):[a in u => P(a) & P(f(a))]

Suppose...

3. x in u
(Premise)

Apply initial premise

4. x in u => P(x)
(U Spec, 2)

5. P(x)
(Detach, 4, 3)

Apply definition of f

6. x in u => f(x) in u
(U Spec, 1)

7. f(x) in u
(Detach, 6, 3)

Apply initial premise

8. f(x) in u => P(f(x))
(U Spec, 2, 7)

9. P(f(x))
(Detach, 8, 7)

10. P(x) & P(f(x))
(Join, 5, 9)

As Required:

11. ALL(a):[a in u => P(a) & P(f(a))]
(Conclusion, 3)

As Required:

12. ALL(a):[a in u => P(a)]
=> ALL(a):[a in u => P(a) & P(f(a))]
(Conclusion, 2)

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, January 2, 2022 at 2:20:35 PM UTC-5, Mostowski Collapse wrote:

> > Can this be proved in DC Proof?
> >
> > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] (Corr.)
> >

Yes, but you have to make the domain of discourse explicit. In mathematics, it can't just be lurking unseen in the shadows.

Define: f on the domain of discourse u

1. ALL(a):[a in u => f(a) in u]
(Axiom)

Suppose...

2. ALL(a):[a in u => P(a)]
(Premise)

Suppose...

3. x in u
(Premise)

Apply initial premise

4. x in u => P(x)
(U Spec, 2)

5. P(x)
(Detach, 4, 3)

Apply definition of f

6. x in u => f(x) in u
(U Spec, 1)

7. f(x) in u
(Detach, 6, 3)

Apply initial premise

8. f(x) in u => P(f(x))
(U Spec, 2, 7)

9. P(f(x))
(Detach, 8, 7)

10. P(x) & P(f(x))
(Join, 5, 9)

As Required:

11. ALL(a):[a in u => P(a) & P(f(a))]
(Conclusion, 3)

As Required:

12. ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]
(Conclusion, 2)

Dan

Dan-O-Matik fights the evils of darkness:
> In mathematics, it can't just be lurking unseen in the shadows.

Well you can replace P(a) by a in u, and you get:

ALL(a):[a in u => a in u] => ALL(a):[a in u => a in u & f(a) in u]

Since ALL(a):[a in u => a in u] is trivial you get:

ALL(a):[a in u => a in u & f(a) in u]

I thought in DC Puff f must always have a domain?

LMAO!

Dan Christensen schrieb am Montag, 3. Januar 2022 um 05:36:39 UTC+1:
> On Sunday, January 2, 2022 at 2:20:35 PM UTC-5, Mostowski Collapse wrote:
>
> > > Can this be proved in DC Proof?
> > >
> > > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] (Corr.)
> > >
>
> Yes, but you have to make the domain of discourse explicit. In mathematics, it can't just be lurking unseen in the shadows.
>
> Define: f on the domain of discourse u
>
> 1. ALL(a):[a in u => f(a) in u]
> (Axiom)
>
> Suppose...
>
> 2. ALL(a):[a in u => P(a)]
> (Premise)
>
> Suppose...
>
> 3. x in u
> (Premise)
>
> Apply initial premise
>
> 4. x in u => P(x)
> (U Spec, 2)
>
> 5. P(x)
> (Detach, 4, 3)
>
> Apply definition of f
>
> 6. x in u => f(x) in u
> (U Spec, 1)
>
> 7. f(x) in u
> (Detach, 6, 3)
>
> Apply initial premise
>
> 8. f(x) in u => P(f(x))
> (U Spec, 2, 7)
>
> 9. P(f(x))
> (Detach, 8, 7)
>
> 10. P(x) & P(f(x))
> (Join, 5, 9)
>
> As Required:
>
> 11. ALL(a):[a in u => P(a) & P(f(a))]
> (Conclusion, 3)
>
> As Required:
>
> 12. ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]
> (Conclusion, 2)
>
> Dan

From ALL(a):[a in u => a in u & f(a) in u] it also follows:

ALL(a):[a in u => f(a) in u]

But what if you had elsewhere ALL(a):[a in dom => f(a) in cod],
even maybe with dom ⊆ u and cod ⊆ u, you will nevertheless
obtain the above? Which is nothing else than confirmation

that FOL function symbols are total, even when you have
the Dan-O-Matik ALL(a):[a in dom => f(a) in cod], which makes
Dan-O-Matik cite Terrence Tao, we nevertheless fall back

to essentially ∀x∃yf(x)=y. Isn't this amazing that dcproof4.exe
with its adhoc fixes, does not solve the problem of Burses Paradox,
it rather aggravates it, since it leads us digging deeper into

the evils of darkness, and when we lift the curtains of DC Puff
we find more totality of FOL function symbols lurking in the
shadows. To adapt a famous proverb by Dan-O-Matik:

"Deal with it, Dan-O-Matik. You are looking like a complete
idiot here in the same league as AP, JG and WM."

Disclaimer: Maybe there are more and more fixes of
dcproof4.exe, a whole tower of patch work, and the above
exact same derivation doesn't work.

But what do we know about an adhoc logic such as DC Puff
which even doesn't have a name and is nowhere found in
any mathematics textbooks?

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 13:25:59 UTC+1:
> Dan-O-Matik fights the evils of darkness:
> > In mathematics, it can't just be lurking unseen in the shadows.
> Well you can replace P(a) by a in u, and you get:
>
> ALL(a):[a in u => a in u] => ALL(a):[a in u => a in u & f(a) in u]
>
> Since ALL(a):[a in u => a in u] is trivial you get:
>
> ALL(a):[a in u => a in u & f(a) in u]
>
> I thought in DC Puff f must always have a domain?
>
> LMAO!
> Dan Christensen schrieb am Montag, 3. Januar 2022 um 05:36:39 UTC+1:
> > On Sunday, January 2, 2022 at 2:20:35 PM UTC-5, Mostowski Collapse wrote:
> >
> > > > Can this be proved in DC Proof?
> > > >
> > > > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] (Corr.)
> > > >
> >
> > Yes, but you have to make the domain of discourse explicit. In mathematics, it can't just be lurking unseen in the shadows.
> >
> > Define: f on the domain of discourse u
> >
> > 1. ALL(a):[a in u => f(a) in u]
> > (Axiom)
> >
> > Suppose...
> >
> > 2. ALL(a):[a in u => P(a)]
> > (Premise)
> >
> > Suppose...
> >
> > 3. x in u
> > (Premise)
> >
> > Apply initial premise
> >
> > 4. x in u => P(x)
> > (U Spec, 2)
> >
> > 5. P(x)
> > (Detach, 4, 3)
> >
> > Apply definition of f
> >
> > 6. x in u => f(x) in u
> > (U Spec, 1)
> >
> > 7. f(x) in u
> > (Detach, 6, 3)
> >
> > Apply initial premise
> >
> > 8. f(x) in u => P(f(x))
> > (U Spec, 2, 7)
> >
> > 9. P(f(x))
> > (Detach, 8, 7)
> >
> > 10. P(x) & P(f(x))
> > (Join, 5, 9)
> >
> > As Required:
> >
> > 11. ALL(a):[a in u => P(a) & P(f(a))]
> > (Conclusion, 3)
> >
> > As Required:
> >
> > 12. ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]
> > (Conclusion, 2)
> >
> > Dan

On Monday, January 3, 2022 at 7:25:59 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 3. Januar 2022 um 05:36:39 UTC+1:
> > On Sunday, January 2, 2022 at 2:20:35 PM UTC-5, Mostowski Collapse wrote:
> >
> > > > Can this be proved in DC Proof?
> > > >
> > > > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] (Corr.)
> > > >
> >
> > Yes, but you have to make the domain of discourse explicit. In mathematics, it can't just be lurking unseen in the shadows.
> >
> > Define: f on the domain of discourse u
> >
> > 1. ALL(a):[a in u => f(a) in u]
> > (Axiom)
> >
> > Suppose...
> >
> > 2. ALL(a):[a in u => P(a)]
> > (Premise)
> >
> > Suppose...
> >
> > 3. x in u
> > (Premise)
> >
> > Apply initial premise
> >
> > 4. x in u => P(x)
> > (U Spec, 2)
> >
> > 5. P(x)
> > (Detach, 4, 3)
> >
> > Apply definition of f
> >
> > 6. x in u => f(x) in u
> > (U Spec, 1)
> >
> > 7. f(x) in u
> > (Detach, 6, 3)
> >
> > Apply initial premise
> >
> > 8. f(x) in u => P(f(x))
> > (U Spec, 2, 7)
> >
> > 9. P(f(x))
> > (Detach, 8, 7)
> >
> > 10. P(x) & P(f(x))
> > (Join, 5, 9)
> >
> > As Required:
> >
> > 11. ALL(a):[a in u => P(a) & P(f(a))]
> > (Conclusion, 3)
> >
> > As Required:
> >
> > 12. ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]
> > (Conclusion, 2)
> >

> Dan-O-Matik fights the evils of darkness:

>
> I thought in DC Proof f must always have a domain?
>

Do pay attention, Jan Burse. Both the domain and codomain are u. See line 1.

Dan

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

Thats FOL semantics, yes.

Dan Christensen schrieb am Montag, 3. Januar 2022 um 14:15:29 UTC+1:
> On Monday, January 3, 2022 at 7:25:59 AM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Montag, 3. Januar 2022 um 05:36:39 UTC+1:
> > > On Sunday, January 2, 2022 at 2:20:35 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > > Can this be proved in DC Proof?
> > > > >
> > > > > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] (Corr.)
> > > > >
> > >
> > > Yes, but you have to make the domain of discourse explicit. In mathematics, it can't just be lurking unseen in the shadows.
> > >
> > > Define: f on the domain of discourse u
> > >
> > > 1. ALL(a):[a in u => f(a) in u]
> > > (Axiom)
> > >
> > > Suppose...
> > >
> > > 2. ALL(a):[a in u => P(a)]
> > > (Premise)
> > >
> > > Suppose...
> > >
> > > 3. x in u
> > > (Premise)
> > >
> > > Apply initial premise
> > >
> > > 4. x in u => P(x)
> > > (U Spec, 2)
> > >
> > > 5. P(x)
> > > (Detach, 4, 3)
> > >
> > > Apply definition of f
> > >
> > > 6. x in u => f(x) in u
> > > (U Spec, 1)
> > >
> > > 7. f(x) in u
> > > (Detach, 6, 3)
> > >
> > > Apply initial premise
> > >
> > > 8. f(x) in u => P(f(x))
> > > (U Spec, 2, 7)
> > >
> > > 9. P(f(x))
> > > (Detach, 8, 7)
> > >
> > > 10. P(x) & P(f(x))
> > > (Join, 5, 9)
> > >
> > > As Required:
> > >
> > > 11. ALL(a):[a in u => P(a) & P(f(a))]
> > > (Conclusion, 3)
> > >
> > > As Required:
> > >
> > > 12. ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]
> > > (Conclusion, 2)
> > >
> > Dan-O-Matik fights the evils of darkness:
>
> >
> > I thought in DC Proof f must always have a domain?
> >
>
> Do pay attention, Jan Burse. Both the domain and codomain are u. See line 1.
>
> Dan
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

My expectation was rather that:

ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]

Isn't provable in DC Proof.

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 14:21:54 UTC+1:
> Thats FOL semantics, yes.
> Dan Christensen schrieb am Montag, 3. Januar 2022 um 14:15:29 UTC+1:
> > On Monday, January 3, 2022 at 7:25:59 AM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Montag, 3. Januar 2022 um 05:36:39 UTC+1:
> > > > On Sunday, January 2, 2022 at 2:20:35 PM UTC-5, Mostowski Collapse wrote:
> > > >
> > > > > > Can this be proved in DC Proof?
> > > > > >
> > > > > > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] (Corr.)
> > > > > >
> > > >
> > > > Yes, but you have to make the domain of discourse explicit. In mathematics, it can't just be lurking unseen in the shadows.
> > > >
> > > > Define: f on the domain of discourse u
> > > >
> > > > 1. ALL(a):[a in u => f(a) in u]
> > > > (Axiom)
> > > >
> > > > Suppose...
> > > >
> > > > 2. ALL(a):[a in u => P(a)]
> > > > (Premise)
> > > >
> > > > Suppose...
> > > >
> > > > 3. x in u
> > > > (Premise)
> > > >
> > > > Apply initial premise
> > > >
> > > > 4. x in u => P(x)
> > > > (U Spec, 2)
> > > >
> > > > 5. P(x)
> > > > (Detach, 4, 3)
> > > >
> > > > Apply definition of f
> > > >
> > > > 6. x in u => f(x) in u
> > > > (U Spec, 1)
> > > >
> > > > 7. f(x) in u
> > > > (Detach, 6, 3)
> > > >
> > > > Apply initial premise
> > > >
> > > > 8. f(x) in u => P(f(x))
> > > > (U Spec, 2, 7)
> > > >
> > > > 9. P(f(x))
> > > > (Detach, 8, 7)
> > > >
> > > > 10. P(x) & P(f(x))
> > > > (Join, 5, 9)
> > > >
> > > > As Required:
> > > >
> > > > 11. ALL(a):[a in u => P(a) & P(f(a))]
> > > > (Conclusion, 3)
> > > >
> > > > As Required:
> > > >
> > > > 12. ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]
> > > > (Conclusion, 2)
> > > >
> > > Dan-O-Matik fights the evils of darkness:
> >
> > >
> > > I thought in DC Proof f must always have a domain?
> > >
> >
> > Do pay attention, Jan Burse. Both the domain and codomain are u. See line 1.
> >
> > Dan
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

That it wouldn't be provable can be simulated in FOL
by thinking in terms of (Function over U) and not in terms
of (Function from U to U). This would somehow cover

emptyness from free logic. Since a (Function over U)
might send an argument to outside of U. So we then
have, if we think only in terms of (Function over U):

Normally with FOL:
∀xPx → ∀x(Px ∧ Pf(x)) is valid.
https://www.umsu.de/trees/#~6xPx~5~6x%28Px~1Pf%28x%29%29

Abnormally with "free logic" touch:
∀x(Ux → Px) → ∀x(Ux → (Px ∧ Pf(x))) is invalid.
Countermodel:
Domain: { 0, 1 }
f: { (0,1), (1,0) }
U: { 0 }
P: { 0 }
https://www.umsu.de/trees/#~6x%28Ux~5Px%29~5~6x%28Ux~5%28Px~1Pf%28x%29%29%29

No need to postulate ∀x(Ux → Uf(x)).

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 14:25:36 UTC+1:
> My expectation was rather that:
> ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]
> Isn't provable in DC Proof.
> Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 14:21:54 UTC+1:
> > Thats FOL semantics, yes.
> > Dan Christensen schrieb am Montag, 3. Januar 2022 um 14:15:29 UTC+1:
> > > On Monday, January 3, 2022 at 7:25:59 AM UTC-5, Mostowski Collapse wrote:
> > >
> > > > Dan Christensen schrieb am Montag, 3. Januar 2022 um 05:36:39 UTC+1:
> > > > > On Sunday, January 2, 2022 at 2:20:35 PM UTC-5, Mostowski Collapse wrote:
> > > > >
> > > > > > > Can this be proved in DC Proof?
> > > > > > >
> > > > > > > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))] (Corr.)
> > > > > > >
> > > > >
> > > > > Yes, but you have to make the domain of discourse explicit. In mathematics, it can't just be lurking unseen in the shadows.
> > > > >
> > > > > Define: f on the domain of discourse u
> > > > >
> > > > > 1. ALL(a):[a in u => f(a) in u]
> > > > > (Axiom)
> > > > >
> > > > > Suppose...
> > > > >
> > > > > 2. ALL(a):[a in u => P(a)]
> > > > > (Premise)
> > > > >
> > > > > Suppose...
> > > > >
> > > > > 3. x in u
> > > > > (Premise)
> > > > >
> > > > > Apply initial premise
> > > > >
> > > > > 4. x in u => P(x)
> > > > > (U Spec, 2)
> > > > >
> > > > > 5. P(x)
> > > > > (Detach, 4, 3)
> > > > >
> > > > > Apply definition of f
> > > > >
> > > > > 6. x in u => f(x) in u
> > > > > (U Spec, 1)
> > > > >
> > > > > 7. f(x) in u
> > > > > (Detach, 6, 3)
> > > > >
> > > > > Apply initial premise
> > > > >
> > > > > 8. f(x) in u => P(f(x))
> > > > > (U Spec, 2, 7)
> > > > >
> > > > > 9. P(f(x))
> > > > > (Detach, 8, 7)
> > > > >
> > > > > 10. P(x) & P(f(x))
> > > > > (Join, 5, 9)
> > > > >
> > > > > As Required:
> > > > >
> > > > > 11. ALL(a):[a in u => P(a) & P(f(a))]
> > > > > (Conclusion, 3)
> > > > >
> > > > > As Required:
> > > > >
> > > > > 12. ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]
> > > > > (Conclusion, 2)
> > > > >
> > > > Dan-O-Matik fights the evils of darkness:
> > >
> > > >
> > > > I thought in DC Proof f must always have a domain?
> > > >
> > >
> > > Do pay attention, Jan Burse. Both the domain and codomain are u. See line 1.
> > >
> > > 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, January 3, 2022 at 8:25:36 AM UTC-5, Mostowski Collapse wrote:
> My expectation was rather that:
> ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]
> Isn't provable in DC Proof.

You will have to settle for:

ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]

Too much detail for you? Too bad.

Dan

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

You are changing topic, are you hunted by some shadows, Dr. Frankenstein?
This here shouldn't be provable as well in DC Proof, its already not provable in FOL:

∀x(Exu → Px) → ∀x(Exu → (Px ∧ Pf(x))) is invalid.
Countermodel:
Domain: { 0, 1 }
u: 0
f: { (0,1), (1,0) }
E: { (0,0) }
P: { 0 }
https://www.umsu.de/trees/#~6x%28Exu~5Px%29~5~6x%28Exu~5%28Px~1Pf%28x%29%29%29

Dan Christensen schrieb am Montag, 3. Januar 2022 um 14:57:54 UTC+1:
> On Monday, January 3, 2022 at 8:25:36 AM UTC-5, Mostowski Collapse wrote:
> > My expectation was rather that:
> > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]
> > Isn't provable in DC Proof.
> You will have to settle for:
> ALL(a):[a in u => P(a)] => ALL(a):[a in u => P(a) & P(f(a))]
> Too much detail for you? Too bad.
> 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, January 3, 2022 at 11:19:04 AM UTC-5, Mostowski Collapse wrote:
> You are changing topic, are you hunted by some shadows, Dr. Frankenstein?
> This here shouldn't be provable as well in DC Proof, its already not provable in FOL:
>
> ∀x(Exu → Px) → ∀x(Exu → (Px ∧ Pf(x))) is invalid.
> Countermodel:
> Domain: { 0, 1 }
> u: 0
> f: { (0,1), (1,0) }
> E: { (0,0) }
> P: { 0 }
> https://www.umsu.de/trees/#~6x%28Exu~5Px%29~5~6x%28Exu~5%28Px~1Pf%28x%29%29%29

You really MUST pay attention, Jan Burse! Once again, you forgot the initial axiom on line 1.

1. ALL(a):[a in u => f(a) in u]
(Axiom)

From TPG: "(∀x(Exu → Ef(x)u) ∧ ∀x(Exu → Px)) → ∀x(Exu → (Px ∧ Pf(x))) is valid."

https://www.umsu.de/trees/#~6x(Exu~5Ef(x)u)~1~6x(Exu~5Px)~5~6x(Exu~5(Px~1Pf(x)))

Dan

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

I do not assume something like this, when I ask whether:

ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]

is provable in DC Proof. I didn't say the above is a FOL formula.
If it were a FOL formula I wouldn't use the idiosyncratic ALL(x)
or EXIST(z). Most of the time when I post problems towards

DC Proof, I do not assume they are translated to FOL. I
am genuinely interested what is provable and what is not provable
in DC Proof. So this here is a DC Proof problem, there is no idea

that it means a FOL formula, it doesn't mean FOL, it means
what ever from day to day changing semantics of ALL(x)
is in DC Proof:

ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]

On the other hand this here is a FOL problem:

∀xPx → ∀x(Px ∧ Pf(x))

Got it? Or are you too stupid?

Dan Christensen schrieb am Montag, 3. Januar 2022 um 18:07:19 UTC+1:
> On Monday, January 3, 2022 at 11:19:04 AM UTC-5, Mostowski Collapse wrote:
> > You are changing topic, are you hunted by some shadows, Dr. Frankenstein?
> > This here shouldn't be provable as well in DC Proof, its already not provable in FOL:
> >
> > ∀x(Exu → Px) → ∀x(Exu → (Px ∧ Pf(x))) is invalid.
> > Countermodel:
> > Domain: { 0, 1 }
> > u: 0
> > f: { (0,1), (1,0) }
> > E: { (0,0) }
> > P: { 0 }
> > https://www.umsu.de/trees/#~6x%28Exu~5Px%29~5~6x%28Exu~5%28Px~1Pf%28x%29%29%29
> You really MUST pay attention, Jan Burse! Once again, you forgot the initial axiom on line 1.
>
> 1. ALL(a):[a in u => f(a) in u]
> (Axiom)
>
> From TPG: "(∀x(Exu → Ef(x)u) ∧ ∀x(Exu → Px)) → ∀x(Exu → (Px ∧ Pf(x))) is valid."
>
> https://www.umsu.de/trees/#~6x(Exu~5Ef(x)u)~1~6x(Exu~5Px)~5~6x(Exu~5(Px~1Pf(x)))
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

You can check yourself, I nowhere stated that the formula
must be interpreted by FOL. You violated Occams Razor
by adding stuff that was never asked:

Mostowski Collapse schrieb am Sonntag, 2. Januar 2022 um 20:18:53 UTC+1:
> Can this be proved in DC Proof?
>
> ALL(x):[P(x)=>ALL(y):[P(y) & P(f(y))]]
>
> Here is a LK calculus proof:
>
> ?- prove0((![X='x']:p(X) => ![Y='y']:(p(Y) & p(f(Y)))), 1).
>
> 1. p(a) ⊢ p(a) (ax)
> 2. ∀xp(x) ⊢ p(a) (L∀)
> 3. p(f(a)) ⊢ p(f(a)) (ax)
> 4. ∀xp(x) ⊢ p(f(a)) (L∀)
> 5. ∀xp(x) ⊢ p(a) ∧ p(f(a)) (R∧, 2)
> 6. ∀xp(x) ⊢ ∀y(p(y) ∧ p(f(y))) (R∀)
> 7. ⊢ ∀xp(x) ⇒ ∀y(p(y) ∧ p(f(y))) (R⇒)
>
> http://www.xlog.ch/izytab/moblet/en/docs/18_live/40_bin2021/paste07/package.html
>
> Adapted from an example for another proof method:
> https://en.wikipedia.org/wiki/Method_of_analytic_tableaux#First-order_tableau_with_unification
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/30qnX6aHAwAJ

Whats wrong with you?

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 18:17:01 UTC+1:
> I do not assume something like this, when I ask whether:
> ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]
> is provable in DC Proof. I didn't say the above is a FOL formula.
> If it were a FOL formula I wouldn't use the idiosyncratic ALL(x)
> or EXIST(z). Most of the time when I post problems towards
>
> DC Proof, I do not assume they are translated to FOL. I
> am genuinely interested what is provable and what is not provable
> in DC Proof. So this here is a DC Proof problem, there is no idea
>
> that it means a FOL formula, it doesn't mean FOL, it means
> what ever from day to day changing semantics of ALL(x)
> is in DC Proof:
> ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]
> On the other hand this here is a FOL problem:
>
> ∀xPx → ∀x(Px ∧ Pf(x))
>
> Got it? Or are you too stupid?
> Dan Christensen schrieb am Montag, 3. Januar 2022 um 18:07:19 UTC+1:
> > On Monday, January 3, 2022 at 11:19:04 AM UTC-5, Mostowski Collapse wrote:
> > > You are changing topic, are you hunted by some shadows, Dr. Frankenstein?
> > > This here shouldn't be provable as well in DC Proof, its already not provable in FOL:
> > >
> > > ∀x(Exu → Px) → ∀x(Exu → (Px ∧ Pf(x))) is invalid.
> > > Countermodel:
> > > Domain: { 0, 1 }
> > > u: 0
> > > f: { (0,1), (1,0) }
> > > E: { (0,0) }
> > > P: { 0 }
> > > https://www.umsu.de/trees/#~6x%28Exu~5Px%29~5~6x%28Exu~5%28Px~1Pf%28x%29%29%29
> > You really MUST pay attention, Jan Burse! Once again, you forgot the initial axiom on line 1.
> >
> > 1. ALL(a):[a in u => f(a) in u]
> > (Axiom)
> >
> > From TPG: "(∀x(Exu → Ef(x)u) ∧ ∀x(Exu → Px)) → ∀x(Exu → (Px ∧ Pf(x))) is valid."
> >
> > https://www.umsu.de/trees/#~6x(Exu~5Ef(x)u)~1~6x(Exu~5Px)~5~6x(Exu~5(Px~1Pf(x)))
> > 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, January 3, 2022 at 12:17:01 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 3. Januar 2022 um 18:07:19 UTC+1:
> > On Monday, January 3, 2022 at 11:19:04 AM UTC-5, Mostowski Collapse wrote:
> > > You are changing topic, are you hunted by some shadows, Dr. Frankenstein?
> > > This here shouldn't be provable as well in DC Proof, its already not provable in FOL:
> > >
> > > ∀x(Exu → Px) → ∀x(Exu → (Px ∧ Pf(x))) is invalid.
> > > Countermodel:
> > > Domain: { 0, 1 }
> > > u: 0
> > > f: { (0,1), (1,0) }
> > > E: { (0,0) }
> > > P: { 0 }
> > > https://www.umsu.de/trees/#~6x%28Exu~5Px%29~5~6x%28Exu~5%28Px~1Pf%28x%29%29%29
> > You really MUST pay attention, Jan Burse! Once again, you forgot the initial axiom on line 1.
> >
> > 1. ALL(a):[a in u => f(a) in u]
> > (Axiom)
> >
> > From TPG: "(∀x(Exu → Ef(x)u) ∧ ∀x(Exu → Px)) → ∀x(Exu → (Px ∧ Pf(x))) is valid."
> >
> > https://www.umsu.de/trees/#~6x(Exu~5Ef(x)u)~1~6x(Exu~5Px)~5~6x(Exu~5(Px~1Pf(x)))

> I do not assume something like this,

That is why you are getting an invalid result.

> when I ask whether:
> ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]
> is provable in DC Proof.

Too many missing details. No wonder it is not a required subject even in pure math programs (e.g. at MIT).

> I didn't say the above is a FOL formula.

Messy details, eh, Jan Burse? Unfortunately, that's what properly formal proofs are all about.

> If it were a FOL formula I wouldn't use the idiosyncratic ALL(x)
> or EXIST(z). Most of the time when I post problems towards
>
> DC Proof, I do not assume they are translated to FOL.

I'm afraid, it is your version of FOL that is widely viewed as idiosyncratic with its mysterious, unspecified, but non-empty domains of discourse, etc.. It seems mathematicians had to develop their own system of logic, more like that used in DC Proof.

Dan

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

See other thread "Re: Minor updates to DC Proof 2.0".
The question is still unanswered, and your rant doesn't help either.

Dan Christensen schrieb am Montag, 3. Januar 2022 um 19:30:11 UTC+1:
> On Monday, January 3, 2022 at 12:17:01 PM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Montag, 3. Januar 2022 um 18:07:19 UTC+1:
> > > On Monday, January 3, 2022 at 11:19:04 AM UTC-5, Mostowski Collapse wrote:
> > > > You are changing topic, are you hunted by some shadows, Dr. Frankenstein?
> > > > This here shouldn't be provable as well in DC Proof, its already not provable in FOL:
> > > >
> > > > ∀x(Exu → Px) → ∀x(Exu → (Px ∧ Pf(x))) is invalid.
> > > > Countermodel:
> > > > Domain: { 0, 1 }
> > > > u: 0
> > > > f: { (0,1), (1,0) }
> > > > E: { (0,0) }
> > > > P: { 0 }
> > > > https://www.umsu.de/trees/#~6x%28Exu~5Px%29~5~6x%28Exu~5%28Px~1Pf%28x%29%29%29
> > > You really MUST pay attention, Jan Burse! Once again, you forgot the initial axiom on line 1.
> > >
> > > 1. ALL(a):[a in u => f(a) in u]
> > > (Axiom)
> > >
> > > From TPG: "(∀x(Exu → Ef(x)u) ∧ ∀x(Exu → Px)) → ∀x(Exu → (Px ∧ Pf(x))) is valid."
> > >
> > > https://www.umsu.de/trees/#~6x(Exu~5Ef(x)u)~1~6x(Exu~5Px)~5~6x(Exu~5(Px~1Pf(x)))
> > I do not assume something like this,
> That is why you are getting an invalid result.
> > when I ask whether:
> > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]
> > is provable in DC Proof.
> Too many missing details. No wonder it is not a required subject even in pure math programs (e.g. at MIT).
> > I didn't say the above is a FOL formula.
> Messy details, eh, Jan Burse? Unfortunately, that's what properly formal proofs are all about.
> > If it were a FOL formula I wouldn't use the idiosyncratic ALL(x)
> > or EXIST(z). Most of the time when I post problems towards
> >
> > DC Proof, I do not assume they are translated to FOL.
> I'm afraid, it is your version of FOL that is widely viewed as idiosyncratic with its mysterious, unspecified, but non-empty domains of discourse, etc. It seems mathematicians had to develop their own system of logic, more like that used in DC Proof.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Also there is no such thing as my version of FOL.
See here, I am not the author of www.umsu.de/trees:

Normally with FOL:
∀xPx → ∀x(Px ∧ Pf(x)) is valid.
https://www.umsu.de/trees/#~6xPx~5~6x%28Px~1Pf%28x%29%29

Whats wrong with you?

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 19:45:21 UTC+1:
> See other thread "Re: Minor updates to DC Proof 2.0".
> The question is still unanswered, and your rant doesn't help either.
> Dan Christensen schrieb am Montag, 3. Januar 2022 um 19:30:11 UTC+1:
> > On Monday, January 3, 2022 at 12:17:01 PM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Montag, 3. Januar 2022 um 18:07:19 UTC+1:
> > > > On Monday, January 3, 2022 at 11:19:04 AM UTC-5, Mostowski Collapse wrote:
> > > > > You are changing topic, are you hunted by some shadows, Dr. Frankenstein?
> > > > > This here shouldn't be provable as well in DC Proof, its already not provable in FOL:
> > > > >
> > > > > ∀x(Exu → Px) → ∀x(Exu → (Px ∧ Pf(x))) is invalid.
> > > > > Countermodel:
> > > > > Domain: { 0, 1 }
> > > > > u: 0
> > > > > f: { (0,1), (1,0) }
> > > > > E: { (0,0) }
> > > > > P: { 0 }
> > > > > https://www.umsu.de/trees/#~6x%28Exu~5Px%29~5~6x%28Exu~5%28Px~1Pf%28x%29%29%29
> > > > You really MUST pay attention, Jan Burse! Once again, you forgot the initial axiom on line 1.
> > > >
> > > > 1. ALL(a):[a in u => f(a) in u]
> > > > (Axiom)
> > > >
> > > > From TPG: "(∀x(Exu → Ef(x)u) ∧ ∀x(Exu → Px)) → ∀x(Exu → (Px ∧ Pf(x))) is valid."
> > > >
> > > > https://www.umsu.de/trees/#~6x(Exu~5Ef(x)u)~1~6x(Exu~5Px)~5~6x(Exu~5(Px~1Pf(x)))
> > > I do not assume something like this,
> > That is why you are getting an invalid result.
> > > when I ask whether:
> > > ALL(x):P(x)=>ALL(y):[P(y) & P(f(y))]
> > > is provable in DC Proof.
> > Too many missing details. No wonder it is not a required subject even in pure math programs (e.g. at MIT).
> > > I didn't say the above is a FOL formula.
> > Messy details, eh, Jan Burse? Unfortunately, that's what properly formal proofs are all about.
> > > If it were a FOL formula I wouldn't use the idiosyncratic ALL(x)
> > > or EXIST(z). Most of the time when I post problems towards
> > >
> > > DC Proof, I do not assume they are translated to FOL.
> > I'm afraid, it is your version of FOL that is widely viewed as idiosyncratic with its mysterious, unspecified, but non-empty domains of discourse, etc. It seems mathematicians had to develop their own system of logic, more like that used in DC Proof.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Dan-O-Matik went full berserk:
> I'm afraid, it is your version of FOL

Also the prover on my website doesn't originate
from me. Its the prover written by Jens Otten,
which goes by then name leanseq_v5.pl:

Build Your Own First-Order Prover
Invited Tutorial at CADE in Natal/Brazil
(24 August 2019)
http://jens-otten.de/tutorial_cade19/

Whats wrong with you?