Dana Scott fan club

[Ross Finlayson]

Dana Scott fan club

Been reading some more into Dana Scott. He has a pretty good intuition and is
also a grandiose sort of hedge. Also he knows things and isn't wrong.

Been reading a bit into the Habermas school or Frankfurt school.

Cohen's "Equations from G-d" was a pretty good historical outline about
Boole and de Morgan than about Russell about "pure mathematics" in the
19'th century, still though I believe in a stronger platonism and that there's
a science of mathematics but its study is _of_ the real "pure mathematics".

Was reading some Knuth the other day about combinatorics historically,
quite a well-rounded guy.

[Mild Shock]

Dan Christensen hates Scott's trick, that we have:

∀xA(x) <=> ∀y∀x(x ∈ y => A(x))

[Dan Christensen]

On Sunday, July 9, 2023 at 3:25:08 PM UTC-4, Mild Shock wrote:
> Dan Christensen hates Scott's trick, that we have:
>
> ∀xA(x) <=> ∀y∀x(x ∈ y => A(x))

Let's see your formal proof. Then I should be able to translate it into the equivalent in DC Proof.

Dan

[Mild Shock]

Its not so difficult to prove. The => direction
is trivial. And the <= direction you can consider the
sub case y={x} that (*), which needs unordered pair:

∀x(x ∈ {x} => A(x)) <= ∀y∀x(x ∈ y => A(x))

And because x ∈ {x} is always true, we have:

∀xA(x) <= ∀y∀x(x ∈ y => A(x))

(*) The specialization to singleton y={x} from an
arbitrary set y is an instance of Aristoteles Barbara:

∀x(P(x)=>Q(x)) & ∀x(Q(x)=>A(x)) => ∀x(P(x)=>A(x))

[Mild Shock]

Lets define:

Foobar(y) = ∀x(x ∈ y => A(x))

BARBARA is then:
https://en.wikipedia.org/wiki/Syllogism#Barbara_%28AAA-1%29

Every set is a foobar
Every singleton is a set
----------------------------
Every singleton is a foobar

[Dan Christensen]

On Tuesday, July 11, 2023 at 4:33:31 PM UTC-4, Mild Shock wrote:

> Dan Christensen wrote:
> > On Sunday, July 9, 2023 at 3:25:08 PM UTC-4, Mild Shock wrote:
> >> Dan Christensen hates Scott's trick, that we have:
> >>
> >> ∀xA(x) <=> ∀y∀x(x ∈ y => A(x))
> >
> > Let's see your formal proof. Then I should be able to translate it into the equivalent in DC Proof.
> >

> Its not so difficult to prove. The => direction
> is trivial. And the <= direction you can consider the
> sub case y={x} that (*), which needs unordered pair:
>
> ∀x(x ∈ {x} => A(x)) <= ∀y∀x(x ∈ y => A(x))
>
> And because x ∈ {x} is always true, we have:
> ∀xA(x) <= ∀y∀x(x ∈ y => A(x))
> (*) The specialization to singleton y={x} from an
> arbitrary set y is an instance of Aristoteles Barbara:
>
> ∀x(P(x)=>Q(x)) & ∀x(Q(x)=>A(x)) => ∀x(P(x)=>A(x))

This is not a formal proof. You need a numbered sequence of statements, each one being generated by the application by a single axiom of logic or set theory.

Dan

[Mild Shock]

Its a proof sketch. The rest is left as an exercise.

[Dan Christensen]

On Tuesday, July 11, 2023 at 6:17:58 PM UTC-4, Mild Shock wrote:

> >>> On Sunday, July 9, 2023 at 3:25:08 PM UTC-4, Mild Shock wrote:
> >>>> Dan Christensen hates Scott's trick, that we have:
> >>>>
> >>>> ∀xA(x) <=> ∀y∀x(x ∈ y => A(x))
> >>>
> >>> Let's see your formal proof. Then I should be able to translate it into the equivalent in DC Proof.
> >>>
> >
> >> Its not so difficult to prove. The => direction
> >> is trivial. And the <= direction you can consider the
> >> sub case y={x} that (*), which needs unordered pair:
> >>
> >> ∀x(x ∈ {x} => A(x)) <= ∀y∀x(x ∈ y => A(x))
> >>
> >> And because x ∈ {x} is always true, we have:
> >> ∀xA(x) <= ∀y∀x(x ∈ y => A(x))
> >> (*) The specialization to singleton y={x} from an
> >> arbitrary set y is an instance of Aristoteles Barbara:
> >>
> >> ∀x(P(x)=>Q(x)) & ∀x(Q(x)=>A(x)) => ∀x(P(x)=>A(x))
> >

> > This is not a formal proof. You need a numbered sequence of statements, each one being generated by the application by a single axiom of logic or set theory.
> >

> Its a proof sketch. The rest is left as an exercise.

When you are able to provide a formal proof in your system (ZFC?), I will provide a formal proof in my system (the ordinary set theory of most math textbooks).

Dan

[Ross Finlayson]

Been reading Quine's "Set Theory" (and Quine's number theory and Quine's model theory, ...).

I thought it was pretty good until he got up to real numbers and used the term "non-circularize
the argument" in an off-hand way. He started with a good discussion of class/set distinction
then put it aside and coat-tailed up past "higher-order equals". As a structuralist I don't much
agree except that "equals is first-order", so pretty much the usual coat-tails logician's coat-tailing
of "higher-order equals" comes across as "circularized". So, when Quine got to his real numbers
and was like "my rationals are reals instead of my reals are rationals" then there's a quibble about
least-upper-bound property, pretty much I was disappointed in him when he faked a quibble about
least-upper-bound property. Still, I'm only about half-way through so maybe there will be something
better to talk about later in it.

Dana Scott's pretty good. He's like, "Oh you made an algebra? Here's a boolean lattice."


Reading the other days about Schwarz functions and their distributions and Heaviside's function
and hysteresis and ringing and Gibbs, from some late '90's papers from NASA, about doubling-spaces
and the non-standard and infinitesimals, I figure that it still makes pretty great sense the re-Vitali-ization
of measure theory ("after LUB, the other axiom, measure 1.0"), into doubling spaces and Ramsey theory,
figuring they'll need a foundations besides their applied.

The stopping-derivative is kind of an interesting idea, I've been thinking about the identity dimension
and a bunch of great stuff that arrives from re-Vitali-ization and a deconstructive account of the
arithmetic and so on.

[Mild Shock]

Its a proof sketch. The rest is left as an exercise.

Its not that difficult to do it formally. You only
need singletons, means you only need this axiom

from set theory, available for example in ZFC:

https://en.wikipedia.org/wiki/Axiom_of_pairing

Hope this helps!

[Dan Christensen]

On Wednesday, July 12, 2023 at 4:07:02 AM UTC-4, Mild Shock wrote:

> Dan Christensen wrote:
> > On Tuesday, July 11, 2023 at 6:17:58 PM UTC-4, Mild Shock wrote:
> >
> >>>>> On Sunday, July 9, 2023 at 3:25:08 PM UTC-4, Mild Shock wrote:
> >>>>>> Dan Christensen hates Scott's trick, that we have:
> >>>>>>
> >>>>>> ∀xA(x) <=> ∀y∀x(x ∈ y => A(x))
> >>>>>
> >>>>> Let's see your formal proof. Then I should be able to translate it into the equivalent in DC Proof.
> >>>>>
> >>>
> >>>> Its not so difficult to prove. The => direction
> >>>> is trivial. And the <= direction you can consider the
> >>>> sub case y={x} that (*), which needs unordered pair:
> >>>>
> >>>> ∀x(x ∈ {x} => A(x)) <= ∀y∀x(x ∈ y => A(x))
> >>>>
> >>>> And because x ∈ {x} is always true, we have:
> >>>> ∀xA(x) <= ∀y∀x(x ∈ y => A(x))
> >>>> (*) The specialization to singleton y={x} from an
> >>>> arbitrary set y is an instance of Aristoteles Barbara:
> >>>>
> >>>> ∀x(P(x)=>Q(x)) & ∀x(Q(x)=>A(x)) => ∀x(P(x)=>A(x))
> >>>
> >
> >>> This is not a formal proof. You need a numbered sequence of statements, each one being generated by the application by a single axiom of logic or set theory.
> >>>
> >
> >> Its a proof sketch. The rest is left as an exercise.
> >
> > When you are able to provide a formal proof in your system (ZFC?), I will provide a formal proof in my system (the ordinary set theory of most math textbooks).
> >

> Its a proof sketch. The rest is left as an exercise.
> Its not that difficult to do it formally. You only
> need singletons, means you only need this axiom
>
> from set theory, available for example in ZFC:
>
> https://en.wikipedia.org/wiki/Axiom_of_pairing
>

Hmmm... Your inability to provide the required proof makes me wonder if it is provable in ZFC. Just a hunch... Is it because a universal set is required, but not formalizable in ZFC?

Dan

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

[Ross Finlayson]

It's formalizable in less than ZFC, where ZFC introduces _restrictions_
of comprehension, because class/set distinction.

Most modern coat-tails sorts have never even heard of it.

[Dan Christensen]

Go tired of waiting. Making all the behind-the-scenes machinery visible, I prove (58 lines in DC Proof):

ALL(u):[Set(u)

=> [ALL(x):[x in u => A(x)] <=> ALL(y):[Set(y) & ALL(b):[b in y => b in u] => ALL(x):[x in y => A(x)]]]]

I hope this helps.

[Mild Shock]

Thats not the same theorem. The Point of Scott's Trick
is to have a universal quantifier, and not what you do
introduce a universal set. Scott's Trick is real:

https://en.wikipedia.org/wiki/Scott's_trick

Usually its not done with a ∀y where y is a set like in my
example, but rather with a ∀α where α is an ordinal. But
you don't have ordinals in DC Proof. So the simpler variant

is this here, which you didn't prove so far:

∀xA(x) <=> ∀y∀x(x ∈ y => A(x))

So when I wrote "Dan Christensen hates Scott's trick" this
aged like a fine wine. We can only repeat Dan Christensen
hates Scott's trick up to the point that

