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.

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

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

Ross Finlayson schrieb am Sonntag, 9. Juli 2023 um 18:56:52 UTC+2:
> 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.

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

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

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

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

Mild Shock wrote:
>
> 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))
>
> 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.
>>
>> Dan
>>
>

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

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

Dan Christensen wrote:
> 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
>

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 tp provide a formal proof in your system (ZFC?), I will provide a formal provide one in my system.

Dan

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

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.

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 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).
>
> Dan
>

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

On Wednesday, July 12, 2023 at 8:08:31 AM UTC-7, Dan Christensen wrote:
> 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

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.

On Tuesday, July 11, 2023 at 7:27:15 PM UTC-4, 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).
>

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.

Dan

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

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.

Dan Christensen wrote:
> On Tuesday, July 11, 2023 at 7:27:15 PM UTC-4, 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).
>>
>
> 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.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>
>
>
>
>

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.

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
>
> 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.
> Dan Christensen wrote:
> > On Tuesday, July 11, 2023 at 7:27:15 PM UTC-4, 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).
> >>
> >
> > 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.
> >

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

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

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

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

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

Dan

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

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.

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).
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

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?

Mild Shock schrieb am Donnerstag, 13. Juli 2023 um 10:32:15 UTC+2:
> 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.
> 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).
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, 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.

Dan

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

You are 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?

Dan Christensen schrieb am Donnerstag, 13. Juli 2023 um 17:27:10 UTC+2:
> 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.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

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.

Mild Shock schrieb am Donnerstag, 13. Juli 2023 um 19:39:59 UTC+2:
> 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?
> Dan Christensen schrieb am Donnerstag, 13. Juli 2023 um 17:27:10 UTC+2:
> > 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.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

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

> Dan Christensen schrieb am Donnerstag, 13. Juli 2023 um 17:27:10 UTC+2:
> > 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.

[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?

Dan

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