We can also do it Gödel style, follows also, proving seriality
and functionality without the codomain, all FOL validity:

∀x∀y(Ax → (Pxy ↔ f(x)=y)), ∀x∀y((Ax ∧ Pxy) → By)
entails ∀x(Ax → ∃yPxy).

∀x∀y(Ax → (Pxy ↔ f(x)=y)), ∀x∀y((Ax ∧ Pxy) → By)
entails ∀x∀y∀z((Ax ∧ (Pxy ∧ Pxz)) → y=z).

Or doing it even more drastic, also not assume some codomain:

∀x∀y(Ax → (Pxy ↔ f(x)=y))
entails ∀x(Ax → ∃yPxy).

∀x∀y(Ax → (Pxy ↔ f(x)=y)
entails ∀x∀y∀z((Ax ∧ (Pxy ∧ Pxz)) → y=z).

Try yourself:
https://www.umsu.de/trees

Mostowski Collapse schrieb am Montag, 10. Januar 2022 um 23:00:55 UTC+1:
> Its very unclear why DC Proof even needs a Function Axiom?
> Litterally translating Terrence Tao, he says, establishing
> a link from a graph to a FOL function symbol:
>
> /* Terrence Tao */
> ∀x∀y(Xx → (Pxy ↔ f(x)=y))
>
> Its easy to prove then, no axiom needed, FOL validity:
>
> /* Dan-O-Matik Nonsense */
> ∀x∀y(Ax → (Pxy ↔ f(x)=y)), /* Terrence Tao */
> ∀x∀y((Ax ∧ Pxy) → By) /* Function Axiom Domain & Codomain */
> entails ∀x(Ax → Bf(x)). /* Function Axiom Dan-O-Matik Nonsense */
> https://www.umsu.de/trees/#~6x~6y%28Ax~5%28Pxy~4f%28x%29=y%29%29,~6x~6y%28Ax~1Pxy~5By%29|=~6x%28Ax~5Bf%28x%29%29
>
> We can also prove that most of the LHS of the Function Axiom
> is unnecessary, again no axiom needed, FOL validity:
>
> /* Seriality is Redundant */
> ∀x∀y(Ax → (Pxy ↔ f(x)=y)), /* Terrence Tao */
> ∀x∀y((Ax ∧ Pxy) → By) /* Function Axiom Domain & Codomain */
> entails ∀x(Ax → ∃y(By ∧ Pxy)). /* Function Axiom Seriality */
> https://www.umsu.de/trees/#~6x~6y%28Ax~5%28Pxy~4f%28x%29=y%29%29,~6x~6y%28Ax~1Pxy~5By%29|=~6x%28Ax~5~7y%28By~1Pxy%29%29
>
> /* Functionality is Redundant */
> ∀x∀y(Ax → (Pxy ↔ f(x)=y)), /* Terrence Tao */
> ∀x∀y((Ax ∧ Pxy) → By) /* Function Axiom Domain & Codomain */
> entails ∀x∀y∀z((Ax ∧ (By ∧ (Pxy ∧ (Bz ∧ Pxz)))) → y=z). /* Function Axiom Seriality */
> https://www.umsu.de/trees/#~6x~6y%28Ax~5%28Pxy~4f%28x%29=y%29%29,~6x~6y%28Ax~1Pxy~5By%29|=~6x~6y~6z%28Ax~1By~1Pxy~1Bz~1Pxz~5y=z%29

On Monday, January 10, 2022 at 5:00:55 PM UTC-5, Mostowski Collapse wrote:
> Its very unclear why DC Proof even needs a Function Axiom?

You need it to construct or prove the existence of any required functions. If you start with Peano's Axioms for only N, S and 0, you will need some way to prove the existence of other stuff like addition, multiplication and exponentiation functions using only the axioms of set theory.

Dan

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

Its usually done with other axioms. See other thread.

Dan Christensen schrieb am Montag, 10. Januar 2022 um 23:15:54 UTC+1:
> On Monday, January 10, 2022 at 5:00:55 PM UTC-5, Mostowski Collapse wrote:
> > Its very unclear why DC Proof even needs a Function Axiom?
> You need it to construct or prove the existence of any required functions.. If you start with Peano's Axioms for only N, S and 0, you will need some way to prove the existence of other stuff like addition, multiplication and exponentiation functions using only the axioms of set theory.
> 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 10, 2022 at 5:30:54 PM UTC-5, Mostowski Collapse wrote:
> Its usually done with other axioms. See other thread.
>

Looks like a pedagogical nightmare. I prefer my more straightforward approach.

Dan

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

No, its rather easy. And more useful. Since it also defines f=g.

Dan Christensen schrieb am Montag, 10. Januar 2022 um 23:42:37 UTC+1:
> On Monday, January 10, 2022 at 5:30:54 PM UTC-5, Mostowski Collapse wrote:
> > Its usually done with other axioms. See other thread.
> >
> Looks like a pedagogical nightmare. I prefer my more straightforward approach.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Maybe you find the axioms even here. If not,
it is nevertheless the classic to explain FOL, SOL and HOL.
See chapter "Der Erweiterte Prädikatenkalkül".

Grundzüge der theoretischen Logik
von David Hilbert, Wilhelm Ackermann - 1938
https://books.google.ch/books?id=NEiGBwAAQBAJ&printsec=frontcover&hl=de&source=gbs_ge_summary_r&cad=0#v=onepage&q&f=false

Principles of Mathematical Logic - Wikipedia Article
https://en.wikipedia.org/wiki/Principles_of_Mathematical_Logic

Mostowski Collapse schrieb am Montag, 10. Januar 2022 um 23:43:50 UTC+1:
> No, its rather easy. And more useful. Since it also defines f=g.
> Dan Christensen schrieb am Montag, 10. Januar 2022 um 23:42:37 UTC+1:
> > On Monday, January 10, 2022 at 5:30:54 PM UTC-5, Mostowski Collapse wrote:
> > > Its usually done with other axioms. See other thread.
> > >
> > Looks like a pedagogical nightmare. I prefer my more straightforward approach.
> > 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 10, 2022 at 5:43:50 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 10. Januar 2022 um 23:42:37 UTC+1:
> > On Monday, January 10, 2022 at 5:30:54 PM UTC-5, Mostowski Collapse wrote:
> > > Its usually done with other axioms. See other thread.
> > >
> > Looks like a pedagogical nightmare. I prefer my more straightforward approach.

> No, its rather easy. And more useful. Since it also defines f=g.

Bullshit! And you end up with Burse's Paradox. No thanks!!!

Dan

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

No you don't end up with this paradox, if you avoid higher
order and FOL function symbols all together. You would
then not prove the existence of a FOL function symbol,
but simply the existence of a set-like function.

You then don't need to add any axioms at all, FOL and
ZFC is sufficient. For example to prove existence of
an inverse function for every injective and surjective
function f : A -> B is very easy with FOL and ZFC alone.

You make the following detour:

Assume FOL Function f Get non-unique FOL Function f^(-1)
| ^
Comprehension | | Function Axiom
v |
Get unique Set-like Function g ----> Get unique Set-like Function g^(-1)

But nobody does it like that, because your Function
Axion renders a non-unique result. Usually people
prove the matter as follows:

Assume Set-like Function g ----> Get unique Set-like Function g^(-1)

No detour over a stupid Function Axiom. But to do
it correctly and directly with set-like functions, you
need to read function application g(x) differently.

Dont use g(x) with FOL function symbol semantic when
g is a set-like function. Read it for example g'x where
' is the Peano apostroph. There are like a dozen more

methods to do it correctly.

Dan Christensen schrieb am Montag, 10. Januar 2022 um 23:57:29 UTC+1:
> On Monday, January 10, 2022 at 5:43:50 PM UTC-5, Mostowski Collapse wrote:
>
>
>
> > Dan Christensen schrieb am Montag, 10. Januar 2022 um 23:42:37 UTC+1:
> > > On Monday, January 10, 2022 at 5:30:54 PM UTC-5, Mostowski Collapse wrote:
> > > > Its usually done with other axioms. See other thread.
> > > >
> > > Looks like a pedagogical nightmare. I prefer my more straightforward approach.
>
> > No, its rather easy. And more useful. Since it also defines f=g.
> Bullshit! And you end up with Burse's Paradox. No thanks!!!
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

A method that has recently become popular
is the Maybe monad. You find this for example
in Isabelle/HOL etc..

Example: the Maybe monad
The Maybe Monad is a simple but very useful
example of a monadic computation

You need a constant "none" and a compound
"some". You can then indeed model a
set-like function F as a FOL function symbol f,

by stipulating:

some(y) (x,y) e F
f(x) = <
none ¬∃y(x,y) e F

And now there is a bijection between the
set theory function space A -> B and
a collection of FOL function symbols:

A -> B <--> { f | ∀(x e A => ∃(y e B & f(x)=some(y)) &
∀(~(x e A) => f(x)=none) }

By suitable axioms for none and some, it
can be arrange that the FOL equality fits
directly with the free logic equality, where

there is a single emptyness, and emptyness
equals itself but doesn't equal non-emptyness.
Your (Dan-O-Matik Forall) rule could be modelled by:

ALL(x):P(x)
---------------- (Dan-O-Matik Forall)
P(some(t))

Or you define it as:

ALL(x):P(x) <=> ∀yP(some(y))

LoL

Mostowski Collapse schrieb:> No you don't end up with this paradox, if
you avoid higher
> order and FOL function symbols all together. You would
> then not prove the existence of a FOL function symbol,
> but simply the existence of a set-like function.
>
> You then don't need to add any axioms at all, FOL and
> ZFC is sufficient. For example to prove existence of
> an inverse function for every injective and surjective
> function f : A -> B is very easy with FOL and ZFC alone.
>
> You make the following detour:
>
> Assume FOL Function f Get non-unique FOL Function
f^(-1)
> |
^
> Comprehension | |
Function Axiom
> v
|
> Get unique Set-like Function g ----> Get unique Set-like
Function g^(-1)
>
> But nobody does it like that, because your Function
> Axion renders a non-unique result. Usually people
> prove the matter as follows:
>
> Assume Set-like Function g ----> Get unique Set-like
Function g^(-1)
>
> No detour over a stupid Function Axiom. But to do
> it correctly and directly with set-like functions, you
> need to read function application g(x) differently.
>
> Dont use g(x) with FOL function symbol semantic when
> g is a set-like function. Read it for example g'x where
> ' is the Peano apostroph. There are like a dozen more
>
> methods to do it correctly.

Oops, forget the link:

Example: the Maybe monad
The Maybe Monad is a simple but very useful example of a monadic computation
https://www.futurelearn.com/info/courses/functional-programming-haskell/0/steps/27247

The simple example in the above would
be to take the head of a list. But unfortunately
an empty list has no head.

So how do you model a list in DC Proof,
and this mapping:

head : List -> Maybe(List) ?

How do you do this in DC Proof? No chance
to do it with your nonsense ALL(x):[x e A => f(x) e B].
This would lead to absolutely nowhere.

Because in Functional Programming the
Burse Paradox is very important. In Functional
Programming we might want to query

a list for a head, and then decide upon
whether there is a head or not, what to do next.
The Burse Paradox helps making a decision,

since it says that the value of function outside
its domain is never in the shadows. Thats just
Dan-O-Matik nonsense.

Mostowski Collapse schrieb am Dienstag, 11. Januar 2022 um 02:18:44 UTC+1:
> A method that has recently become popular
> is the Maybe monad. You find this for example
> in Isabelle/HOL etc..
>
> Example: the Maybe monad
> The Maybe Monad is a simple but very useful
> example of a monadic computation
>
> You need a constant "none" and a compound
> "some". You can then indeed model a
> set-like function F as a FOL function symbol f,
>
> by stipulating:
>
> some(y) (x,y) e F
> f(x) = <
> none ¬∃y(x,y) e F
>
> And now there is a bijection between the
> set theory function space A -> B and
> a collection of FOL function symbols:
>
> A -> B <--> { f | ∀(x e A => ∃(y e B & f(x)=some(y)) &
> ∀(~(x e A) => f(x)=none) }
>
> By suitable axioms for none and some, it
> can be arrange that the FOL equality fits
> directly with the free logic equality, where
>
> there is a single emptyness, and emptyness
> equals itself but doesn't equal non-emptyness.
> Your (Dan-O-Matik Forall) rule could be modelled by:
>
> ALL(x):P(x)
> ---------------- (Dan-O-Matik Forall)
> P(some(t))
>
> Or you define it as:
>
> ALL(x):P(x) <=> ∀yP(some(y))
>
> LoL
>
> Mostowski Collapse schrieb:> No you don't end up with this paradox, if
> you avoid higher
> > order and FOL function symbols all together. You would
> > then not prove the existence of a FOL function symbol,
> > but simply the existence of a set-like function.
> >
> > You then don't need to add any axioms at all, FOL and
> > ZFC is sufficient. For example to prove existence of
> > an inverse function for every injective and surjective
> > function f : A -> B is very easy with FOL and ZFC alone.
> >
> > You make the following detour:
> >
> > Assume FOL Function f Get non-unique FOL Function
> f^(-1)
> > |
> ^
> > Comprehension | |
> Function Axiom
> > v
> |
> > Get unique Set-like Function g ----> Get unique Set-like
> Function g^(-1)
> >
> > But nobody does it like that, because your Function
> > Axion renders a non-unique result. Usually people
> > prove the matter as follows:
> >
> > Assume Set-like Function g ----> Get unique Set-like
> Function g^(-1)
> >
> > No detour over a stupid Function Axiom. But to do
> > it correctly and directly with set-like functions, you
> > need to read function application g(x) differently.
> >
> > Dont use g(x) with FOL function symbol semantic when
> > g is a set-like function. Read it for example g'x where
> > ' is the Peano apostroph. There are like a dozen more
> >
> > methods to do it correctly.

On Monday, January 10, 2022 at 8:04:49 PM UTC-5, Mostowski Collapse wrote:
> No you don't end up with this paradox, if you avoid higher
> order and FOL function symbols all together. You would
> then not prove the existence of a FOL function symbol,
> but simply the existence of a set-like function.
>
> You then don't need to add any axioms at all, FOL and
> ZFC is sufficient.

Aye, there's the rub! For the most part, those axioms are seldom used in most textbook math proofs. Must be frustrating as hell for you. What they actually use is what I have endeavoured to implement in DC Proof. So, you can have your Burse's Paradox if you like. I will stick with what actually works in mathematical practice, 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

As usual you are talking nonsense and
even contradicting your own DC poop tool.
Can you prove the following in DC Proof:

ALL(n):ALL(x):[n e N & x e R & x > 0 => 1 + n*x =< (1+x)^n]
https://shemesh.larc.nasa.gov/fm/pvs/TheMartian/

dcproof5.exe changed the menus. Now it
generates some nonsense axioms about Peano,
and multiplication like that:

8 ALL(a):ALL(b):[a ε n & b ε n => a*b ε n]
& ALL(a):[a ε n => a*1=a]
& ALL(a):ALL(b):[a ε n & b ε n => a*(b+1)=a*b+a]
Definition

But how do you do a multiplication in R?
The above might or might not agree with R
outside of N, because in your own words

ALL(a):ALL(b):[a ε n & b ε n => a*b ε n] would
leave a*b in the shadows when ~a ε n | ~b ε n.
So you could have ALL(a):ALL(b):[a ε n & b ε n

=> a*b ε n] and ALL(a):ALL(b):[a ε r & b ε r =>
a*b ε r] side by side. But you cannot apply
your Peano induction axiom without ZFC.

Because you have to construct a set, subset
of n, with the following properties:

1 ε a
ALL(b):[b ε a => b+1 ε a]

You need to construct this set for x > 0 =>
1 + n*x =< (1+x)^n. So every application of
induction in DC Proof will need set theory.

So why bash set theory, when your induction
axiom is set theoretical?

You don't make sense Dan-O-Matik.

Dan Christensen schrieb am Dienstag, 11. Januar 2022 um 04:13:39 UTC+1:
> > You then don't need to add any axioms at all, FOL and ZFC is sufficient..
> Aye, there's the rub! For the most part, those axioms are seldom used in most textbook math proofs.

So stop talking nonsense about some text book
paranoia. Here is the axiom your are presenting
for induction inside your DC poop tool:

7 ALL(a):[Set(a) & 1 ε a &
ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]]
Axiom

So you need set theory very deeply. I guess
you will need more axioms from set theory
if you would construct R.

What ZFC axioms are needed for R? The
Martian Problem has both N and R in it.
Can you do it in DC poop?

Mostowski Collapse schrieb am Mittwoch, 12. Januar 2022 um 23:21:58 UTC+1:
> As usual you are talking nonsense and
> even contradicting your own DC poop tool.
> Can you prove the following in DC Proof:
>
> ALL(n):ALL(x):[n e N & x e R & x > 0 => 1 + n*x =< (1+x)^n]
> https://shemesh.larc.nasa.gov/fm/pvs/TheMartian/
>
> dcproof5.exe changed the menus. Now it
> generates some nonsense axioms about Peano,
> and multiplication like that:
>
> 8 ALL(a):ALL(b):[a ε n & b ε n => a*b ε n]
> & ALL(a):[a ε n => a*1=a]
> & ALL(a):ALL(b):[a ε n & b ε n => a*(b+1)=a*b+a]
> Definition
>
> But how do you do a multiplication in R?
> The above might or might not agree with R
> outside of N, because in your own words
>
> ALL(a):ALL(b):[a ε n & b ε n => a*b ε n] would
> leave a*b in the shadows when ~a ε n | ~b ε n.
> So you could have ALL(a):ALL(b):[a ε n & b ε n
>
> => a*b ε n] and ALL(a):ALL(b):[a ε r & b ε r =>
> a*b ε r] side by side. But you cannot apply
> your Peano induction axiom without ZFC.
>
> Because you have to construct a set, subset
> of n, with the following properties:
>
> 1 ε a
> ALL(b):[b ε a => b+1 ε a]
>
> You need to construct this set for x > 0 =>
> 1 + n*x =< (1+x)^n. So every application of
> induction in DC Proof will need set theory.
>
> So why bash set theory, when your induction
> axiom is set theoretical?
>
> You don't make sense Dan-O-Matik.
> Dan Christensen schrieb am Dienstag, 11. Januar 2022 um 04:13:39 UTC+1:
> > > You then don't need to add any axioms at all, FOL and ZFC is sufficient.
> > Aye, there's the rub! For the most part, those axioms are seldom used in most textbook math proofs.

On Wednesday, January 12, 2022 at 5:21:58 PM UTC-5, Mostowski Collapse wrote:

>
> dcproof5.exe changed the menus. Now it
> generates some nonsense axioms about Peano,
> and multiplication like that:
>
> 8 ALL(a):ALL(b):[a ε n & b ε n => a*b ε n]
> & ALL(a):[a ε n => a*1=a]
> & ALL(a):ALL(b):[a ε n & b ε n => a*(b+1)=a*b+a]
> Definition
>

In proofs that I post here and at my blog, I always use 0 as the first natural number. (See axioms below)
> But how do you do a multiplication in R?

I recommend starting by introducing the field axioms, etc. for the real numbers.

> .. But you cannot apply
> your Peano induction axiom without ZFC.
>

As you must know by now, I usually introduce Peano's Axioms at the beginning of proofs as:

1. Set(n)
(Axiom)

2. 0 in n
(Axiom)

3. ALL(a):[a in n => s(a) in n]
(Axiom)

4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
(Axiom)

5. ALL(a):[a in n => ~s(a)=0]
(Axiom)

6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in a => s(b) in a]
=> ALL(b):[b in n => b in a]]]
(Axiom)