he cannot prove it.

[Jim Burns]

On 7/12/2023 11:08 AM, Dan Christensen wrote:
> On Wednesday, July 12, 2023
> at 4:07:02 AM UTC-4, Mild Shock wrote:

>> Its a proof sketch. The rest is left as an exercise.
>> Its not that difficult to do it formally. You only
>> need singletons, means you only need this axiom
>> from set theory, available for example in ZFC:
>> https://en.wikipedia.org/wiki/Axiom_of_pairing
>
> Hmmm...
> Your inability to provide the required proof

... is not shown by providing a proof sketch.

For the purpose of demonstrating that
a fully formal proof exists,
for anything longer than a few lines,
a proof sketch is _better_ than
that fully formal proof itself.

Roughly speaking,
a fully-formal proof is to assembly-langauge
as
a proof sketch is to a high-level programming
language like Perl.

> makes me wonder if it is provable in ZFC.

Some day, you (DC) may be able to tell from
a proof sketch whether the fully-formal proof
sketched exists. That is the point of a
proof sketch, after all.

Being able to tell doesn't seem to be a
very rare skill. Perhaps it's helpful to be
more interested in the ideas presented
than in using formalization as some kind of
dominance-display.

[Dan Christensen]

HA, HA! You could not prove the theorem in your wonky system. Now you are complaining that I provided too much detail in my system using the implicit rules of logic and axioms of set theory as used in proofs in most math textbooks. Read it and weep: https://www.dcproof.com/JanBurse15.htm

[Dan Christensen]

On Wednesday, July 12, 2023 at 6:54:18 PM UTC-4, Jim Burns wrote:
> On 7/12/2023 11:08 AM, Dan Christensen wrote:
> > On Wednesday, July 12, 2023
> > at 4:07:02 AM UTC-4, Mild Shock wrote:
>
> >> Its a proof sketch. The rest is left as an exercise.
> >> Its not that difficult to do it formally. You only
> >> need singletons, means you only need this axiom
> >> from set theory, available for example in ZFC:
> >> https://en.wikipedia.org/wiki/Axiom_of_pairing
> >
> > Hmmm...
> > Your inability to provide the required proof
> ... is not shown by providing a proof sketch.
>
> For the purpose of demonstrating that
> a fully formal proof exists,
> for anything longer than a few lines,
> a proof sketch is _better_ than
> that fully formal proof itself.
>

JB's "sketch" seemed to me to be more of a cryptic hint than any kind of outline.

Dan

[Dan Christensen]

On Wednesday, July 12, 2023 at 6:33:13 PM UTC-4, Mild Shock wrote:
> Thats not the same theorem. The Point of Scott's Trick
> is to have a universal quantifier, and not what you do
> introduce a universal set. Scott's Trick is real:
>
> https://en.wikipedia.org/wiki/Scott's_trick
>

[snip]

You have now seen my proof: https://www.dcproof.com/JanBurse15.htm

Maybe you can use it to derive your own purely ZFC version (with no additional axioms), but I don't see how it would work without formally naming a set that is the "domain of discourse" (the set u introduced on line 1 of my proof).

[Mild Shock]

Dumbo, maybe you are not aware whats a proof.
But a proof is usually defined as follows:

a) A number of statements S1, .., Sn
b) Each statement Si is a application of an inference rule or axiom schema
from previous statements Sj1,..,Sjn with i > jk
c) The last statement Sn equals the desired theorem

Your nonsense lacks requirement c).
The requirement was to prove:

∀xA(x) <=> ∀y∀x(x ∈ y => A(x))

Please try again moron.

[Mild Shock]

Come on Dan-O-Matik. Scott's Trick is about set theory.
You only proved, which doesn't need unordered pair:

u ⊆ P <=> ∀a(a ⊆ u => a ⊆ P)

Its quite trivial, even Wolfgang Schartz tool can prove
it without unordered pair, and thus without ZFC.

∀x(Exu → Exp) ↔ ∀a(∀y(Eya → Eyu) → ∀z(Eza → Ezp)) is valid.
https://www.umsu.de/trees/#~6x(Exu~5Exp)~4~6a(~6y(Eya~5Eyu)~5~6z(Eza~5Ezp))

But the task is to prove, which needs unordered pair or something
equivalent to unordered pair, i.e. needs something like ZFC:

∀xA(x) <=> ∀y∀x(x ∈ y => A(x))

Maybe get some brains idiot?

[Dan Christensen]

On Thursday, July 13, 2023 at 4:32:15 AM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Donnerstag, 13. Juli 2023 um 05:39:01 UTC+2:
> > On Wednesday, July 12, 2023 at 6:33:13 PM UTC-4, Mild Shock wrote:
> > > Thats not the same theorem. The Point of Scott's Trick
> > > is to have a universal quantifier, and not what you do
> > > introduce a universal set. Scott's Trick is real:
> > >
> > > https://en.wikipedia.org/wiki/Scott's_trick
> > >
> > [snip]
> >
> > You have now seen my proof: https://www.dcproof.com/JanBurse15.htm
> >
> > Maybe you can use it to derive your own purely ZFC version (with no additional axioms), but I don't see how it would work without formally naming a set that is the "domain of discourse" (the set u introduced on line 1 of my proof).

[snip childish abuse]

> But a proof is usually defined as follows:
>
> a) A number of statements S1, .., Sn
> b) Each statement Si is a application of an inference rule or axiom schema
> from previous statements Sj1,..,Sjn with i > jk
> c) The last statement Sn equals the desired theorem
>
> Your nonsense lacks requirement c).
> The requirement was to prove:
> ∀xA(x) <=> ∀y∀x(x ∈ y => A(x))

As is common practice in "standard" FOL, this "theorem" of yours leaves out important details like the domain of quantification for each quantifier. In mathematics, this is NOT the common practice. You should try, as I did, to fill in those missing details, Mr. Collapse:

ALL(u):[Set(u)

=> [ALL(x):[x in u => A(x)] <=> ALL(y):[Set(y) & ALL(b):[b in y => b in u] => ALL(x):[x in y => A(x)]]]]

Where u = the "domain of discourse," an arbitrary set in this case.

[Mild Shock]

You are quite a moron.

Renaming doesn't help. Its still not the same:

> ALL(u):[Set(u)
> => [ALL(x):[x in u => A(x)]
<=> ALL(y):[Set(y) & ALL(b):[b in y => b in u] => ALL(x):[x in y => A(x)]]]]

Is provable from logic alone:

∀x(Exu → Ax) ↔ ∀y(∀b(Eby → Ebu) → ∀x(Exy → Ax)) is valid.
https://www.umsu.de/trees/#~6x(Exu~5Ax)~4~6y(~6b(Eby~5Ebu)~5~6x(Exy~5Ax))

But my formula is not provable from logic alone:

∀xAx ↔ ∀y∀x(Exy → Ax) is invalid.
https://www.umsu.de/trees/#~6xA(x)~4~6y~6x(Exy~5A(x))

Whats wrong with you?

[Mild Shock]

There are 3 errors in your u relativization translation:

Error 1) You translated my formula 2nd order style.
You translated this here:

∀xAx ↔ ∀y∀x(x ∈ y → Ax)

Into this here, assuming x is 1st order and y is 2nd order:

∀x(x ∈ u → Ax) ↔ ∀y(y ⊆ u → ∀x(x ∈ y → Ax))

Which is not what the formula says. The formula
has both x ∈ u and y ∈ u. If you translate it this way:

∀x(x ∈ u → Ax) ↔ ∀y(y ∈ u → ∀x(x ∈ y → Ax))

Its not anymore provable from logic alone:

∀x(Exu → Ax) ↔ ∀y(Eyu → ∀x(Exy → Ax)) is invalid.
https://www.umsu.de/trees/#~6x(Exu~5Ax)~4~6y(Eyu~5~6x(Exy~5Ax))

Error 2)
You didn't translate the second quantifer ∀x. With translation
of the second quantifier the formula would be:

∀x(x ∈ u → Ax) ↔ ∀y(y ∈ u → ∀x(x ∈ u → (x ∈ y → Ax)))

Its again not anymore provable from logic alone:

∀x(Exu → Ax) ↔ ∀y(Eyu → ∀x(Exu → (Exy → Ax))) is invalid.
https://www.umsu.de/trees/#~6x(Exu~5Ax)~4~6y(Eyu~5~6x(Exu~5(Exy~5Ax)))

Error 3)
You assume a translation is needed, but the problem is
posed as is, namely as follow:

∀xAx ↔ ∀y∀x(x ∈ y → Ax)

The formula can be proved when you use unordered pair.
Only you are too dumb to prove it,

because you are completely brain damaged.

[Dan Christensen]

[snip childish abuse]

>
> Renaming doesn't help.

[snip]

The mysterious set that shall not be named. Really???

As is common practice in mathematics, I am NAMING, not RE-naming the supposed "domain of discussion," namely the set u, in this case. Why is that so problematic for you, Mr. Collapse?

[Mild Shock]

You only demonstrated so far:

- You didn't understand the proof sketch and
couldn't prove: ∀xAx ↔ ∀y∀x(x ∈ y → Ax)

- You don't know how to consistently relativize to u and
couldn't translate: ∀xAx ↔ ∀y∀x(x ∈ y → Ax)

Do you want me to spoil it, and show the proof? Its
really easy. As a first step you can try the following lemma:

Lemma: Singletons Exist
======================
Proof Sketch: Use that unordered pairs exist:
https://en.wikipedia.org/wiki/Axiom_of_pairing
So for any x,y the set {x,y} exist.
Now prove that the set {x} exists, for any x.

With this Lemma at hand, it should be really really easy
to prove ∀xAx ↔ ∀y∀x(x ∈ y → Ax) .

[Dan Christensen]

On Thursday, July 13, 2023 at 1:54:27 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

> There are 3 errors in your u relativization translation:
>
> Error 1) You translated my formula 2nd order style.
> You translated this here:
>
> ∀xAx ↔ ∀y∀x(x ∈ y → Ax)
>
> Into this here, assuming x is 1st order and y is 2nd order:
>
> ∀x(x ∈ u → Ax) ↔ ∀y(y ⊆ u → ∀x(x ∈ y → Ax))
>

