Dans delusional functions and the drinker paradox

[Mostowski Collapse]

Unfortunately Dans function in DC Proof are not what a
mathematician would expect from functions. In set theory
one can express undefinedness of f at x by:

~EXIST(y):(x,y) e f

In free logic one could use instead:

E!f(x)

How should we prove this incarnation of the drinker
paradox with DC Proof. Its impossible! There are two
more variants of the Drinker paradox:

∀x¬P x ∨ ∃xP x
∀xP x ∨ ∃x¬P x
https://arxiv.org/abs/1805.06216

How would DC Proof prove this here:

Given an arbitrary function f that is real value and
not necessarily total, i.e. a function that maps the real
line to the real line that is possibly partial.

Proof the following:

i) Either the function is everywhere undefined or there
is at least a point where the function is defined.

ii) Either the function is everywhere defined or there
is at least a point where the function is undefined.

Can this be directly expressed and proved in DC Proof?

[Dan Christensen]

On Sunday, May 7, 2023 at 4:56:28 PM UTC-4, Mostowski Collapse wrote:
> Unfortunately Dans function in DC Proof are not what a
> mathematician would expect from functions. In set theory
> one can express undefinedness of f at x by:
>
> ~EXIST(y):(x,y) e f
>

Surely not EVERY mathematician. Oh, look, here is something by an actual mathematician. You may have heard of him.

"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
--Terence Tao, "Analysis I," p.49

The last sentence suggests that if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) is indeterminate.

Definition in DC Proof notation:

ALL(x):ALL(y):[Set(x) & Set(y) & ALL(c):[c in a => EXIST(d):[d in b & [P(c,d) & ALL(e):[e in b => [P(c,e) => e=d]]]]]

=> EXIST(f):ALL(c):[c in x => f(c) in y & P(c,f(c))]]

Theorem:

ALL(x):ALL(y):[Set(x) & Set(y) & ALL(c):[c in x => EXIST(d):[d in y & [P(c,d) & ALL(e):[e in y => [P(c,e) => e=d]]]]]

=> EXIST(f):ALL(a):ALL(b):[a in x & b in y => [b=f(a) <=> P(a,b)]]]

> How should we prove this incarnation of the drinker
> paradox with DC Proof. Its impossible!

[snip]

On the contrary, here is a more or less direct translation of Smullyan's predicate logic proof in to DC Proof format:

EXIST(a):U(a) => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]

http://www.dcproof.com/SmullyansDrinkerPrinciple.htm (28 lines)

And here is my own generalized set theoretic proof that is based on the non-existence of the universal set:

For any proposition Q, be it true or false, we have:

ALL(s):[Set(s) => EXIST(x):[x in s => Q]]

Proof: http://www.dcproof.com/STGeneralizedDrinkersThm.htm (9 lines)

Let s = the set of all drinkers D, and Q = ALL(x):[Pub(x) => x in D] where Pub(x) means x is in the pub

Dan

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

[Mostowski Collapse]

If you don't know how to prove it, check out this example of
Terrence Tao how to deal with quantification over partial functions:

> Exercise 10.3.5 from Analysis Vol.1 by Terence Tao.
> Give an example of a subset X⊆R and a function f:X→R
> which is differentiable on X, is such that f′(x)>0
> for all x∈X, but f is not strictly monotone increasing.

A solution to the exercise 10.3.5 by Terrence Tao,
is indeed a partial function:

A function such that f′(x)>0, but not strictly monotone increasing.
https://math.stackexchange.com/a/830397

Maybe just follow Terrence Tao to prove it. We are waiting!

[Dan Christensen]

On Sunday, May 7, 2023 at 4:56:28 PM UTC-4, Mostowski Collapse wrote:

[snip]

> Given an arbitrary function f that is real value and
> not necessarily total, i.e. a function that maps the real
> line to the real line that is possibly partial.
>
> Proof the following:
>
> i) Either the function is everywhere undefined or there
> is at least a point where the function is defined.
>
> ii) Either the function is everywhere defined or there
> is at least a point where the function is undefined.
>
> Can this be directly expressed and proved in DC Proof?