No need for the pedagogical nightmare that is ZFC -- AOI, etc.

Dan

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

From your posts about a) making use of sets and
then b) bashing ZFC, I can only conclude that you
are either schizophrenic or paranoid or both.

You nowhere proved so far:

|- EXISTS(n):Peano(n)

When I use your Peano nonsense and prove A(n
from it, then all I prove is:

|- ALL(n):[Peano(n) => A(n)]

But do I know whether EXISTS(n):Peano(n) ?

Dan Christensen schrieb am Mittwoch, 12. Januar 2022 um 23:57:10 UTC+1:
> On Wednesday, January 12, 2022 at 5:21:58 PM UTC-5, Mostowski Collapse wrote:
>
> >
> > dcproof5.exe changed the menus. Now it
> > generates some nonsense axioms about Peano,
> > and multiplication like that:
> >
> > 8 ALL(a):ALL(b):[a ε n & b ε n => a*b ε n]
> > & ALL(a):[a ε n => a*1=a]
> > & ALL(a):ALL(b):[a ε n & b ε n => a*(b+1)=a*b+a]
> > Definition
> >
> In proofs that I post here and at my blog, I always use 0 as the first natural number. (See axioms below)
> > But how do you do a multiplication in R?
> I recommend starting by introducing the field axioms, etc. for the real numbers.
>
> > .. But you cannot apply
> > your Peano induction axiom without ZFC.
> >
> As you must know by now, I usually introduce Peano's Axioms at the beginning of proofs as:
>
> 1. Set(n)
> (Axiom)
>
> 2. 0 in n
> (Axiom)
>
> 3. ALL(a):[a in n => s(a) in n]
> (Axiom)
>
> 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> (Axiom)
>
> 5. ALL(a):[a in n => ~s(a)=0]
> (Axiom)
>
> 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> => [0 in a & ALL(b):[b in a => s(b) in a]
> => ALL(b):[b in n => b in a]]]
> (Axiom)
>
> No need for the pedagogical nightmare that is ZFC -- AOI, etc.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On the other hand, ZFC proofs existence of omega.
Why are you paranoid and schizoprenic about that?