I have simply given a name to your mysterious, unnamed "domain of discourse," i.e. the set u. Why must it remain unnamed?

ALL(u):[Set(u)

=> [ALL(x):[x in u => A(x)] <=> ALL(y):[Set(y) & ALL(b):[b in y => b in u] => ALL(x):[x in y => A(x)]]]]

> Which is not what the formula says.

It would if you had actually named your mysterious "domain of discussion."

> The formula
> has both x ∈ u and y ∈ u. If you translate it this way:
>
> ∀x(x ∈ u → Ax) ↔ ∀y(y ∈ u → ∀x(x ∈ y → Ax))
>
> Its not anymore provable from logic alone:
>
> ∀x(Exu → Ax) ↔ ∀y(Eyu → ∀x(Exy → Ax)) is invalid.
> https://www.umsu.de/trees/#~6x(Exu~5Ax)~4~6y(Eyu~5~6x(Exy~5Ax))
>

It seems to need an axiom of set theory.

> Error 2)
> You didn't translate the second quantifer ∀x.

x is quantified twice as it is your initial statement.

> With translation
> of the second quantifier the formula would be:
>
> ∀x(x ∈ u → Ax) ↔ ∀y(y ∈ u → ∀x(x ∈ u → (x ∈ y → Ax)))
>
> Its again not anymore provable from logic alone:
>
> ∀x(Exu → Ax) ↔ ∀y(Eyu → ∀x(Exu → (Exy → Ax))) is invalid.
> https://www.umsu.de/trees/#~6x(Exu~5Ax)~4~6y(Eyu~5~6x(Exu~5(Exy~5Ax)))
>
> Error 3)
> You assume a translation is needed, but the problem is
> posed as is, namely as follow:
>
> ∀xAx ↔ ∀y∀x(x ∈ y → Ax)
>
> The formula can be proved when you use unordered pair.

[snip childish abuse]

I have simply revealed the inner workings of your system that you somehow want to keep hidden from view. Deal with it, Mr. Collapse.

[Dan Christensen]

On Thursday, July 13, 2023 at 2:10:37 PM UTC-4, Mild Shock wrote:
> You only demonstrated so far:
>
> - You didn't understand the proof sketch and
> couldn't prove: ∀xAx ↔ ∀y∀x(x ∈ y → Ax)
>

On the contrary, I revealed its inner workings that, for some bizarre reason, you prefer to keep hidden from the reader.

> - You don't know how to consistently relativize to u and
> couldn't translate: ∀xAx ↔ ∀y∀x(x ∈ y → Ax)
>
> Do you want me to spoil it, and show the proof? Its
> really easy. As a first step you can try the following lemma:
>
> Lemma: Singletons Exist
> ======================
> Proof Sketch: Use that unordered pairs exist:
> https://en.wikipedia.org/wiki/Axiom_of_pairing
> So for any x,y the set {x,y} exist.

Not necessary in my proof. I simply take a subset of the supposed domain of discussion.

[Mild Shock]

You proved the wrong thing. Try proving
what is given as an exercise theorem:

∀xAx ↔ ∀y∀x(x ∈ y → Ax)

Or do you claim its not provable in DC Poop?

[Mild Shock]

Woa! The lemma is already hard for some proof tools.
For example Wolfgang Schwartz tool hangs:

Tool doesn't find proof [Pairing implies Singleton] #23
https://github.com/wo/tpg/issues/23

But after some long winding roads, I could make a proof in DC
Poop of the Singleton Lemma. I cannot yet use my proof search

because I don't have yet biconditional <=> in my tip development
branch. So only a manual proof here in DC Poop:

44 ALL(a):ALL(b):EXIST(c):ALL(d):[d ε c <=> d=a | d=b]
=> ALL(b):EXIST(c):ALL(d):[d ε c <=> d=b]
Conclusion, 1

---------------------------- begin proof -------------------------------------

1 ALL(a):ALL(b):EXIST(c):ALL(d):[d ε c <=> d=a | d=b]
Premise

2 ~ALL(b):EXIST(c):ALL(d):[d ε c <=> d=b]
Premise

3 ~~EXIST(b):~EXIST(c):ALL(d):[d ε c <=> d=b]
Quant, 2

4 EXIST(b):~EXIST(c):ALL(d):[d ε c <=> d=b]
Rem DNeg, 3

5 ~EXIST(c):ALL(d):[d ε c <=> d=u]
E Spec, 4

6 ALL(b):EXIST(c):ALL(d):[d ε c <=> d=u | d=b]
U Spec, 1

7 EXIST(c):ALL(d):[d ε c <=> d=u | d=u]
U Spec, 6

8 ALL(d):[d ε v <=> d=u | d=u]
E Spec, 7

9 ~~ALL(c):~ALL(d):[d ε c <=> d=u]
Quant, 5

10 ALL(c):~ALL(d):[d ε c <=> d=u]
Rem DNeg, 9

11 ~ALL(d):[d ε v <=> d=u]
U Spec, 10

12 ~~EXIST(d):~[d ε v <=> d=u]
Quant, 11

13 EXIST(d):~[d ε v <=> d=u]
Rem DNeg, 12

14 ~[w ε v <=> w=u]
E Spec, 13

15 w ε v <=> w=u | w=u
U Spec, 8

16 [w ε v => w=u | w=u] & [w=u | w=u => w ε v]
Iff-And, 15

17 w ε v => w=u | w=u
Split, 16

18 w=u | w=u => w ε v
Split, 16

19 w ε v
Premise

20 w=u | w=u
Detach, 17, 19

21 ~w=u
Premise

22 ~w=u => w=u
Imply-Or, 20

23 w=u
Detach, 22, 21

24 ~w=u & w=u
Join, 21, 23

25 ~~w=u
Conclusion, 21

26 w=u
Rem DNeg, 25

27 w ε v => w=u
Conclusion, 19

28 w=u
Premise

29 ~[w=u | w=u]
Premise

30 ~~[~w=u & ~w=u]
DeMorgan, 29

31 ~w=u & ~w=u
Rem DNeg, 30

32 ~w=u
Split, 31

33 ~w=u
Split, 31

34 w=u & ~w=u
Join, 28, 33

35 ~~[w=u | w=u]
Conclusion, 29

36 w=u | w=u
Rem DNeg, 35

37 w ε v
Detach, 18, 36

38 w=u => w ε v
Conclusion, 28

39 [w ε v => w=u] & [w=u => w ε v]
Join, 27, 38

40 w ε v <=> w=u
Iff-And, 39

41 ~[w ε v <=> w=u] & [w ε v <=> w=u]
Join, 14, 40

42 ~~ALL(b):EXIST(c):ALL(d):[d ε c <=> d=b]
Conclusion, 2

43 ALL(b):EXIST(c):ALL(d):[d ε c <=> d=b]
Rem DNeg, 42

44 ALL(a):ALL(b):EXIST(c):ALL(d):[d ε c <=> d=a | d=b]
=> ALL(b):EXIST(c):ALL(d):[d ε c <=> d=b]
Conclusion, 1

---------------------------- end proof -------------------------------------

[Dan Christensen]

On Thursday, July 13, 2023 at 4:01:18 PM UTC-4, Mild Shock wrote:
> You proved the wrong thing. Try proving
> what is given as an exercise theorem:
> ∀xAx ↔ ∀y∀x(x ∈ y → Ax)

You should try to prove it, as is common practice in mathematics, by specifying the name of an arbitrary set as the so-called "domain of discourse." See, for example, my proof: https://www.dcproof.com/JanBurse15.htm

No can do??? Oh, well...

[Mild Shock]

Your translation is nonsense:

ALL(u):[Set(u)
=> [ALL(a):[a e u => P(a)]
<=> ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]]]]
https://www.dcproof.com/JanBurse15.htm

Where do you get ALL(b):[b e a => b e u] from?
It means a ⊆ u. Where do you see y ⊆ u here:

∀xAx ↔ ∀y∀x(x ∈ y → Ax)

There is no requirement that y ⊆ u. Its not a SOL theorem.
Its a FOL/ZFC theorem where EVERYTHING IS A SET.
A correct translation would be, you only need Set:

ALL(x):[Set(x) => A(x)] <=> ALL(y):[Set(y) => ALL(x):[Set(x) => [x e y => A(x)]]]

Do you have a proof of the above?

[Mild Shock]

Maybe you think ZFC means Zorro Fried Chicken? Eh?

"In set theory, Zermelo–Fraenkel set theory, named after
mathematicians Ernst Zermelo and Abraham Fraenkel, is
an axiomatic system that was proposed in the early twentieth
century in order to formulate a theory of sets"
https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory

So in ZFC we have EVERYTHING IS A SET.

Whats wrong with you?

[Mild Shock]

So lets go back to the sketch, and finalize the proof:

> Its not so difficult to prove. The => direction
> is trivial. And the <= direction you can consider the
> sub case y={x} that (*), which needs unordered pair:

Lets see wether the => direction is trivial. Yes it needs nothing:

∀xAx → ∀y∀x(Exy → Ax) is valid.
https://www.umsu.de/trees/#~6xAx~5~6y~6x%28Exy~5Ax%29

And now the <= direction using the Singleton lemma:

(∀b∃c∀d(Edc ↔ d=b) ∧ ∀y∀x(Exy → Ax)) → ∀xAx is valid.
https://www.umsu.de/trees/#~6b~7c~6d%28Edc~4d=b%29~1~6y~6x%28Exy~5Ax%29~5~6xAx

Q.E.D. Was this so difficult?

[Dan Christensen]

On Thursday, July 13, 2023 at 4:40:41 PM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Donnerstag, 13. Juli 2023 um 22:27:58 UTC+2:
> > On Thursday, July 13, 2023 at 4:01:18 PM UTC-4, Mild Shock wrote:
> > > You proved the wrong thing. Try proving
> > > what is given as an exercise theorem:
> > > ∀xAx ↔ ∀y∀x(x ∈ y → Ax)
> > You should try to prove it, as is common practice in mathematics, by specifying the name of an arbitrary set as the so-called "domain of discourse." See, for example, my proof: https://www.dcproof.com/JanBurse15.htm
> >
> > No can do??? Oh, well...

