DC Proof is the biggest teaching mistake

[Mostowski Collapse]

That an empty universe of discourse is allowed has
recently become a hiding space for being lazy.
That an empty universe of discourse is allowed prevents

the inference ALL(x):A(x) => EXIST(x):A(x). But why would
this be even important? It doesn't buy you anything. For
example in the Peano "construction" it is proved:

1) ALL(f):[Dedekind(f) => EXIST(w):Peano(w)]

Now DC Proof prevents going to from 1) to 2):

2) EXIST(f):[Dedekind(f) => EXIST(w):Peano(w)]

Does DC Proof think that the enemy 2) could be used to derive 3)?

3) EXIST(f):Dedekind(f)

Hint: It doesn't, 2) does not imply 3). Guess why?

LMAO!

[Dan Christensen]

On Monday, November 22, 2021 at 5:38:04 AM UTC-5, Mostowski Collapse wrote:
> That an empty universe of discourse is allowed has
> recently become a hiding space for being lazy.

On the contrary, assuming a non-empty universe is a shortcut for lazy logicians. In mathematics, quantifiers are usually restricted to some set, e.g. an arbitrary, possibly empty, a set of numbers, a set of functions, or a set of points in space.

> That an empty universe of discourse is allowed prevents
>
> the inference ALL(x):A(x) => EXIST(x):A(x).

In mathematics, this might be stated as: ALL(x):[x in S => A(x)] => EXIST(x):[x in S & A(x)] for some set S. Of course, this would be false if S is empty. Lazy logicians, however, are simply not interested in such a possibility. Too much work, I guess.

> But why would
> this be even important? It doesn't buy you anything. For
> example in the Peano "construction" it is proved:
>
> 1) ALL(f):[Dedekind(f) => EXIST(w):Peano(w)]
>

.
Actually I prove that that from any Dedekind infinite set X, we can select a subset N on which the Peano Axiom will hold. More formally:
.
ALL(x):ALL(f):[Set(x)
.
& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
.
=> EXIST(n):EXIST(x0):[Set(n)
.
& ALL(a):[a in n => a in x]
& x0 in n
& ALL(a):[a in n => f(a) in n]
& ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
& ALL(a):[a in n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b in a => b in n] => [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]
.
Formal proof here: https://dcproof.com/ConstructN.htm
.

> Now DC Proof prevents going to from 1) to 2):
>
> 2) EXIST(f):[Dedekind(f) => EXIST(w):Peano(w)]
>

.
Where do you get such nonsense, Jan Burse? I could as easily have proven:
.
EXIST(x):EXIST(f):[Set(x)
.
& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]]
.
=> EXIST(n):EXIST(f):EXIST(x0):[Set(n)
.
& x0 in n
& ALL(a):[a in n => f(a) in n]
& ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
& ALL(a):[a in n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b in a => b in n] => [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]
.
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]

Shouldn't be provable in a logic with a possibly empty
domain of discourse. Because any statement

EXIST(a):A(a)

Is false for the empty domain. So how should it
be possible to prove some EXIST(a):A(a) sentence

from no axioms? Or did you use some axiom that
postulates the existence of some object?

[Dan Christensen]

> Shouldn't be provable in a logic with a possibly empty
> domain of discourse. Because any statement
>
> EXIST(a):A(a)
>
> Is false for the empty domain.

.
True, but so what???

.
> So how should it
> be possible to prove some EXIST(a):A(a) sentence
>
> from no axioms?

.
In DC Proof, there is no theorem or built-in axiom of the form EXIST(a):A(a). You could, of course, have a premise of that form. You could also introduce an axiom of that form at the beginning of your proof. I hope this helps.

[Kip Foh]

🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴
🔴🔴🔴🔴🔴🌕🌕🔴🌕🌕🔴🔴🔴🔴🔴
🔴🔴🔴🔴🌕🌕🌕🔴🔴🌕🌕🔴🔴🔴🔴
🔴🔴🔴🌕🌕🌕🌕🔴🔴🔴🌕🌕🔴🔴🔴
🔴🔴🌕🌕🌕🌕🔴🔴🔴🔴🌕🌕🌕🔴🔴
🔴🌕🌕🌕🌕🌕🌕🔴🔴🔴🔴🌕🌕🔴🔴
🔴🔴🌕🌕🔴🌕🌕🌕🔴🔴🔴🌕🌕🌕🔴
🔴🔴🔴🔴🔴🔴🌕🌕🌕🔴🔴🔴🌕🌕🔴
🔴🔴🔴🔴🔴🔴🔴🌕🌕🌕🔴🌕🌕🌕🔴
🔴🔴🔴🔴🌕🔴🔴🔴🌕🌕🌕🌕🌕🔴🔴
🔴🔴🔴🌕🌕🌕🔴🔴🔴🌕🌕🌕🔴🔴🔴
🔴🌕🌕🌕🔴🌕🌕🌕🌕🌕🌕🌕🌕🔴🔴
🔴🌕🌕🔴🔴🔴🌕🌕🌕🔴🔴🌕🌕🔴🔴
🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴

[Mostowski Collapse]

Why would you even be interested in proving this?

> 2) EXIST(f):[Dedekind(f) => EXIST(w):Peano(w)]

Its not a step on the way to prove this:
> 3) EXIST(f):Dedekind(f)

You can check yourself:

https://www.umsu.de/trees

∃x(Dx → ∃yPy) → ∃xDx is invalid.
Countermodel:
Domain: { 0 }
D: { }
P: { 0 }

Dan Christensen schrieb am Montag, 22. November 2021 um 21:16:13 UTC+1:
> ... wants to prove 2), which isn't possible in DC Proof ...

[Dan Christensen]

On Monday, November 22, 2021 at 7:45:07 PM UTC-5, Mostowski Collapse wrote:
> Why would you even be interested in proving this?
> > 2) EXIST(f):[Dedekind(f) => EXIST(w):Peano(w)]

I wouldn't.

> Its not a step on the way to prove this:
> > 3) EXIST(f):Dedekind(f)
>

I wouldn't want to prove this either.

> You can check yourself:
>
> https://www.umsu.de/trees
>
> ∃x(Dx → ∃yPy) → ∃xDx is invalid.
> Countermodel:
> Domain: { 0 }
> D: { }
> P: { 0 }
>

That Tree Proof Generator works only for standard FOL, not set theory.

Dan

[Mostowski Collapse]

Mathematics proves things like, using some
foundational axioms. Thats standard routine:

3) EXIST(f):Dedekind(f)

You are only too lazy, but say it has to do with empty
domain. But in fact it doesn't have anything to do with
empty domain.

Why should the unwillinglesss to prove something,
i.e. Zorns Lemma, etc.. etc.. something to do with
the empty domain?

Thats only a strawman argument. Your red herring
is stinky as hell.

[Mostowski Collapse]

For example when constructing the reals, its
standard to then prove:

1) EXIST(x):[x e R & x^2 = 2]

