*** Breaking News ***
The La Plata Astronomical Observatory Report
*** Breaking News ***

Dan-O-Matik suggests that certain points on a hyperbola
are indeterminate. So that we cannot decide whether they
lie or do not lie on the curve.

Is it possibly that Dan-O-Matik has now shed more lights
on WM dark numbers, in that he has ultimately found dark
booleans? N_def from WM would then be N with

dark boolean membership? I guess this would explain
why AP brain fartos ellipses became ovals, when he entered
his kitchen, possibly there is too much dark boolean

in his kitchen. Lets further dig into the problem. This
parametric plot shows one branch of hyperbola:

https://www.wolframalpha.com/input/?i=parametric+plot+%28cosh%28t%29%2C+sinh%28t%29%29

This is the same hyperbola when we rotate it by 45° degree:

https://www.wolframalpha.com/input/?i=parametric+plot+%28%28cosh%28t%29%2Bsinh%28t%29%29%2Fsqrt%282%29%2C+%28cosh%28t%29-sinh%28t%29%29%2Fsqrt%282%29%29

Is there some parameter t and/or some other branch, so that
we possibly reach the point (0,1) on the plane. Or is the point (0,1)
necessarily never reached? Just flyby by the hyperbola?

On Sunday, December 5, 2021 at 2:29:02 PM UTC-5, Mostowski Collapse wrote:
> *** Breaking News ***
> The La Plata Astronomical Observatory Report
> *** Breaking News ***
>
> Dan-O-Matik suggests that certain points on a hyperbola
> are indeterminate. So that we cannot decide whether they
> lie or do not lie on the curve.
>

Poor Jan Burse seems to have left planet Earth behind to join the inhabitants of planet Crank. Very sad indeed. If any readers here are actually interested, they can find my reply just now to his identical posting as sci.logic

Dan

Can you go back and forth 45° rotation with your definition?
You know a 45° rotation is a bijection. And with bijection we
are back to beginner math. If you biject two function graphs

A and B, by the bijective function:

h : A -> B, h bijection

Then you can check x e B , by checking h^-1(x) e A. Does your
claim f(0)≠1 unprovable still hold when you 45° rotate?

Dan Christensen schrieb am Sonntag, 5. Dezember 2021 um 22:24:59 UTC+1:
> On Sunday, December 5, 2021 at 2:29:02 PM UTC-5, Mostowski Collapse wrote:
> > *** Breaking News ***
> > The La Plata Astronomical Observatory Report
> > *** Breaking News ***
> >
> > Dan-O-Matik suggests that certain points on a hyperbola
> > are indeterminate. So that we cannot decide whether they
> > lie or do not lie on the curve.
> >
> Poor Jan Burse seems to have left planet Earth behind to join the inhabitants of planet Crank. Very sad indeed. If any readers here are actually interested, they can find my reply just now to his identical posting as sci.logic
>
> Dan

Dan Christensen wrote:

> Poor Jan Burse seems to have left planet Earth behind to join the
> inhabitants of planet Crank. Very sad indeed. If any readers here are
> actually interested, they can find my reply just now to his identical
> posting as sci.logic

COVID Outbreak On US Cruise Ship Despite Fully Vaxxed Passengers
https://www.zerohedge.com/covid-19/covid-outbreak-us-cruise-ship-despite-
fully-vaxxed-passengers

Despite a 100% vaccination rate on the vessel, there was still an
outbreak of COVID, suggesting that vaccine effectiveness is severely
waning (read induced).

Conclusion:

/* conic section hyperbola */
- Like the 45° diagonal through the origin
never intersects with x^2 - y^2 = 1

/* rectangular hyperbola */
- The vertical through the origin
never intersects with x*y = 1

So ~F(0,1), since (0,1) is a point on the vertical through the origin.

Mostowski Collapse schrieb am Sonntag, 5. Dezember 2021 um 22:37:43 UTC+1:
> Can you go back and forth 45° rotation with your definition?
> You know a 45° rotation is a bijection. And with bijection we
> are back to beginner math. If you biject two function graphs
>
> A and B, by the bijective function:
>
> h : A -> B, h bijection
>
> Then you can check x e B , by checking h^-1(x) e A. Does your
> claim f(0)≠1 unprovable still hold when you 45° rotate?
> Dan Christensen schrieb am Sonntag, 5. Dezember 2021 um 22:24:59 UTC+1:
> > On Sunday, December 5, 2021 at 2:29:02 PM UTC-5, Mostowski Collapse wrote:
> > > *** Breaking News ***
> > > The La Plata Astronomical Observatory Report
> > > *** Breaking News ***
> > >
> > > Dan-O-Matik suggests that certain points on a hyperbola
> > > are indeterminate. So that we cannot decide whether they
> > > lie or do not lie on the curve.
> > >
> > Poor Jan Burse seems to have left planet Earth behind to join the inhabitants of planet Crank. Very sad indeed. If any readers here are actually interested, they can find my reply just now to his identical posting as sci.logic
> >
> > Dan

Interesting link:

404 We couldn't find the content you're looking for.
https://www.zerohedge.com/covid-19/covid-outbreak-us-cruise-ship-despite-fully-vaxxed-passengers