i) The domain of definition of partial function f is either empty or not empty. If it is empty, then f is undefined everywhere. If it is not empty, then it defined for at least one element in that domain. What is there to prove?

ii) Similarly, the domain of definition of partial function is either equal to the superset under consideration, or it isn't. If they are equal (a total function) then f is defined everywhere in that superset. If the two sets are not equal, then there must an element of the superset where f is undefined.

[Mostowski Collapse]

Its the Drinker Paradox, prove it. Its from here:

∀x¬P x ∨ ∃xP x
∀xP x ∨ ∃x¬P x

The Drinker Paradox and its Dual
https://arxiv.org/abs/1805.06216

[Mostowski Collapse]

Mostlikely you need that the real line is non-empty.
Otherwise it doesn't work. On the other hand,
I wouldn't know that the Russell Paradox is needed.

[Mostowski Collapse]

Means your spamming:

> For any proposition Q, be it true or false, we have:
> ALL(s):[Set(s) => EXIST(x):[x in s => Q]]
> Proof: http://www.dcproof.com/STGeneralizedDrinkersThm.htm (9 lines)

Was irrelevant. Right?

[Dan Christensen]

On Monday, May 8, 2023 at 10:08:04 AM UTC-4, Mostowski Collapse wrote:
> Means your spamming:
> > For any proposition Q, be it true or false, we have:
> > ALL(s):[Set(s) => EXIST(x):[x in s => Q]]
> > Proof: http://www.dcproof.com/STGeneralizedDrinkersThm.htm (9 lines)

> Was irrelevant. Right?

Unfortunately for you, Mr. Collapse, readers can judge for themselves. Must be frustrating as hell for you.

Dan

[Julio Di Egidio]

On Monday, 8 May 2023 at 16:04:07 UTC+2, Mostowski Collapse wrote:

> Its the Drinker Paradox, prove it. Its from here:
> ∀x¬P x ∨ ∃xP x
> ∀xP x ∨ ∃x¬P x
> The Drinker Paradox and its Dual
> <https://arxiv.org/abs/1805.06216>

So, where's the proof of that in DC Proof?
I must have missed it...

Julio

[Julio Di Egidio]

Since the classical rules are available:

```
Th. ALL(x):[~P(x)] | EXIST(x):[P(x)]
=> ~ALL(x):[~P(x)] => EXIST(x):[P(x)]
=> EXIST(x):[P(x)] => EXIST(x):[P(x)]
=> [].

Th. ALL(x):[P(x)] | EXIST(x):[~P(x)]
=> ~ALL(x):[P(x)] => EXIST(x):[~P(x)]
=> EXIST(x):[~P(x)] => EXIST(x):[~P(x)]
=> [].
```

That said, give back to Caesar (a hand, not an arm):

```
Th.0: ~EXIST(s):[Set(s) & ALL(a):[a e s]]
by <https://www.dcproof.com/UniversalSet.htm>.

Th.1: ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
by <https://www.dcproof.com/STGeneralizedDrinkersThm.htm>
with Th.0 as an axiom.

Th.2A: ALL(s):[Set(s) => EXIST(x):[x e s => s=s]]
by same proof as for Th.1 (see Arb Or in 6).

Th.3A: from Th.2A
=> ALL(s):[Set(s) => EXIST(x):[~x e s | s=s]]
=> ALL(s):[Set(s) => EXIST(x):[s = s]]
=> ALL(s):[Set(s) => s = s] (* ok! *)

Th.2B: ALL(s):[Set(s) => EXIST(x):[x e s => s <> s)]]
by same proof as for Th.1 (see Arb Or in 6).

Th.3B: from Th.B
=> ALL(s):[Set(s) => EXIST(x):[~x e s | s <> s]]
=> ALL(s):[Set(s) => EXIST(x):[~x e s]]
=> ALL(s):[Set(s) => ~ALL(x):[x e s]] (* Th.0! *)
```

I still have to investigate if the axiom is problematic per se
(just I am confident there is plenty of literature about it),
anyway, no problems with its consequences that I can see.

Julio

[Mostowski Collapse]

You cannot apply this theorem:

28 ALL(s):[Set(s) => EXIST(a):~a e s]
Rem DNeg, 27
http://www.dcproof.com/UniversalSet.htm