How do you want construct R correctly
if you cannot construct N correctly?

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 00:21:16 UTC+1:
> From your posts about a) making use of sets and
> then b) bashing ZFC, I can only conclude that you
> are either schizophrenic or paranoid or both.
>
> You nowhere proved so far:
>
> |- EXISTS(n):Peano(n)
>
> When I use your Peano nonsense and prove A(n)
> from it, then all I prove is:
>
> |- ALL(n):[Peano(n) => A(n)]
>
> But do I know whether EXISTS(n):Peano(n) ?
> Dan Christensen schrieb am Mittwoch, 12. Januar 2022 um 23:57:10 UTC+1:
> > On Wednesday, January 12, 2022 at 5:21:58 PM UTC-5, Mostowski Collapse wrote:
> >
> > >
> > > dcproof5.exe changed the menus. Now it
> > > generates some nonsense axioms about Peano,
> > > and multiplication like that:
> > >
> > > 8 ALL(a):ALL(b):[a ε n & b ε n => a*b ε n]
> > > & ALL(a):[a ε n => a*1=a]
> > > & ALL(a):ALL(b):[a ε n & b ε n => a*(b+1)=a*b+a]
> > > Definition
> > >
> > In proofs that I post here and at my blog, I always use 0 as the first natural number. (See axioms below)
> > > But how do you do a multiplication in R?
> > I recommend starting by introducing the field axioms, etc. for the real numbers.
> >
> > > .. But you cannot apply
> > > your Peano induction axiom without ZFC.
> > >
> > As you must know by now, I usually introduce Peano's Axioms at the beginning of proofs as:
> >
> > 1. Set(n)
> > (Axiom)
> >
> > 2. 0 in n
> > (Axiom)
> >
> > 3. ALL(a):[a in n => s(a) in n]
> > (Axiom)
> >
> > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > (Axiom)
> >
> > 5. ALL(a):[a in n => ~s(a)=0]
> > (Axiom)
> >
> > 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in a => s(b) in a]
> > => ALL(b):[b in n => b in a]]]
> > (Axiom)
> >
> > No need for the pedagogical nightmare that is ZFC -- AOI, etc.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