> Your translation is nonsense:
>
> ALL(u):[Set(u)
> => [ALL(a):[a e u => P(a)]
> <=> ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]]]]
> https://www.dcproof.com/JanBurse15.htm
>
> Where do you get ALL(b):[b e a => b e u] from?

'a' is a subset of u, with u being the so-called "domain of discourse."

> It means a ⊆ u.

Yes.

> Where do you see y ⊆ u here:
> ∀xAx ↔ ∀y∀x(x ∈ y → Ax)

The set of all objects under consideration are just those elements of u. If you have a set, each element of it will be an element of u. It works. Do you have a better idea?

> There is no requirement that y ⊆ u. Its not a SOL theorem.
> Its a FOL/ZFC theorem where EVERYTHING IS A SET.
> A correct translation would be, you only need Set:
>
> ALL(x):[Set(x) => A(x)] <=> ALL(y):[Set(y) => ALL(x):[Set(x) => [x e y => A(x)]]]
>

What is the domain of discourse? Some arbitrary set? Are 'Set' and 'A' are just arbitrary unary predicates. Is 'e' just an arbitrary binary relation? Or do you have axioms about 'Set', 'A' and 'e'?

[Dan Christensen]

On Thursday, July 13, 2023 at 4:45:12 PM UTC-4, Mild Shock wrote:
> Maybe you think ZFC means Zorro Fried Chicken? Eh?
>
> "In set theory, Zermelo–Fraenkel set theory, named after
> mathematicians Ernst Zermelo and Abraham Fraenkel, is
> an axiomatic system that was proposed in the early twentieth
> century in order to formulate a theory of sets"
> https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory
>
> So in ZFC we have EVERYTHING IS A SET.
>

How is this relevant? BTW it is not assumed that everything is set in DC Proof.

[Mild Shock]

Who cares? Here everything is a set. Or if there are ur-elements,
then there is also a comulative hiearchy. Means you have not
only sets of urelements, but also sets of sets of urelements,

and so on. Why is this so. As soon as you see V_α, then this
is a reference to the von Neumann hierarchy. And the full
fledge use case of Scott's trick is this here:

If V ∩ [a] is non-empty, we can define a set, which represents
[a], even if [a] is a proper class. Namely, there exists a least ordinal α,
such that V_α ∩ [a] is non-empty.
https://en.wikipedia.org/wiki/Scott%27s_trick#Scott's_trick_in_general

The sets in V are divided into the transfinite hierarchy V_α ,
called the cumulative hierarchy, based on their rank.
https://en.wikipedia.org/wiki/Von_Neumann_universe

So a ⊆ u is certainly wrong. Because this means that there
is a rank, the rank of u, which limits the universe. But the
cumulative hierarchy has no maximum rank.

Got it?

Similarly, in my example: The singleton {x} is the smallest
set y such that x e y.

[Dan Christensen]

On Thursday, July 13, 2023 at 4:52:49 PM UTC-4, Mild Shock wrote:
> So lets go back to the sketch, and finalize the proof:
> > Its not so difficult to prove. The => direction
> > is trivial. And the <= direction you can consider the
> > sub case y={x} that (*), which needs unordered pair:
> Lets see wether the => direction is trivial. Yes it needs nothing:
>
> ∀xAx → ∀y∀x(Exy → Ax) is valid.
> https://www.umsu.de/trees/#~6xAx~5~6y~6x%28Exy~5Ax%29
>
> And now the <= direction using the Singleton lemma:
>
> (∀b∃c∀d(Edc ↔ d=b) ∧ ∀y∀x(Exy → Ax)) → ∀xAx is valid.
> https://www.umsu.de/trees/#~6b~7c~6d%28Edc~4d=b%29~1~6y~6x%28Exy~5Ax%29~5~6xAx
>

Doesn't your Singleton lemma require ZFC (e.g. a Pairing Axiom)? You will probably want to specify a set to be the "domain of discourse" and include it in your theorem.

[Mild Shock]

Are you sleep walking? Read the thread carefully.
How many times do you find the phrase in this thread?

"unordered pair"

How many times do you find a link to this axiom:

https://en.wikipedia.org/wiki/Axiom_of_pairing

You even find a DC Proof of this Lemma:

44 ALL(a):ALL(b):EXIST(c):ALL(d):[d ε c <=> d=a | d=b]
=> ALL(b):EXIST(c):ALL(d):[d ε c <=> d=b]
Conclusion, 1

[Mild Shock]

You don't have the Pairing Axiom in DC Proof.
Who cares? Dana Scott didn't work with DC Proof.

As soon as you have the Lemma, its like riding
the back of a tornado. You can prove it in a blink!

∀xAx → ∀y∀x(Exy → Ax) is valid.
https://www.umsu.de/trees/#~6xAx~5~6y~6x%28Exy~5Ax%29

(∀b∃c∀d(Edc ↔ d=b) ∧ ∀y∀x(Exy → Ax)) → ∀xAx is valid.
https://www.umsu.de/trees/#~6b~7c~6d%28Edc~4d=b%29~1~6y~6x%28Exy~5Ax%29~5~6xAx

[Dan Christensen]

On Thursday, July 13, 2023 at 5:36:19 PM UTC-4, Mild Shock wrote:
> You don't have the Pairing Axiom in DC Proof.

In almost every field of mathematics, there are one or more underlying sets of objects, e.g. the set of natural numbers in number theory. Other objects are constructed from elements of these underlying sets, e.g. functions on those sets. Rarely if ever do they deal with arbitrary objects outside the context of sets assumed or proven to exist. As such, I have never found a need to deal with such objects and have not required axioms such as the ZFC Pairing Axiom. To construct a singleton, for example, I find that the Subset Axiom is quite sufficient.

[Ross Finlayson]

On Tuesday, July 11, 2023 at 11:11:57 PM UTC-7, Ross Finlayson wrote:
> On Sunday, July 9, 2023 at 9:56:52 AM UTC-7, Ross Finlayson wrote:
> > Dana Scott fan club
> >
> > Been reading some more into Dana Scott. He has a pretty good intuition and is
> > also a grandiose sort of hedge. Also he knows things and isn't wrong.
> >
> > Been reading a bit into the Habermas school or Frankfurt school.
> >
> > Cohen's "Equations from G-d" was a pretty good historical outline about
> > Boole and de Morgan than about Russell about "pure mathematics" in the
> > 19'th century, still though I believe in a stronger platonism and that there's
> > a science of mathematics but its study is _of_ the real "pure mathematics".
> >
> > Was reading some Knuth the other day about combinatorics historically,
> > quite a well-rounded guy.
> Been reading Quine's "Set Theory" (and Quine's number theory and Quine's model theory, ...).
>
> I thought it was pretty good until he got up to real numbers and used the term "non-circularize
> the argument" in an off-hand way. He started with a good discussion of class/set distinction
> then put it aside and coat-tailed up past "higher-order equals". As a structuralist I don't much
> agree except that "equals is first-order", so pretty much the usual coat-tails logician's coat-tailing
> of "higher-order equals" comes across as "circularized". So, when Quine got to his real numbers
> and was like "my rationals are reals instead of my reals are rationals" then there's a quibble about
> least-upper-bound property, pretty much I was disappointed in him when he faked a quibble about
> least-upper-bound property. Still, I'm only about half-way through so maybe there will be something
> better to talk about later in it.
>
> Dana Scott's pretty good. He's like, "Oh you made an algebra? Here's a boolean lattice."
>
>
> Reading the other days about Schwarz functions and their distributions and Heaviside's function
> and hysteresis and ringing and Gibbs, from some late '90's papers from NASA, about doubling-spaces
> and the non-standard and infinitesimals, I figure that it still makes pretty great sense the re-Vitali-ization
> of measure theory ("after LUB, the other axiom, measure 1.0"), into doubling spaces and Ramsey theory,
> figuring they'll need a foundations besides their applied.
>
> The stopping-derivative is kind of an interesting idea, I've been thinking about the identity dimension
> and a bunch of great stuff that arrives from re-Vitali-ization and a deconstructive account of the
> arithmetic and so on.

Well I kept reading Quine's book on set theory, "Set Theory ...", and it's really pretty great
and one of the better or the best overall books on set theory.

He goes on to explain the various perspectives and approaches to the objects of set theory,

elements have memberships (elt, set theory, Mengen),
classes have members (contains, part theory, Unmenge),

and explains various organizations of primary objects

Frege and his numbers,
von Neumann and about functions,
Russell with types,
Zermelo and well-foundings

and about well-orderings and ordering theory.

What I notice of it is as the various concerns of the concepts of the objects,
circle about a common drain,

set and part theory,
ordering theory,
number theory,
function theory

so this sits very well with my approaches to ubiquitous ordinals,
topology and function theory making for geometry, that to make
for a circularizing of the circularizing, has that pretty much I can mark
the salient points in Quine that have where these approaches define
each other in terms of each other, and suss out a unified approach to
them-all.

When it comes to coat-tails, here it's canonry, where fully I intend that
it's one giant coat-tails. (And none.)

For foundations, it's a foundations of logical objects, mathematical objects,
all one theory.


Yeah, I'm pretty happy I wrote an apologetics for modern mathematics and
paleo-classical post-modern extra-standard ubiquitous ordinals in primary
objects and ur-elements after all universal theory.

Don't need another one, ....

Quine shirt-sleeves quite a few good quotes on the topic.

[Mild Shock]

So you don't belong to the Dana Scott fan club. So then hush,
go away, seems you are not involved in foundation and/or meta
mathematics. Especially you are not aware of ORDINALS and the

RANK of a set. BTW: Its not so difficult to understand how the ZFC
Universe works. Just lookup wikipedia how the cumulative hiearchy
relates to the regularity axiom (which you have also missing in DC Proof),

and you find. Dana Scott (1974) went further and claimed that:

The truth is that there is only one satisfactory way of avoiding
the paradoxes: namely, the use of some form of the theory of types.
That was at the basis of both Russell's and Zermelo's intuitions.
Indeed the best way to regard Zermelo's theory is as a simplification
and extension of Russell's. (We mean Russell's simple theory of types,
of course.) The simplification was to make the types cumulative.
Thus mixing of types is easier and annoying repetitions are avoided.
Once the later types are allowed to accumulate the earlier ones, we
can then easily imagine extending the types into the transfinite—just
how far we want to go must necessarily be left open. Now Russell made
his types explicit in his notation and Zermelo left them implicit. [emphasis in original]
https://en.wikipedia.org/wiki/Axiom_of_regularity

You have a lot of gaps Dan-O-Matik. Of course its up to you whether
you want to fill them or not. But its quite funny that you never publish
blog posts about ordinals or the rank of a set. These things have

kept some great minds busy, like Cantor, etc.. But I guess small
minds like Dan-O-Matik simply don't have any sensory at all for the
questions concerning infinity involved in these matters. The result

is that Dan-O-Matiks understanding of sets results in abonimations
like utter bullshit as in his Generalized Drinker Paradox.

[Mild Shock]

Let's make set theory great again!

Its not so difficult to learn classical set theory, there are books,
you know. Also the worlds has still libraries despite the internet.

Recommended reading:

Basic Set Theory by Azriel Levy
https://www.amazon.com/dp/0486420795

Only 15 bucks on Amazon.

Have Fun!

[Mild Shock]

The problem is, everytime Dan-O-Matik refers to "set theory",
on sci.logic or sci.math, as a recommendation or as explication
what he is doing, he is not refering to "set theory" proper.

He is refering to his "theory in DC Proof". which is not a " set theory"
proper. Its rather a kind of "type theory". One test case, only
involving the pairing axiom, whether your "theory" is a set

theory or not, is this theorem:

∀xA(x) <=> ∀y∀x(x ∈ y => A(x))

It is not formalizable so easily in a "type theory". But goes
smooth in a "set theory". Try doing the above in a "type theory"
based prover, like for example Coq.

I didn't try yet in Coq. But for example you need a set membership
where x and y have the same type "set". So if you start doing
the usual Coq thing interpreting x ∈ y as x(y), you won't grasp

Dana Scotts trick. Unless you have a Scott Domain where
U = U -> U, i.e. some reflective Domain. Such domains are for
example explained here (Note this is another Scott in the

authorship, but the paper talks at length about Dana Scott):

Introduction to Higher Order Categorical Logic
Joachim Lambek & Philip J. Scott
Cambridge University Press (1986)
https://raw.githubusercontent.com/Mzk-Levi/texts/master/Lambek%20J.%2C%20Scott%20P.J.%20Introduction%20to%20Higher%20Order%20Categorical%20Logic.pdf

[Mild Shock]

Corr.: Typo

the usual Coq thing interpreting x ∈ y as y(x), you won't grasp

Dana Scotts trick. Unless you have a Scott Domain where
U = U -> U, i.e. some reflective Domain. Such domains are for

[Dan Christensen]

On Friday, July 14, 2023 at 4:22:23 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> The problem is, everytime Dan-O-Matik refers to "set theory",
> on sci.logic or sci.math, as a recommendation or as explication
> what he is doing, he is not refering to "set theory" proper.
>

[snip]

I am referring to axioms implicitly used in most textbook proofs--not ZFC as it turns out. Deal with it, Mr. Collapse.

[Mild Shock]

Well why do you name it set theory than, if its not set theory.
I mean you can read the 1908 paper of Zermelo. He uses singletons
to model natural numbers:

1 = {{}}
2 = {{{}}}
3 = {{{{}}}}
Etc...

The so called Zermelo successor is succ(x) = {x}. Something
you don't have in DC Proof. So why call it "set theory" when its not set theory?

[Mild Shock]

Maybe call it "little-set theory". It is well known that most mathematics
needs only a little set theory. I guess little set theory would work
with sets from V_ω+ω. Can you prove the existence of V_ω+ω in

DC Proof, with the existing axioms of DC Proof? You even don't have
an axiom of infinity. So you cannot prove existence of ω. But lets
assume ω exists, could you show that V_ω+ω exists in DC Proof ?

V_ω+ω is called the universe for ordinary mathematics. See also
here, which a reference to a book by Smullyan & Fitting:

"V_ω+ω is the universe of "ordinary mathematics",
and is a model of Zermelo set theory.
https://en.wikipedia.org/wiki/Von_Neumann_universe

[Dan Christensen]

On Friday, July 14, 2023 at 4:49:49 PM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Freitag, 14. Juli 2023 um 17:22:46 UTC+2:
> > On Friday, July 14, 2023 at 4:22:23 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> > > The problem is, everytime Dan-O-Matik refers to "set theory",
> > > on sci.logic or sci.math, as a recommendation or as explication
> > > what he is doing, he is not refering to "set theory" proper.
> > >
> > [snip]
> >
> > I am referring to axioms implicitly used in most textbook proofs--not ZFC as it turns out. Deal with it, Mr. Collapse.

> Well why do you name it set theory

Again, it is the "set theory" is actually used in most textbook proofs.

than, if its not set theory.
> I mean you can read the 1908 paper of Zermelo. He uses singletons
> to model natural numbers:
>
> 1 = {{}}
> 2 = {{{}}}
> 3 = {{{{}}}}
> Etc...
>

3 is not usually considered to be a set in most textbook proofs. Must be frustrating as hell for you.

> The so called Zermelo successor is succ(x) = {x}.

I prefer Peano's Axioms as follows:

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

[Dan Christensen]

On Friday, July 14, 2023 at 5:00:42 PM UTC-4, Mild Shock wrote:
> Maybe call it "little-set theory". It is well known that most mathematics
> needs only a little set theory.

In DC Proof, I have formalized the set theory used in most mathematics.

> I guess little set theory would work
> with sets from V_ω+ω. Can you prove the existence of V_ω+ω in
>

[snip]

V cannot even be proven to exist in ZFC, so why bother?

> You even don't have
> an axiom of infinity.

No set or other object is postulated to exist in DC Proof, but users can introduce their own versions of an axiom of infinity. I prefer simply stating Peano's Axioms at the beginning of a proof (see my previous posting here).

> So you cannot prove existence of ω.

[snip]

If you are determined to prove the existence of the set of natural numbers, you can start by assuming the existence of an arbitrary Dedekind infinite set (an alternative axiom of infinity) :

1. EXIST(a):EXIST(f):[Set(a) & ALL(b):[b in a => f(b) in a] <------------- f: a --> a
& ALL(b):ALL(c):[b in a & c in a => [f(b)=f(c) => b=c]] <-------------------- f is injective
& EXIST(b):[b in a & ALL(c):[c in a => ~f(c)=b]]] <---------------------------- f is not surjective

[Dan Christensen]

On Friday, July 14, 2023 at 4:05:55 AM UTC-4, Mild Shock wrote:
[snip]

> The truth is that there is only one satisfactory way of avoiding
> the paradoxes: namely, the use of some form of the theory of types.
> That was at the basis of both Russell's and Zermelo's intuitions.

[snip]

DC Proof avoids Russell's Paradox and the existence of a universal set by not assuming (as in Frege's axioms) that for every unary predicate P, we can infer the existence of a set {x : P(x)}.

Using my Subset Axiom, however, for any set S and unary predicate P, we can infer the existence of a set {x in S: P(x)}, no type theory required.

[Daniel Pehoushek]

here is a sample of real sets that are bit encoded in my system
pspace to qspace transform uses bit encoded sets
here is the code (equations) for transforming a set of boolean models to a set of valid quantifications
it depends on add in set theory which depends on bignum counting
vee is a number less than n the number of variables
the set is bit encoded by 32 bit nums and needs space to hold set members
boolean variables encode each member

the transform is from pspace in dnf to qspace in monotone dnf
the result is the solution of all qbfs in twelve lines
the original set of members transforms to quantifications

there is a followup transform from monotone dnf to monotone cnf
daniel2380+++

// plan left right of all set members with set union/intersection
void plan (num vee, numnums& set)
{ when(set.size()==zero || vee == qvars.size()) return;
numnums left; numnums right; split(vee, set, left, right);
plan(vee + one, left); plan(vee + one, right); juggle (vee, left, right);
// ezistential q variables are in left universal remain on right
for (num g = zero; g < left.size(); g++) ezis(*(left[g]), vee);}

// left right union and intersection
void juggle (num vee, numnums& left, numnums& right)
{if(left.size()==zero){for(num g=zero;g<right.size();g++)left.add(right[g]);right.setsize(zero);return;}
when(vee == qvars.size()) return;
numnums al; numnums ar; split(vee + one, left, al, ar); left.setsize(zero);
numnums bl; numnums br; split(vee + one, right, bl, br); right.setsize(zero);
juggle(vee + one, al, bl); juggle(vee + one, ar, br);
for (num g=zero; g < al.size(); g++) left.add(al[g]); for (num g=zero; g < ar.size(); g++) left.add(ar[g]);
for (num g=zero; g < bl.size(); g++) right.add(bl[g]); for (num g=zero; g < br.size(); g++) right.add(br[g]); }

static num be(nums& s, num b) { return (s[b >> five] & (ones[b & fifthtau])); } //
static joy ezis(nums& s, num b) { s[b >> five] &= zeroes[b & fifthtau]; } //
static joy split /*leftright around bit*/(num b, numnums& s, numnums& l, numnums& r) // left right on bit b
{for (num g = zero; g < s.size(); g++) if (be((*s[g]), b)) r.add(s[g]); else l.add(s[g]); } //

[Dan Christensen]

On Friday, July 14, 2023 at 11:45:21 PM UTC-4, Dan Christensen wrote:

> On Friday, July 14, 2023 at 4:05:55 AM UTC-4, Mild Shock wrote:
> [snip]
> > The truth is that there is only one satisfactory way of avoiding
> > the paradoxes: namely, the use of some form of the theory of types.
> > That was at the basis of both Russell's and Zermelo's intuitions.
> [snip]
>
> DC Proof avoids Russell's Paradox and the existence of a universal set by not assuming (as in Frege's axioms) that for every unary predicate P, we can infer the existence of a set {x : P(x)}.
>
> Using my Subset Axiom, however, for any set S and unary predicate P, we can infer the existence of a set {x in S: P(x)}, no type theory required.