To give an example of an irrational number and
that now exists. This is not the same as:

2) ALL(x):[x e Q => x^2 <> 2]

I have never seen a proof of 1) or 2) in DC Proof.

LoL

[Mostowski Collapse]

When constructing the reals bottom up, you will
likely need countable infinite sequences, and to
show the existence of sqrt(2),

you will then need the existence of a particular
countable infinite sequence, but a countable infinite
sequence needs the existence of omega I guess.

Its not enough to have a predicate that somehow
delivers the countable infinite sequence, you then
end up in WM potential infinity, the point

of constructing the reals is to have first class real number
objects, so yes, it is EXTREMLY IMPORTANT, to be be able
to prove things like:

EXIST(f):Dedekind(f)

EXIST(w):Peano(w)

Etc..

Its the bread and butter of theorem proving, otherwise
your domain of discourse can be empty, in the case of DC
Proof, but when its non-empty one still doesn't

know whether it might contain an sqrt(2) object in the
form of an existence proof.

LMAO!

[Mostowski Collapse]

If you don't have sqrt(2) as a real number object, you might
have it as a class. But you refuse to work with classes.
Dedekind cuts, can be also viewed as classes. Assume

Q is some WM potential infinite class, then this Dedekind
cut is also a class:

{ x e Q | x^2 < 2 }

But class have the drawback that you cannot put them
into the scope of quantifiers,

usually if they are only FOL syntactic suggar, you hardly
see them in quantifier scopes. You can check yourself
how many analysis theorems are existence theorems:

- Mean Value Theorem?
- Rolle's theorem
- Etc.. etc..

They are all existence theorems. Proving them the same
way as you did prove Peano, like here:

ALL(f):[Dedekind(f) => EXIST(w):Peano(w)]

Is a little unsatisfactory, because the proof leaves open
whether Dedekind(f) exists, and what the foundation
for it would be.

[Dan Christensen]

> Dan Christensen schrieb am Dienstag, 23. November 2021 um 03:17:05 UTC+1:
> > On Monday, November 22, 2021 at 7:45:07 PM UTC-5, Mostowski Collapse wrote:

.

> Mathematics proves things like, using some
> foundational axioms. Thats standard routine:
>
> 3) EXIST(f):Dedekind(f)
>

Again, I proved:

ALL(x):ALL(f):[Set(x)

& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
.
=> EXIST(n):EXIST(x0):[Set(n)

& ALL(a):[a in n => a in x]
& x0 in n
& ALL(a):[a in n => f(a) in n]
& ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
& ALL(a):[a in n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b in a => b in n] => [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]
.

This universal generalization is a theorem, and the last line of my proof.

.
Formal proof here: https://dcproof.com/ConstructN.htm
.

The first line is the premise:
.
1 Set(x)

& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
.

The first statement could just as easily have been introduced it as an axiom. It's up to the user.

If the first statement was introduced as an axiom, then the first line would be:

EXIST(x):EXIST(f):[Set(x)

& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]

In words, there exists a Dedekind infinite set.

Then the last line would be this theorem:

EXIST(n):EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a in n => a in x] & x0 in n

& ALL(a):[a in n => f(a) in n]
& ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
& ALL(a):[a in n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b in a => b in n]
=> [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]

In words, there exists a set on which the Peano axioms hold.

> You are only too lazy, but say it has to do with empty
> domain. But in fact it doesn't have anything to do with
> empty domain.
>

That makes no sense, Jan Burse. Sorry.

[Mostowski Collapse]

Nope you cannot introduce this as an axiom. It
would consume the name f.

Thats the whole point of Zermelos version from
1908. We don't need to know and even give
a name to the set that is inductive,

we only need an axiom that states its existence.
The rest should work out in logic.

[Mostowski Collapse]

And this here is not FOL, when you use this here as an axiom:

EXIST(x):EXIST(f):[Set(x)

& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]

In FOL you cannot quantify over function symbols.
Only over variables.

So there is still no axiom around, and still no
proof around, which would prove:

EXIST(w):Peano(w)

[Mostowski Collapse]

FOL = First Order Logic

A function symbols is a second order logic object.
If U is the universe of discourse, a class, a variable x
is first order since it ranges over U, i.e. x e U.

But a n-ary function symbol f ranges over subsets
of U^n, basically an n-ary function symbols is
f e P(U^n) plus some restriction that f is functional.

U is first order, P(U) is second order, P(P(U)) is third order
etc.. In FOL you cannot quantify over higher order objects,
you can only quantify over first order objects.

When you provide second order logic, you have to
be careful to keep the logic consistent, especially since
you allow self application in your DC Proof.

Why would you allow the end-user to add arbitrary
second order axioms. Am I also allowed to do that,
or do you call these axioms "wonky"?

[Mostowski Collapse]

And this is buggy nonsense, it refers to x, but when you have
an axiom EXIST(x):... how can you refer to x? You just copy
pasted garbage nonsense.

Dan-O-Matik halucinated:

> Then the last line would be this theorem:
> EXIST(n):EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a in n => a in x] & x0 in n
> & ALL(a):[a in n => f(a) in n]
> & ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
> & ALL(a):[a in n => ~f(a)=x0]
> & ALL(a):[Set(a)
> & ALL(b):[b in a => b in n]
> => [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]
> In words, there exists a set on which the Peano axioms hold.

Maybe there is an easy fix for the x reference, but

it is again second order. Its not a statement inside FOL,
you use EXIST(f) a second order quantifier. ZFC is a FOL theory.
The construction of omega in ZFC is a FOL thing,

no second order logic involved.

[Dan Christensen]

On Tuesday, November 23, 2021 at 1:39:56 PM UTC-5, Mostowski Collapse wrote:

> > The first line is the premise:
> > .
> > 1 Set(x)
> > & ALL(a):[a in x => f(a) in x]
> > & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> > & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
> > .
> > The first statement could just as easily have been introduced it as an axiom. It's up to the user.
> >

[unsnipping]

> > If the first statement was introduced as an axiom, then the first line would be:
> >

> > EXIST(x):EXIST(f):[Set(x)

> > & ALL(a):[a in x => f(a) in x]
> > & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> > & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]

> Nope you cannot introduce this as an axiom.

.
. The part you snipped could certainly be an axiom. Deal with it, Jan Burse. Don't just snip it.

.
> It
> would consume the name f.
>

.
Now, you are sounding like WM. Never a good thing!

.
> Thats the whole point of Zermelos version from
> 1908. We don't need to know and even give
> a name to the set that is inductive,
>

.
AOI is a real dog's breakfast IMHO. Postulating the existence of a Dedekind infinite set (as an axiom or premise) is much more appealing and intuitive, and more or less equivalent IIUC.
.
Dan
.

[Mostowski Collapse]

Why do you talk nonsense all day?

Its only equivalent when you have the axiom of regularity,
or otherwise show injectivety of

succ(x) = x u {x}

You postulate injectivity here, in the third clause:

EXIST(x):EXIST(f):[Set(x)
& ALL(a):[a in x => f(a) in x]

& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]] /* Injectivity */

& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]

The AOI doesn't postulate injectivity anywhere. Also the
AOI doesn't postulate non-surjectivity.

Why do you think Zermelos AOI and Dedekind Infinite are
the same. There are like 3 or 4 different notions

of infinite, which are all subtly different. This is folklore,
would need some time to lookup all the options,

that are usually considered.

[Dan Christensen]

On Tuesday, November 23, 2021 at 4:54:45 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Dienstag, 23. November 2021 um 21:18:06 UTC+1:
> > AOI is a real dog's breakfast IMHO. Postulating the existence of a Dedekind infinite set (as an axiom or premise) is much more appealing and intuitive, and more or less equivalent IIUC.
> > .

> Why do you talk nonsense all day?
>

> Its only equivalent when you have the axiom of regularity...

Like I said, a dog's breakfast. A pedagogical nightmare. And while Dedekind infinite sets are often mentioned in math textbooks, the ZFC axioms are seldom if ever mentioned other than in passing, as I recall.

If you really must derive Peano's Axioms, it is much better to start with a Dedekind infinite set. It is simpler and far more intuitive. That said, I prefer to simply start by stating Peano's Axioms and skip the derivation. Interestingly, that the set of natural numbers exists is even more self-evident than either alternative.

Dan

[Mostowski Collapse]

You continue talking nonsense as usual.

[Fritz Feldhase]

On Tuesday, November 23, 2021 at 6:30:57 PM UTC+1, Dan Christensen wrote:

> Again, I proved:

& ALL(a):[Set(a)
& ALL(b):[b in a => b in n]
=> [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]

The usual form of induction in this case would be

& ALL(a):[Set(a)
& ALL(b):[b in a => b in n]
=> [x0 in a & ALL(b):[b in a => f(b) in a]

=> n = a]]]]

[Dan Christensen]

> I find this form of PMI to be less useful in proofs.

[Mostowski Collapse]

Dan-O-Matik was talking nonsense:

> And while Dedekind infinite sets are often mentioned in math
textbooks, the ZFC axioms are seldom if ever mentioned other
than in passing, as I recall.

An example of a simple theorem where you need some ZF axiom is:

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

The above is provable in FOL+ZF.
It is not provable in DC Proof alone.

[Mostowski Collapse]

Additionally assuming f : x -> y for some x,y is
not required to prove it in FOL+ZF. It would be also
nonsense, since the preimage a is not supposed

to be a subset of x. It can be any set a from the
whole universe of discoure. How would this theorem
then work? Well you need something from ZF,

but FOL itself also helps, since one can prove:

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

[Mostowski Collapse]

I am not suggesting Borel determinancy as an exercise:
“Skolem needed a snack, so he ate enough for an entire wedding party”.
https://golem.ph.utexas.edu/category/2021/07/borel_determinacy_does_not_require_replacement.html

I am myself a little astonished that the basic math
problem needs some axiom? Right? If I have time
I will provide a proof of it using the axiom I have

in mind. I don't know yet how to show that it cannot
be proved without the axiom or a weaker form of it.
But I am assuming I will be not in a hurry since DC

Proof will not be able to prove the same basic math.

[Mostowski Collapse]

Can we buy these double chimpazee copper bracelets
already on Amazon? Here is your fallacy explained.

We can prove:

/* provable */
F is hyperbola => ALL(x):[x≠0 => x*F(x)=1]

But we cannot prove:

/* not provable */
ALL(x):[x≠0 => x*F(x)=1] => F is hyperbola

Got it?

[Mostowski Collapse]

Even a blind mole can show both claims:

> /* provable */
> F is hyperbola => ALL(x):[x≠0 => x*F(x)=1]

/* serial */
∀a∃bFab ∧
/* functional */
(∀a∀b∀c((Fab ∧ Fac) → b=c) ∧
/* hyperbola */
∀a∀b(Fab ↔ m(a,b)=z))
entails
/* double chimpanzee */
∀a(¬a=z → ∃b(Fab ∧ m(a,b)=z)).
https://www.umsu.de/trees/#~6a~7bFab~1~6a~6b~6c%28Fab~1Fac~5b=c%29~1~6a~6b%28Fab~4m%28a,b%29=z%29|=~6a%28~3a=z~5~7b%28Fab~1m%28a,b%29=z%29%29

> /* not provable */
> ALL(x):[x≠0 => x*F(x)=1] => F is hyperbola

/* serial */
∀a∃bFab ∧
/* functional */
(∀a∀b∀c((Fab ∧ Fac) → b=c) ∧
/* double chimpanzee */
∀a(¬a=z → ∃b(Fab ∧ m(a,b)=z)))
does not entail
/* hyperbola */
∀a∀b(Fab ↔ m(a,b)=z).
https://www.umsu.de/trees/#~6a~7bFab~1~6a~6b~6c%28Fab~1Fac~5b=c%29~1~6a%28~3a=z~5~7b%28Fab~1m%28a,b%29=z%29%29|=~6a~6b%28Fab~4m%28a,b%29=z%29

[Dan Christensen]

On Sunday, December 5, 2021 at 10:59:15 AM UTC-5, Mostowski Collapse wrote:
> Can we buy these double chimpazee copper bracelets
> already on Amazon? Here is your fallacy explained.
>
> We can prove:
>
> /* provable */
> F is hyperbola => ALL(x):[x≠0 => x*F(x)=1]
>
> But we cannot prove:
>
> /* not provable */
> ALL(x):[x≠0 => x*F(x)=1] => F is hyperbola
>
> Got it?

We are STILL waiting for your formal proof that f(0)=1 is false given the definition of f: For all real x and y, if x=/=0 then we have f(x)=y <=> x*y=1. Do your homework, Jan Burse!

Dan

[Mostowski Collapse]

Corr.:
Need to fix my blind mole proof, serial shouldn't
be there. Don't know how much is needed to capture
"hyperbola" axiomatically.

But I already proved it, what Dan-O-Matik thinks I
didn't prove. For F is hyperbola we have ~F(0,1).
For F is double chimpanzee we cannot decide ~F(0,1).

Thats the fallacy of the double chimpanzee:

Mostowski Collapse schrieb am Sonntag, 5. Dezember 2021 um 13:33:34 UTC+1:
> There is no "if". The algebraic geometry definition is:
> F(x,y) <=> x*y = 1
> Algebraic geometry is a branch of mathematics,
> classically studying zeros of multivariate polynomials.
> https://en.wikipedia.org/wiki/Algebraic_geometry
>
> Its easy to prove ~F(0,1), just substitute:
>
> ~F(0,1) <=>
> ~0*1 = 1 <=>
> ~0 = 1 <=>
> true
https://groups.google.com/g/sci.logic/c/DBQJkCTGO_I/m/ny6lfI6jBQAJ