R is exactly an example where you possibly need
more than only handwaving. Also the axiom of infinity
does not imply R. You can easily have axiom of

infinity and not some R. For a start, you probably
need the power set axiom. Do you have the power set
axiom in DC Proof? No. You could then possibly do

something like, where Constr is the construction:

ALL(n):[Peano(n) => Field(Constr(n))]

Then from:

EXIST(n):Peano(n)

We can infer:

EXIST(r):Reals(r)

Something you cannot anymore prove with your
new (Forall) rule? Since you would get circular
R(n) e S, before you have Reals.

LMAO!

Dunno, but in FOL it works:

(∀n(Pn → Fc(n)) ∧ ∃nPn) → ∃rFr is valid.
https://www.umsu.de/trees/#~6n%28Pn~5Fc%28n%29%29~1~7nPn~5~7rFr

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 00:24:51 UTC+1:
> On the other hand, ZFC proofs existence of omega.
> Why are you paranoid and schizoprenic about that?
>
> How do you want construct R correctly
> if you cannot construct N correctly?
> Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 00:21:16 UTC+1:
> > From your posts about a) making use of sets and
> > then b) bashing ZFC, I can only conclude that you
> > are either schizophrenic or paranoid or both.
> >
> > You nowhere proved so far:
> >
> > |- EXISTS(n):Peano(n)
> >
> > When I use your Peano nonsense and prove A(n)
> > from it, then all I prove is:
> >
> > |- ALL(n):[Peano(n) => A(n)]
> >
> > But do I know whether EXISTS(n):Peano(n) ?
> > Dan Christensen schrieb am Mittwoch, 12. Januar 2022 um 23:57:10 UTC+1:
> > > On Wednesday, January 12, 2022 at 5:21:58 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > >
> > > > dcproof5.exe changed the menus. Now it
> > > > generates some nonsense axioms about Peano,
> > > > and multiplication like that:
> > > >
> > > > 8 ALL(a):ALL(b):[a ε n & b ε n => a*b ε n]
> > > > & ALL(a):[a ε n => a*1=a]
> > > > & ALL(a):ALL(b):[a ε n & b ε n => a*(b+1)=a*b+a]
> > > > Definition
> > > >
> > > In proofs that I post here and at my blog, I always use 0 as the first natural number. (See axioms below)
> > > > But how do you do a multiplication in R?
> > > I recommend starting by introducing the field axioms, etc. for the real numbers.
> > >
> > > > .. But you cannot apply
> > > > your Peano induction axiom without ZFC.
> > > >
> > > As you must know by now, I usually introduce Peano's Axioms at the beginning of proofs as:
> > >
> > > 1. Set(n)
> > > (Axiom)
> > >
> > > 2. 0 in n
> > > (Axiom)
> > >
> > > 3. ALL(a):[a in n => s(a) in n]
> > > (Axiom)
> > >
> > > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > > (Axiom)
> > >
> > > 5. ALL(a):[a in n => ~s(a)=0]
> > > (Axiom)
> > >
> > > 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > > => [0 in a & ALL(b):[b in a => s(b) in a]
> > > => ALL(b):[b in n => b in a]]]
> > > (Axiom)
> > >
> > > No need for the pedagogical nightmare that is ZFC -- AOI, etc.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