This feature would seem to avoid the internal contradictions of Frege's axioms as exhibited by Russell's Paradox and the notion of a universal set.

[Mild Shock]

Maybe start with something simpler.
Can this here proved in DC Proof to exist:

ω+ω

It looks as follows:

0, 1, 2, 3, ... 0', 1', 2', 3', ...

See also:
https://en.wikipedia.org/wiki/Ordinal_arithmetic#Addition

[Dan Christensen]

(Correction)

On Saturday, July 15, 2023 at 2:50:33 PM UTC-4, Mild Shock wrote:
> Maybe start with something simpler.
> Can this here proved in DC Proof to exist:
>
> ω+ω
>
> It looks as follows:
>
> 0, 1, 2, 3, ... 0', 1', 2', 3', ...
>

You might use the following axiom to specify N={0, 1, 2, ... } and N'={0', 1', 2', ... } and take the union N U N'.

1. EXIST(m):EXIST(m0):EXIST(f): [Set(m) & m0 in m & ALL(a):[a in m => f(a) in m]
& ALL(a):ALL(b):[a in m & b in m => [f(a)=f(b) => a=b]]
& ALL(a):[a in m => ~f(a)=m0]
& ALL(a):[Set(a) & ALL(b):[b in a => b in m] => [m0 in a & ALL(b):[b in a => f(b) in a] => ALL(b):[b in m => b in a]]]]
Axiom

> See also:
> https://en.wikipedia.org/wiki/Ordinal_arithmetic#Addition

I'm not sure, but you might be able to formalize the axioms there in DC Proof. It is not something that interests me. Thanks anyway.

[Mild Shock]

How do you produce N' in DC Proof?

[Mild Shock]

Ref: https://github.com/wo/tpg/issues/23

Wolfgang Schwarz fixed his tool. This one can
now be automatically proved.

∀a∀b∃c∀d(Edc ↔ (d=a ∨ d=b)) → ∀b∃c∀d(Edc ↔ d=b) is valid.
https://www.umsu.de/trees/#~6a~6b~7c~6d%28Edc~4%28d=a~2d=b%29%29~5~6b~7c~6d%28Edc~4d=b%29

Nice!

[Dan Christensen]

On Monday, July 17, 2023 at 3:17:29 AM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Sonntag, 16. Juli 2023 um 21:36:51 UTC+2:
> > (Correction)
> > On Saturday, July 15, 2023 at 2:50:33 PM UTC-4, Mild Shock wrote:
> > > Maybe start with something simpler.
> > > Can this here proved in DC Proof to exist:
> > >
> > > ω+ω
> > >
> > > It looks as follows:
> > >
> > > 0, 1, 2, 3, ... 0', 1', 2', 3', ...
> > >
> > You might use the following axiom to specify N={0, 1, 2, ... } and N'={0', 1', 2', ... } and take the union N U N'.
> >
> > 1. EXIST(m):EXIST(m0):EXIST(f): [Set(m) & m0 in m & ALL(a):[a in m => f(a) in m]
> > & ALL(a):ALL(b):[a in m & b in m => [f(a)=f(b) => a=b]]
> > & ALL(a):[a in m => ~f(a)=m0]
> > & ALL(a):[Set(a) & ALL(b):[b in a => b in m] => [m0 in a & ALL(b):[b in a => f(b) in a] => ALL(b):[b in m => b in a]]]]
> > Axiom
> >

[snip]

> How do you produce N' in DC Proof?

You would apply the above axiom twice, specifying different names the second time: n, 0, s then n', 0', s'

[Mild Shock]

Your such a Ordinal Baby Dan-O-Matik
And how would you prove the existence of:

ω
ω+ω
ω+ω+ω
ω+ω+ω+ω
Etc..

Namely the existence of ω*n?
Hint: ω+ω is the special case ω*2.

Dan Christensen schrieb:

[Dan Christensen]

On Monday, July 17, 2023 at 2:11:11 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:


> [snip childish abuse]

> And how would you prove the existence of:
>
> ω
> ω+ω
> ω+ω+ω
> ω+ω+ω+ω
> Etc..
>

Again, this is simply not something that interests me. See my blog for the kinds of things that do interest me.

Dan

[Mild Shock]

Dana Scott fan club challenge. Show that "obj" as a set
and naively modelled here by Dan Christensen:

Toward a Formal, Machine-Parsable Definition of a Category
https://groups.google.com/g/sci.math/c/gDtJtH8RHvc

Cannot be a set if we assume certain category theory equations,
which might be seen as consistent in category theory itself.

Disclaimer: I don't have such equations just now at hand, working on it.

[Ross Finlayson]

Picked up a copy of a translation one of Kant's less-than-usually-ambitiously-titled
"On the old saw: That may be right in theory but it won't work in practice",
and it helps remind me that lots of modern neo-Platonists are pseudo-Platonists
and that a strong Platonism again is sort of superior for stronger logicists.

It's like when Russell quipped "mathematics is I dunno" ("mathematics is that where
we never know what we're doing nor whether it's true") and it's like, no, Russell,
it's pretty much the opposite.

[Ross Finlayson]

Your rejection of strong platonism won't work in the practice of strong platonism.

It's pretty simple: you don't have to accept being Russell's dupe.
The Russellian duplicity of the Russellian hypocrisy of the Russell "paradox"
being axiomatized away, it's just a mental convenience for agreeably a large
class of concerns, that if you don't know the difference, and maintain through
all derivations why it's not so, Russell's "I usurped Frege", then, that would
result an ignoramus, who agreeably doesn't need to know the difference,
or a hypocrite, or a charlatan.


For foundation's sake though, it's unacceptable.

[Mild Shock]

It is in SETS FOR MATHEMATICS, how things are not sets.
Even with only reading half of the book.

"Subsets are not mere sets with a special property but are
explicit inclusion maps. (This helps one to realize that
many constructions involving subsets are simplified and
usefully generalized when applied appropriately to maps that
are not necessarily subsets.)"
http://patryshev.com/books/Sets%20for%20Mathematics.pdf

You just reject this definition:

A ⊆ B <=> ∀x(x ∈ A => x ∈ B)

And go with this definition, note in WILLIAM LAWVERE, the
arrows are basically sets:

"Historically many mathematicians such as Dedekind
and Banach used the same symbol ⊆ for both membership
and inclusion, and indeed it is quite reasonable to
define x belongs to y for any two maps with codomain A
and even to use the same symbol for it"
http://patryshev.com/books/Sets%20for%20Mathematics.pdf

x ⊆ y <=> ∃z(x = y*z)

[Mild Shock]

Now I am having fun with minimal logic, which rejects not
only ex falso quodlibet, but equivalently it rejects counter
example theorem:

~(P -> Q) => P /\ ~Q

Usually this can be used in set theory, to say if A ⊆ B
doesn't hold, then there must be a point c such that
c ∈ A and ~c ∈ B. By the usual logical transformation,

whereby the elimination of ∀x and the introduction of
∃x is not problematic, since ∃x would be anyway typically
defined as ~∀x~:

~∀x(x ∈ A => x ∈ B)
---------------------------------
∃x(x ∈ A /\ ~x ∈ B)

I guess in category you cannot say te same. ~(x ⊆ y) does
not automatically imply that there is such a point. The book
is full of examples from analysis and geometry,

but I think the book is not very accessible. Maybe starting
with minimal logic would be more productive. Disclaimer:
There might be also differences between minimal logic, and

category theory. Just discovering a few things right now,
such like the above involvedment of counter example theorem.

[Ross Finlayson]

It's said Quine said "Quine said that ''quotation has a certain anomalous feature''."

https://en.wikipedia.org/wiki/Use%E2%80%93mention_distinction

Here it's kind of that quotation enters a syntax, about syntax, and about the lexical and
syntax, that there's a simple sort of inner and outer syntax, about what results for an
overall language that syntax becomes category and attribute, that symbols as quantities,
reflect that there's overall a context of all the objects, of a universe of objects their language.

[Mild Shock]

Rossy Boy just got expelled from Dana Scott fan club
because of his extraordinary idiocy. He is so clueless
about set theory, even a cat that brings home some

friends is 100 times smarter than Rossy Boy:

Bonjour ! When your cat brings home a friend 🤣
https://www.youtube.com/watch?v=cbjvy5ruIpo

Ross Finlayson schrieb am Samstag, 5. August 2023 um 21:28:28 UTC+2:
> ... usual gibberish nobody cares about ...

[Ross Finlayson]

Wow, 100 times, ....

I started this chapter of a Dana Scott fan club and you're welcome
to come and go as you please, the reason why though I'm a fan of
Dana Scott is because he's noticed the hypocrisies that a lot of
people either buy or shill and went and built boolean lattices and
such which make rid of them on their own merits, his own.

I'm pretty sure it's not because of being an irrational, fatuous, flatulent,
flake (or fake). Indeed it's not. But, it's simple to employ such rhetoric,
especially when it's not a real person.

[Mild Shock]

Is Dana Scott a deer, a moose or a raccon, that
you braught with you, Rossy Boy cat?

When your cat brings home a friend 🤣

https://www.youtube.com/watch?v=5g8Z02fsHfI

The biggest hypocrite here on sci.logic and sci.math
is Rossy Boy, which is ironic, the way how uneasy

he feels with logic and/or mathematics.

LoL

[Ross Finlayson]

I can only imagine you refer to "the logic" and "the mathematics",
a strong platonist and monist's mathematics and logic, that is resulting
from a theory of truth, that also sets up science as justified, and most
matters of application as thusly so ("the scientific").

That is to say, I know you don't, but still I do.

Dana Scott's a Californio so I guess that makes him a bear.

Point is though that he's a man and a logician and not a Burse's-butt-joke.

Once there was a cat. Over time it brought in fifty or more birds and
rodents, sometimes just an explosion of feathers, sometimes just a
squirrel's kidney. Once its eye got scratched, ended up keeping it inside.
So anyways relocated to the boonies, a flock of wild turkeys came
through one day, it sized them up and that was about it.

