So where does the crankness of Dan Christens
come from. Why does it water his garden when
it rains? Any explanation for his nonsense so

that we would see some practical relevance?
I mean every theorem that has the form of Euclids
theorem, i.e. provides some axiomatic evidence

for some object, like this here:

> Euclid's theorem is a fundamental statement in
> number theory that asserts that there are infinitely
> many prime numbers.
https://en.wikipedia.org/wiki/Euclid's_theorem

Automatically implies a non-empty domain.
You can try yourself in your DC Proof. If you
have some theorem in mathematics of the form:

1 EXIST(x):A(x)
Axiom

It automatically implies:

4 EXIST(x):x=x
E Gen, 3

This time I managed to a more direct proof:

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

1 EXIST(x):A(x)
Axiom

2 A(u)
E Spec, 1

3 u=u
Reflex

4 EXIST(x):x=x
E Gen, 3

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

Mostowski Collapse schrieb am Montag, 31. Oktober 2022 um 17:14:22 UTC+1:
> We can say a mathematical theory does not
> have the non-empty domain assumption
> if we cannot prove EXIST(x):x=x. But this is
>
> already the case (in DC Proof) for:
>
> 1 Set(n)
> Axiom
>
> It implies:
>
> 9 EXIST(x):x=x
> Rem DNeg, 8
>
> So are there any mathematical theories that
> don't share the non-empty domain assumption?
> It doesn't matter whether they are
>
> explicit or implicit. It only matters whether
> mathematics works with theories T such
> that T |/- EXIST(x):x=x ?
>
> If some such really exists, then a tool like
> DC Proof would make sense. Otherwise its
> a useless feature.
>
> --------------------- begin proof ----------------------------
>
> 1 Set(n)
> Axiom
>
> 2 ~EXIST(x):x=x
> Premise
>
> 3 ~~ALL(x):~x=x
> Quant, 2
>
> 4 ALL(x):~x=x
> Rem DNeg, 3
>
> 5 ~n=n
> U Spec, 4
>
> 6 n=n
> Reflex
>
> 7 ~n=n & n=n
> Join, 5, 6
>
> 8 ~~EXIST(x):x=x
> Conclusion, 2
>
> 9 EXIST(x):x=x
> Rem DNeg, 8
>
> --------------------- end proof ----------------------------
> Mostowski Collapse schrieb am Montag, 31. Oktober 2022 um 17:04:19 UTC+1:
> > Could you please show us numbers, where you
> > don't assume a non-empty domain, like here,
> > from DC Poops menu item:
> >
> > 1 Set(n)
> > Axiom
> >
> > 2 1 ε n
> > Axiom
> >
> > And then do this proof:
> >
> > > Euclid's theorem is a fundamental statement in
> > > number theory that asserts that there are infinitely
> > > many prime numbers.
> > https://en.wikipedia.org/wiki/Euclid's_theorem

On Monday, October 31, 2022 at 12:04:19 PM UTC-4, Mostowski Collapse wrote:
> Could you please show us numbers, where you
> don't assume a non-empty domain, like here,
> from DC Poops menu item:
>
> 1 Set(n)
> Axiom
>
> 2 1 ε n
> Axiom
>
[snip]

You are missing the point, Jan Burse. In DC Proof, if you want something to exist, you must explicitly assume or prove its existence as you have here. You cannot infer EXIST(a):P(a) given only that ALL(a):P(a) as in FOL.

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 a liar. No I didn't miss the point. I am only asking
where it is used. Whats its practical usage? Can you point
to a mathematical theorem, i.e. a pair P |- Q, in literature,

where we could not also prove:

P |- EXIST(x):x=x

So where it would matter, that we can omit this assumption.
After so many years, you never braught up an example
where omitting the assumption leads to something useful.

Now you picked the drinker praradox, which has the form
EXIST(x):A(x). But such a result always requires such an
assumption in a free logic, in a logic like DC Proof,

you can verify yourself:

1 EXIST(x):A(x)
Axiom

2 A(u)
E Spec, 1

3 u=u
Reflex

4 EXIST(x):x=x
E Gen, 3

The above works also when EXIST(x):A(x) is the drinker paradox
EXIST(x):[D(x)=>ALL(y):D(y)]. But what is a practical example,
where EXIST(x):x=x is not part of theory? Do you have a single

such practical example as demanded now?

Mostowski Collapse wrote:

> You are a liar. No I didn't miss the point. I am only asking where it is
> used. Whats its practical usage? Can you point to a mathematical
> theorem, i.e. a pair P |- Q, in literature, where we could not also
> prove: P |- EXIST(x):x=x

yet another "uKrainian" humanitarian corridor.

Maybe you are not aware, miss the point, that
we get to P |- EXIST(x):x=x via a simple
modus ponens, like here:

P |- EXIST(x):A(x) |- EXIST(x):A(x) => EXIST(x):x=x
------------------------------------------------------- (MP)
P |- EXIST(x):x=x

So you need only prove once, and then you can
use your (Det = Apply Detachment Rule) button:

1 EXIST(x):A(x)
Premise

2 A(u)
E Spec, 1

3 u=u
Reflex

4 EXIST(x):x=x
E Gen, 3

5 EXIST(x):A(x) => EXIST(x):x=x
Conclusion, 1

So every mathematical theorem P |- Q
where Q has the form EXIST(x):A(x) is already
ruled out, as a candidate where we would

need DC Proof, the feature that it can work
with an empty domain. Can you point to a
mathematical theorem, i.e. a pair P |- Q, in

literature, where we could not also prove:

P |- EXIST(x):x=x

On Monday, October 31, 2022 at 12:53:17 PM UTC-4, Mostowski Collapse wrote:
> You are a liar. No I didn't miss the point. I am only asking
> where it is used. Whats its practical usage? Can you point
> to a mathematical theorem, i.e. a pair P |- Q, in literature,
>
> where we could not also prove:
>
> P |- EXIST(x):x=x
>

Just about field of mathematics assumes one or more underlying set(s), e.g. a set of numbers, points in space, a group or ring. So, of course, in number theory, you can prove EXIST(a):[a in N & a=a]. The restriction to N is essential. Not sure what your point is, Jan Burse.

Dan

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

Dan Christensen wrote:

> On Monday, October 31, 2022 at 12:53:17 PM UTC-4, Mostowski Collapse
> wrote:
>> P |- EXIST(x):x=x
>
> Just about field of mathematics assumes one or more underlying set(s),
> e.g. a set of numbers, points in space, a group or ring. So, of course,

not good to be a *slava_uKraina* nazi, right now, huh?

What can you do for "uKraina"?? Can you send some money and wepans, huh??
*slava_uKraina*, for "uKraina", huh, so the cocaine gay actor zelenske make
more billions of money, huh?? Go fuck, you can do nothen for the
*slava_uKraina*.

Kiev residents line up to get some water
https://%62%69%74%63%68%75%74%65.com/%76%69%64%65%6f/cdW2XsTAUDC8/

On Monday, October 31, 2022 at 2:49:00 PM UTC-4, Buddie Fiore wrote:
> Dan Christensen wrote:
>
> > On Monday, October 31, 2022 at 12:53:17 PM UTC-4, Mostowski Collapse
> > wrote:
> >> P |- EXIST(x):x=x
> >
> > Just about field of mathematics assumes one or more underlying set(s),
> > e.g. a set of numbers, points in space, a group or ring. So, of course,
> not good to be a *slava_uKraina* nazi, right now, huh?
>

You will soon be lining up to have your head shaved with a rusty blade, Nazi Boy. It's probably too late to escape from Nazi ruSSia. Better go into hiding and wait for, umm... who knows?

I nowhere said that you should infer EXIST(a):P(a),
from ALL(a):P(a). I only asked for an example where
a mathematician does not infer EXIST(a):P(a)
from ALL(a):P(a). You pretend mathematics doesn't

do that, which would make your tool necessary.
But I guess your tool is as necessary as tool
to neuter cats, in world where all cats were already
neutered. Whats your example where a matematician

doesn't infer EXIST(a):P(a) from ALL(a):P(a)?

Could you please give such an example in the wild?
Smullyans Drinker Paradox is not such an example,
he infers EXIST(a):P(a) from ALL(a):P(a). So where
your Jim, the Jim of an empty domain? Where is

your real world example of a mathematician or
math textbook, where it is not infered EXIST(a):P(a)
from ALL(a):P(a). Do you have such an example that
would justify the existence of DC Proof and free logic?