Corr.: Typo R(_) -> Constr(_)

Something you cannot anymore prove with your
new (Forall) rule? Since you would get circular
Constr(n) e S, before you have Reals.

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 00:34:26 UTC+1:
> R is exactly an example where you possibly need
> more than only handwaving. Also the axiom of infinity
> does not imply R. You can easily have axiom of
>
> infinity and not some R. For a start, you probably
> need the power set axiom. Do you have the power set
> axiom in DC Proof? No. You could then possibly do
>
> something like, where Constr is the construction:
>
> ALL(n):[Peano(n) => Field(Constr(n))]
>
> Then from:
>
> EXIST(n):Peano(n)
>
> We can infer:
>
> EXIST(r):Reals(r)
>
> Something you cannot anymore prove with your
> new (Forall) rule? Since you would get circular
> R(n) e S, before you have Reals.
>
> LMAO!
>
> Dunno, but in FOL it works:
>
> (∀n(Pn → Fc(n)) ∧ ∃nPn) → ∃rFr is valid.
> https://www.umsu.de/trees/#~6n%28Pn~5Fc%28n%29%29~1~7nPn~5~7rFr
> Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 00:24:51 UTC+1:
> > On the other hand, ZFC proofs existence of omega.
> > Why are you paranoid and schizoprenic about that?
> >
> > How do you want construct R correctly
> > if you cannot construct N correctly?
> > Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 00:21:16 UTC+1:
> > > From your posts about a) making use of sets and
> > > then b) bashing ZFC, I can only conclude that you
> > > are either schizophrenic or paranoid or both.
> > >
> > > You nowhere proved so far:
> > >
> > > |- EXISTS(n):Peano(n)
> > >
> > > When I use your Peano nonsense and prove A(n)
> > > from it, then all I prove is:
> > >
> > > |- ALL(n):[Peano(n) => A(n)]
> > >
> > > But do I know whether EXISTS(n):Peano(n) ?
> > > Dan Christensen schrieb am Mittwoch, 12. Januar 2022 um 23:57:10 UTC+1:
> > > > On Wednesday, January 12, 2022 at 5:21:58 PM UTC-5, Mostowski Collapse wrote:
> > > >
> > > > >
> > > > > dcproof5.exe changed the menus. Now it
> > > > > generates some nonsense axioms about Peano,
> > > > > and multiplication like that:
> > > > >
> > > > > 8 ALL(a):ALL(b):[a ε n & b ε n => a*b ε n]
> > > > > & ALL(a):[a ε n => a*1=a]
> > > > > & ALL(a):ALL(b):[a ε n & b ε n => a*(b+1)=a*b+a]
> > > > > Definition
> > > > >
> > > > In proofs that I post here and at my blog, I always use 0 as the first natural number. (See axioms below)
> > > > > But how do you do a multiplication in R?
> > > > I recommend starting by introducing the field axioms, etc. for the real numbers.
> > > >
> > > > > .. But you cannot apply
> > > > > your Peano induction axiom without ZFC.
> > > > >
> > > > As you must know by now, I usually introduce Peano's Axioms at the beginning of proofs as:
> > > >
> > > > 1. Set(n)
> > > > (Axiom)
> > > >
> > > > 2. 0 in n
> > > > (Axiom)
> > > >
> > > > 3. ALL(a):[a in n => s(a) in n]
> > > > (Axiom)
> > > >
> > > > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > > > (Axiom)
> > > >
> > > > 5. ALL(a):[a in n => ~s(a)=0]
> > > > (Axiom)
> > > >
> > > > 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > > > => [0 in a & ALL(b):[b in a => s(b) in a]
> > > > => ALL(b):[b in n => b in a]]]
> > > > (Axiom)
> > > >
> > > > No need for the pedagogical nightmare that is ZFC -- AOI, etc.
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com