Still though somehow it was an effortless hunter.


Anyways though I'm at great _ease_ about mathematics because I have at
least _three_ definitions continuity, which is at least _two_ more than
usual plebeians of the dillettante or work-a-day formalist variety.

Also having a theory that's true in itself, yeah I figure that any
"science's theory of everything" has to be a "logic and mathematics'
theory of everything", first.

Then we can get into Goedel and the regular and beyond it, sort of
the entire development from fin de siecle 1900's to 21'st century today.

Anyways the line-continuity and field-continuity concepts sort of help
align something like Dana Scott et alia's circle and box modalities' notations.
(And provide formal constructivist foundations they exist.)

[Ross Finlayson]

It's like the other day Dana Scott was giving a speech and
he said "I heard about untyped lambda calculus, and then
really what made it tractable was typed lambda calculus,
but one day I was waking from a nap and had a vision, that
the underlying logic was again an untyped lambda calculus".

And they say old dogs can't learn new tricks, ....

[Steven Lahkmi]

Almost forget about you. Ross, do you have some non-solved mathematical/foundational problem that you may want to propose ?

[Mild Shock]

Currently one of the most pressing unsolved
mathematical/foundational problem is: Where's Waldo?

Anybody a clue where the Liar Paradox is here:

https://dcproof.com/LiarParadox2.htm

[Ross Finlayson]

On Monday, September 4, 2023 at 1:03:24 PM UTC-7, Steven Lahkmi wrote:
> Almost forget about you. Ross, do you have some non-solved mathematical/foundational problem that you may want to propose ?

I got "Borel versus Combinatorics".

Mostly though I already proposed a bunch of solutions to resolving mathematical and logical
paradox for the none thereof.

It's just one, though, ..., one good theory.

[Mild Shock]

Dan Christensen wrote:
> To construct a singleton, for example, I find
> that the Subset Axiom is quite sufficient.

Can you show us? For example this proof:

Mild Shock schrieb am Dienstag, 5. September 2023 um 01:40:37 UTC+2:
> /* Singletons Axiom */
> 1 ALL(x):EXIST(y):ALL(z):[z @ y <=> z=x]
> Axiom
>
> /* Theorem Indiscernibility implies Extensionality */
> 36 ALL(a):ALL(b):[ALL(y):[a @ y <=> b @ y] => ALL(y):[y @ a <=> y @ b]]
> 4 Conclusion, 2
https://groups.google.com/g/sci.logic/c/o1kH0z15rc8/m/7F9oK1QMAQAJ

Can this be done with the Subset Axiom?

Dan Christensen schrieb am Freitag, 14. Juli 2023 um 06:15:26 UTC+2:

> On Thursday, July 13, 2023 at 5:36:19 PM UTC-4, Mild Shock wrote:
> > You don't have the Pairing Axiom in DC Proof.

> In almost every field of mathematics, there are one or more underlying sets of objects, e.g. the set of natural numbers in number theory. Other objects are constructed from elements of these underlying sets, e.g. functions on those sets. Rarely if ever do they deal with arbitrary objects outside the context of sets assumed or proven to exist. As such, I have never found a need to deal with such objects and have not required axioms such as the ZFC Pairing Axiom. To construct a singleton, for example, I find that the Subset Axiom is quite sufficient.

[Ross Finlayson]

I wanted to learn about reality, so I started looking into truth, and for mathematics the
key seemed the duality of the continuous and the discrete, then, well, learning ensued.

I'd studied calculus and delta-epsilonics and knew there was more to it, when I found that
everything had been picked the one side of the un-attainable continuity, as from some
un-attained discreteness, then I went about establishing that there are more than the one
definition of completeness for continuity, for the usual milieu the real numbers.

Then it's similar for monism and atomism, and elements and membership, and counting
and numbering, these various complementary notions, defined as infinite completions
or limits the one side the other, then arrives at a general description of the inductive impasse,
that without both ways is neither way.

The various pathologies of the extension of the inductive impasse, like "well-ordering the reals",
numbering in counting, or "an ordinary infinity", when there's one that isn't, or "making something
from fallacy", that isn't true, these are addressed to be dispatched, "resolving paradoxes",
and not just "defining limits".

In this manner such notions as class/set distinction, impredicativity, quantifier disambiguation,
and a bunch other sorts the usual "vagaries or inconsistencies of naive logics", get fixed up,
aobut infinities and the fixed point and the inductive impasses, and, the bridges up after
the transfer principle, these ponts which bridge the inductive impasses, in the middle,
the "middle of nowhere", now "the center of the space".

The "Borel vs. Combinatorics", then, is that in Cantor space or the space of all sequences of
zero's and one's, 0's and 1's, Borel says "almost all" and Combinatorics says "almost none"
have a particular property. So, they disagree, it's an inconsistency.

Then, I helped square it up as a "square Cantor space", and help make for "half". It has a lot
to do with the very real nature of a space of a continuum of 0's and 1's, it's what I've found.


The Dana Scott fan club has a similar notion of "circle and box modalities",
and a usual appendage to modern-ish model theories add "the illative" or
as an infinite union besides pair-wise union, but then they about immediately
contradict each other, because neither will give.

So, arriving at a usual notion of a theory meeting the requirements and desiderata of
at least one theory that's true, is that there's exactly one that's true, then lots of
what were results in formal fundamental inequalities, just result bounds in rates.

Not that they aren't still distinct: just that they aren't still unique.

That's my theory and it's stuck with me.

[Dan Christensen]

On Monday, September 4, 2023 at 8:26:36 PM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Freitag, 14. Juli 2023 um 06:15:26 UTC+2:
> > On Thursday, July 13, 2023 at 5:36:19 PM UTC-4, Mild Shock wrote:
> > > You don't have the Pairing Axiom in DC Proof.
> > In almost every field of mathematics, there are one or more underlying sets of objects, e.g. the set of natural numbers in number theory. Other objects are constructed from elements of these underlying sets, e.g. functions on those sets. Rarely if ever do they deal with arbitrary objects outside the context of sets assumed or proven to exist. As such, I have never found a need to deal with such objects and have not required axioms such as the ZFC Pairing Axiom. To construct a singleton, for example, I find that the Subset Axiom is quite sufficient.

> Dan Christensen wrote:
> > To construct a singleton, for example, I find
> > that the Subset Axiom is quite sufficient.
>
> Can you show us?

[snip]

Example: ALL(a):[a in r => EXIST(b):[Set(b) & [a in b & ALL(c):[c in b => c=a]]]] where r = the set of real numbers

1. Set(r)
Axiom

2. x in r
Premise

3. EXIST(b):[Set(b) & ALL(c):[c in b <=> c in r & c=x]]
Subset, 1

4. Set(y) & ALL(c):[c in y <=> c in r & c=x]
E Spec, 3

5. Set(y)
Split, 4

6. ALL(c):[c in y <=> c in r & c=x]
Split, 4

7. x in y <=> x in r & x=x
U Spec, 6

8. [x in y => x in r & x=x] & [x in r & x=x => x in y]
Iff-And, 7

9. x in r & x=x => x in y
Split, 8

10. x=x
Reflex

11. x in r & x=x
Join, 2, 10

12. x in y
Detach, 9, 11

13. z in y
Premise

14. z in y <=> z in r & z=x
U Spec, 6

15. [z in y => z in r & z=x] & [z in r & z=x => z in y]
Iff-And, 14

16. z in y => z in r & z=x
Split, 15

17. z in r & z=x
Detach, 16, 13

18. z=x
Split, 17

19. ALL(c):[c in y => c=x]
Conclusion, 13

20. x in y & ALL(c):[c in y => c=x]
Join, 12, 19

21. Set(y) & [x in y & ALL(c):[c in y => c=x]]
Join, 5, 20

22. ALL(a):[a in r => EXIST(b):[Set(b) & [a in b & ALL(c):[c in b => c=a]]]]
Conclusion, 2

[Ross Finlayson]

Why, what do you think's wrong with it?

[Ross Finlayson]

I don't need to send this post!

Why I do, ....

[Mild Shock]

Thats not the requested Singleton Lemma, which would be needed here:
You have c in b => c=a but the requiretent would be c in b <=> c=a:

Mild Shock schrieb am Dienstag, 5. September 2023 um 01:40:37 UTC+2:
> /* Singletons Axiom */
> 1 ALL(x):EXIST(y):ALL(z):[z @ y <=> z=x]
> Axiom
>
> /* Theorem Indiscernibility implies Extensionality */
> 36 ALL(a):ALL(b):[ALL(y):[a @ y <=> b @ y] => ALL(y):[y @ a <=> y @ b]]
> 4 Conclusion, 2
https://groups.google.com/g/sci.logic/c/o1kH0z15rc8/m/7F9oK1QMAQAJ

Try again!

[Mild Shock]

I believe you cannot do it in DC Proof. Since it has to
work for any set x. So since you don't have an Universal Set in
set theory, there is no "r" such that "x in r" for any set x.

Maybe some Dana Scott trick could do it, don't know.
But just right now I don't see how you could replicate
the Singleton Lemma in DC Proof:

> /* Singletons Axiom */
> 1 ALL(x):EXIST(y):ALL(z):[z @ y <=> z=x]
> Axiom

I was thinking of using:
- Power Set Axiom
- Subset Axiom

This works in ZFC as a replacement for Singleton via
Unordered Pairing. But I don't think it works in DC Proof.
But maybe it works if we further assume Set(x).

Then it we would have the Power Set P(x), and could filter
it via the Subset Axiom, to get {x}. But this would also mean
that we have a different Singleton Lemma, namely

one that only works for Set(x), but what about Urelements?

[Mild Shock]

Corr.: Typo

I believe you cannot do it in DC Proof. Since it has to

work for any x. So since you don't have an Universal Set in

[Ross Finlayson]

It's not like I really knew why I did it: but it's still done!

Now I know, though.

[Dan Christensen]