Respectively:

ALL(s):[Set(s) => EXIST(a):[a e s => Q]]

Because you don't have, not provable, where f : A ->> B,
is shorthand for EXIST(C):[C ⊆ A & f : C -> B]:

ALL(f):[Set(f) <=> f : R ->> R]

Set(_) doesn't span the functions described in the problem.
Set(_) does span the set universe in general, also called
the "absolute infinite" or "inconsistent multiplicity" by Cantor.

But the segment that is of interest here, the slice of
cake so to speek from the set universe, this slice of
cake is only f : R ->> R. See also:

Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 22:56:28 UTC+2:
> "How would DC Proof prove this here:

> Given an arbitrary function f that is real value and
> not necessarily total, i.e. a function that maps the real
> line to the real line that is possibly partial.
> Proof the following:
> i) Either the function is everywhere undefined or there
> is at least a point where the function is defined.
> ii) Either the function is everywhere defined or there
> is at least a point where the function is undefined."

> https://groups.google.com/g/sci.logic/c/yxICDw_Q7-s/m/iZ3KikwvBwAJ

[Julio Di Egidio]

On Tuesday, 9 May 2023 at 17:53:14 UTC+2, Mostowski Collapse wrote:

> You cannot apply this theorem:

> ALL(s):[Set(s) => EXIST(a):[a e s => Q]]
>

> Because you don't have, where f : A ->> B

> is shorthand for EXIST(C):[C ⊆ A & f : C -> B]:
> ALL(f):[Set(f) <=> f : R ->> R]

But I have not used that substitution, so
what the heck are you even talking about?

Julio

[Mostowski Collapse]

The problem is to prove the Drinker Paradox for some function
space "S" and some binary property "P" of definedness of the individual
functions of this function space and their argument values,

from the real line "R". So the desired theorems are:

i) Either the function is everywhere undefined or there
is at least a point where the function is defined.

ALL(f):[S(f) => ALL(x):[R(x) => ~P(f,x)] v EXIST(x):[R(x) & P(x,f)]]

ii) Either the function is everywhere defined or there
> is at least a point where the function is undefined

ALL(f):[S(f) => ALL(x):[R(x) => P(f,x)] v EXIST(x):[R(x) & ~P(x,f)]]

To apply Dan Christensens "General Drinker Paradox",
You would need to be able to transform the above into
something along:

ALL(s):[Set(s) => EXIST(a):[a e s => Q]]

But there are a lot of obstacles here. Not only uses the
desired theorem "S" instead "Set". Also the EXISTS quantifier
is bounded, it uses "R".

[Mostowski Collapse]

Corr.:Typo, was switching postitions of x,f:

i) ALL(f):[S(f) => ALL(x):[R(x) => ~P(f,x)] v EXIST(x):[R(x) & P(f,x)]]
ii) ALL(f):[S(f) => ALL(x):[R(x) => P(f,x)] v EXIST(x):[R(x) & ~P(f,x)]]

But since the desired theorems are Drinker Paradoxes, i.e.
FOL theorems, without the need for set theory, they are provable
from logic alone. We even don't need to know in detail what "S"

and what "P" are, since we can easily prove them. Interestingly we
also don't need the assumption that the real line "R" is non empty,
because ALL(x):[R(x) => ...] is trivially true if "R" is empty.

So I get:

∀f(Sf → (∀x(Rx → ¬Pfx) ∨ ∃x(Rx ∧ Pfx))) is valid.
https://www.umsu.de/trees/#~6f(Sf~5~6x(Rx~5~3Pfx)~2~7x(Rx~1Pfx))

And its dual:

∀f(Sf → (∀x(Rx → Pfx) ∨ ∃x(Rx ∧ ¬Pfx))) is valid.
https://www.umsu.de/trees/#~6f(Sf~5~6x(Rx~5Pfx)~2~7x(Rx~1~3Pfx))

[Mostowski Collapse]

That we don't need that the real line is non-empty,
lets me think that to arrive at this here:

∀x¬P x ∨ ∃yP y
∀xP x ∨ ∃y¬P y
https://arxiv.org/abs/1805.06216

From this here:

∃y(P y → ∀xP x)
∃y(∃xP x → P y)
https://arxiv.org/abs/1805.06216

Works differently in a logic like FOL that assumes an
non-empty domain and in a logic like DC Proof, that doesn't
necesarily assume a non-empty domain.

In DC Proof one cannot prove:

∀xP x ∨ ∃y¬P y → ∃y(P y → ∀xP x)
∀x¬P x ∨ ∃yP y → ∃y(∃xP x → P y)

The counter example is the empty domain. Right?

[Julio Di Egidio]

On Tuesday, 9 May 2023 at 22:41:03 UTC+2, Mostowski Collapse wrote:

> <stupidities ad nauseam>

It's at least clear at this point that you are either
insane and/or a fucking agent of the enemy.

*Troll alert*

Julio

[Mostowski Collapse]

Ha Ha. Are you angry that:

∀xP x ∨ ∃y¬P y → ∃y(P y → ∀xP x)
∀x¬P x ∨ ∃yP y → ∃y(∃xP x → P y)

Doesn't hold in DC Proof? Try it. You cannot prove
it in DC Proof. You might learn something about
DC Proof and how it tries to avoid inferences

as long as it has not been established that the
domain is non-empty. You can start with something
easier maybe that isn't provable in DC Proof:

/* Not Provable in DC Proof */
ALL(x):P(x) => EXIST(x):P(x)

Whereas it is provable in FOL:

∀xPx → ∃xPx is valid.
https://www.umsu.de/trees/#~6xPx~5~7xPx

How long are you already on sci.logic?

LoL

P.S.: Dan Christensen is very proud that ALL(x):P(x) => EXIST(x):P(x)
isn't provable, and he tries his best to not introduce some axioms
that would nevertheless allow it. For example his Set Theory

axioms do not allow to infer an empty set, unlike other Set Theories,
even Zermelo postualted its existence. The trick in DC Proof is
to have the precondition Set(_) which guards against such mishaps,

you can download the horrors of DC Proof here:

http://www.dcproof.com/

Try it!

[Dan Christensen]

On Tuesday, May 9, 2023 at 5:45:59 PM UTC-4, Mostowski Collapse wrote:

> You can start with something
> easier maybe that isn't provable in DC Proof:
>
> /* Not Provable in DC Proof */
> ALL(x):P(x) => EXIST(x):P(x)
>

Otherwise, it would be quite useless for students learning the basic methods of proof actually used in most textbook proofs where free variables can only be introduced by axiom, premise or existential specification. Deal with it, Mr. Collapse.

If, for some reason, you want to simulate aspects standard FOL in DC Proof, start with an axiom of the form EXIST(a):U(a). Then for every subsequent quantifier, restrict it with that predicate.

[Dan Christensen]

On Monday, May 8, 2023 at 12:13:18 AM UTC-4, Dan Christensen wrote:
> On Sunday, May 7, 2023 at 4:56:28 PM UTC-4, Mostowski Collapse wrote:
> > Unfortunately Dans function in DC Proof are not what a
> > mathematician would expect from functions. In set theory
> > one can express undefinedness of f at x by:
> >
> > ~EXIST(y):(x,y) e f
> >
> Surely not EVERY mathematician. Oh, look, here is something by an actual mathematician. You may have heard of him.
>
> "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y, such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> --Terence Tao, "Analysis I," p.49
>
> The last sentence suggests that if either x ∈ X or y ∈ Y is false, then the truth value of y=f(x) is indeterminate.
>
> Definition in DC Proof notation:
>
> ALL(x):ALL(y):[Set(x) & Set(y) & ALL(c):[c in a => EXIST(d):[d in b & [P(c,d) & ALL(e):[e in b => [P(c,e) => e=d]]]]]
>
> => EXIST(f):ALL(c):[c in x => f(c) in y & P(c,f(c))]]
>
> Theorem:
>
> ALL(x):ALL(y):[Set(x) & Set(y) & ALL(c):[c in x => EXIST(d):[d in y & [P(c,d) & ALL(e):[e in y => [P(c,e) => e=d]]]]]
>
> => EXIST(f):ALL(a):ALL(b):[a in x & b in y => [b=f(a) <=> P(a,b)]]]

Also...

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