[Mostowski Collapse]

Ok here is a corrected proof, now saying for the reciprocal
hyperbola, that the reciprocal hyperbola is defined for x≠0
and otherwise undefined for x=0.

Also fixed a typo concerning the one (i.e. 1=o):

> /* provable */
> F is hyperbola => ALL(x):[x≠0 => x*F(x)=1]

∀a∀b∀c((Fab ∧ Fac) → b=c) ∧

(∀a(¬a=z ↔ ∃bFab) ∧
∀a∀b(Fab ↔ m(a,b)=o))
entails ∀a(¬a=z → ∃b(Fab ∧ m(a,b)=o)).
https://www.umsu.de/trees

> /* not provable */
> ALL(x):[x≠0 => x*F(x)=1] => F is hyperbola

∀a∀b∀c((Fab ∧ Fac) → b=c) ∧

∀a(¬a=z → ∃b(Fab ∧ m(a,b)=o))
does not entail
∀a(¬a=z ↔ ∃bFab) ∧
∀a∀b(Fab ↔ m(a,b)=o).
https://www.umsu.de/trees

[FredJeffries]

So you claim that f(0) = 1 is true?

[Dan Christensen]

No. Since f(0) is undefined (from the definition), I claim that no truth value can be attached to f(0)=1. IIUC that makes it unprovable, not false.

[Dan Christensen]

On Sunday, December 5, 2021 at 11:43:21 AM UTC-5, Mostowski Collapse wrote:
> Ok here is a corrected proof, now saying for the reciprocal
> hyperbola, that the reciprocal hyperbola is defined for x≠0
> and otherwise undefined for x=0.
>
> Also fixed a typo concerning the one (i.e. 1=o):
> > /* provable */
> > F is hyperbola => ALL(x):[x≠0 => x*F(x)=1]
> ∀a∀b∀c((Fab ∧ Fac) → b=c) ∧
> (∀a(¬a=z ↔ ∃bFab) ∧
> ∀a∀b(Fab ↔ m(a,b)=o))
> entails ∀a(¬a=z → ∃b(Fab ∧ m(a,b)=o)).
> https://www.umsu.de/trees
> > /* not provable */
> > ALL(x):[x≠0 => x*F(x)=1] => F is hyperbola
> ∀a∀b∀c((Fab ∧ Fac) → b=c) ∧
> ∀a(¬a=z → ∃b(Fab ∧ m(a,b)=o))
> does not entail
> ∀a(¬a=z ↔ ∃bFab) ∧
> ∀a∀b(Fab ↔ m(a,b)=o).

I'm looking for the bit where it concludes:

ALL(x):ALL(y):[ x in R & y in R => [x=/=0 => f(x) in R & [f(x)=y <=> x*y=1]]] => f(0)=/=1

Or some equivalent in your notation.

[Mostowski Collapse]

Why would somebody try to prove that?
When its not provable? It is easy to show
that it has a counter model.

BUT THIS DOESN'T MAKE IT A CORRECT
MATHEMATICAL DEFINITION. AU CONTRAIRE!

Here is the countermodel (z=0 and o=1):

∀x(¬x=z → ∀y(f(x)=y ↔ m(x,y)=o)) → ¬f(z)=o is invalid.
Countermodel:
Domain: { 0 }
z: 0
o: 0
f: { (0,0) }
m: { (0,0,0) }
https://www.umsu.de/trees

[Mostowski Collapse]

On the other hand one can prove:

F is the reciprocal hyperbola => ~F(0,1)

Here is the rather trivial proof:

Mostowski Collapse schrieb am Sonntag, 5. Dezember 2021 um 13:33:34 UTC+1:
> There is no "if". The algebraic geometry definition is:
> F(x,y) <=> x*y = 1
> Algebraic geometry is a branch of mathematics,
> classically studying zeros of multivariate polynomials.
> https://en.wikipedia.org/wiki/Algebraic_geometry
>
> Its easy to prove ~F(0,1), just substitute:
>
> ~F(0,1) <=>
> ~0*1 = 1 <=>
> ~0 = 1 <=>
> true
https://groups.google.com/g/sci.logic/c/DBQJkCTGO_I/m/ny6lfI6jBQAJ

[Mostowski Collapse]

Maybe you cannot cope with the mental disonnance between you
double chimpanzee nonsense and standard mathematics
that is found in all mathematic text books.

You can also try to derive the reciprocal hyperbola from a conic section:
https://en.wikipedia.org/wiki/Conic_section

Rotate a certain conic section by 45° degree. The question
whether F(0,1) is member or not member of the reciprocal hyperbola
is then the same question whether a point when you

rotate it back by 45° degree, lies on the cone and on the plane.
Its easy to show that the point still lies on the plane, but not
on the cone, therefore ~F(0,1).

You could also already start with a rotated cone.

[Dan Christensen]

On Sunday, December 5, 2021 at 1:50:19 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 5. Dezember 2021 um 19:18:18 UTC+1:
> > On Sunday, December 5, 2021 at 11:43:21 AM UTC-5, Mostowski Collapse wrote:
> > > Ok here is a corrected proof, now saying for the reciprocal
> > > hyperbola, that the reciprocal hyperbola is defined for x≠0
> > > and otherwise undefined for x=0.
> > >
> > > Also fixed a typo concerning the one (i.e. 1=o):
> > > > /* provable */
> > > > F is hyperbola => ALL(x):[x≠0 => x*F(x)=1]
> > > ∀a∀b∀c((Fab ∧ Fac) → b=c) ∧
> > > (∀a(¬a=z ↔ ∃bFab) ∧
> > > ∀a∀b(Fab ↔ m(a,b)=o))
> > > entails ∀a(¬a=z → ∃b(Fab ∧ m(a,b)=o)).
> > > https://www.umsu.de/trees
> > > > /* not provable */
> > > > ALL(x):[x≠0 => x*F(x)=1] => F is hyperbola
> > > ∀a∀b∀c((Fab ∧ Fac) → b=c) ∧
> > > ∀a(¬a=z → ∃b(Fab ∧ m(a,b)=o))
> > > does not entail
> > > ∀a(¬a=z ↔ ∃bFab) ∧
> > > ∀a∀b(Fab ↔ m(a,b)=o).
> > I'm looking for the bit where it concludes:
> >
> > ALL(x):ALL(y):[ x in R & y in R => [x=/=0 => f(x) in R & [f(x)=y <=> x*y=1]]] => f(0)=/=1
> >
> > Or some equivalent in your notation.

> Why would somebody try to prove that?
> When its not provable?

Ah, now we may be getting somewhere! f(0)=/=1 is unprovable, right, Jan Burse?

[Mostowski Collapse]

I am already telling you for the 1000-th times:

hyperbola: f(0)≠1 provable

double chimpanzee: f(0)≠1 unprovable

[Dan Christensen]

Yikes! Talk to us in a few days when you have sobered up, Jan Burse. Or just admit f(0)=/=1 is unprovable since f(0) is undefined.