Reese Page schrieb am Sonntag, 5. Dezember 2021 um 22:46:25 UTC+1:
> Dan Christensen wrote:
>
> > Poor Jan Burse seems to have left planet Earth behind to join the
> > inhabitants of planet Crank. Very sad indeed. If any readers here are
> > actually interested, they can find my reply just now to his identical
> > posting as sci.logic
> COVID Outbreak On US Cruise Ship Despite Fully Vaxxed Passengers
> https://www.zerohedge.com/covid-19/covid-outbreak-us-cruise-ship-despite-
> fully-vaxxed-passengers
>
> Despite a 100% vaccination rate on the vessel, there was still an
> outbreak of COVID, suggesting that vaccine effectiveness is severely
> waning (read induced).

Here is a challenge for DC Proof.

My father thinks
Everybody who thinks exists
----------------------------------------------------
My father exists

Can this be proved in DC Proof?

Or maybe this example:

I think
Whatever thinks exists
----------------------------------------------------
I exist

Takle it with the maybe monad. With an
ordinary quantifer, everything works fine:

I encode x exists as ∃y(some(y)=x).
We can then prove:

(Ti ∧ ∀x(Tx → ∃ys(y)=x)) → ∃ys(y)=i is valid.
https://www.umsu.de/trees/#Ti~1~6x%28Tx~5~7y%28s%28y%29=x%29%29~5~7y%28s%28y%29=i%29

Now change the forall quantifier to the
Dan-O-Matik forall quantifier:

(Ti ∧ ∀x(Ts(x) → ∃ys(y)=s(x))) → ∃ys(y)=i is invalid.
Countermodel:
Domain: { 0, 1 }
i: 0
s: { (0,1), (1,1) }
T: { 0 }
https://www.umsu.de/trees/#Ti~1~6x%28Ts%28x%29~5~7y%28s%28y%29=s%28x%29%29%29~5~7y%28s%28y%29=i%29

He He, cool!

Mostowski Collapse schrieb am Dienstag, 11. Januar 2022 um 02:42:55 UTC+1:
> Here is a challenge for DC Proof.
>
> My father thinks
> Everybody who thinks exists
> ----------------------------------------------------
> My father exists
>
> Can this be proved in DC Proof?

On 1/10/2022 8:59 PM, Mostowski Collapse wrote:
> Or maybe this example:
>
> I think
> Whatever thinks exists
> ----------------------------------------------------
> I exist

How about this?
The barber shaves the men who do not shave themselves.
Who shaves the barber?

Thats easy:

Prolog Barber Paradox in JavaScript/Python
https://qiita.com/j4n_bur53/items/59128d9eeb61b86dd133

Here is something more recent, a semantic tableaux rendering:

1. ¬∃x ∀y ((¬s(y,y) ⇒ s(x,y)) ∧ (s(x,y) ⇒ ¬s(y,y)))
2. ¬∀y ((¬s(y,y) ⇒ s(a,y)) ∧ (s(a,y) ⇒ ¬s(y,y))) (F∃ 2)
3. ¬((¬s(a,a) ⇒ s(a,a)) ∧ (s(a,a) ⇒ ¬s(a,a))) (F∀ 3)
4. ¬(s(a,a) ⇒ ¬s(a,a)) (F∧ 4)
5. ¬(¬s(a,a) ⇒ s(a,a)) (F∧ 4)

6. ¬s(a,a) (F⇒ 6)

7. s(a,a) (F⇒ 5)
✓

7. ¬¬s(a,a) (F⇒ 5)
8. s(a,a) (F¬ 8)
✓

6. ¬s(a,a) (F⇒ 6)

7. s(a,a) (F⇒ 5)
✓

7. ¬¬s(a,a) (F⇒ 5)
8. s(a,a) (F¬ 8)
✓

Well to be precise, its a Smullyan tree since the closed
branches end in ✓, and not in ✗.

I didn't try yet with Dan-O-Matik quantifier. Well Dan-O-Matik
quantifier is maybe the wrong name, DC Proof does not
really define:

ALL(x):P(x) :<=> ∀xP(some(x))

Its rather that DC Proof requires something like:

ALL(x):P(f(x)) :<=> ∀x(x e S => P(f(x)))

Michael Moroney schrieb am Dienstag, 11. Januar 2022 um 06:11:52 UTC+1:
> On 1/10/2022 8:59 PM, Mostowski Collapse wrote:
> > Or maybe this example:
> >
> > I think
> > Whatever thinks exists
> > ----------------------------------------------------
> > I exist
> How about this?
> The barber shaves the men who do not shave themselves.
> Who shaves the barber?

With Maybe quantifier, the little brother of Dan-O-Matik quantifier,
the whole thingy is not anymore provable. Because of a name
clash I couldn't use s for some, so was using j for just:

¬∃x∀y((¬sj(y)j(y) → sxj(y)) ∧ (sxj(y) → ¬sj(y)j(y))) is invalid.
Countermodel:
Domain: { 0, 1 }
j: { (0,1), (1,1) }
s: { (0,1) }
https://www.umsu.de/trees/#~3~7x~6y%28%28~3s%28j%28y%29,j%28y%29%29~5s%28x,j%28y%29%29%29~1%28s%28x,j%28y%29%29~5~3s%28j%28y%29,j%28y%29%29%29%29

There are different modellings of Maybe:
- Isabelle/HOL: none / some(_), see also:

datatype 'a option None
| Some (the: 'a)
https://isabelle.in.tum.de/library/HOL/HOL/Option.html

- Haskell: nothing / just(_)

https://hackage.haskell.org/package/base-4.16.0.0/docs/Data-Maybe.html
data Maybe a =
Nothing
| Just a
But Isabelle/HOL and Haskell are multi-sorted logics
with a type system, not directly comparable with FOL.

Mostowski Collapse schrieb am Dienstag, 11. Januar 2022 um 10:33:45 UTC+1:
> Thats easy:
>
> Prolog Barber Paradox in JavaScript/Python
> https://qiita.com/j4n_bur53/items/59128d9eeb61b86dd133
>
> Here is something more recent, a semantic tableaux rendering:
>
> 1. ¬∃x ∀y ((¬s(y,y) ⇒ s(x,y)) ∧ (s(x,y) ⇒ ¬s(y,y)))
> 2. ¬∀y ((¬s(y,y) ⇒ s(a,y)) ∧ (s(a,y) ⇒ ¬s(y,y))) (F∃ 2)
> 3. ¬((¬s(a,a) ⇒ s(a,a)) ∧ (s(a,a) ⇒ ¬s(a,a))) (F∀ 3)
> 4. ¬(s(a,a) ⇒ ¬s(a,a)) (F∧ 4)
> 5. ¬(¬s(a,a) ⇒ s(a,a)) (F∧ 4)
>
> 6. ¬s(a,a) (F⇒ 6)
>
> 7. s(a,a) (F⇒ 5)
> ✓
>
> 7. ¬¬s(a,a) (F⇒ 5)
> 8. s(a,a) (F¬ 8)
> ✓
>
> 6. ¬s(a,a) (F⇒ 6)
>
> 7. s(a,a) (F⇒ 5)
> ✓
>
> 7. ¬¬s(a,a) (F⇒ 5)
> 8. s(a,a) (F¬ 8)
> ✓
>
> Well to be precise, its a Smullyan tree since the closed
> branches end in ✓, and not in ✗.
>
> I didn't try yet with Dan-O-Matik quantifier. Well Dan-O-Matik
> quantifier is maybe the wrong name, DC Proof does not
> really define:
>
> ALL(x):P(x) :<=> ∀xP(some(x))
>
> Its rather that DC Proof requires something like:
>
> ALL(x):P(f(x)) :<=> ∀x(x e S => P(f(x)))
> Michael Moroney schrieb am Dienstag, 11. Januar 2022 um 06:11:52 UTC+1:
> > On 1/10/2022 8:59 PM, Mostowski Collapse wrote:
> > > Or maybe this example:
> > >
> > > I think
> > > Whatever thinks exists
> > > ----------------------------------------------------
> > > I exist
> > How about this?
> > The barber shaves the men who do not shave themselves.
> > Who shaves the barber?

Lets say a quantifier of this definition would be the
little brother of the Dan-O-Matik quantifier:

/* Maybe Quantifier */
ALL(x):P(x) :<=> ∀xP(some(x))

In Isabelle/HOL etc.. the option type is a polymorphic
type. So for each sort a , there some sort option(a).
What would happen if we are in the ZFC universum.
We could model option(V) as follows:

Isabelle/HOL. ZFC
none {}
some(x) {x}

So we would encode option(V) inside V itself. We could
then create a new Peano Apostroph:

/ {y} for ∃!z(x,z) e F & (x,y) e F
F'x = <
\ {} for ~∃!z(x,z) e F

We could also provide an alternative Set(_) predicate.
Alternative to what Dan-O-Matik does. Set would be a
predicate over option(V), and could be defined as follows:

Set(x) <=> ∃y({y}=x)

So Set(_) would be the non-emptyness predicate in
the sense of free-logic.

Hm...

P.S.: We could use this in yet another Peano apostroph:

/ {y} for ∃!z(∃t({t}=x) & (t,z) e F) & ∃t({t}=x) & (t,y) e F
F'x = <
\ {} for ~∃!z(∃t({t}=x) & (t,z) e F)

So the graph would be still F ⊆ V x V, but the Peano apostoph
provides a view one some F' ⊆ V x option(V). Not only
would the Peano apostroph make the codomain option(V),

but it would also make decision in the domain, depending
on whether an argument x is in option(V) \ {} or not. So
we could then prove for the Peano apostoph:

∀x(~Set(x) => ~Set(F'x))

Mostowski Collapse schrieb am Dienstag, 11. Januar 2022 um 10:45:13 UTC+1:
> With Maybe quantifier, the little brother of Dan-O-Matik quantifier,
> the whole thingy is not anymore provable. Because of a name
> clash I couldn't use s for some, so was using j for just:
>
> ¬∃x∀y((¬sj(y)j(y) → sxj(y)) ∧ (sxj(y) → ¬sj(y)j(y))) is invalid.
> Countermodel:
> Domain: { 0, 1 }
> j: { (0,1), (1,1) }
> s: { (0,1) }
> https://www.umsu.de/trees/#~3~7x~6y%28%28~3s%28j%28y%29,j%28y%29%29~5s%28x,j%28y%29%29%29~1%28s%28x,j%28y%29%29~5~3s%28j%28y%29,j%28y%29%29%29%29
>
> There are different modellings of Maybe:
> - Isabelle/HOL: none / some(_), see also:
>
> datatype 'a option =
> None
> | Some (the: 'a)
> https://isabelle.in.tum.de/library/HOL/HOL/Option.html
>
> - Haskell: nothing / just(_)
>
> https://hackage.haskell.org/package/base-4.16.0.0/docs/Data-Maybe.html
> data Maybe a =
> Nothing
> | Just a
> But Isabelle/HOL and Haskell are multi-sorted logics
> with a type system, not directly comparable with FOL.
> Mostowski Collapse schrieb am Dienstag, 11. Januar 2022 um 10:33:45 UTC+1:
> > Thats easy:
> >
> > Prolog Barber Paradox in JavaScript/Python
> > https://qiita.com/j4n_bur53/items/59128d9eeb61b86dd133
> >
> > Here is something more recent, a semantic tableaux rendering:
> >
> > 1. ¬∃x ∀y ((¬s(y,y) ⇒ s(x,y)) ∧ (s(x,y) ⇒ ¬s(y,y)))
> > 2. ¬∀y ((¬s(y,y) ⇒ s(a,y)) ∧ (s(a,y) ⇒ ¬s(y,y))) (F∃ 2)
> > 3. ¬((¬s(a,a) ⇒ s(a,a)) ∧ (s(a,a) ⇒ ¬s(a,a))) (F∀ 3)
> > 4. ¬(s(a,a) ⇒ ¬s(a,a)) (F∧ 4)
> > 5. ¬(¬s(a,a) ⇒ s(a,a)) (F∧ 4)
> >
> > 6. ¬s(a,a) (F⇒ 6)
> >
> > 7. s(a,a) (F⇒ 5)
> > ✓
> >
> > 7. ¬¬s(a,a) (F⇒ 5)
> > 8. s(a,a) (F¬ 8)
> > ✓
> >
> > 6. ¬s(a,a) (F⇒ 6)
> >
> > 7. s(a,a) (F⇒ 5)
> > ✓
> >
> > 7. ¬¬s(a,a) (F⇒ 5)
> > 8. s(a,a) (F¬ 8)
> > ✓
> >
> > Well to be precise, its a Smullyan tree since the closed
> > branches end in ✓, and not in ✗.
> >
> > I didn't try yet with Dan-O-Matik quantifier. Well Dan-O-Matik
> > quantifier is maybe the wrong name, DC Proof does not
> > really define:
> >
> > ALL(x):P(x) :<=> ∀xP(some(x))
> >
> > Its rather that DC Proof requires something like:
> >
> > ALL(x):P(f(x)) :<=> ∀x(x e S => P(f(x)))
> > Michael Moroney schrieb am Dienstag, 11. Januar 2022 um 06:11:52 UTC+1:
> > > On 1/10/2022 8:59 PM, Mostowski Collapse wrote:
> > > > Or maybe this example:
> > > >
> > > > I think
> > > > Whatever thinks exists
> > > > ----------------------------------------------------
> > > > I exist
> > > How about this?
> > > The barber shaves the men who do not shave themselves.
> > > Who shaves the barber?

On 1/11/2022 6:35 AM, Mostowski Collapse wrote:

Who shaves the barber?

For those who aren't familiar with this famous contradiction, if the
barber shaves himself, the barber shaves the barber meaning the barber
doesn't shave himself.

If the barber doesn't shave himself, he is shaved by the barber, so the
barber shaves himself.

Does the code deal with this ad absurdium correctly?

> Lets say a quantifier of this definition would be the
> little brother of the Dan-O-Matik quantifier:
>
> /* Maybe Quantifier */
> ALL(x):P(x) :<=> ∀xP(some(x))
>
> In Isabelle/HOL etc.. the option type is a polymorphic
> type. So for each sort a , there some sort option(a).
> What would happen if we are in the ZFC universum.
> We could model option(V) as follows:
>
> Isabelle/HOL. ZFC
> none {}
> some(x) {x}
>
> So we would encode option(V) inside V itself. We could
> then create a new Peano Apostroph:
>
> / {y} for ∃!z(x,z) e F & (x,y) e F
> F'x = <
> \ {} for ~∃!z(x,z) e F
>
> We could also provide an alternative Set(_) predicate.
> Alternative to what Dan-O-Matik does. Set would be a
> predicate over option(V), and could be defined as follows:
>
> Set(x) <=> ∃y({y}=x)
>
> So Set(_) would be the non-emptyness predicate in
> the sense of free-logic.
>
> Hm...
>
> P.S.: We could use this in yet another Peano apostroph:
>
> / {y} for ∃!z(∃t({t}=x) & (t,z) e F) & ∃t({t}=x) & (t,y) e F
> F'x = <
> \ {} for ~∃!z(∃t({t}=x) & (t,z) e F)
>
> So the graph would be still F ⊆ V x V, but the Peano apostoph
> provides a view one some F' ⊆ V x option(V). Not only
> would the Peano apostroph make the codomain option(V),
>
> but it would also make decision in the domain, depending
> on whether an argument x is in option(V) \ {} or not. So
> we could then prove for the Peano apostoph:
>
> ∀x(~Set(x) => ~Set(F'x))
>
> Mostowski Collapse schrieb am Dienstag, 11. Januar 2022 um 10:45:13 UTC+1:
>> With Maybe quantifier, the little brother of Dan-O-Matik quantifier,
>> the whole thingy is not anymore provable. Because of a name
>> clash I couldn't use s for some, so was using j for just:
>>
>> ¬∃x∀y((¬sj(y)j(y) → sxj(y)) ∧ (sxj(y) → ¬sj(y)j(y))) is invalid.
>> Countermodel:
>> Domain: { 0, 1 }
>> j: { (0,1), (1,1) }
>> s: { (0,1) }
>> https://www.umsu.de/trees/#~3~7x~6y%28%28~3s%28j%28y%29,j%28y%29%29~5s%28x,j%28y%29%29%29~1%28s%28x,j%28y%29%29~5~3s%28j%28y%29,j%28y%29%29%29%29
>>
>> There are different modellings of Maybe:
>> - Isabelle/HOL: none / some(_), see also:
>>
>> datatype 'a option =
>> None
>> | Some (the: 'a)
>> https://isabelle.in.tum.de/library/HOL/HOL/Option.html
>>
>> - Haskell: nothing / just(_)
>>
>> https://hackage.haskell.org/package/base-4.16.0.0/docs/Data-Maybe.html
>> data Maybe a =
>> Nothing
>> | Just a
>> But Isabelle/HOL and Haskell are multi-sorted logics
>> with a type system, not directly comparable with FOL.
>> Mostowski Collapse schrieb am Dienstag, 11. Januar 2022 um 10:33:45 UTC+1:
>>> Thats easy:
>>>
>>> Prolog Barber Paradox in JavaScript/Python
>>> https://qiita.com/j4n_bur53/items/59128d9eeb61b86dd133
>>>
>>> Here is something more recent, a semantic tableaux rendering:
>>>
>>> 1. ¬∃x ∀y ((¬s(y,y) ⇒ s(x,y)) ∧ (s(x,y) ⇒ ¬s(y,y)))
>>> 2. ¬∀y ((¬s(y,y) ⇒ s(a,y)) ∧ (s(a,y) ⇒ ¬s(y,y))) (F∃ 2)
>>> 3. ¬((¬s(a,a) ⇒ s(a,a)) ∧ (s(a,a) ⇒ ¬s(a,a))) (F∀ 3)
>>> 4. ¬(s(a,a) ⇒ ¬s(a,a)) (F∧ 4)
>>> 5. ¬(¬s(a,a) ⇒ s(a,a)) (F∧ 4)
>>>
>>> 6. ¬s(a,a) (F⇒ 6)
>>>
>>> 7. s(a,a) (F⇒ 5)
>>> ✓
>>>
>>> 7. ¬¬s(a,a) (F⇒ 5)
>>> 8. s(a,a) (F¬ 8)
>>> ✓
>>>
>>> 6. ¬s(a,a) (F⇒ 6)
>>>
>>> 7. s(a,a) (F⇒ 5)
>>> ✓
>>>
>>> 7. ¬¬s(a,a) (F⇒ 5)
>>> 8. s(a,a) (F¬ 8)
>>> ✓
>>>
>>> Well to be precise, its a Smullyan tree since the closed
>>> branches end in ✓, and not in ✗.
>>>
>>> I didn't try yet with Dan-O-Matik quantifier. Well Dan-O-Matik
>>> quantifier is maybe the wrong name, DC Proof does not
>>> really define:
>>>
>>> ALL(x):P(x) :<=> ∀xP(some(x))
>>>
>>> Its rather that DC Proof requires something like:
>>>
>>> ALL(x):P(f(x)) :<=> ∀x(x e S => P(f(x)))
>>> Michael Moroney schrieb am Dienstag, 11. Januar 2022 um 06:11:52 UTC+1:
>>>> On 1/10/2022 8:59 PM, Mostowski Collapse wrote:
>>>>> Or maybe this example:
>>>>>
>>>>> I think
>>>>> Whatever thinks exists
>>>>> ----------------------------------------------------
>>>>> I exist
>>>> How about this?
>>>> The barber shaves the men who do not shave themselves.
>>>> Who shaves the barber?

On Tuesday, January 11, 2022 at 12:11:52 AM UTC-5, Michael Moroney wrote:
> On 1/10/2022 8:59 PM, Mostowski Collapse wrote:
> > Or maybe this example:
> >
> > I think
> > Whatever thinks exists
> > ----------------------------------------------------
> > I exist
> How about this?
> The barber shaves the men who do not shave themselves.
> Who shaves the barber?

See my blog posting on various versions of the Barber Paradox at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/

There, I resolve the most advanced version as follows:

ALL(v):ALL(barber):ALL(m):[Set(v)
& barber in v
& Set(m)
& ALL(a):[a in m => a in v]
=> [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
& ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
<=> ~barber in m]]

where

v = the set of all villagers
m = the set of all men in the village
s = the shaving relation on v, a set of ordered pairs, (x,y) e s means x shaves y

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, January 12, 2022 at 1:17:15 AM UTC-5, Dan Christensen wrote:
> On Tuesday, January 11, 2022 at 12:11:52 AM UTC-5, Michael Moroney wrote:
> > On 1/10/2022 8:59 PM, Mostowski Collapse wrote:
> > > Or maybe this example:
> > >
> > > I think
> > > Whatever thinks exists
> > > ----------------------------------------------------
> > > I exist
> > How about this?
> > The barber shaves the men who do not shave themselves.
> > Who shaves the barber?
> See my blog posting on various versions of the Barber Paradox at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/
>
> There, I resolve the most advanced version as follows:
>
> ALL(v):ALL(barber):ALL(m):[Set(v)
> & barber in v
> & Set(m)
> & ALL(a):[a in m => a in v]
> => [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
> & ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
> <=> ~barber in m]]
>
> where
>
> v = the set of all villagers
> m = the set of all men in the village
> s = the shaving relation on v, a set of ordered pairs, (x,y) e s means x shaves y
>

In words, a barber living in a village can shave those and only those men living there who do not shave themselves if and only if that barber is not a man.

> 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, January 12, 2022 at 11:22:59 AM UTC-5, Dan Christensen wrote:
> On Wednesday, January 12, 2022 at 1:17:15 AM UTC-5, Dan Christensen wrote:
> > On Tuesday, January 11, 2022 at 12:11:52 AM UTC-5, Michael Moroney wrote:
> > > On 1/10/2022 8:59 PM, Mostowski Collapse wrote:
> > > > Or maybe this example:
> > > >
> > > > I think
> > > > Whatever thinks exists
> > > > ----------------------------------------------------
> > > > I exist
> > > How about this?
> > > The barber shaves the men who do not shave themselves.
> > > Who shaves the barber?
> > See my blog posting on various versions of the Barber Paradox at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/
> >
> > There, I resolve the most advanced version as follows:
> >
> > ALL(v):ALL(barber):ALL(m):[Set(v)
> > & barber in v
> > & Set(m)
> > & ALL(a):[a in m => a in v]
> > => [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
> > & ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
> > <=> ~barber in m]]
> >
> > where
> >
> > v = the set of all villagers
> > m = the set of all men in the village
> > s = the shaving relation on v, a set of ordered pairs, (x,y) e s means x shaves y
> >
> In words, a barber living in a village can shave those and only those men living there who do not shave themselves if and only if that barber is not a man.

Formal proof (100 lines): http://www.dcproof.com/BP12.htm

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

"If the barber doesn't shave himself, he is shaved by
the barber, so the barber shaves himself."

Just use a constant b for the barber, because,
this here is provable, I listed a proof already:

|- ¬∃x ∀y ((¬s(y,y) ⇒ s(x,y)) ∧ (s(x,y) ⇒ ¬s(y,y)))

You can prove anything from this here,
via ex falso quodlibet:

∀y ((¬s(y,y) ⇒ s(b,y)) ∧ (s(b,y) ⇒ ¬s(y,y)))

For example:

∀y((¬syy → sby) ∧ (sby → ¬syy)) entails sbb.
https://www.umsu.de/trees/#~6y%28%28~3s%28y,y%29~5s%28b,y%29%29~1%28s%28b,y%29~5~3s%28y,y%29%29%29|=s%28b,b%29

My recent prover agrees, but I don't have yet
E-mail compatible output. But you can try yourself
and view some MathJax generated Smullyan tree:

?- prove0((![Y='y']: ((~ s(Y,Y) => s(b,Y)) & (s(b,Y) => ~ s(Y,Y))) => s(b,b)), 2), !.
http://www.xlog.ch/izytab/moblet/en/docs/18_live/38_bin2022/paste11/package..html

I am working on easier input currently, and
also an E-mail compatible output for Smullyan
trees, but this is not yet online.

Please be patient. BTW becaus of ex falso, you
cannot only prove sbb, you can also prove ~sbb:

?- prove0((![Y='y']: ((~ s(Y,Y) => s(b,Y)) & (s(b,Y) => ~ s(Y,Y))) => ~s(b,b)), 2), !.
http://www.xlog.ch/izytab/moblet/en/docs/18_live/38_bin2022/paste11/package..html

LoL

Michael Moroney schrieb am Dienstag, 11. Januar 2022 um 17:04:06 UTC+1:
> On 1/11/2022 6:35 AM, Mostowski Collapse wrote:
>
> Who shaves the barber?
>
> For those who aren't familiar with this famous contradiction, if the
> barber shaves himself, the barber shaves the barber meaning the barber
> doesn't shave himself.
>
> If the barber doesn't shave himself, he is shaved by the barber, so the
> barber shaves himself.
>
> Does the code deal with this ad absurdium correctly?

When you only use one half of the barber requirement,
the first half, then its not so easy. Good guy Wolfgang
Schwartz can provide counter models:

This one works:

∀y(¬syy → sby) entails sbb.
https://www.umsu.de/trees/#~6y%28~3syy~5sby%29|=s%28b,b%29

But this one doesn't work:

∀y(¬syy → sby) does not entail ¬sbb.
Countermodel:
Domain: { 0 }
b: 0
s: { (0,0) }
https://www.umsu.de/trees/#~6y%28~3syy~5sby%29|=~3s%28b,b%29

Mostowski Collapse schrieb am Mittwoch, 12. Januar 2022 um 22:59:07 UTC+1:
> "If the barber doesn't shave himself, he is shaved by
> the barber, so the barber shaves himself."
> Just use a constant b for the barber, because,
> this here is provable, I listed a proof already:
>
> |- ¬∃x ∀y ((¬s(y,y) ⇒ s(x,y)) ∧ (s(x,y) ⇒ ¬s(y,y)))
>
> You can prove anything from this here,
> via ex falso quodlibet:
>
> ∀y ((¬s(y,y) ⇒ s(b,y)) ∧ (s(b,y) ⇒ ¬s(y,y)))
>
> For example:
>
> ∀y((¬syy → sby) ∧ (sby → ¬syy)) entails sbb.
> https://www.umsu.de/trees/#~6y%28%28~3s%28y,y%29~5s%28b,y%29%29~1%28s%28b,y%29~5~3s%28y,y%29%29%29|=s%28b,b%29
>
> My recent prover agrees, but I don't have yet
> E-mail compatible output. But you can try yourself
> and view some MathJax generated Smullyan tree:
>
> ?- prove0((![Y='y']: ((~ s(Y,Y) => s(b,Y)) & (s(b,Y) => ~ s(Y,Y))) => s(b,b)), 2), !.
> http://www.xlog.ch/izytab/moblet/en/docs/18_live/38_bin2022/paste11/package.html
>
> I am working on easier input currently, and
> also an E-mail compatible output for Smullyan
> trees, but this is not yet online.
>
> Please be patient. BTW becaus of ex falso, you
> cannot only prove sbb, you can also prove ~sbb:
>
> ?- prove0((![Y='y']: ((~ s(Y,Y) => s(b,Y)) & (s(b,Y) => ~ s(Y,Y))) => ~s(b,b)), 2), !.
> http://www.xlog.ch/izytab/moblet/en/docs/18_live/38_bin2022/paste11/package.html
>
> LoL
> Michael Moroney schrieb am Dienstag, 11. Januar 2022 um 17:04:06 UTC+1:
> > On 1/11/2022 6:35 AM, Mostowski Collapse wrote:
> >
> > Who shaves the barber?
> >
> > For those who aren't familiar with this famous contradiction, if the
> > barber shaves himself, the barber shaves the barber meaning the barber
> > doesn't shave himself.
> >
> > If the barber doesn't shave himself, he is shaved by the barber, so the
> > barber shaves himself.
> >
> > Does the code deal with this ad absurdium correctly?

So you didn't do regression testing of your changes?
DC Proof is not a reliable to tool. It nowhere automatically
records in the generated HTML files the version of DC Proof.

For example in the link
http://www.dcproof.com/ProofByInduction.html
I find:

Apply definition of n for f(x)

30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
U Spec, 11

What is the f(x) e S before line 30? I suspect it is not
an U Spec from dcproof5.exe with two reference
lines, it has only one reference line 11.

LoL

Alternatively instead of only posting HTML, you could
also post additionally a link to the machine readable
proof, so that one can load it into DC Proof,

and verify that then proof goes through. All tools
such as Isabelle/HOL, Coq, etc.. have such a format,
and publishing a proof means publishing this

format and not some pretty printing. Although
in Isabelle/HOL, Coq, etc.. the format is very simple.
Mostlikely ASCII, maybe recently Unicode,

but not binary. The pretty printing is then often
LaTex or HTML. You only post pretty printing, nobody
can verify, with a press of a button, what you did.

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 08:47:18 UTC+1:
> So you didn't do regression testing of your changes?
> DC Proof is not a reliable to tool. It nowhere automatically
> records in the generated HTML files the version of DC Proof.
>
> For example in the link
> http://www.dcproof.com/ProofByInduction.html
> I find:
>
> Apply definition of n for f(x)
>
> 30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
> & s1 e b
> & ALL(c):[c e b & c e s => f(c) e b]
> => f(x) e b]
> U Spec, 11
>
> What is the f(x) e S before line 30? I suspect it is not
> an U Spec from dcproof5.exe with two reference
> lines, it has only one reference line 11.
>
> LoL

On Thursday, January 13, 2022 at 2:47:18 AM UTC-5, Mostowski Collapse wrote:
> So you didn't do regression testing of your changes?
> DC Proof is not a reliable to tool. It nowhere automatically
> records in the generated HTML files the version of DC Proof.
>
> For example in the link
> http://www.dcproof.com/ProofByInduction.html
> I find:
>
> Apply definition of n for f(x)
>
> 30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
> & s1 e b
> & ALL(c):[c e b & c e s => f(c) e b]
> => f(x) e b]
> U Spec, 11
>
> What is the f(x) e S before line 30?

On line 1, f is defined to be a function on s. On line 28, we see that x in s. So, f(x) in s as on line 35.

In none of the proofs I have posted here or at my blog do I assume that f(x) would be anything other than an element of a set, so the minor change to my Function Axiom presents no problem for my previous work. It just prevents a few wonky results. (Hee, hee!) And it makes the axiom a little easier to explain without overloading the function name. Non-programmers probably wouldn't get that f could be different but related things depending on the context.

Dan

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

But line 35 is after line 30. So you cannot use U Spec, 11.
It might have worked in dcproof2.exe. But I guess it doesn't
work in dcproof5.exe anymore.

Should I show a screenshot of the error when I try to
replay the alleged proof?

Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 16:40:39 UTC+1:
> On Thursday, January 13, 2022 at 2:47:18 AM UTC-5, Mostowski Collapse wrote:
> > So you didn't do regression testing of your changes?
> > DC Proof is not a reliable to tool. It nowhere automatically
> > records in the generated HTML files the version of DC Proof.
> >
> > For example in the link
> > http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html
> > I find:
> >
> > Apply definition of n for f(x)
> >
> > 30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
> > & s1 e b
> > & ALL(c):[c e b & c e s => f(c) e b]
> > => f(x) e b]
> > U Spec, 11
> >
> > What is the f(x) e S before line 30?
> On line 1, f is defined to be a function on s. On line 28, we see that x in s. So, f(x) in s as on line 35.
>
> In none of the proofs I have posted here or at my blog do I assume that f(x) would be anything other than an element of a set, so the minor change to my Function Axiom presents no problem for my previous work. It just prevents a few wonky results. (Hee, hee!) And it makes the axiom a little easier to explain without overloading the function name. Non-programmers probably wouldn't get that f could be different but related things depending on the context.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Your Dedekind -> Peano proof doesn't work anymore.
Its the same problem like in this proof, where
this step doesn't work anymore:

> This is the proof that worked in dcproof2.exe, but
> does not work anymore in dcproof5.exe:
> [...]
> 8 ~Field(constr(a))
> U Spec, 6, 7
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ

Because there is no constr(a) e S.

The new error message is:
'constr(a)' must be an element of a set

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 16:46:21 UTC+1:
> But line 35 is after line 30. So you cannot use U Spec, 11.
> It might have worked in dcproof2.exe. But I guess it doesn't
> work in dcproof5.exe anymore.
>
> Should I show a screenshot of the error when I try to
> replay the alleged proof?
> Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 16:40:39 UTC+1:
> > On Thursday, January 13, 2022 at 2:47:18 AM UTC-5, Mostowski Collapse wrote:
> > > So you didn't do regression testing of your changes?
> > > DC Proof is not a reliable to tool. It nowhere automatically
> > > records in the generated HTML files the version of DC Proof.
> > >
> > > For example in the link
> > > http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html
> > > I find:
> > >
> > > Apply definition of n for f(x)
> > >
> > > 30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
> > > & s1 e b
> > > & ALL(c):[c e b & c e s => f(c) e b]
> > > => f(x) e b]
> > > U Spec, 11
> > >
> > > What is the f(x) e S before line 30?
> > On line 1, f is defined to be a function on s. On line 28, we see that x in s. So, f(x) in s as on line 35.
> >
> > In none of the proofs I have posted here or at my blog do I assume that f(x) would be anything other than an element of a set, so the minor change to my Function Axiom presents no problem for my previous work. It just prevents a few wonky results. (Hee, hee!) And it makes the axiom a little easier to explain without overloading the function name. Non-programmers probably wouldn't get that f could be different but related things depending on the context.
> > 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, January 13, 2022 at 10:46:21 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 16:40:39 UTC+1:
> > On Thursday, January 13, 2022 at 2:47:18 AM UTC-5, Mostowski Collapse wrote:
> > > So you didn't do regression testing of your changes?
> > > DC Proof is not a reliable to tool. It nowhere automatically
> > > records in the generated HTML files the version of DC Proof.
> > >
> > > For example in the link
> > > http://www.dcproof.com/ProofByInduction.html
> > > I find:
> > >
> > > Apply definition of n for f(x)
> > >
> > > 30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
> > > & s1 e b
> > > & ALL(c):[c e b & c e s => f(c) e b]
> > > => f(x) e b]
> > > U Spec, 11
> > >
> > > What is the f(x) e S before line 30?
> > On line 1, f is defined to be a function on s. On line 28, we see that x in s. So, f(x) in s as on line 35.
> >
> > In none of the proofs I have posted here or at my blog do I assume that f(x) would be anything other than an element of a set, so the minor change to my Function Axiom presents no problem for my previous work. It just prevents a few wonky results. (Hee, hee!) And it makes the axiom a little easier to explain without overloading the function name. Non-programmers probably wouldn't get that f could be different but related things depending on the context.

> But line 35 is after line 30. So you cannot use U Spec, 11.

Lines 34 and 35 could easily be inserted BEFORE line 35 as would be required with my recent changes. Not a big deal. Like I said, in none of the proofs I have posted here or at my blog do I assume that f(x), for example, would be anything other than an element of a set

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, January 13, 2022 at 10:46:21 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 16:40:39 UTC+1:
> > On Thursday, January 13, 2022 at 2:47:18 AM UTC-5, Mostowski Collapse wrote:
> > > So you didn't do regression testing of your changes?
> > > DC Proof is not a reliable to tool. It nowhere automatically
> > > records in the generated HTML files the version of DC Proof.
> > >
> > > For example in the link
> > > http://www.dcproof.com/ProofByInduction.html
> > > I find:
> > >
> > > Apply definition of n for f(x)
> > >
> > > 30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
> > > & s1 e b
> > > & ALL(c):[c e b & c e s => f(c) e b]
> > > => f(x) e b]
> > > U Spec, 11
> > >
> > > What is the f(x) e S before line 30?
> > On line 1, f is defined to be a function on s. On line 28, we see that x in s. So, f(x) in s as on line 35.
> >
> > In none of the proofs I have posted here or at my blog do I assume that f(x) would be anything other than an element of a set, so the minor change to my Function Axiom presents no problem for my previous work. It just prevents a few wonky results. (Hee, hee!) And it makes the axiom a little easier to explain without overloading the function name. Non-programmers probably wouldn't get that f could be different but related things depending on the context.

> But line 35 is after line 30. So you cannot use U Spec, 11.

Lines 34 and 35 could easily be inserted BEFORE line 30 as would be required with my recent changes. Not a big deal. Like I said, in none of the proofs I have posted here or at my blog do I assume that f(x), for example, would be anything other than an element of a set

Dan

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