=> ALL(g):[Set'(g) & ALL(a):ALL(b):[(a,b) in g <=> a in x & b in y & b=f(a)]

=> ALL(a):[a in x => EXIST(b):[(a,b) in g & ALL(c):[c in y => [(a,c) in g => c=b]]]]]]

[Mostowski Collapse]

Looks rather irrelevant to me. How do you express:

i) Either the function is everywhere undefined or there
is at least a point where the function is defined.

ii) Either the function is everywhere defined or there
is at least a point where the function is undefined.

Dan Christensen schrieb am Freitag, 12. Mai 2023 um 00:08:00 UTC+2:
> Also...
> ALL(a):[a in x => ...

[Dan Christensen]

On Friday, May 12, 2023 at 6:07:04 AM UTC-4, Mostowski Collapse wrote:
> How do you express:
> i) Either the function is everywhere undefined or there
> is at least a point where the function is defined.
>
> ii) Either the function is everywhere defined or there
> is at least a point where the function is undefined.

Let f be a partial function mapping set x to set y, with domain of definition dom.

1. Set(x)
Axiom

2. Set(y)
Axiom

3. Set(dom)
Axiom

4. Set(cod)
Axiom

5. ALL(a):[a in dom => a in x]
Axiom

6. ALL(a):[a in cod => a in y]
Axiom

7. ALL(a):[a in dom => f(a) in cod]
Axiom

We say that f is everywhere undefined if dom is empty.

We say that there is at least one point where the function is defined if dom is not empty.

We say that f is everywhere defined if dom is x=dom (at total function)

We say that there is at least one point where f is undefined if x is a proper superset of dom.

Also see my reply to you 3 days ago on this matter.

[Mostowski Collapse]

The theorem should start:

forall all functions f such that .....

How do you get dom of a function f? Your are still operating
with a lot of informal context that cannot be formalized. You are hopelessly
lost for this simple problem of formalizing also the preamble:

> Given an arbitrary function f that is real value and
> not necessarily total, i.e. a function that maps the real
> line to the real line that is possibly partial.

So f is given. How do you formalize it?

[Dan Christensen]

> The theorem should start:
>
> forall all functions f such that .....
>
> How do you get dom of a function f?

[snip]

"In mathematics, a partial function f from a set X to a set Y is a function from a subset S of X (possibly the whole X itself) to Y. The subset S, that is, the domain [dom] of f viewed as a function, is called the domain of definition or natural domain of f. If S equals X, that is, if f is defined on every element in X, then f is said to be a total function."
https://en.wikipedia.org/wiki/Partial_function

dom=S (the "domain of definition")

> So f is given. How do you formalize it?

See line 7

[Mostowski Collapse]

Here is a proposal to turn a partial function into a predicate:

"Now let us give a more detailed description of the result we have obtained.
We define a dependent family of types Ak representing recursive algorithms of
arity k : N . An algorithm f : A^k defines a (partial) recursive function denoted
[f] and which is represented in Coq as a predicate [f] : N^k → N → Prop"
https://hal.science/hal-02333333/document

Section 3 has again something with sigma types.
"Reifying ∃P into ΣP for P". But the predicate proposal is
a little disappointing. Was expecting something else, that

keeps the function nature of partial functions, and does
it like Terrence Tao, i.e. just use a smaller domain. Maybe
there are other approaches as well around?

In the above approach expressing that a unary function
f : A^1 is defined at a point x amounts to the statement,
needing Section 3.1 "Existential Quantification in Coq":

∃y : [f] x y

[Mostowski Collapse]

Here is a trick to let free logic talk about an explicit domain X and
not the implicit domain of discourse D only. Just require, i.e. case
we want to model f: X -> Y.

~x ∈ X → ~E!f(x)
x ∈ X → E!f(x) & f(x) ∈ Y

So we can use D outside value as a marker for definedness on an
explicitly given domain X. Thats quite different from Dan-O-Matiks
ultra moronic nonsense:

x ∈ X → f(x) ∈ Y

The difference is two clauses and both clauses also talk about
one-place “existence” predicate, ‘E!’ (sometimes written simply as ‘E’).
https://plato.stanford.edu/entries/logic-free/