Dan

[Mostowski Collapse]

Not in the hyperbola, in the f(0)≠1 provable

[Mostowski Collapse]

Or more precisly, when:

ALL(a):ALL(b):(F(a,b) <=> a*b=1)

Then ~F(0,1).

F(x)=y is the reciprocal function, usually denoted by 1/x=y.

[FredJeffries]

On Sunday, December 5, 2021 at 9:51:40 AM UTC-8, Dan Christensen wrote:
> On Sunday, December 5, 2021 at 11:54:12 AM UTC-5, FredJeffries wrote:
> > On Sunday, December 5, 2021 at 8:17:24 AM UTC-8, Dan Christensen wrote:
> > > On Sunday, December 5, 2021 at 10:59:15 AM UTC-5, Mostowski Collapse wrote:
> > > > Can we buy these double chimpazee copper bracelets
> > > > already on Amazon? Here is your fallacy explained.
> > > >
> > > > We can prove:
> > > >
> > > > /* provable */
> > > > F is hyperbola => ALL(x):[x≠0 => x*F(x)=1]
> > > >
> > > > But we cannot prove:
> > > >
> > > > /* not provable */
> > > > ALL(x):[x≠0 => x*F(x)=1] => F is hyperbola
> > > >
> > > > Got it?
> > > We are STILL waiting for your formal proof that f(0)=1 is false given the definition of f: For all real x and y, if x=/=0 then we have f(x)=y <=> x*y=1.
>
> > So you claim that f(0) = 1 is true?
> No. Since f(0) is undefined (from the definition), I claim that no truth value can be attached to f(0)=1. IIUC that makes it unprovable, not false.

prove it

[Mostowski Collapse]

Now this is like fukushima. I guess Dan-O-Matiks
brain is now melting. We finally found it:

∀x(Px → Qf(x)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
A Dan-O-Matik function is a binary relation iff the domain is the universal class
https://www.umsu.de/trees/#~6x%28Px~5Qf%28x%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29

We could only chill fukushima, if Dan-O-Matik were
as cool as this man here, who sings many languages:

Alpha Blondy - Jérusalem
https://www.youtube.com/watch?v=WcqK9Ls7Eos

But Dan-O-Matik isn't cool, he doesn't grasp that a FOL
function symbol and a set-like function are not the same.

[Mostowski Collapse]

Actually learning 3 languages would be helpful:
- FOL function symbol
- class-like functions
- set-like functions

[Mostowski Collapse]

But there is cure, Dan-O-Matik could exercise and get fluent
in all 3 languages by this little booklet:

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

Only 20 bucks or so.

[Mostowski Collapse]

Unfortunately Dan-O-Matik is only genuinely stupid:

Two things are infinite: the universe and human
stupidity; and I’m not sure about th’universe!
- Albert Einstein

Dan-O-Matik even tops that. He still doesn't understand
FOL, and how a FOL function symbol works. A definition def
for A -> B would be WELL DEFINED if we can prove the folllowing:

(*) def(f) & def(g) => f=g

Dan-O-Matik doesn't understand that this is impossible
for FOL function symbols with his serial formula. From
computer science there are ways to fix it.

For example one fix introduces a new symbol undefined ⊥.
We have to assume the universe of discourse is non-empty.
And then uses Dan-O-Matik serial formula:

ALL(x):[x in A => f(x) in B]

And adds this axiom:

ALL(x):[~x in A => f(x)=⊥]

Now you can prove (*). But most mathematicians do it more
easy, they don't use FOL function symbols, but set like function
symbols, since the domain A is already set like:

ALL(x):[~x in A => ~EXIST(y):(x,y) e f]

[Mostowski Collapse]

For example JavaScript implements undefined ⊥:

Legts get back to the 10 booleans array problem.
Just open any browser, switch to development view,
and enter in the console:

> a=[0,0,0,0,0,0,0,0,0,0];a[10]
undefined

In JavaScript accessing out of bound gives undefined.
There is a bound check, but there is no exception but a
special value.

This is closer to some logical modelling of automated
verification of programs which uses undefined ⊥.

[Mostowski Collapse]

Corr.: The WELL DEFINED issue arises when for example
A={0} and B={0}, we then want from def(h) <=> h : A -> B:

(*) def(f) & def(g) => f=g

Otherwise issue arises with the collection of functions,
they just become too big if we don't constrain FOL function

symbols outside of the domain.

[Mostowski Collapse]

How would one formulate in DC Proof, which is supposed to
be the tool for mathematics textbooks, the following:

if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined

See also:

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

Ha Ha, on page 7:

The axioms DES are of clear philosophical interest, providing one solution
of the familiar puzzles as to how to handle non-referring definite descriptions,
such as in ‘the present king of France is bald’. But they also serve to regulate
the use of mathematical definitions such a lim xn

[Mostowski Collapse]

But Fefi was sloppy, when defining his Impredicative Theory of
Operations and Classes (IOC), at least in this paper in sec 7
there is a blooper, when he says:

Now write: (i) f:(A→B)for∀x∈A(fx∈B)

Thats Dan-O-Matik nonsense! Did he fix that in another
publication? Same problem in Gerhard Jäger, these things
were never really used? Page 6:

(f :a→b) := (∀x∈a)(fx∈b)
https://home.inf.unibe.ch/ltg/publications/2009/jae09b.pdf

But maybe harmless for what they do with it? Fefi only
uses it to express totality over the natural numbers for
his gcd toy example.

[Dan Christensen]

On Monday, December 13, 2021 at 4:26:00 PM UTC-5, Mostowski Collapse wrote:
> How would one formulate in DC Proof, which is supposed to
> be the tool for mathematics textbooks, the following:
>
> if (f + g)′(x) is undefined then f′(x) or g′(x) are undefined
>

Again, f(x) is said to be undefined if x is not in the domain of f. Learn some logic, Jan Burse!

Dan

[Mostowski Collapse]

Thats not the correct approach in logic. Since Peano, we find something else:

"Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
has the same meaning as the more familiar but ambiguous notation F(x).
For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
See df-fv 5865. In the ASCII (input) representation there are spaces around the
grave accent; there is a single accent when it is used directly, and it is
doubled within comments."
http://us.metamath.org/mpeuni/conventions.html

Metamath can use the same symbol for function F and the function graph F,
in the above F is the same referent. Metamath uses then the empty set as
undefined marker, in case an argument is not in dom(F).

There are even aspects of definite description, F need not be a function graph
per see. They can therefore prove the following definite descriptions theorem.
It is not like in Russell, where we get false, its more we get the defined marker:

/* Provable in Metamath */
~ EXISTUNIQUE(x) (a,x) e F => (F'a) = {}

I don't think DC Proof/Donnie Darko has such a maker u:

/* Not Provable in DC Proof with Donnie Darke Function approach */
~ EXISTUNIQUE(x) (a,x) e F => F(a) = u

The Peano apostroph was later adopted by for example Withhead Russell,
Quine, Takeuti Zaring. It only needs some set theory like ZFC. So yes, DC
Proof with Donnie Darke Function approach is not what is common in logic.

[Mostowski Collapse]

So only ALL(a):[a e x => f(x) e b] , the Donnie Darko approach, like
dark numbers in WM, is just WM with extra steps, not saying
what is f outside of the domain a is not what we do in logic.

Thats just too dark for logic, these dark booleans. LoL

[Mostowski Collapse]

The only new development in logic might be these partial function
logics, where we dont need f'x can go back to f(x), but we have
axioms and inference rules for the operator ↓ .

But there is even a simpler approach than using an operator ↓,
one can also use a special value ⊥. DC Proof didn't make any
choice so far, its Function action

postulates same referent f for both the function graph
and the function, but the Function axiom is quite weak:

- It only applies when f is a function graph
- It doesn't say what f(x) should be outside of the domain

This is unlike the f'x approach which allows both. Then the
f(x) approach is less subject to the first problem, but the second
problem is solved in the new f(x) apprach either through

an operator ↓ or a special value ⊥ .

[Mostowski Collapse]

Then there is a whole field where the underlying logic is changed,
and where the underlying logic is not anymore classical logic,
but where for example 3-valued logic is used.

A prominent example is the SQL database system query language,
which has even an ISO standard. In SQL there is a special value ⊥,
written NULL. But there is also a third truth value.

"Since Null is not a member of any data domain, it is not considered
a "value", but rather a marker (or placeholder) indicating the
undefined value. [...] SQL implements three logical results, so SQL
implementations must provide for a specialized three-valued logic (3VL)."
https://en.wikipedia.org/wiki/Null_%28SQL%29#Comparisons_with_NULL_and_the_three-valued_logic_%283VL%29

[Dan Christensen]

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

Dan

[Mostowski Collapse]

Thats exactly why EXISTUNIQUE doesn't work. I 100'% agree
with Terence Tao. When you use a FOL function symbol,
and you only prove:

ALL(a):[x e a => ALL(y):[y e b => [(x,y) e F <=> f(x)=y]]]

Then obviously f(x) for ~(x e a) isn't pinned down. And then
you can for example not replace the EXIST quantfier in the
below, by an EXISTUNIQUE quantifier:

/* Doesn't work with EXISTUNIQUE also as per Terence Tao */
ALL(a):[Set(a) => EXIST(f):ALL(b):[b in a => f(b)=b]]

I am only trying to explain you the basic facts of beginner
mathematics. The metamath page does something different,
it doesn't use two symbols F and f, as in Terence Tao.

With the metamath approach you can prove EXISTUNIQUE.
With the Terence Tao approach you cannot prove
EXISTUNIQUE.

Whats wrong with you?

[Mostowski Collapse]

With the metamath approach you can prove EXISTUNIQUE

when the undefined marker is not in the codomain. Its like
here, the undefined marker is supposed to usually

not be used in codomains:

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 10:07:32 UTC+1:
> "Since Null is not a member of any data domain, it is not considered
> a "value", but rather a marker (or placeholder) indicating the
> undefined value. [...]

> https://en.wikipedia.org/wiki/Null_%28SQL%29#Comparisons_with_NULL_and_the_three-valued_logic_%283VL%29
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/JYKAbTdhCAAJ

But since you deal with identity functions, EXISTUNIQUE
will be provable when the undefined marker is not
in the domain, I guess you only look at identity

functions where dom=codom.

[Mostowski Collapse]

So maybe what Fefi (Solom Feferman) explains is the more
cleaner approach. You don't have to fiddle with domains and
codomains, there is only new operator ↓. In the metamath

approach you would require that functions are kind of
normalized, for example that a function f = { ... (x, ⊥) ...}
would be forbidden, whereas a function that doesn't

have the ordered pair (x, ⊥) would be tolerated.

[Mostowski Collapse]

The deeper problem is not Terrence Tao versus Dan-O-Matik
versus metamath. In all 3 approaches this here then fails:

/* Not Provable */
ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]

Thats very easy to see. Just chew on the downgrade Lemma:

/* Downgrade Lemma */
ALL(b):[b in a => b in c] & ALL(b):[b in c => f(b)=b]] => ALL(b):[b in a => f(b)=b]]