This is the proof that worked in dcproof2.exe, but
does not work anymore in dcproof5.exe:

ALL(n):[Peano(n) => Field(constr(n))]
Premise

2 EXIST(n):Peano(n)
Premise

3 ~EXIST(r):Field(r)
Premise

4 Peano(a)
E Spec, 2

5 ~~ALL(r):~Field(r)
Quant, 3

6 ALL(r):~Field(r)
Rem DNeg, 5

7 Peano(a) => Field(constr(a))
U Spec, 1

8 ~Field(constr(a))
U Spec, 6, 7

9 Field(constr(a))
Detach, 7, 4

10 Field(constr(a)) & ~Field(constr(a))
Join, 9, 8

11 ~~EXIST(r):Field(r)
Conclusion, 3

12 EXIST(r):Field(r)
Rem DNeg, 11

13 EXIST(n):Peano(n) => EXIST(r):Field(r)
Conclusion, 2

14 ALL(constr):[ALL(n):[Peano(n) => Field(constr(n))]
=> [EXIST(n):Peano(n) => EXIST(r):Field(r)]]
Conclusion, 1

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 00:38:33 UTC+1:
> Corr.: Typo R(_) -> Constr(_)
> Something you cannot anymore prove with your
> new (Forall) rule? Since you would get circular
> Constr(n) e S, before you have Reals.
>
> Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 00:34:26 UTC+1:
> > Dunno, but in FOL it works:
> >
> > (∀n(Pn → Fc(n)) ∧ ∃nPn) → ∃rFr is valid.
> > https://www.umsu.de/trees/#~6n%28Pn~5Fc%28n%29%29~1~7nPn~5~7rFr