Dan Christensen schrieb am Montag, 31. Oktober 2022 um 18:22:32 UTC+1:
> On Monday, October 31, 2022 at 12:53:17 PM UTC-4, Mostowski Collapse wrote:
> > You are a liar. No I didn't miss the point. I am only asking
> > where it is used. Whats its practical usage? Can you point
> > to a mathematical theorem, i.e. a pair P |- Q, in literature,
> >
> > where we could not also prove:
> >
> > P |- EXIST(x):x=x
> >
> Just about field of mathematics assumes one or more underlying set(s), e.g. a set of numbers, points in space, a group or ring. So, of course, in number theory, you can prove EXIST(a):[a in N & a=a]. The restriction to N is essential. Not sure what your point is, Jan Burse.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen wrote:

> On Monday, October 31, 2022 at 2:49:00 PM UTC-4, Buddie Fiore wrote:
>> Dan Christensen wrote:
>>
>> > On Monday, October 31, 2022 at 12:53:17 PM UTC-4, Mostowski Collapse
>> > wrote:
>> >> P |- EXIST(x):x=x
>> >
>> > Just about field of mathematics assumes one or more underlying
>> > set(s),
>> > e.g. a set of numbers, points in space, a group or ring. So, of
>> > course,
>> not good to be a *slava_uKraina* nazi, right now, huh?
>
> You will soon be lining up to have your head shaved with a rusty blade,

so you are not going to support the *slava_uKraina*, or you don't
undrestand tensors, once again.

Send some fucking moeny to cocaine zelenske, and water to the people. You,
nazi khazar bitch. You soon are going to emigrate to Antarctica, now for
good. *I_fuck_your_ass*, bitch. *slava_uKraina*, bitch.

I see a big problem with empty-poop-universe and
DC Proof. The empty-poop-universe isn't totally empty.

Take this empty-poop-universe counter example:

∀c((P→Qc) ∧ (Qc→R)) → (P→R) is valid.
https://www.umsu.de/trees/#~6c%28%28P~5Qc%29~1%28Qc~5R%29%29~5%28P~5R%29

∀c(Uc → ((P→Qc) ∧ (Qc→R))) → (P→R) is invalid.
https://www.umsu.de/trees/#~6c%28Uc~5%28P~5Qc%29~1%28Qc~5R%29%29~5%28P~5R%29

Countermodel:
Domain: { 0 }
U: { }
P: true
Q: { 0 }
R: false

U is empty, U={}, so c cannot take any value anymore,
∀ reduces to true, and ∃ would reduce to false.

But the propositional variables P and R are as chatty
as before. They can take different truth values.

So the empty-poop-universe is a lie! Its not empty.

This refutes Rossy Boys claim, there is only one empty
domain [of discourse] ? Well there is possibly only one empty
domain U={}. But the domain [of disourse], if taken as

a model, as also predicate symbols. These predicate symbols,
let R stand for such a predicate symbol and its interpretation,
are interpreted as R ⊆ D^n.

Now what happens to a propositional variable. Lets say a
propositional variable P and its interpretation is just a
predicate symbol of zero arity and we need to

have a view for: P ⊆ D^0

One can define D^0 as { ε } where ε is the empty tupel.
But if D = {}, should D^0 also be the singleton of the
empty tupel. Didn't write Dan-O-Matik about

Oh the Ambiguity of 0^0. What is the empty tupel
even in a set theory universe? The two truth values
false and true, can be seen as the two subsets

of { ε } namely {} and { ε }. So an empty universe
has nevertheless a empty tupel?

Mostowski Collapse schrieb am Donnerstag, 3. November 2022 um 18:35:04 UTC+1:
> I see a big problem with empty-poop-universe and
> DC Proof. The empty-poop-universe isn't totally empty.
>
> Take this empty-poop-universe counter example:
>
> ∀c((P→Qc) ∧ (Qc→R)) → (P→R) is valid.
> https://www.umsu.de/trees/#~6c%28%28P~5Qc%29~1%28Qc~5R%29%29~5%28P~5R%29
>
> ∀c(Uc → ((P→Qc) ∧ (Qc→R))) → (P→R) is invalid.
> https://www.umsu.de/trees/#~6c%28Uc~5%28P~5Qc%29~1%28Qc~5R%29%29~5%28P~5R%29
>
> Countermodel:
> Domain: { 0 }
> U: { }
> P: true
> Q: { 0 }
> R: false
>
> U is empty, U={}, so c cannot take any value anymore,
> ∀ reduces to true, and ∃ would reduce to false.
>
> But the propositional variables P and R are as chatty
> as before. They can take different truth values.
>
> So the empty-poop-universe is a lie! Its not empty.