On Tuesday, September 5, 2023 at 5:39:17 AM UTC-4, Mild Shock wrote:
> Corr.: Typo
> I believe you cannot do it in DC Proof. Since it has to
> work for any x. So since you don't have an Universal Set in

> > I believe you cannot do it in DC Proof. Since it has to
> > work for any set x. So since you don't have an Universal Set in
> > set theory, there is no "r" such that "x in r" for any set x.
> >
> > Maybe some Dana Scott trick could do it, don't know.
> > But just right now I don't see how you could replicate
> > the Singleton Lemma in DC Proof:
> > > /* Singletons Axiom */
> > > 1 ALL(x):EXIST(y):ALL(z):[z @ y <=> z=x]
> > > Axiom
> > I was thinking of using:
> > - Power Set Axiom
> > - Subset Axiom
> >
> > This works in ZFC as a replacement for Singleton via
> > Unordered Pairing.

It is almost never required in textbook math proofs. If you think you need it, you are probably on the wrong track. If you insist, you could introduce an axiom like:

1. ALL(a):ALL(b):EXIST(c):[Set(c) & a in c & b in c & ALL(d):[d in c => d=a | d=b]]
Axiom

[Mild Shock]

Its used in this proof, showing that "indiscernible" implies "extensional".
You find such a proof also in math text books. Maybe there is a proof
using something else than Singleton? The goal is to prove:

> 36 ALL(a):ALL(b):[ALL(y):[a @ y <=> b @ y] => ALL(y):[y @ a <=> y @ b]]
> 4 Conclusion, 2

Can you prove it otherwise? With another "Ansatz", than Singletons?

[Mild Shock]

Nope, Power Set doesn't work. What would work if there
were a replacement axiom in DC Proof. Replacement is stronger
than subset. But DC Proof has no replacement axiom.

See also:

Proving the pairing axiom from the rest of ZF
https://math.stackexchange.com/q/141646

So how would one prove this here in DC Proof:

> 36 ALL(a):ALL(b):[ALL(y):[a @ y <=> b @ y] => ALL(y):[y @ a <=> y @ b]]
> 4 Conclusion, 2

Its impossible, right?

[Mild Shock]

What is the replacement axiom. Well its the _F_ in the
_ZF_ set theory. It was introduce 1922 by Abraham _F_raenkel
into the set theory of Ernst _Z_ermelo from 1908

Axiom schema of replacement
https://en.wikipedia.org/wiki/Axiom_schema_of_replacement

An axiom schema simply missing in DC Poop. So DC Poop
does even not provide ZF? LoL

[Dan Christensen]

On Tuesday, September 5, 2023 at 6:00:36 PM UTC-4, Mild Shock wrote:
> What is the replacement axiom. Well its the _F_ in the
> _ZF_ set theory. It was introduce 1922 by Abraham _F_raenkel
> into the set theory of Ernst _Z_ermelo from 1908
>
> Axiom schema of replacement
> https://en.wikipedia.org/wiki/Axiom_schema_of_replacement
>

> An axiom schema simply missing in DC Proof

I think you will find it isn't used much in textbook math proofs. From your link, "The axiom schema of replacement is not necessary for the proofs of most theorems of ordinary mathematics." Users with very specialized interests can, of course, introduce their own version of this axiom in DC Proof using the Axiom Rule on the Logic menu.

[Ross Finlayson]

It's funny ex falso quodlibet and "tell me a lie,
I'll believe anything you say", compared to
"from nothing, I get all of mathematics,
tell me something I don't know".

Ex falso nihilum, ex nihilum veritas.

Verite.

[Ross Finlayson]

Burse bot Mostowski:

"While empty set and Axiom III might have something
to do with surreal numbers, thats why I am intersted
in the discussion.

I doubt that Judea Pearl, who specializes in probabilistic
reasoning, has anything to do with surreal numbers.
I even don't know why causality came up.

Rossi Robots AI has an old fetisch which you see further
below. He mentioned material implication there. And indeed
material implication can be used

to explain vacously true formulas, provided the
sort is modelled as a predicate. Material implication
does not cover this here with an empty sort:

forall x:A B(x)

it would be a kind of an empty conjunction and
by convention true. Material implication on
the other hand enters the picture here:

forall x (A(x) => B(x))

But also only if the domain is non empty. It
would then explain a vacously true formula in
that A(x) fails for all x's, and therefore

material implication doesn't care. So reducing
vacously true to material implication is only
half way possible. Its a logical effect in

its own if we look at the unsorted quantifier
in a free logic. " -- 2020

[Ross Finlayson]

On Thursday, July 13, 2023 at 11:51:10 PM UTC-7, Ross Finlayson wrote:
> On Tuesday, July 11, 2023 at 11:11:57 PM UTC-7, Ross Finlayson wrote:
> > On Sunday, July 9, 2023 at 9:56:52 AM UTC-7, Ross Finlayson wrote:
> > > Dana Scott fan club
> > >
> > > Been reading some more into Dana Scott. He has a pretty good intuition and is
> > > also a grandiose sort of hedge. Also he knows things and isn't wrong.
> > >
> > > Been reading a bit into the Habermas school or Frankfurt school.
> > >
> > > Cohen's "Equations from G-d" was a pretty good historical outline about
> > > Boole and de Morgan than about Russell about "pure mathematics" in the
> > > 19'th century, still though I believe in a stronger platonism and that there's
> > > a science of mathematics but its study is _of_ the real "pure mathematics".
> > >
> > > Was reading some Knuth the other day about combinatorics historically,
> > > quite a well-rounded guy.
> > Been reading Quine's "Set Theory" (and Quine's number theory and Quine's model theory, ...).
> >
> > I thought it was pretty good until he got up to real numbers and used the term "non-circularize
> > the argument" in an off-hand way. He started with a good discussion of class/set distinction
> > then put it aside and coat-tailed up past "higher-order equals". As a structuralist I don't much
> > agree except that "equals is first-order", so pretty much the usual coat-tails logician's coat-tailing
> > of "higher-order equals" comes across as "circularized". So, when Quine got to his real numbers
> > and was like "my rationals are reals instead of my reals are rationals" then there's a quibble about
> > least-upper-bound property, pretty much I was disappointed in him when he faked a quibble about
> > least-upper-bound property. Still, I'm only about half-way through so maybe there will be something
> > better to talk about later in it.
> >
> > Dana Scott's pretty good. He's like, "Oh you made an algebra? Here's a boolean lattice."
> >
> >
> > Reading the other days about Schwarz functions and their distributions and Heaviside's function
> > and hysteresis and ringing and Gibbs, from some late '90's papers from NASA, about doubling-spaces
> > and the non-standard and infinitesimals, I figure that it still makes pretty great sense the re-Vitali-ization
> > of measure theory ("after LUB, the other axiom, measure 1.0"), into doubling spaces and Ramsey theory,
> > figuring they'll need a foundations besides their applied.
> >
> > The stopping-derivative is kind of an interesting idea, I've been thinking about the identity dimension
> > and a bunch of great stuff that arrives from re-Vitali-ization and a deconstructive account of the
> > arithmetic and so on.
>
> Well I kept reading Quine's book on set theory, "Set Theory ...", and it's really pretty great
> and one of the better or the best overall books on set theory.
>
> He goes on to explain the various perspectives and approaches to the objects of set theory,
>
> elements have memberships (elt, set theory, Mengen),
> classes have members (contains, part theory, Unmenge),
>
> and explains various organizations of primary objects
>
> Frege and his numbers,
> von Neumann and about functions,
> Russell with types,
> Zermelo and well-foundings
>
> and about well-orderings and ordering theory.
>
> What I notice of it is as the various concerns of the concepts of the objects,
> circle about a common drain,
>
> set and part theory,
> ordering theory,
> number theory,
> function theory
>
> so this sits very well with my approaches to ubiquitous ordinals,
> topology and function theory making for geometry, that to make
> for a circularizing of the circularizing, has that pretty much I can mark
> the salient points in Quine that have where these approaches define
> each other in terms of each other, and suss out a unified approach to
> them-all.
>
> When it comes to coat-tails, here it's canonry, where fully I intend that
> it's one giant coat-tails. (And none.)
>
> For foundations, it's a foundations of logical objects, mathematical objects,
> all one theory.
>
>
> Yeah, I'm pretty happy I wrote an apologetics for modern mathematics and
> paleo-classical post-modern extra-standard ubiquitous ordinals in primary
> objects and ur-elements after all universal theory.
>
> Don't need another one, ....
>
> Quine shirt-sleeves quite a few good quotes on the topic.


Here's an example of a 2023 paper about continuous domains that references a Scott topology.

https://arxiv.org/abs/2301.09940

It sort of makes you wonder how such a, "countable continuous domain", could be, without tipping each other's carts.

"In the infinitary logic", ....

It's funny if you search for "countable continuous domain" nothing shows up, but "modern foundations" "set theory"
"countable continuous domain" sort of arrives here.

[Ross Finlayson]

If you're interested in some of Scott's examples of topologies and
topologies via logic, you might appreciate Vickers' "Topology via Logic".

The usual open topology of course and zero being rational gets into
why otherwise for example rationals and irrationals would be indistinguishable
except for their countability. "Topology via Logic" introduces others.

This Hofmann-Mislove theorem also sort of provides a complement/alternative,
to something like Dedekind completeness, if you don't not look the other way.

Then, one might aver that this leads to contradictions unless there's some way
to model various sorts of continuous domains, like line/field/signal reals.

[Ross Finlayson]

Anybody with a mathematics degree has probably sat a topology course.

Then, usually the usual open topology is very well explored, there are others.

The book "Counterexamples in Topology" is pretty great, ..., there are others.

See, one reason I'm a fan of Dana Scott is that he knows enough about the
entire edifice of the usual "modern mathematics" to arrive at why it's reasonable
that there are alternative derivations with alternative conclusions, that, thusly
as mathematics, would need to see a quite necessary revision of what's otherwise,
"foundations", for it all to sit together without contradicting itself.

[Mild Shock]

Who remembers this in December 2023?

Pumping lemma for regular languages
https://en.wikipedia.org/wiki/Pumping_lemma_for_regular_languages

It was first proven by Michael Rabin and Dana Scott in 1959