On Wednesday, January 12, 2022 at 6:21:16 PM UTC-5, Mostowski Collapse wrote:

> You nowhere proved so far:
>
> |- EXISTS(n):Peano(n)
>

Wrong. I have posted the link here several times: http://www.dcproof.com/ProofByInduction.htm

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, January 12, 2022 at 6:21:16 PM UTC-5, Mostowski Collapse wrote:

> You nowhere proved so far:
>
> |- EXISTS(n):Peano(n)
>

Wrong. I have posted the link here several times: http://www.dcproof.com/ProofByInduction.html

Dan

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

What axiom shows?

|- EXIST(f):Dedekind(f)

Most likely its also an old proof with dcproof2.exe,
that doesn't work anymore with dcproof5.exe.
So even if you had the above, you could not

anymore prove:

|- EXISTS(n):Peano(n)

For example in the link
http://www.dcproof.com/ProofByInduction.html
I find:

Apply definition of n for f(x)

30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
U Spec, 11

What is the f(x) e S before line 30? Its not
an U Spec from dcproof5.exe with two reference
lines, it has only one reference line 11.

Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 02:57:54 UTC+1:
> On Wednesday, January 12, 2022 at 6:21:16 PM UTC-5, Mostowski Collapse wrote:
>
> > You nowhere proved so far:
> >
> > |- EXISTS(n):Peano(n)
> >
> Wrong. I have posted the link here several times: http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 13, 2022 at 2:39:50 AM UTC-5, Mostowski Collapse wrote:
> What axiom shows?
>
> |- EXIST(f):Dedekind(f)
>