Of course I am doing a stretch here, conflating object
level and meta level. But sometimes object and meta
level do blend into each other. Is there a formula

that can detect that we are in an empty universe.
For DC Proof possibly this formula would do:

¬∀c((P→Qc) ∧ (Qc→R)) → (P→R)

Whats the easiest? This here?

¬∃x(x=x)

Are there formulas for the empty tuple?

Mostowski Collapse schrieb am Donnerstag, 3. November 2022 um 18:55:04 UTC+1:
> This refutes Rossy Boys claim, there is only one empty
> domain [of discourse] ? Well there is possibly only one empty
> domain U={}. But the domain [of disourse], if taken as
>
> a model, as also predicate symbols. These predicate symbols,
> let R stand for such a predicate symbol and its interpretation,
> are interpreted as R ⊆ D^n.
>
> Now what happens to a propositional variable. Lets say a
> propositional variable P and its interpretation is just a
> predicate symbol of zero arity and we need to
>
> have a view for: P ⊆ D^0
>
> One can define D^0 as { ε } where ε is the empty tupel.
> But if D = {}, should D^0 also be the singleton of the
> empty tupel. Didn't write Dan-O-Matik about
>
> Oh the Ambiguity of 0^0. What is the empty tupel
> even in a set theory universe? The two truth values
> false and true, can be seen as the two subsets
>
> of { ε } namely {} and { ε }. So an empty universe
> has nevertheless a empty tupel?
> Mostowski Collapse schrieb am Donnerstag, 3. November 2022 um 18:35:04 UTC+1:
> > I see a big problem with empty-poop-universe and
> > DC Proof. The empty-poop-universe isn't totally empty.
> >
> > Take this empty-poop-universe counter example:
> >
> > ∀c((P→Qc) ∧ (Qc→R)) → (P→R) is valid.
> > https://www.umsu.de/trees/#~6c%28%28P~5Qc%29~1%28Qc~5R%29%29~5%28P~5R%29
> >
> > ∀c(Uc → ((P→Qc) ∧ (Qc→R))) → (P→R) is invalid.
> > https://www.umsu.de/trees/#~6c%28Uc~5%28P~5Qc%29~1%28Qc~5R%29%29~5%28P~5R%29
> >
> > Countermodel:
> > Domain: { 0 }
> > U: { }
> > P: true
> > Q: { 0 }
> > R: false
> >
> > U is empty, U={}, so c cannot take any value anymore,
> > ∀ reduces to true, and ∃ would reduce to false.
> >
> > But the propositional variables P and R are as chatty
> > as before. They can take different truth values.
> >
> > So the empty-poop-universe is a lie! Its not empty.

On Monday, October 31, 2022 at 3:48:15 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 31. Oktober 2022 um 18:22:32 UTC+1:
> > On Monday, October 31, 2022 at 12:53:17 PM UTC-4, Mostowski Collapse wrote:
> > > You are a liar. No I didn't miss the point. I am only asking
> > > where it is used. Whats its practical usage? Can you point
> > > to a mathematical theorem, i.e. a pair P |- Q, in literature,
> > >
> > > where we could not also prove:
> > >
> > > P |- EXIST(x):x=x
> > >
> > Just about field of mathematics assumes one or more underlying set(s), e.g. a set of numbers, points in space, a group or ring. So, of course, in number theory, you can prove EXIST(a):[a in N & a=a]. The restriction to N is essential. Not sure what your point is, Jan Burse.

> I nowhere said that you should infer EXIST(a):P(a),
> from ALL(a):P(a). I only asked for an example where
> a mathematician does not infer EXIST(a):P(a)
> from ALL(a):P(a).

[snip]

This makes no sense, Jan Burse. What mathematician has ever proven that ALL(a):P(a) => EXIST(a):P(a) for arbitrary predicate P? Your mysterious domains of discourse are pretty much only found in the realm of philosophers and theologians. Perhaps you didn't know, but in mathematics, universal quantifiers are usually explicitly restricted to some specifically name set or other domain. And those sets and domains are not necessarily non-empty. Deal with it, Jan Burse.

Dan

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

Every mathematician which follows the modern structuralism
of mathematics. Where matematics is about so called structures,
which consist of a) a signature:

https://en.wikipedia.org/wiki/Signature_%28logic%29