The tree tool of Wolfgang Schwartz can prove it, you
can also prove it with DC Proof, can't you:

/* Encoding E__ stands for _ in _ */
∀x(Exa → Exc), ∀x(Exc → f(x)=x) entails ∀x(Exa → f(x)=x).
https://www.umsu.de/trees/#~6x%28Exa~5Exb%29,~6x%28Exb~5f%28x%29=x%29|=~6x%28Exa~5f%28x%29=x%29

Do you know what it says?
Do you know why it prevents EXISTUNIQUE?

[Mostowski Collapse]

It prevents EXISTUNIQUE because you can find (f1,c1)
and (f2, c2), where f1≠f2 and:

ALL(b):[b in c1 => f1(b)=b]]

ALL(b):[b in c2 => f2(b)=b]]

Now if you futher have constructed (f1,c1) and (f2,c2)
such that a ⊆ c1 and a ⊆ c2, then you can downgrade
the two and you get:

ALL(b):[b in a => f1(b)=b]]

ALL(b):[b in a => f2(b)=b]]

And this breaks EXISTUNIQUE. Its really extremly trivial.
Just use the Downgrade Lemma.

[Dan Christensen]

Set my reply just now to your identical posting as sci.math.

Dan

On Tuesday, December 14, 2021 at 2:49:27 PM UTC-5, Mostowski Collapse wrote:
> The deeper problem is not Terrence Tao versus Dan-O-Matik
> versus metamath. In all 3 approaches this here then fails:
>
> /* Not Provable */
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
>

...

[Mostowski Collapse]

You used this EXISTUNIQUE(f,a):

EXISTUNIQUE(f,a):A(f) <=> EXIST(h):A(h) & ALL(f):ALL(g):[A(f) & A(g) => f|a = g|a]

But my claim is you cannot prove it with EXISTUNIQUE(f):

EXISTUNIQUE(f):A(f) <=> EXIST(h):A(h) & ALL(f):ALL(g):[A(f) & A(g) => f = g]

I made this pretty clear here, when I wrote:
"You didn't prove f=g"

Whats wrong with you?

[Mostowski Collapse]

I dont think DC proof correctly associates functions and function graphs.
You can also try Terence Tao decrement example:

Example 3.3.2:
Unfortunately this does not define a function, because
when x = 0 there is no natural number y whose increment
is equal to x (Axiom 2.3). On the other hand, we can legitimately
define a decrement function h : N\{0} → N associated to
the property P(x,y) defined by y++ = x.
https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf

I think its is provable:

~EXIST(y):P(0,y)

Or do you claim otherwise?
Do you also have dark booleans for decrement?