ZFC has an axiom postulating the existence of an infinite set. Similarly, my proof postulates the exist of an infinite set.

http://www.dcproof.com/ProofByInduction.html

> Most likely its also an old proof with dcproof2.exe,
> that doesn't work anymore with dcproof5.exe.
> So even if you had the above, you could not
>
> anymore prove:
>
> |- EXISTS(n):Peano(n)
>
> For example in the link
> http://www.dcproof.com/ProofByInduction.html
> I find:
>
> Apply definition of n for f(x)
>
> 30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
> & s1 e b
> & ALL(c):[c e b & c e s => f(c) e b]
> => f(x) e b]
> U Spec, 11
>
> What is the f(x) e S before line 30?

When we postulate the existence of a Dedekind infinite set X, we postulate the existence of a function f: X --> X that is injective but not surjective. It was introduced on 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

Your Dedekind -> Peano proof doesn't work anymore.
Its the same problem like in this proof, where
this step doesn't work anymore:

> This is the proof that worked in dcproof2.exe, but
> does not work anymore in dcproof5.exe:
> [...]
> 8 ~Field(constr(a))
> U Spec, 6, 7
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ

Because there is no constr(a) e S.

The new error message is:
'constr(a)' must be an element of a set
Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 15:25:12 UTC+1:
> On Thursday, January 13, 2022 at 2:39:50 AM UTC-5, Mostowski Collapse wrote:
> > What axiom shows?
> >
> > |- EXIST(f):Dedekind(f)
> >
> ZFC has an axiom postulating the existence of an infinite set. Similarly, my proof postulates the exist of an infinite set.
>
> http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html
> > Most likely its also an old proof with dcproof2.exe,
> > that doesn't work anymore with dcproof5.exe.
> > So even if you had the above, you could not
> >
> > anymore prove:
> >
> > |- EXISTS(n):Peano(n)
> >
> > For example in the link
> > http://www.dcproof.com/ProofByInduction.html
> > I find:
> >
> > Apply definition of n for f(x)
> >
> > 30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
> > & s1 e b
> > & ALL(c):[c e b & c e s => f(c) e b]
> > => f(x) e b]
> > U Spec, 11
> >
> > What is the f(x) e S before line 30?
> When we postulate the existence of a Dedekind infinite set X, we postulate the existence of a function f: X --> X that is injective but not surjective. It was introduced on 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 Thursday, January 13, 2022 at 10:56:59 AM UTC-5, Mostowski Collapse wrote:
> Your Dedekind -> Peano proof doesn't work anymore.
> Its the same problem like in this proof, where
> this step doesn't work anymore:
> > This is the proof that worked in dcproof2.exe, but
> > does not work anymore in dcproof5.exe:
> > [...]
> > 8 ~Field(constr(a))
> > U Spec, 6, 7
> https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ
>

Doesn't look like any of my proofs. Looks suspiciously wonky... Jan Burse. (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