And then for a corresponding b) structures:

https://en.wikipedia.org/wiki/Structure_%28mathematical_logic%29

In classical first-order logic, the definition of a structure prohibits
the empty domain. Now in this form of structuralism for
any predicate P in the language of a signature:

∀xPx → ∃xPx is valid.
https://www.umsu.de/trees/#~6xP%28x%29~5~7xP%28x%29

Dan Christensen schrieb am Donnerstag, 3. November 2022 um 19:12:38 UTC+1:
> This makes no sense, Jan Burse. What mathematician has ever
> proven that ALL(a):P(a) => EXIST(a):P(a) for arbitrary predicate P?

On Thursday, November 3, 2022 at 2:23:15 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 3. November 2022 um 19:12:38 UTC+1:
> > This makes no sense, Jan Burse. What mathematician has ever
> > proven that ALL(a):P(a) => EXIST(a):P(a) for arbitrary predicate P?

> Every mathematician which follows the modern structuralism
> of mathematics.

[snip]

All 3 of them?

Dan

Dan Christensen wrote:
> universal quantifiers are usually explicitly restricted
> to some specifically name set or other domain.

Thats a typical first order translation of multi-sorted logic.
But if you have multi-sorted logic, or typed logic, sorts or
types that are a domain of a structure are usually non-empty.

So I guess in most typed logics you have this provable:

∀x:T.Px → ∃x:T.Px

You can try yourself. Can you derive the above?

Dan Christensen schrieb:
> On Thursday, November 3, 2022 at 2:23:15 PM UTC-4, Mostowski Collapse wrote:
>
>> Dan Christensen schrieb am Donnerstag, 3. November 2022 um 19:12:38 UTC+1:
>>> This makes no sense, Jan Burse. What mathematician has ever
>>> proven that ALL(a):P(a) => EXIST(a):P(a) for arbitrary predicate P?
>
>> Every mathematician which follows the modern structuralism
>> of mathematics.
>
> [snip]
>
> All 3 of them?
>
> Dan
>

On Thursday, November 3, 2022 at 2:41:52 PM UTC-4, Mostowski Collapse wrote:
> Dan Christensen wrote:
> > universal quantifiers are usually explicitly restricted
> > to some specifically name set or other domain.
> Thats a typical first order translation of multi-sorted logic.
> But if you have multi-sorted logic, or typed logic, sorts or
> types that are a domain of a structure are usually non-empty.
>

It might be so much more useful otherwise.

> So I guess in most typed logics you have this provable:
>
> ∀x:T.Px → ∃x:T.Px
>

Not familiar with that notation. Not that interested either. Thanks anyway, Jan Burse.

Dan

Dan Christensen Donnerstag, 3. November 2022 um 19:47:28 UTC+1:
> Not familiar with that notation. Not that
> interested either. Thanks anyway, Jan Burse.

Come on, make up your minde. Just a few
minutes ago you wrote you want it:

Dan Christensen Donnerstag, 3. November 2022 um 19:12:38 UTC+1:
> Perhaps you didn't know, but in mathematics,
> universal quantifiers are usually explicitly
> restricted to some specifically name set or other domain.

The notation is very simple:
∀x:T.Px

∀= "universal quantifiers"
T = "your name set or other domain"

Your credility status just sunk like the LZ 129 „Hindenburg“.
But I have good news, your crank status increased.
So is this provable, yes or no, in type theory?

∀x:T.Px → ∃x:T.Px

Dan Christensen schrieb:
> On Thursday, November 3, 2022 at 2:41:52 PM UTC-4, Mostowski Collapse wrote:
>> Dan Christensen wrote:
>>> universal quantifiers are usually explicitly restricted
>>> to some specifically name set or other domain.
>> Thats a typical first order translation of multi-sorted logic.
>> But if you have multi-sorted logic, or typed logic, sorts or
>> types that are a domain of a structure are usually non-empty.
>>
>
> It might be so much more useful otherwise.
>
>
>> So I guess in most typed logics you have this provable:
>>
>> ∀x:T.Px → ∃x:T.Px
>>
>
> Not familiar with that notation. Not that interested either. Thanks anyway, Jan Burse.
>
> Dan
>

In FOL its only provable if the domain
is non-empty, you can try yourself:

∀x(Tx → Px) → ∃x(Tx ∧ Px) is invalid.
https://www.umsu.de/trees/#~6x%28Tx~5Px%29~5~7x%28Tx~1Px%29