LMAO!

[Mostowski Collapse]

Or asked differently how many decrement functions are
there in Peano arithmetic? Can you prove:

EXISTUNIQUE(h):"h is the decrement function"

[Mostowski Collapse]

What is easier to use, DC proof or ZFC? DC proof
claims that certain things are given:

> ALL(a):[a in D => f(a) in C] where D and C are the given domain and
> codomain sets. In this case, "f(x)" is undefined and quite meaningless for x not in D.

Is this true when we talk about functions? The domains
and co-domains cannot always be given so easily. Thats the
Dan-O-Matik paradox. For example there is this theorem:

"Every injective function f has an inverse function g on its range"

If f: A -> B, whats the domain of g? What does need less
steps to prove the above, DC proof or ZFC?

[Mostowski Collapse]

With ZFC I only need to do the following:

1) let g = { (y, x) | (x, y) in f}, show it is a set

2) show g is a function when f is injective

3) conclude dom(g) = ran(f)

I am pretty sure DC proof needs much more work. Since to
start with ALL(a):[a in A => f(a) in B] and end with existence
of g, D and C such that ALL(a):[a in D => g(a) in C],

it will anyway first construct g in the form of a set and then
use its function axiom. So its kind of set theory with extra
steps. Utter unnecessary nonsense to be precise.

[Dan Christensen]

See my reply just now to your identical postings at sci.math

Dan

[Mostowski Collapse]

You are changing topic. I dont mind if you need Set(_)
as well in DC poop. The question is rather can you
prove this textbook theorem, i. e. EXIST(g) :

"Every injective function f has an inverse function g on its range"

But I guess you already gave up. A few weeks ago you
boasted ZFC or set theory is not found in everyday math.
What about the above theorem, what is needed in DC poop?

[Mostowski Collapse]

So you cannot show existence of g?

Hiding behind some absurd claims the encoding
of functions as set of pairs is bizzar?

How do you show existence of g = f^-1 in DC proof?

LoL

[Mostowski Collapse]

Can you prove your ExistenceOfInverse without
using bizzar sets, like this here:

Define: f' (as subset of yx)
17 Set'(f')
Split, 16
18 ALL(a):ALL(b):[(a,b) e f' <=> (a,b) e yx & f(b)=a]
http://dcproof.com/ExistenceOfInverse.htm

Or do you admit that you were loosing your head,
accusing other people of bizzar ideas, whereas
your DC poop cannot do without just these bizzar

ideas. I guess everybody will agree that

ALL(a) : ALL(b) : [~(a, b) e yx => ~(a, b) e f']

Maybe you stole the proof somewhere? And you are
cheater? How can you not know that you yourself
use bizzar concepts in DC poop?

[Dan Christensen]

On Sunday, December 26, 2021 at 5:06:23 AM UTC-5, Mostowski Collapse wrote:
> So you cannot show existence of g?
>

See my reply today to your identical posting at sci.math

Dan

[Mostowski Collapse]

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

[Mostowski Collapse]

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

[Dan Christensen]

See my reply to your identical posting at sci.math.

Dan

[Mostowski Collapse]

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!

[Mostowski Collapse]

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]

I dont know how to fix your DC Puff and do what you
want to do. Some free logics dont touch (Refl):

"Positive semantics treat formulas of the
form t=t as true, whether or not t is empty."
https://plato.stanford.edu/entries/logic-free/#possem

But since you touched (Refl), you probably also
need to touch (Subst). On the other hand touching
(Forall) seems to be in line with the SEP article.

See axiom A4 here: ∀xA→(E!t→A(t/x))
https://plato.stanford.edu/entries/logic-free/#ax

Disclaimer: Maybe Free Logic is even not the
correct optic for what DC Puff wants to do.

[Dan Christensen]

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

Dan

On Monday, January 3, 2022 at 7:27:59 AM UTC-5, Mostowski Collapse wrote:
> 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]
>

...

[Mostowski Collapse]

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

[Mostowski Collapse]

So DC Proof has something like Emperor penguins from antarctica
as functions, with the exotic USpec. What are they?

There are at least two approaches according two wikipedia for functions:
i) Set-like function, which requires:
(Relation): ∀x∀y (x,y) e f => x e dom & y e cod
ii) An ordered tripple f=(dom, cod,F)
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

Both approaches allow querying the domain dom(f) of a function f:
i) Set-like functions, it can be defined, and is a set because of (Relation):
dom(f) := { x | EXIST(y):(x,y) e f }
ii) An ordered tripple f=(dom, cod,F), it can be defined:
dom(f) := π1(f), i.e. projection on the first component of the ordered tripple

So both approaches i) and ii) have a notion dom(f). Why do the
Emperor penguins from antarctica from DC Proof, the functions with
the strange USpec not have a notion dom(f), either through some

definition or through some axiom? Thats quite counter to the current
mathematical practice of either i) or ii), which both do provide querying
the domain of a function.

[Dan Christensen]

See my reply just now to a nearly identical posting at sci.math.

Dan

On Monday, January 3, 2022 at 5:55:46 PM UTC-5, Mostowski Collapse wrote:
> So DC Proof has something like Emperor penguins from antarctica
> as functions, with the exotic USpec. What are they?
>
> There are at least two approaches according two wikipedia for functions:
> i) Set-like function, which requires:
> (Relation): ∀x∀y (x,y) e f => x e dom & y e cod
> ii) An ordered tripple f=(dom, cod,F)
> https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
>

...

[Mostowski Collapse]

DC Proof is subject to "Fake it till you make it". You claim:

Dan Christensen schrieb am Dienstag, 4. Januar 2022 um 06:45:47 UTC+1:
> For any given function f: A --> B, you can easily construct {(x,y) in AxB: f(x)=y}

Its not provable in DC Proof. You cannot prove in DC Proof:

ALL(x):[x e A => f(x) e B] => dom(f)=A

Because there is even no notion dom(f) in DC Proof.

P.S.:On the other hand in standard mathematics, you can prove:
f: A --> B => dom(f)=A

Just check out Kurt Gödel, like 100 years ago:
https://archive.org/details/dli.ernet.469738/page/n1/mode/2up

[Mostowski Collapse]

Here is a quizz, which collections are in some bijection?

1) { f | f : Q -> R }, where R the real numbers and Q the rational numbers

2) { f | f : R -> R },

3) { f | f : R -> R, f continuous }

And the same quizz again for:

1) { f | "Dan-O-Matik f : Q -> R" }, where R the real numbers and Q the rational numbers

2) { f | "Dan-O-Matik f : R -> R" },

3) { f | "Dan-O-Matik f : R -> R", f continuous }

[Mostowski Collapse]

You find your beloved CBS theorem, together with the
correct reading of function spaces, namely set exponentiation:

B^A = { f | f : A -> B }
https://math.stackexchange.com/questions/901735/meaning-of-a-set-in-the-exponent

One can also rephrase the quiz as, cardinalities of:

1) R^Q

2) R^R

3) C(R,R), where C(A,B) are the continues functions from B^A

Things you cannot correctly and concisely prove in DC Proof.
It just doesn't provide text book math that every mathematician
is confluent. Instead it confounds f : A -> B with ALL(x):[x e A =>

f(x) e B] which is utter nonsense. You dont get the same set
exponentiation with the Dan-O-Matik nonsense:

B^A =\= { f | ALL(x):[x e A => f(x) e B] }

[Mostowski Collapse]

Also stop talking utter nonsense like:
> Nothing there to support your claim that we can make
logical inferences about a function outside of it domain of definition.

Well you defined it yourself, what F = B^A is:
Dan Christensen schrieb am Mittwoch, 5. Januar 2022 um 22:23:41 UTC+1:
> You could easily construct F = {f in P(AxB) : For all x in A, there exists unique y in B such that (x, y) in f}.
https://groups.google.com/g/sci.math/c/IWbD8BdJkv8/m/3nY0WjN6BAAJ

If we have f e F, then we have also f e P(A x B).
Its really easy to prove:

x not in A => ~EXIST(y):(x,y) in f

Just think what the cross product is, and
what the power set is.

Do your homework.

Hint: f e P(A x B) implies f ⊆ A x B.

[Mostowski Collapse]

How flat chested is DC Proof? LoL It doesn't have a power set axiom?

These two sets are provably equal, i.e. F1 = F2:

F1 = {f in P(AxB) : For all x in A, there exists unique y in B such that (x, y) in f}.

F2 = {f ⊆ A x B : For all x in A, there exists unique y in B such that (x, y) in f}.

They both define the function space A -> B aka B^A. They are used:

F1:

Zermelo Fraenkel Powerset
Richard E. BORCHERDS - 30.11.2021
https://www.youtube.com/watch?v=XCMvljsu84s

F2:

In the relational approach, a function f: X→Y is a binary relation between
X and Y that associates to each element of X exactly one element of Y.
Any subset of the Cartesian product of two sets X and Y defines a binary
relation R ⊆ X × Y between these two sets.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

Whats wrong with you? Its easy to prove:

f e B^A , x not in A => ~EXIST(y):(x,y) in f

[Mostowski Collapse]

Warning: I am looking at the direction -->, the old topic, and
not at the direction <--, the new topic.

Looks like DC proof is extremly flat chested. There is not
only no power set axiom. Also the function axiom doesn't
have a lot of steam. The function axiom defines a map

from function space to Dan-O-Matik nonsense:

A -> B --> {g | ALL(x):[x =in A => g(x) in B]}

Lets denote what the function axiom gives for f : A -> B
by def(_). Dan-O-Matik can only prove, which IS NOT
INJECTIVITY of the function axiom:

(*)
def(g) & def(g') => ALL(a):[a in x => g'(a)=g(a)]

But its an easy folklore exercise to obtain a more
stronger result by a better function axiom, namely.
which is INJECTIVITY of the better function axiom:

(**)
def'(g) & def'(g') => ALL(a):[g'(a)=g(a)]

How is this done? Well its relatively easy to use
von Neumann-Gödel-Bernays set theory (NBG) to have
this classes g, where ' is the Peano apostroph:

def'(g) :<=> ∀x∀y( (x,y) e g <=> f'x = y )

The class g is a function on the domain of discourse,
so that we can use g(x)=y instead of (x,y) e g unrestrictedly.
One can then prove (**) as required.

See also:

The Peano apostroph is also defined here. Kurt Gödel
does it Chapter II, page 16 here, after Definition 4.63:

Consistency of the Continuum Hypothesis. (AM-3), Volume 3
Annals of Mathematics Studies Band 264
https://www.orellfuessli.ch/shop/home/artikeldetails/A1004884502

See also:

In the foundations of mathematics, von Neumann–Bernays–Gödel
set theory (NBG) is an axiomatic set theory that is a conservative
extension of Zermelo–Fraenkel-Choice set theory (ZFC).
https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory

[Mostowski Collapse]

Injectivity can now be examined, since only now
by ALL(a):[g'(a)=g(a)] we have a mapping from
function space to Dan-O-Matik nonsense. Lets

write (_)* for this mapping via Peano apostroph:

A -> B --> {g | ALL(x):[x =in A => g(x) in B]}

Its now easy to show f1,f2 : A -> B and f1=\=f2
that then f1*=\=f2*. So the direction --> is indeed
a map and an injectivity.

But there are also other injective --> mappings possible.
What about the other directio <-- ? Can a reverse mapping
be an injection?

[Mostowski Collapse]

Actually this is a nice logic exercise, show that
there is no bijection? At least in the finite case,
by invoking anti-monotonity:

Does this bijection hold?
A -> B <---> { f | ALL(x):[x e A => f(x) e B] }

In the finite case we would have a bijection
with a finite ordinal number, or in other words we
would have that same finite cardinality:

|A -> B| = |{ f | ALL(x):[x e A => f(x) e B] }| = n

Now by anti-monotonity for A ⊆ A' we would
have { f | ALL(x):[x e A' => f(x) e B] } ⊆ { f | ALL(x):[x e A
=> f(x) e B] }. And therefore:

|{ f | ALL(x):[x e A' => f(x) e B] }| = n' & n' =< n.

On the other hand the function space cardinality
is like this, |A -> B| = |B|^|A|. Lets say |A|=k and
|A'|=k' and |B|=j, k=\=k'. So that

we would have:

k < k' => j^k >= j^k'

Quite some nonsense for natural numbers.

[Mostowski Collapse]

Check out for yourself:

"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

[Mostowski Collapse]

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

[Mostowski Collapse]

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

[Dan Christensen]

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

Dan

On Monday, January 10, 2022 at 5:08:41 PM UTC-5, Mostowski Collapse wrote:
> 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:
>

...

[Mostowski Collapse]

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.

[Mostowski Collapse]

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?

[Dan Christensen]

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

On Wednesday, January 12, 2022 at 5:30:30 PM UTC-5, Mostowski Collapse wrote:
> So stop talking nonsense about some text book

...

[Mostowski Collapse]

Fraenkel did nothing. The AOI is found in a paper by Zermelo.
Its an axiom of the form:

EXIST(S): ....

And then you can derive from it, where w is omega:

EXIST(w): ...

I don't see an axiom of this shape in your proof, neither
a conclusion of this shape in your proof. It only says:

ALL(f):[Dedekind(f) -> Peano(constr(f))].

But in DC Proof, we cannot anymore derive existence
from the above, see here:

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 02:48:21 UTC+1:
> This is the proof that worked in dcproof2.exe, but
> does not work anymore in dcproof5.exe:
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ

JUST REPLACE Peano by Dedekind, and Field by Peano.

You also called the above proof schema wonky,
since it wasn't invented by you. But it was a way
in the past to show Dedekind -> Peano, but as

of now it is open how to do it. We are still waiting...