(∃xTx ∧ ∀x(Tx → Px)) → ∃x(Tx ∧ Px) is valid.
https://www.umsu.de/trees/#~7xTx~1~6x%28Tx~5Px%29~5~7x%28Tx~1Px%29

So which type theory proves this:

∀x:T.Px → ∃x:T.Px

And which type theory doesn't prove it?

And why how is it prove in some type theories?

Mostowski Collapse schrieb:
>
> Dan Christensen Donnerstag, 3. November 2022 um 19:47:28 UTC+1:
> > Not familiar with that notation. Not that
> > interested either. Thanks anyway, Jan Burse.
>
> Come on, make up your minde. Just a few
> minutes ago you wrote you want it:
>
> Dan Christensen Donnerstag, 3. November 2022 um 19:12:38 UTC+1:
> > Perhaps you didn't know, but in mathematics,
> > universal quantifiers are usually explicitly
> > restricted to some specifically name set or other domain.
>
> The notation is very simple:
> ∀x:T.Px
>
> ∀= "universal quantifiers"
> T = "your name set or other domain"
>
>
> Your credility status just sunk like the LZ 129 „Hindenburg“.
> But I have good news, your crank status increased.
> So is this provable, yes or no, in type theory?
>
> ∀x:T.Px → ∃x:T.Px
>
> Dan Christensen schrieb:
>> On Thursday, November 3, 2022 at 2:41:52 PM UTC-4, Mostowski Collapse
>> wrote:
>>> Dan Christensen wrote:
>>>> universal quantifiers are usually explicitly restricted
>>>> to some specifically name set or other domain.
>>> Thats a typical first order translation of multi-sorted logic.
>>> But if you have multi-sorted logic, or typed logic, sorts or
>>> types that are a domain of a structure are usually non-empty.
>>>
>>
>> It might be so much more useful otherwise.
>>
>>
>>> So I guess in most typed logics you have this provable:
>>>
>>> ∀x:T.Px → ∃x:T.Px
>>>
>>
>> Not familiar with that notation. Not that interested either. Thanks
>> anyway, Jan Burse.
>>
>> Dan
>>
>

On Thursday, November 3, 2022 at 3:10:54 PM UTC-4, Mostowski Collapse wrote:
> Dan Christensen Donnerstag, 3. November 2022 um 19:47:28 UTC+1:
> > Not familiar with that notation. Not that
> > interested either. Thanks anyway, Jan Burse.
> Come on, make up your minde. Just a few
> minutes ago you wrote you want it:
>
> Dan Christensen Donnerstag, 3. November 2022 um 19:12:38 UTC+1:
> > Perhaps you didn't know, but in mathematics,
> > universal quantifiers are usually explicitly
> > restricted to some specifically name set or other domain.
> The notation is very simple:
> ∀x:T.Px
>
> ∀= "universal quantifiers"
> T = "your name set or other domain"
>

So, using more standard notation, if you have ALL(a):[ a in T => P(a)], you can only infer EXIST(a):[a in T & P(a)] if T is non-empty. Look familiar, Jan Burse?

Dan

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

Thats the result in FOL. But the result in type theory is different.
Usually type theory has these two rules:

∀x:T.Px
-------------- (∀E)
Pt

Pt
-------------- (∃I)
∃x:T.Px

You can then easily prove ∀x:T.Px → ∃x:T.Px.
The problem is a little bit the erasure of t:T judgement.

Dan Christensen schrieb am Donnerstag, 3. November 2022 um 22:00:22 UTC+1:
> On Thursday, November 3, 2022 at 3:10:54 PM UTC-4, Mostowski Collapse wrote:
> > Dan Christensen Donnerstag, 3. November 2022 um 19:47:28 UTC+1:
> > > Not familiar with that notation. Not that
> > > interested either. Thanks anyway, Jan Burse.
> > Come on, make up your minde. Just a few
> > minutes ago you wrote you want it:
> >
> > Dan Christensen Donnerstag, 3. November 2022 um 19:12:38 UTC+1:
> > > Perhaps you didn't know, but in mathematics,
> > > universal quantifiers are usually explicitly
> > > restricted to some specifically name set or other domain.
> > The notation is very simple:
> > ∀x:T.Px
> >
> > ∀= "universal quantifiers"
> > T = "your name set or other domain"
> >
> So, using more standard notation, if you have ALL(a):[ a in T => P(a)], you can only infer EXIST(a):[a in T & P(a)] if T is non-empty. Look familiar, Jan Burse?
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Because FOL is already careful enough, nobody needs
DC Proof. FOL has already this Skepticism built-in:

∀x(Tx → Px) → ∃x(Tx ∧ Px) is invalid.
https://www.umsu.de/trees/#~6x%28Tx~5Px%29~5~7x%28Tx~1Px%29

(∃xTx ∧ ∀x(Tx → Px)) → ∃x(Tx ∧ Px) is valid.
https://www.umsu.de/trees/#~7xTx~1~6x%28Tx~5Px%29~5~7x%28Tx~1Px%29

But Mathematicians don't use FOL, they use Type
Theory. All their variables have always some type.
And they use Type Theory and regularly assume that

some of their Types are non-empty. Mathematicians
don't reason on the bottom of FOL. Their reasoning
is more higher level and based on types. Thats why

the first proof assistant AUTOMATH was based on types.

L. S. van Benthem Jutting, as part of this Ph.D. thesis in 1976,
translated Edmund Landau's Foundations of Analysis into
Automath and checked its correctness.
https://en.wikipedia.org/wiki/Automath

1.0. The presupposed logic
i) Variables have well defined ranges which are not too different from
types [vD, 2,2] in AUT-QE, Cf.:
ii) Predicates have restricted domains, which again can be interpreted as
types in AUT-QE. Cf.
https://pure.tue.nl/ws/files/1710991/23183.pdf

Mostowski Collapse schrieb am Donnerstag, 3. November 2022 um 22:44:01 UTC+1:
> Thats the result in FOL. But the result in type theory is different.
> Usually type theory has these two rules:
>
> ∀x:T.Px
> -------------- (∀E)
> Pt
>
> Pt
> -------------- (∃I)
> ∃x:T.Px
>
> You can then easily prove ∀x:T.Px → ∃x:T.Px.
> The problem is a little bit the erasure of t:T judgement.
> Dan Christensen schrieb am Donnerstag, 3. November 2022 um 22:00:22 UTC+1:
> > On Thursday, November 3, 2022 at 3:10:54 PM UTC-4, Mostowski Collapse wrote:
> > > Dan Christensen Donnerstag, 3. November 2022 um 19:47:28 UTC+1:
> > > > Not familiar with that notation. Not that
> > > > interested either. Thanks anyway, Jan Burse.
> > > Come on, make up your minde. Just a few
> > > minutes ago you wrote you want it:
> > >
> > > Dan Christensen Donnerstag, 3. November 2022 um 19:12:38 UTC+1:
> > > > Perhaps you didn't know, but in mathematics,
> > > > universal quantifiers are usually explicitly
> > > > restricted to some specifically name set or other domain.
> > > The notation is very simple:
> > > ∀x:T.Px
> > >
> > > ∀= "universal quantifiers"
> > > T = "your name set or other domain"
> > >
> > So, using more standard notation, if you have ALL(a):[ a in T => P(a)], you can only infer EXIST(a):[a in T & P(a)] if T is non-empty. Look familiar, Jan Burse?
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, November 3, 2022 at 6:02:45 PM UTC-4, Mostowski Collapse wrote:
> Because FOL is already careful enough, nobody needs
> DC Proof.

A system from which you can derive ALL(a):P(a) => EXIST(a):P(a) would be quite useless for learning the methods of mathematical proof. It might a nice little toy system for philosophy or theology classes, but students should be told it may not work in real life.

Dan

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

Why? You still didn't give a reason why it is useless.
FOL has all the scepticism you want built. You say
yourself ALL(a):P(a) is uncommon.

Only your beloved ALL(a):[P(a)=>Q(a)] is used.
Try deriving EXIST(a):[P(a)&Q(a)]. Can you
derive it in FOL?

Dan Christensen schrieb am Donnerstag, 3. November 2022 um 23:40:46 UTC+1:
> On Thursday, November 3, 2022 at 6:02:45 PM UTC-4, Mostowski Collapse wrote:
> > Because FOL is already careful enough, nobody needs
> > DC Proof.
> A system from which you can derive ALL(a):P(a) => EXIST(a):P(a) would be quite useless for learning the methods of mathematical proof. It might a nice little toy system for philosophy or theology classes, but students should be told it may not work in real life.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com