There is no such Barber!

[Julio Di Egidio]

I am learning Coq (which is based on constructive logic), so
I thought let's look at the Barber's Paradox, i.e. let's see if I can
get a "contradiction" and how... Now this is a question about
(constructive) logic, not Coq:

- Proposition:
There is a barber who lives on an island.
The barber shaves all and only those men who
live on the island who do not shave themselves.
- Question:
Does the barber shave himself?

I have managed the following:

(* [shaves] is any [T -> T -> Prop]. *)
Parameter shaves : forall {T : Set}, T -> T -> Prop.

(* [exists_barber] is there is a barber so and so. *)
Definition exists_barber {T : Set} :=
exists b : T,
forall x : T,
shaves b x <-> ~ (shaves x x).

(* [exists_barber] is false! *)
Theorem barber_paradox {T : Set} :
~ @exists_barber T.
(* Easily proven. Hint: case analysis on
either the barber shaves himself or he doesn't. *)

And then I am not sure what I have got. Either my formalization
misses the point somewhere, or I have proven that [exists_barber]
is identically false (in the constructive sense that the opposite is
provable)! In particular, since by [exfalso] (also constructively)
anything follows, the barber shave himself AND he does not!!

TL;DR: I get [exists_barber] is false, not somehow "contradictory".

Comments/suggestions?

Julio

Some refs I have used:
<https://en.wikipedia.org/wiki/Barber_paradox>
<https://www.umsl.edu/~siegelj/SetTheoryandTopology/TheBarber.html>

[Julio Di Egidio]

On Sunday, 5 March 2023 at 12:03:51 UTC+1, Julio Di Egidio wrote:
<snip>

> Does the barber shave himself?
>
> I have managed the following:
>
> (* [shaves] is any [T -> T -> Prop]. *)
> Parameter shaves : forall {T : Set}, T -> T -> Prop.
>
> (* [exists_barber] is there is a barber so and so. *)
> Definition exists_barber {T : Set} :=
> exists b : T,
> forall x : T,
> shaves b x <-> ~ (shaves x x).
>
> (* [exists_barber] is false! *)
> Theorem barber_paradox {T : Set} :
> ~ @exists_barber T.
> (* Easily proven. Hint: case analysis on
> either the barber shaves himself or he doesn't. *)

<snip>

These also are easily provable:

(* [the_barber b] is a barber so and so. *)
Definition the_barber (b : T) : Prop :=
forall x : T,
shaves b x <-> ~ shaves x x.

(* [the_barber_does_shave_himself]. *)
Lemma the_barber_does_shave_himself :
forall x : T,
the_barber x ->
shaves x x.
(* Proof here *) Admitted.

(* [the_barber_does_not_shave_himself]. *)
Lemma the_barber_does_not_shave_himself :
forall x : T,
the_barber x ->
~ shaves x x.
(* Proof here *) Admitted.

TL;DR: I get that there is no such barber!

More precisely:

Nobody is *that* barber, i.e. there can be no such barber,
and that *is* the solution of the "paradox".

Contrast that with how WP puts it here (*):
"Nobody is a barber, so there is no solution to the paradox.[2][3]"
but then both [2] and [3], especially [3], say exactly what I have
concluded above...
(*) <https://en.wikipedia.org/wiki/Barber_paradox#In_first-order_logic>

Case closed as far as I am concerned.

Julio

[Ben Bacarisse]

I think you have it exactly right. The existence of such a person
leads, logically, to a contradiction so, as you have found, the
statement of existence is false. It's only a paradox because the
phrasing in English makes the existence of such a person sound
reasonable.

You could define exists_mystery_n as "exists natural number n such that
n > 7 and n < 3" and Coq would prove to you that that clause is false.
It's only not a paradox, because the contradiction is too obvious --
it's simply an unsatisfyable existence claim.

There are other formulations where the existence can't be avoided, and
then the contradiction will dominate. For example, in SNOBOL you can
write a pattern (just a string) that matches all patterns that don't
match themselves. Since you've written it as actual executable code, it
exists (in some sense at least) but when you try to match it against
itself, the SNOBOL engine fails to give an answer, because there can't
really be any such pattern. Any attempt to write it just leads to code
that is undefined as run time.

--
Ben.

[Julio Di Egidio]

On Sunday, 5 March 2023 at 14:04:39 UTC+1, Ben Bacarisse wrote:

> I think you have it exactly right. The existence of such a person
> leads, logically, to a contradiction so, as you have found, the
> statement of existence is false.

You miss the fine print and the whole point as usual. As
I have made more precise in a later post, I have actually
found no "contradiction", just a false statement.

Indeed, while it is easy to prove the following:

Theorem no_such_barber : forall x : T,
~ the_barber x.

we still cannot prove any kind of contradiction proper:

Theorem the_barber_iff_not_the_barber : forall x : T,
the_barber x <-> ~ the_barber x.
Proof.
(* Forward case is easy, reverse case we cannot
prove since [forall] does not imply [exists].
Or, maybe not with these definitions, or maybe
not without classical logic... *)
Abort.

The following is provable, but of course just trivial.

Theorem the_barber_iff_not_the_barber : forall x : T,
the_barber x ->
the_barber x <-> ~ the_barber x.
Proof.
(* This is trivial since ex falso quod libet. *)
intros x B.
apply no_such_barber in B.
inversion B.
Qed.

> It's only a paradox because the
> phrasing in English makes the existence of such a person sound
> reasonable.

Your phrasing is completely upside down. Indeed, if one doesn't use Logic
(if one cannot *reason*), everything is "reasonable", but I for one can and
do parse that hypothesis as self-contradictory immediately and just fine:
the question was/is how to formalize that understanding, and the fact
that a self-contradictory premise translates to a false assumption to me
remains rather puzzling...

Julio

[Julio Di Egidio]

On Sunday, 5 March 2023 at 16:38:34 UTC+1, Julio Di Egidio wrote:
> On Sunday, 5 March 2023 at 14:04:39 UTC+1, Ben Bacarisse wrote:
>
> > I think you have it exactly right. The existence of such a person
> > leads, logically, to a contradiction so, as you have found, the
> > statement of existence is false.
>
> You miss the fine print and the whole point as usual. As
> I have made more precise in a later post, I have actually
> found no "contradiction", just a false statement.

Or, if by "logically" you mean by reasoning (by Logic), then it's
a clear explanation of that "so" that I am not finding. Indeed,
"self-contradictory" is just not the same as "false", which in turn
means that the opposite is true and even provably so in this case.
Two altogether different beasts, aren't they?

Again: the fact that a self-contradictory premise translates to a
false assumption to me remains rather puzzling... as in, there is
some kind of information loss there: and it's not the first time I
raise this issue in this group, just I still cannot find any clear
"resolution", to the relationship of mathematical logic to Logic...

Julio

[olcott]

So Russell's barber was only a liar all along.
ZFC fixed this at the set theory level.


--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[Julio Di Egidio]

On Sunday, 5 March 2023 at 17:15:00 UTC+1, olcott wrote:
> On 3/5/2023 7:04 AM, Ben Bacarisse wrote:

<snip>

> > There are other formulations where the existence can't be avoided, and
> > then the contradiction will dominate. For example, in SNOBOL you can
> > write a pattern (just a string) that matches all patterns that don't
> > match themselves. Since you've written it as actual executable code, it
> > exists (in some sense at least) but when you try to match it against
> > itself, the SNOBOL engine fails to give an answer, because there can't
> > really be any such pattern. Any attempt to write it just leads to code
> > that is undefined as run time.

"Undefined" as in non-terminating. I am thinking
whether this captures "self-contradiction" better.

> So Russell's barber was only a liar all along.

Ex falso quodlibet...

Julio

[olcott]

*In correct reasoning*
A proves B means that B is a semantically necessary consequence of A.
If the Moon is made from green cheese then the Moon is made from cheese.

From FALSE nothing can be proved.
From a contradiction FALSE can be proved.

[Ross Finlayson]

No, no, it's "nihilum", "ex falso nihilum".

Truth is total, ..., logic is modal.

[Julio Di Egidio]

> No, no, it's "nihilum", "ex falso nihilum".

Nope, should be ex contradictione nihilum, that is a
self-contradictory statement is no statement all, which is
the essence of Logic, and of course I was just mocking
Russell, and that false is the same as self-contradictory,
and the whole Aristotelian disaster that we are with it.

> Truth is total, ..., logic is modal.

Logic is total -> truth is modal -> you are liars.

Julio

[Julio Di Egidio]

Ex Contradictione Non Sequitur Quodlibet
<https://sqig.math.ist.utl.pt/pub/MarcosJ/01-CM-ECNSQL.pdf>
for a survey and investigation of the mathematical logic(s).
People just do not anymore know what Logic proper is, or
philosophy proper, as opposed to the fraud of it and everything.

Julio

[Mostowski Collapse]

Yes, Julio is right:

This is nonsense:
olcot: From FALSE nothing can be proved.

This is nonsense:
ross: No, no, it's "nihilum", "ex falso nihilum".

This is correct, at least in classical logic:
Julio, from the paper:
(1) Contradictory with respect to ~ (or simply contradictory)
If there exists a formula A such that Γ |- A and Γ |- ~A .
(2) Trivial
If for every B, we have Γ |- B.
In classical logic (1) and (2) are equivalent.

Proof:
(1) => (2):
Γ |- A Γ |- ~A
------------------------ (&Intro) ------------------------- (Tauto)
Γ |- A & ~A A & ~A -> B
---------------------------------------------------------------- (->Elim)
Γ |- B

See also:

A B ((A ∧ ¬A) → B)
F F T
F T T
T F T
T T T
https://web.stanford.edu/class/cs103/tools/truth-table-tool/

(2) => (1):
Trivial just specialize B to A or ~A.
Q.E.D.

Now use Γ = {⊥}.

Proof:
----------------- (Ax) ------------------------- (Tauto)
⊥ |- ⊥ ⊥ → B
---------------------------------------------- (->Elim)
⊥ |- B

See also:
B (⊥ → B)
F T
T T
https://web.stanford.edu/class/cs103/tools/truth-table-tool/
Q.E.D.

[Mostowski Collapse]

Dan Christensen might object, that (2) => (1)
doesn't hold, since the domain might be empty,
i.e. there are no formulas.

LoL

[Julio Di Egidio]

On Tuesday, 7 March 2023 at 16:15:35 UTC+1,

Mostowski "the top-poster" Collapse wrote:
> Yes, Julio is right:
>
> This is nonsense:
> olcot: From FALSE nothing can be proved.
>
> This is nonsense:
> ross: No, no, it's "nihilum", "ex falso nihilum".
>
> This is correct, at least in classical logic:

> Julio, from the paper: [*]

> (1) Contradictory with respect to ~ (or simply contradictory)
> If there exists a formula A such that Γ |- A and Γ |- ~A .
> (2) Trivial If for every B, we have Γ |- B.
> In classical logic (1) and (2) are equivalent.

[*] <https://sqig.math.ist.utl.pt/pub/MarcosJ/01-CM-ECNSQL.pdf>

But the problem is that not even (1) captures "self-contradiction"
proper. Indeed (1) and (2) come up equivalent even in constructive
logic. Here is a rendition, a proof of False then similar:

```coq
Parameter P : Prop.

Axiom P_holds : P.
Axiom not_P_holds : ~ P.

Lemma ex_contra_quodlibet :
False.
Proof.
assert (HP : P) by apply P_holds.
assert (HN : ~ P) by apply not_P_holds.
tauto. (* constructive *)
Qed.

Lemma ex_contra :
P /\ ~ P.
Proof.
split.
- apply P_holds.
- apply not_P_holds.
Qed.

Lemma not_ex_contra :
~ (P /\ ~ P).
Proof.
tauto. (* constructive *)
Qed.
```

Exactly the same outcome with
[Axiom P_iff_not_P : P <-> ~ P]
or with
[Axiom P_and_not_P : P /\ ~ P].
and other variations, e.g. assumptions instead of axioms.

"Self-contradiction" proper is more like the interpreter should give
up at that point. And I think a big hint that these must indeed be
apples and oranges (and that it is not simply about negation) is that
"self-contradiction" is not just "contradiction" and what that means.

Julio

[Graham Cooper]

On Monday, March 6, 2023 at 2:38:34 AM UTC+11, Julio Di Egidio wrote:
> On Sunday, 5 March 2023 at 14:04:39 UTC+1, Ben Bacarisse wrote:
>
> > I think you have it exactly right. The existence of such a person
> > leads, logically, to a contradiction so, as you have found, the
> > statement of existence is false.
> You miss the fine print and the whole point as usual. As
> I have made more precise in a later post, I have actually
> found no "contradiction", just a false statement.
>
> Indeed, while it is easy to prove the following:
>
> Theorem no_such_barber : forall x : T,
> ~ the_barber x.
>
> we still cannot prove any kind of contradiction proper:
>
> Theorem the_barber_iff_not_the_barber : forall x : T,
> the_barber x <-> ~ the_barber x.
> Proof.

Just state the problem EXIST(barber) ...
then you get a CONTRADICTION

www.new-math.com
www.miniPROLOG.com

[Mostowski Collapse]

"constructive logic". What makes Coq constructive
are various things, some go beyond propositional logic.
In intuitionistic propositional logic this here is also valid:

((A ∧ ¬A) → B)
(⊥ → B)

The reason is that intuitionistic propositional logic is not
paraconsistent, its only paracomplete. So intuitionistic
logic does reject this here (LEM):

p v ~p
https://en.wikipedia.org/wiki/Law_of_excluded_middle

But it doesn't reject this here (LNC):

~(p & ~p)
https://en.wikipedia.org/wiki/Law_of_noncontradiction

Coq does also reject LEM, you have to explicitly state it,
in case you want to use it. But LEM is not so much
involved in ex falso quodlibet.

[Mostowski Collapse]

Because Coq doesn't possibly reject LNC, you have
to check, but I think it is so, since it inherits from
intuitionistic propositional logic,

this means also that the barber is not very interesting
for Coq, although you might find something interesting,
as you say, self contradiction could be something

else than only contradiction. On the other hand for
what Coq rejects, i.e. LEM, you find here a nice compilation.
What you would need to assume to get classical logic:

https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html

[Mostowski Collapse]

Concering self contradiction, I guess CIC, has some
sanitized form of recursion, making it less contradictory.
Whereas here for CC, the Girard Paradox is discussend:

Metamathematical investigations of a calculus of constructions
Thierry Coquand - January 1987
https://www.researchgate.net/publication/238979654

But this was back in January 1987. Now people talk
about proof irrelevance and stuff, and there is was
a Homotopy Type Theory (HoTT) frency.

[Julio Di Egidio]

On Wednesday, 8 March 2023 at 12:49:23 UTC+1, Mostowski Collapse wrote:

> Coq does also reject LEM

When Dunning-Kruger is a compliment...

LEM is << known to be >> *compatible* with
constructive logic, so we can safely add it as
an axiom. Just proofs that use LEM in an
essential way won't be constructive, i.e. the
proof won't give us a witness.

Conversely, << when there is a [constructive]
proof of [exists x, P x], it is always possible to
explicitly exhibit a value of [x] for which we can
prove [P x] -- in other words, every proof of
existence is constructive. >>

Classical vs. Constructive Logic
<https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html#lab214>

Julio

[Ross Finlayson]

Thanks, Julio, that's at least an interesting paper that makes
clear that material implication is bogus.

Then, in a Comenius language where only truths are well-formed,
"false" is only a prototype value of expressed contradiction, so
that "ex falso" and "ex contradictione" result about same.



Here I make some reading of a book of Maugin.

https://www.youtube.com/watch?v=v82ZeL_-hy0

[Mostowski Collapse]

The "reject" means only its not built.
No need to jump at me. You see it here that
it is not built-in, you have to opt-in:

Hypothesis em : forall A:Prop, or A (~ A).
https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html

So LEM ∉ CC and CIC, and then you can
form proofs like form example:

2.4. CC |- LEM + dep elim on bool -> proof-irrelevance

2.5. CIC |- LEM -> proof-irrelevance

[Mostowski Collapse]

Thats a fallacy:

Just proofs that use LEM in an "essential way" won't
be constructive, i.e. the proof won't give us a witness.

You are jumping to conclusions from LEM ∉ CC and
LEM ∉ CIC, and the idea that a proof in CC and CIC
is constructive, you are jumping to the conclusion

that CC+LEM and CIC+LEM proofs are non-constructive,
if they use LEM in an "essential way"? Define "essential
way"? In general its not the case that LEM always leads

to non-constructivity, for example in a finite domain:

A v ~A

Is not problematic.

[Mostowski Collapse]

Your fallacy is this fallacy, with P={logic
without LEM} and Q={constructive}:

P => Q
-------------------
~P => ~Q

Something tells its a fallacy:

(P→Q) → (¬P → ¬Q) is invalid.
https://www.umsu.de/trees/#(P~5Q)~5(~3P~5~3Q)

Try again!

Mostowski Collapse schrieb am Donnerstag, 9. März 2023 um 02:35:11 UTC+1:

[Ross Finlayson]

What if "predicates of LEM: TND" is just a domain and "A & ~A -> ~ (A e TND)".

[Mostowski Collapse]

Why do you have a potato in your mouth, while talking?

[Mostowski Collapse]

Was expecting a more british accent like when David Atten-
borough does a nature video. Now it sounds like a hill billy accent.

Sir David Frederick Attenborough
https://en.wikipedia.org/wiki/David_Attenborough

So please don't read any more books. Please, don't do it!

[Julio Di Egidio]

On Thursday, 9 March 2023 at 02:43:11 UTC+1, Mostowski Collapse wrote:

> you are jumping to the conclusion
> that CC+LEM and CIC+LEM proofs are non-constructive,
> if they use LEM in an "essential way"? Define "essential
> way"?

Proofs that use LEM "in an essential way" are proofs
that cannot be carried out without LEM. Which is plain
English for the thinking person.

> In general its not the case that LEM always leads
> to non-constructivity, for example in a finite domain:
> A v ~A Is not problematic.

For all *decidable* propositions A, indeed A\/~A is a
plain tautology, amounting to the boolean statement
true OR false. But not all propositions are decidable.

Do you now understand what a constructive proof is?

Julio

[Mostowski Collapse]

Thats a dead end. Excluding LEM as in constructive logic,
can serve a certain purpose. But logical requirements
such as for example, for some theory and logic:

- If EXIST(x):P(x) is provable, then there is some
term t so that P(t) is provable.
- if P v Q is provable, then eithr P is provable
or Q is provable

Can make the logic unnatural unusable. What about
the Yale Shooting problem. Did you try to formalize it.
Will it satisfy the above properties?

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

[Mostowski Collapse]

This is also fun,

A theory K is a scapegoat theory if, for any wf B(x) that has x
as its only free variable, there is a closed term t such that.
|- EXIST(x):~B(x) => ~B(t)
- Elliott Mendelson, Introduction to Mathematical Logic

And then there is exercise 2.63.

[Julio Di Egidio]

On Friday, 10 March 2023 at 21:43:19 UTC+1, Mostowski Collapse wrote:
> Thats a dead end. Excluding LEM as in constructive logic,
> can serve a certain purpose. But logical requirements
> such as for example, for some theory and logic:
>
> - If EXIST(x):P(x) is provable, then there is some
> term t so that P(t) is provable.
> - if P v Q is provable, then eithr P is provable
> or Q is provable

Neither of which require LEM.

As someone used to say, stupidity is a moral defect.

*Moron Alert*

Julio

[Ross Finlayson]

Tautology in words really approaches continuity conditions in equation.

Thus there's for reconciling algebra and geometry, in figures and words,
about the discussion of Banach-Tarski and why Vitali and Hausdorff's
geometric interpretation about the results after analysis of the doubling-space,
make for why sweep for modern foundations is so important and central,
that of course there's for re-Vitali-ization of measure theory, and separating
the continuous domain of the reals and the atomic domain of words,
then how they come together and why Finlayson's slates are the
touchstone of 21'st century apologetics in foundations.


Here's some more reading, https://www.youtube.com/watch?v=5_vmEhWl9oE .

[Julio Di Egidio]

3/4 of the posts in this thread are plain fucking bullshit.

Polluters of ponds should be shot in the face.

Your entire nazi-retarded incivilization...

*Plonk*

Julio

[Ross Finlayson]

But, you can't just invoke Godwin's usenet law, it actually has to be
some emergent outrage, not your rip-cord to end a thread.

If there was Lincoln and "four-score and seven ..." then these days
it was Trump and "gaa...", there's Biden's "c'mon, man...", that,
allez vites, hommes, we here are neither "Socialist Progressives"
nor "Fascists" and neither "Anarcho-Capitalists" not "Stasi puppets",
over here it's a Constitutional republic with individual rights, which
are often held up as the basis of, "universal human rights".
Now, that anybody who took a "loyalty oath" or "NDA" is probably
a traitor, still there's that anybody can share the one monist philosophy
that's a theory of truth, and there is one.

[Mostowski Collapse]

In mathematical logic, the disjunction and existence properties
are the "hallmarks" of constructive theories. LEM would easily
destroy them. Take this here:

> > - if P v Q is provable, then either P is provable or Q is provable

Now observe in classical propositional logic:

p∨¬p is valid.
https://www.umsu.de/trees/#|=p~2~3p

p is invalid.
https://www.umsu.de/trees/#|=p

¬p is invalid.
https://www.umsu.de/trees/#|=~3p

Similarly for the other property in FOL.
Or as Elliott Mendelson has formulated it:

Exxercise 2.63. Paragraph (b):
Prove that no predicate calculus is a scapegoat theory

- Elliott Mendelson, Introduction to Mathematical Logic

[Mostowski Collapse]

This prover tells me also that LEM would destroy the
disjunction properties from within intuitionistic logic itself:

Succeed in proving p\/ ~p --> p\/ ~p (2 msec.)
Fail to prove p\/ ~p --> p (4 msec.)
Fail to prove p\/ ~p --> ~p (5 msec.)
https://www.vidal-rosset.net/g4-prover/

Maybe Prolog, negation of failure would be different.
Giving some default to one side? Or you can even go
farther, you could check out ASP, etc.. logic programming

extensions that allow disjunctiive facts or disjunction
in the head, and see what happens. Or existential quantifiers
in the same place. Interestingly Prolog without any of

these extensions has also these two properties:

- If EXIST(x):P(x) is provable, then there is some
term t so that P(t) is provable.
- if P v Q is provable, then eithr P is provable
or Q is provable

Can you show these two properties for Prolog? Or is
this not common knowledge that Horn Clauses have
the "hallmarks" properties of constructive theories?

Easy or difficult exercise about Prolog?

LoL

[Mostowski Collapse]

But obviously people can deal with Prolog for decades
and not know these simple meta theorems about Prolog.
Then suddently they discover Coq and think they know

something about constructive logic, but the same people
might even still not know that Prolog satisfies the
"hallmarks" of constructive theories. I know at least one

specimen on the internet, that gives me this impression.

LMAO!

[Ross Finlayson]

It seems simply whether p is a predicate of a variable or a constant.

I.e., "p v ~p" "IS" a predicate, "x: p v ~p" simply indicates
"for the domain of x, 'p v ~p' is in its corresponding LEM-domain,
the domain of predicates of x".

That for example a clopen interval is closed, open, what with
respect to otherwise that usually closed and open are antonyms.

[Mostowski Collapse]

The more nagging and interesting problem is,
how would we model the Yale Shooting problem
in Prolog, if the Yale Shooting problem

violates the "hallmarks", on the other hand
Prolog satisfies the "hallmarks". So how should
Prolog model the Yale Shooting problem:

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

In one formulation the Yale Shooting problem
violates the existential property, in the form that
the Yale Shooting problem is not scapegoat theory:

EXIST(t):~alive(t)

Does not imply:

~alive(t)

We only have, if we don't know loaded(0):

~alive(0) v ~alive(1)

[Mostowski Collapse]

Maybe Alec Baldwin should have studied the Yale Shooting
Problem, before becoming a Western Actor:

Actor Alec Baldwin formally charged for fatal shooting on set
https://www.rollingstone.com/tv-movies/tv-movie-news/alec-baldwin-charged-involuntary-manslaughter-rust-shooting-1234600287/

[Ross Finlayson]

Maybe you should've wondered about where COVID came from,
and what is is and what it does,
before blaming the pangolins and shilling miRNA garbage.

[Ross Finlayson]

On Saturday, March 11, 2023 at 11:29:34 AM UTC-8, Mostowski Collapse wrote:

Also your "crypto" shilling is coming across as worth less than a farthing.

[Mostowski Collapse]

Maybe shouldn't reject LEM, it might improve survival.

LoL

[Ross Finlayson]

LEM is just a construct of logic and is what it is,
TND, LEM, PEM, of course in a "the" logic and one modality,
like reality, where abstractions of course are free,
in what are sound and unsound, it's simple that predicates
reflect whether they are well-defined or not,
and "ex falso nihilum" and "ex contradictione revertum".

(If you'll please excuse my Latin is lacking, though fairly
it's not quite a "dead" language, in terms of things like Latin
and Sanskrit, here the point is that contradiction is an
indicator, within what must be a complete reckoning,
in the domain of all the language.)

[Ross Finlayson]

You should look into the Pi-calculus, it might help
resolve your frame problem.


A joke goes a guy from Harvard and a guy from Yale enter a urinal
and after urinating, the guy from Harvard uses the lavatory while
the guy form Yale is combing his hair. The guy from Harvard goes
"at Hah-vahd, we learned to wash our hands after urinating",
and the guy from Yale goes "at Yale, we learned to not piss on our hands".

[Mostowski Collapse]

Looks like you are confusing Logic with Harry Potter

https://harrypotter.fandom.com/wiki/Incantation#Known_incantations

Even Lumos Maxima cannot cure your Herpes, Boy!

[Mostowski Collapse]

Why is the Yale Shooting Problem called the Yale Shooting
Problem, and not the Ross Finlaysons Cabana Shooting Problem.
Very easy, according to Wikipedia:

The name of this problem derives from its inventors, Steve
Hanks and Drew McDermott, working at Yale University
when they proposed it. [...] In 2005, the 1985 paper in which
the Yale shooting scenario was first described received
the AAAI Classic Paper award.
https://en.wikipedia.org/wiki/Yale_shooting_problem

Classic Paper Award Corecipients: Steve Hanks and Drew
McDermott Default Reasoning, Nonmonotonic Logics, and
the Frame Problem, presented at the Fifth National Conference
on Artificial Intelligence (AAAI-86), Philadelphia, Pennsylvania

Hope this Helps!

P.S.:

Papers will be judged on the basis of impact, for example:
- Started a new research (sub)area
- Led to important applications
- Answered a long-standing question/issue or clarified what had been murky
- Made a major advance that figures in the history of the subarea
- Has been picked up as important and used by other areas within (or outside of) AI
- Has been very heavily cited
https://aaai.org/about-aaai/aaai-awards/aaai-classic-paper-award/

[Mostowski Collapse]

Why would I need Pi-calculus. There is no concurrency
involved in the Yale Shooting Problem. How many guns
do you count in the Yale Shooting Problem?

[Ross Finlayson]

Meh, go sit with DC, you decalcitrant.

In the box, Burse?

Page one says open, page two says fill, page three says cock, page four says kill.

Turkey.

[Mostowski Collapse]

Whats your point Rossy Boy, does the Herpes hurt?

Ross Finlayson schrieb am Sonntag, 12. März 2023 um 02:57:04 UTC+1:
> Turkey.

[Ross Finlayson]

I don't know which wife keeps beating you, but between me and a few hundred
others' mucosal membranes, I have no pain or sores associated with any sort
of herpes virus, so, it's untruthful and not factual to call me dirty, and I don't
really care how much abreva you slather on each day or what sores your tongue
has all over it, I don't and it's not relevant. There are at least six kinds of herpes,
and Burse is an irritant. I've been with 100 women and have no symptoms to report,
except warm fuzzy heartstrings.

These days I'm more worried about muscoskeletal problems since the liver spent a
long time defeating some of COVID, that the bone marrow is constantly fighting
what were the billions of spike proteins left sitting around from COVID. I.e., in
terms of the "epidemic being over" now "the pandemic is well sit in" and while perhaps
"the quick dying is over" there's that "the long suffering is well underway". When
I watch free old syndicated television so I figure the marketing is toward free old
television viewers, most common ads include: integumentary problems, circulation
problems, muscoskeletal injuries, diabetes resulting from circulatory problems,
gut problems, foot problems, where pretty much all I have here is a few ace bandages.

So, when it comes to physical fitness and mental fitness, I'm graying and overweight
and oh there was the subluxated rib and the hips and knees and mostly the Achilles
tendon, the regular zinc supplement was probably quite critical, then there's things
like not eating or drinking out of disposable containers, the milk thistle was good
and the mullein seemed to help a lot, yesterday I ate a piece of roquefort with a
piece of salmon and some almonds and there's avoiding: salt, sugar, dairy, because
there's hyperkalemia about calcium and there's still quite dairy but less than
being a cheese-etarian. Walnuts and almonds and brazil nuts and such then seem
alright while sea salt and various chlorides are deemed bad. Coffee is down to
three a day and with about a half a pack of organic tobacco cigarettes.
Sometimes there's a few caplets of psyllium or activated charcoal. If they start
innoculating chickens that'll probably be banned too, and I really would enjoy
poke but had a bad reaction and associate it with diverticulitis. So, mostly people
need to highly moderate salt and sugar. Pineapple has an enzyme called bromelain
that from time to time helps dissolve scar tissue. My biggest problem is my ankle,
but I'm jogging again so hopefully will work it over. There's much to be said for
shiatsu or otherwise helping the lymph and glymph, also inversion therapy, and
vibration therapy, that circulation is the root of problems like diabetes. Anyways
ketoacidosis and hyperkalemia needs to be actively avoided by restricting salt, sugar.
I'm mostly happy the subluxated rib went away and no diverticulitis and happy that
my doctor and his hospital is available and I avoid them.


Here your "frame problem" is just the same as any other situation with "undefined
behavior", the "Yale situational-calculus frame-problem" is just undefined behavior
resulting the indeterministic and it's not a logical problem only a non-logical problem.

Then, one might attach to these fluents or indicators of belief an implicit state machine
that indicates whenever the belief changes that the state of belief changing is itself an
event, that otherwise such memoryless automata, don't know which was was up.

I.e., there's simply the notion of what is memory to result that it's as well-defined
then for a program model of deterministic behavior that there are resources that
can be written as a stack-machine, long story short, Turkey, your rules engine is
missing a few, and making it verifiable is as simple as closed categories.

Anyways the "Yale shooting problem" is not problem at all, it's an error.

[Mostowski Collapse]

Hey buddy, what drugs are you consuming? Also on same line

Anyways the Russsell Paradox, is not a paradox, its an ice cream cone.

[Mostowski Collapse]

In Slumber Land, where logic's strange,
The Russell Paradox takes sweet form and change,
A tasty treat, a cone so bright,
With flavors bold and swirls of white.

It rests in hands of those who dream,
And puzzles all who hear its scheme,
For though it's sweet, this paradox cone,
It's not just sugar, and waffle cone.

No, it's a puzzle wrapped in treat,
A riddle that's both sour and sweet,
For Russell's mind has spun it so,
That logic's rules it can't quite follow.

So take a lick, my friend, and see,
How logic's twists can tasty be,
For in Slumber Land, the Russell cone,
Is paradox and treat, all in one.

- ChatGPT Feb 13 Version

[Ross Finlayson]

Define "strong metonymy".

[Mostowski Collapse]

Strong opposite example:

Ross Finlayson and Sane Person are in opposite.

Explain this:

> I.e., "p v ~p" "IS" a predicate, "x: p v ~p" simply indicates
> "for the domain of x, 'p v ~p' is in its corresponding
> LEM-domain, the domain of predicates of x".

An attempt in Formula as Types? But who would the
phrase it " 'p v ~p' is in its corresponding LEM-domain",
or then a phrase "the domain of predicates of x".

What does this gibberish mean?

LoL

Usually in Formula as Types, we have things like
f, i.e. a proof, it has type A -> B, written by the judgement
f : A -> B, it can be viewed as a function f, that sends

every proof p for A, i.e. p : A to a proof f(p) for B,
i.e. f(p) : B, by virtue of Modus Ponense:

f : A -> B p : A
--------------------------------- (MP)
f(p) : B

[Mostowski Collapse]

In classical logic A v ~A and A -> A are the same,
the later is simply justified by the identity function:

id : A -> A

The identity function, respectively the theorem A -> A
is also available in intuitionistic logic (or in constructive
logic, if you prefer the Culio tangent), interestingly the

the theorem A -> A is also available in minimal logic,
which das not only reject LEM, but it rejects also
LNC (Law of Noncontradiction), so we have already

in minimal logic

A v ~A -> (A -> A)

The other direction:

(A -> A) -> (A v ~A)

Does it fail? What would be a counter example?

[Ross Finlayson]

You means "rejects" or "ignores"?

Ignorance is no defense, but, sometimes a little knowledge is dangerous.

The other day I learned that "dunce" was used to describe followers
of Duns Scotus, which seems oxymoronic, but, cargo-cult. Duns Scotus
is course is really great and seems must've had a bigger head than
others of his time and place.

Or, you know, what fit in it.

You can look to him for definitions in infinity and continuity
as the church allowed at the time, who was
at the time the arbiter of knowledge.

Anyways mathematical objects are general, that you
seem to have confused "Sane" and "Blind". If you're interested
there's a diagnostic manual for mental pathologies, you can
find most thinking things having each condition, it's
sort of like a horoscope, and is in general language,
that basically applies to whatever random page you select.
Be careful though, there are a lot of drug pushers,
and these days what they have for happy pills
causes depression, though it only costs pennies per dose to manufature.
I don't know any their effects personally as I've never ate them.

Then, about the description of mathematical objects as mathematical objects,
is that you need make a first-class definition of the objects in themselves,
here about predicates of what are predicates, then about that various
theories of objects, have primary objects with fundamental relations.
Examples include sets, numbers, parts, types, categories, predicates,
functions, these being mostly discrete mathematics of a sort.

[Mostowski Collapse]

Your Ignorance. "Rejection" is the normal speak for
LEM and intuitionistic logic:

For ¬¬(P∨¬P), we have to observe that Intuitionistic
rejection of LEM means that LEM is not valid, not that it is false.
https://math.stackexchange.com/a/4002959

Whats wrong with you and Culio? Have you spent
your lifetime under a rock?

[Mostowski Collapse]

You can also make a text concordance here:

The word reject appears in these sentences (7 times):
... certain axioms from classical mathematics are rejected by intuitionists ...
... it is also in effect a rejection of the hypothetical judgement ...
... Kolmogorov rejected Ex Falso, while Heyting and Glivenko accepted it ...
... Note that that is a very strong rejection: ...
... Kolmogorov in 1925 had explicitly rejected Ex Falso ...
... that intuitionistic mathematics need not reject that axiom ...
... really incompatible with the ground for his rejection of Ex Falso ...
https://plato.stanford.edu/entries/intuitionistic-logic-development

The word reject appears in these sentences (6 times):
... Brouwer rejected formalism per se but admitted the potential usefulness ...
... Rejection of Tertium Non Datur (LEM) ...
... 1. Rejection of Tertium Non Datur (LEM) ...
... an assumption he rejected, anticipating Gödel’s incompleteness theorem ...
... The rejection of LEM has far-reaching consequences ...
... equivalent to Markov’s Principle MP, which Brouwer rejected ...
https://plato.stanford.edu/entries/logic-intuitionistic/

BTW: If you reject ex falso, besides LEM you get minimal logic.
If you accept ex falso and only reject LEM, you get intuitionistic logic.
If you accept both, you get classica logic.

Hope this Helps!

[olcott]

On 3/12/2023 6:28 PM, Mostowski Collapse wrote:
> You can also make a text concordance here:
>
> The word reject appears in these sentences (7 times):
> ... certain axioms from classical mathematics are rejected by intuitionists ...
> ... it is also in effect a rejection of the hypothetical judgement ...
> ... Kolmogorov rejected Ex Falso, while Heyting and Glivenko accepted it ...

Ah finally someone that is not a nitwit.

> ... Note that that is a very strong rejection: ...
> ... Kolmogorov in 1925 had explicitly rejected Ex Falso ...
> ... that intuitionistic mathematics need not reject that axiom ...
> ... really incompatible with the ground for his rejection of Ex Falso ...
> https://plato.stanford.edu/entries/intuitionistic-logic-development
>
> The word reject appears in these sentences (6 times):
> ... Brouwer rejected formalism per se but admitted the potential usefulness ...
> ... Rejection of Tertium Non Datur (LEM) ...
> ... 1. Rejection of Tertium Non Datur (LEM) ...

A logic sentence can be true/false/incorrect
Two examples of incorrect are self-contradictory and vacuous truth object.

LP := ~True(LP) // both
TT := True(TT) // VTO
G := ~Provable(F,G) // Prolog proves VTO

?- G = not(provable(F, G)). % G = ¬(F ⊢ G)

?- unify_with_occurs_check(G, not(provable(F, G))).
false.

> ... an assumption he rejected, anticipating Gödel’s incompleteness theorem ...
> ... The rejection of LEM has far-reaching consequences ...
> ... equivalent to Markov’s Principle MP, which Brouwer rejected ...
> https://plato.stanford.edu/entries/logic-intuitionistic/
>
> BTW: If you reject ex falso, besides LEM you get minimal logic.
> If you accept ex falso and only reject LEM, you get intuitionistic logic.
> If you accept both, you get classica logic.
>
> Hope this Helps!
>
> Mostowski Collapse schrieb am Montag, 13. März 2023 um 00:21:04 UTC+1:
>> Your Ignorance. "Rejection" is the normal speak for
>> LEM and intuitionistic logic:
>>
>> For ¬¬(P∨¬P), we have to observe that Intuitionistic
>> rejection of LEM means that LEM is not valid, not that it is false.
>> https://math.stackexchange.com/a/4002959
>>
>> Whats wrong with you and Culio? Have you spent
>> your lifetime under a rock?
>> Ross Finlayson schrieb am Sonntag, 12. März 2023 um 22:39:55 UTC+1:
>>> You means "rejects" or "ignores"?

--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[olcott]

When we change logic such that the consequent/conclusion is a
semantically necessary consequence of its of its antecedent/premises (as
is the case with syllogisms) then we are back to two-valued logic.

[Mostowski Collapse]

Dont change logic, they are not malleable. Just use some
logic, i.e. like classical, intuitionistic, minimal, etc..

You would also not change your bycicle into a car, in case
you would want to use a car instead of a bycicle.

Or maybe you are already hammering your bycicle,
so that it becomes a car?

[olcott]

On 3/12/2023 7:35 PM, Mostowski Collapse wrote:
> Dont change logic, they are not malleable. Just use some
> logic, i.e. like classical, intuitionistic, minimal, etc..
>

When logic diverges from correct reasoning is must be abandoned and
replaced.

[Mostowski Collapse]

Also you can define some model theory
for intuitionistic logic such that you have a notion
"semantically necessary consequence", i.e.

T |=_I A

So I don't know what you are talking about.
The above has also a provability counter part,
just use some of the calculi:

T |-_I A

The same exists for minimal, classical logic, i.e.
|=_M and |=_C, defining a "semantically necessary
consequence", and also calculi exist |-_M and |-_C.

[olcott]

On 3/12/2023 7:44 PM, Mostowski Collapse wrote:
> Also you can define some model theory
> for intuitionistic logic such that you have a notion
> "semantically necessary consequence", i.e.
>

The syllogism already does this with categorical propositions.
https://en.wikipedia.org/wiki/Categorical_proposition

[olcott]

On 3/12/2023 6:49 PM, olcott wrote:

> On 3/12/2023 6:28 PM, Mostowski Collapse wrote:
>> You can also make a text concordance here:
>>
>> The word reject appears in these sentences (7 times):
>> ... certain axioms from classical mathematics are rejected by
>> intuitionists ...
>> ... it is also in effect a rejection of the hypothetical judgement ...
>> ... Kolmogorov rejected Ex Falso, while Heyting and Glivenko accepted
>> it  ...

Kolmogorov
he says that Ex Falso is unacceptable for the reason that it asserts
something about the consequences of something impossible (van Heijenoort
1967: 421).

https://plato.stanford.edu/entries/intuitionistic-logic-development/#Kolm1925

[Mostowski Collapse]

But categorical propositions are a little limmited.

In philosophy, term logic, also known as traditional
logic, syllogistic logic or Aristotelian logic, is a loose
name for an approach to formal logic that began with
Aristotle and was developed further in ancient history
mostly by his followers, the Peripatetics. It was revived
after the third century CE by Porphyry's Isagoge.
https://en.wikipedia.org/wiki/Term_logic

How do you formulate the Drinker Paradox in Term Logic?

[olcott]

On 3/13/2023 3:29 PM, Mostowski Collapse wrote:
> But categorical propositions are a little limmited.
>
> In philosophy, term logic, also known as traditional
> logic, syllogistic logic or Aristotelian logic, is a loose
> name for an approach to formal logic that began with
> Aristotle and was developed further in ancient history
> mostly by his followers, the Peripatetics. It was revived
> after the third century CE by Porphyry's Isagoge.
> https://en.wikipedia.org/wiki/Term_logic
>
> How do you formulate the Drinker Paradox in Term Logic?
>

If X is drinking in pub Y and X is the only person in pub Y then these
two facts taken together guarantee that if X is drinking in pub Y
then everyone in pub Y is drinking.

Any other way of looking at this seems a little nutty.

> olcott schrieb am Montag, 13. März 2023 um 02:45:32 UTC+1:
>> On 3/12/2023 7:44 PM, Mostowski Collapse wrote:
>>> Also you can define some model theory
>>> for intuitionistic logic such that you have a notion
>>> "semantically necessary consequence", i.e.
>>>
>> The syllogism already does this with categorical propositions.
>> https://en.wikipedia.org/wiki/Categorical_proposition

[Mostowski Collapse]

You have only this available, porpositional combinations of:

All S are P.
No S are P.
Some S are P.
Some S are not P.

To formulate this, plus assuming ∃xPx:

∃x(Px & (Dx -> ∀y(Py -> Dy)))

What you wrote down there is not the above formula,
you transmogrified ∃x into ∃!x. But Smullyan nowhere
talked about "only" person in pub.

He used the phrase "at least one" person. Could
it be that you assume another Drinker Paradox? And
not Smullyans original Drinker Paradox?

[olcott]

On 3/13/2023 5:43 PM, Mostowski Collapse wrote:
> You have only this available, porpositional combinations of:
>
> All S are P.
> No S are P.
> Some S are P.
> Some S are not P.
>

I actually have all natural language semantics available for the maximum
extension of the basic idea of a syllogism.

The most basic idea of a syllogism is that the conclusion semantically
follows from its premises by necessity.

> To formulate this, plus assuming ∃xPx:
>
> ∃x(Px & (Dx -> ∀y(Py -> Dy)))
>
> What you wrote down there is not the above formula,
> you transmogrified ∃x into ∃!x. But Smullyan nowhere
> talked about "only" person in pub.
>
> He used the phrase "at least one" person. Could
> it be that you assume another Drinker Paradox? And
> not Smullyans original Drinker Paradox?
>

It is not a paradox it is either an error or has what I said as its
basis. The only way that the fact that X is drinking proves that
everyone in the pub is drinking is the case where X is the only one in
the pub.

[Mostowski Collapse]

Ever heard of vacous truth? What if x is a person in the pub
that isn't drinking. Doesn't this make the formula true?

∃x(Px & (Dx -> ∀y(Py -> Dy)))

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

LoL

[olcott]

On 3/14/2023 5:01 PM, Mostowski Collapse wrote:
> Ever heard of vacous truth? What if x is a person in the pub
> that isn't drinking. Doesn't this make the formula true?
>

The best example of vacuous truth is the truth teller paradox.

This sentence is true.
What is it true about?
It is true about being true.
What is it true about being true about?
It is true about being true about being true...

Prolog can detect and reject this:
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2

> ∃x(Px & (Dx -> ∀y(Py -> Dy)))
>
> https://en.wikipedia.org/wiki/Vacuous_truth
>
> LoL
>
> lcott schrieb am Montag, 13. März 2023 um 23:54:20 UTC+1:
>> It is not a paradox it is either an error or has what I said as its
>> basis. The only way that the fact that X is drinking proves that
>> everyone in the pub is drinking is the case where X is the only one in
>> the pub.

[Mostowski Collapse]

What makes you think only Prolog can detect that.
Prolog is Horn Clause subset of FOL. It would be
strange if Prolog would have a an occurs check,

and FOL wouldn't have an occurs check. Right?
FOL can also do it. At least Wolfgang Schwartz
tree tool tells me so:

∃xx=t(x) is invalid.
https://www.umsu.de/trees/#~7x(x=t(x))

Countermodel:
Domain: { 0, 1 }
t: { (0,1), (1,0) }

Whats wrong with you?

[olcott]

On 3/14/2023 9:07 PM, Mostowski Collapse wrote:
> What makes you think only Prolog can detect that.
> Prolog is Horn Clause subset of FOL. It would be
> strange if Prolog would have a an occurs check,
>

When we simplify G down to what Gödel says is its essence

We are therefore confronted with a proposition
which asserts its own unprovability.

It is very easy to encode in Prolog

?- G = not(provable(F, G)). % G = ¬(F ⊢ G)

?- unify_with_occurs_check(G, not(provable(F, G))).
false.

[Ross Finlayson]

I found an evaluation copy of this Language and Logic from 1950's
the other day.



"Validity, as we shall see, depends upon the arrangement of the elements in each statement,
not on truth or falsity. Certain arrangements make an argument logical; others make it illogical.
Once an argument has a correct arrangement, that is, is valid, _then and only then_ do true
premises entail a true conclusion."

"Any argument is said to be valid, or logical, if there is one sentence (called the _conclusion_)
that follows necessarily from the other sentences (called _premises_). The conclusion follows
necessarily from the premises when no other statement is possible as a result of the previous
statements. Thus if anyone tells us what he says ''logically follows'', then he means that his
conclusion, or a synonymous statement, _must follow_. If there is even one other alternative
possible, then, strictly speaking, his argument is not valid."


"There are two kinds of logic that can be distinguished. On the one hand there is _deductive logic_,
which pertains to the elements of necessity in all proper thinking. On the other hand there is
_inductive logic_, which pertains to the elements of _probability_ and _reliability_ in all proper
thinking."

It's a pretty interesting little book, contains a lot of concepts together. Quite sensible.




Hey, Burse, one of your bots got stuck on broken again. Takes money to lose money - ....

It still has the little reply card in it, ....

[olcott]

On 3/14/2023 9:55 PM, Ross Finlayson wrote:
> On Tuesday, March 14, 2023 at 3:01:25 PM UTC-7, Mostowski Collapse wrote:
>> Ever heard of vacous truth? What if x is a person in the pub
>> that isn't drinking. Doesn't this make the formula true?
>> ∃x(Px & (Dx -> ∀y(Py -> Dy)))
>> https://en.wikipedia.org/wiki/Vacuous_truth
>>
>> LoL
>> lcott schrieb am Montag, 13. März 2023 um 23:54:20 UTC+1:
>>> It is not a paradox it is either an error or has what I said as its
>>> basis. The only way that the fact that X is drinking proves that
>>> everyone in the pub is drinking is the case where X is the only one in
>>> the pub.
>
> I found an evaluation copy of this Language and Logic from 1950's
> the other day.
>
>
>
> "Validity, as we shall see, depends upon the arrangement of the elements in each statement,
> not on truth or falsity. Certain arrangements make an argument logical; others make it illogical.
> Once an argument has a correct arrangement, that is, is valid, _then and only then_ do true
> premises entail a true conclusion."
>
> "Any argument is said to be valid, or logical, if there is one sentence (called the _conclusion_)
> that follows necessarily from the other sentences (called _premises_).

Semantically necessary as in the way that syllogisms work.

[Mostowski Collapse]

Maybe this matches classical syllogisms, but how about
non-classical sylllogism. What explains that the Drinker
Paradox is not intuitionistically valid? Is this a paradox

or simply an error? But errors have two sides of a coin,
we can ask, are they a bug or a feature? Could be a feature
of intuitionistic logic that it doesn't make the Drinker

Paradox valid. Since it rejects some axiom schemata,
or some inference rules, which a classical semantic
necessesity viewpoint wouldn't reject, whereas a non-

classical semantic necessesity viewpoint does reject it.

[olcott]

On 3/18/2023 3:53 PM, Mostowski Collapse wrote:
> Maybe this matches classical syllogisms, but how about
> non-classical sylllogism. What explains that the Drinker
> Paradox is not intuitionistically valid? Is this a paradox
>
> or simply an error?

"There is someone in the pub such that, if he or she is drinking, then
everyone in the pub is drinking."

The only cause-and-effect relationship that makes the drinker paradox
true is that the pub is otherwise empty except for the drinker.

The drinker paradox is merely silly nonsense. If it wasn't that
Raymond Smullyan said it then it would have been ignored within minutes
and never brought up again.

> But errors have two sides of a coin,
> we can ask, are they a bug or a feature? Could be a feature
> of intuitionistic logic that it doesn't make the Drinker
>
> Paradox valid. Since it rejects some axiom schemata,
> or some inference rules, which a classical semantic
> necessesity viewpoint wouldn't reject, whereas a non-
>
> classical semantic necessesity viewpoint does reject it.
>
> olcott schrieb am Mittwoch, 15. März 2023 um 04:06:12 UTC+1:
>> Semantically necessary as in the way that syllogisms work.

[Mostowski Collapse]

But according to semantical necessesity it is valid:
The non-empty pub is just the domain of discourse:

∃x(Dx → ∀yDy) is valid.
https://www.umsu.de/trees/#~7x(Dx~5~6yDy)

But there is no assumption that there is a drinker.
According to semantical necessesity this is not derivable:

∃xDx is invalid.
https://www.umsu.de/trees/#~7xDx

Or that there is exactly one drinker:
According to semantical necessesity this is not derivable:

∃xDx ∧ ∀xDx is invalid.
https://www.umsu.de/trees/#~7xDx~1~6xDx

What makes you thinking there needs to be
a drinker to make ∃x(Dx → ∀yDy). According
to semantical necessesity, it is vaculously true

when there is no drinker, so this case is not
problematic. Also the formula ∃x(Dx → ∀yDy)
is true, if there are more than one drinker,

or if there are non-drinker. Because the formula
is always true for a non-empty domain of discourse
and an arbitrary drinker class D.

Thats what semantical necessesity tells us.

[Mostowski Collapse]

Do you imply that the Drinker Paradox ∃x(Dx → ∀yDy)
is sometimes false? What is your counter model?
In classical semantical necessesity the

Drinker Paradox is always true, in a model of
with a non-empty domain. In non-classical logics
or if the domain is allowed to be empty, matters are

a little bit more complicated, there are indeed
counter models in non-classical logics.

See also:

The Drinker Paradox and its Dual - Louis Warren et al., 2018
https://ir.canterbury.ac.nz/bitstream/handle/10092/16234/1805.06216v1.pdf

[olcott]

On 3/18/2023 5:09 PM, Mostowski Collapse wrote:
> But according to semantical necessesity it is valid:
> The non-empty pub is just the domain of discourse:
>
> ∃x(Dx → ∀yDy) is valid.
> https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
>
> But there is no assumption that there is a drinker.
> According to semantical necessesity this is not derivable:
>

If the Moon is made from green cheese then it is semantically necessary
that the Moon is made from cheese.

"There is someone in the pub such that, if he or she is drinking, then
everyone in the pub is drinking."

Only in the case where they are the only person in the pub.

[Mostowski Collapse]

How would what you say make the formula:

∃x(Dx→∀yDy)

False? Do you use some non-classical logic?
In classical logic the formula is generally valid:

∃x(Dx → ∀yDy) is valid.

Means its True in all usual FOL models
with non-empty domain.

[olcott]

On 3/18/2023 5:29 PM, Mostowski Collapse wrote:
> How would what you say make the formula:
>
> ∃x(Dx→∀yDy)
>

My foundation of correct reasoning may get rid of the → operator and
replace it with the Semantic Necessity operator: ⊨□

A & B ⊨□ A

[Dan Christensen]

On Sunday, March 5, 2023 at 6:03:51 AM UTC-5, Julio Di Egidio wrote:
> I am learning Coq (which is based on constructive logic), so
> I thought let's look at the Barber's Paradox, i.e. let's see if I can
> get a "contradiction"

[snip]

Can this result be obtained in Coq:

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):[a in m => [(barber,a) in s <=> ~(a,a) in s]] <=> ~barber in m]]

where

v = the set of all village residents

m = the set of men living in the village

s = the shaving relation on v such that (x,y) in s means the x shaves y

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

[Dan Christensen]

On Saturday, March 18, 2023 at 6:14:14 PM UTC-4, Mostowski Collapse wrote:
> Do you imply that the Drinker Paradox ∃x(Dx → ∀yDy)
> is sometimes false? What is your counter model?
> In classical semantical necessesity the
>
> Drinker Paradox is always true, in a model of
> with a non-empty domain. In non-classical logics
> or if the domain is allowed to be empty, matters are
>
> a little bit more complicated, there are indeed
> counter models in non-classical logics.
>

In DC Proof, for any proposition Q, be it true or false, we have EXIST(a):~D(a) => EXIST(b):[D(b) => Q]

PROOF

1 EXIST(a):~D(a)
Premise

2 ~D(x)
E Spec, 1

3 ~D(x) | Q
Arb Or, 2

4 ~~D(x) => Q
Imply-Or, 3

5 D(x) => Q
Rem DNeg, 4

6 EXIST(a):~D(a) => EXIST(b):[D(b) => Q]
Conclusion, 1

[olcott]

On 3/18/2023 5:09 PM, Mostowski Collapse wrote:

> But according to semantical necessesity it is valid:
> The non-empty pub is just the domain of discourse:
>
> ∃x(Dx → ∀yDy) is valid.
> https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
>
> But there is no assumption that there is a drinker.
> According to semantical necessesity this is not derivable:
>

I have had more time to think about this.
Semantic Necessity operator: ⊨□

"There is someone in the pub such that, if he or she is drinking, then
everyone in the pub is drinking."

The above semantically entails that there is only one person in the pub.
∃x(Dx → ∀yDy) ∴ ∀y = x

[Dan Christensen]

On Sunday, March 19, 2023 at 12:31:52 AM UTC-4, olcott wrote:
> On 3/18/2023 5:09 PM, Mostowski Collapse wrote:
> > But according to semantical necessesity it is valid:
> > The non-empty pub is just the domain of discourse:
> >
> > ∃x(Dx → ∀yDy) is valid.
> > https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
> >
> > But there is no assumption that there is a drinker.
> > According to semantical necessesity this is not derivable:
> >
> I have had more time to think about this.
> Semantic Necessity operator: ⊨□
> "There is someone in the pub such that, if he or she is drinking, then
> everyone in the pub is drinking."

The original formulation by Smullyan did not assume that this "lead drinker" was necessarily in any pub:

"[T]here exists someone such that whenever he (or she) drinks, everybody drinks."
--Raymond Smullyan, "What is the name of this book?" 1978, p. 210

It is much simpler this way. One less restriction. Things fall easily into place when you assume there is at least one person somewhere who is not drinking -- by no means a stretch. See my previous posting here for a formal proof.

[Julio Di Egidio]

On Sunday, 19 March 2023 at 06:57:47 UTC+1, Dan Christensen wrote:
> On Sunday, March 19, 2023 at 12:31:52 AM UTC-4, olcott wrote:

> > "There is someone in the pub such that, if he or she is drinking, then
> > everyone in the pub is drinking."
>
> The original formulation by Smullyan did not assume
> that this "lead drinker" was necessarily in any pub:

Of course it did, "people in the pub" is the whole
*universe of discourse* there. Indeed do read
what you quote:

> "[T]here exists someone such that whenever he (or she) drinks, everybody drinks."
> --Raymond Smullyan, "What is the name of this book?" 1978, p. 210

It doesn't mention pubs at all!

You still do not understand what a "universe
of discourse" is and how it is relevant to the
framing of logical problems, in fact to as
*stringent* a framing logical problems as
possible.

Julio

[Julio Di Egidio]

On Saturday, 18 March 2023 at 23:24:07 UTC+1, olcott wrote:
> On 3/18/2023 5:09 PM, Mostowski Collapse wrote:
> > But according to semantical necessesity it is valid:
> > The non-empty pub is just the domain of discourse:
> >
> > ∃x(Dx → ∀yDy) is valid.
> > https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
> >
> > But there is no assumption that there is a drinker.
> > According to semantical necessesity this is not derivable:

Notice that the moron Burse is writing "semantical
necessesity" (sic) while talking of *material implication*,
and that indeed has less than zero to do with semantics,
which is the whole point with these seeming paradoxes!

> If the Moon is made from green cheese then it is semantically necessary
> that the Moon is made from cheese.

Yeah, sort of. The relevant notion in Logic actually
is called (logical) entailment, and a more appropriate
example is: "(to be a) bachelor" entails "(to be) not
married", by the meaning of "bachelor". Whence it
is self-contradictor to say "married bachelor".

Incidentally, semantics has to do with meaning, not
the other way round. I.e. understanding language is
and remains a *pre*requisite to the whole endeavour.

> "There is someone in the pub such that, if he or she is drinking, then
> everyone in the pub is drinking."

In natural language it goes like this:

By the law of excluded middle, we can assume
that either everybody is drinking or someone is
not drinking. We then proceed by case analysis:

In case everybody is drinking, the statement is
trivially true.

In case someone is not drinking, pick anyone who
is not drinking, call them x. Use x as the witness
for the statement in question, such that the
statement becomes "if x is drinking, then everyone
in the pub is drinking." And now consider that x is
in fact *not* drinking, whence, by ex falso quodlibet,
the conclusion holds.

It does use LEM plus some choice principle, but the
whole thing can be reformulated constructively over
some decidable types. What is essential to this
"paradox", to reiterate what I have said initially, is
*(material) implication* and how very little it has to
do with logical consequence/entailment.

Julio

[Julio Di Egidio]

On Wednesday, 15 March 2023 at 03:55:26 UTC+1, Ross Finlayson wrote:

> "There are two kinds of logic that can be distinguished. On the one hand there is _deductive logic_,
> which pertains to the elements of necessity in all proper thinking. On the other hand there is
> _inductive logic_, which pertains to the elements of _probability_ and _reliability_ in all proper
> thinking."
>
> It's a pretty interesting little book, contains a lot of concepts together. Quite sensible.

For years I have been warning to you and others that
that is ugly mainstream bullshit, with explanations as
well as references, but you'll forever keep re-injecting
exactly and always mainstream bullshit ad nauseam...

ESAD, you and the whole nazi-retarded bandwagon.

Julio

[Julio Di Egidio]

On Sunday, 19 March 2023 at 04:18:12 UTC+1, Dan Christensen wrote:
> On Sunday, March 5, 2023 at 6:03:51 AM UTC-5, Julio Di Egidio wrote:
> > I am learning Coq (which is based on constructive logic), so
> > I thought let's look at the Barber's Paradox, i.e. let's see if I can
> > get a "contradiction"
>
> [snip]
>
> Can this result be obtained in Coq:
>
> 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):[a in m => [(barber,a) in s <=> ~(a,a) in s]] <=> ~barber in m]]
>
> where
>
> v = the set of all village residents
> m = the set of men living in the village
> s = the shaving relation on v such that (x,y) in s means the x shaves y
> http://www.dcproof.com/BP12.htm

I should play with it, but it is not the barber paradox
and possibly not even a variant of it: for one thing,
in the original formulation, "shaves" is *any* binary
relation on the domain set (on v in your case), so I
should first ask why EXIST(s) in that nested scope
instead of ALL(s) in an outer scope?

Julio

[Mostowski Collapse]

Well material implication expresses semantical
necessesity. You can give it a semantical meaning,
not only a syntactic meaning by some inference rules.
The semantical meaning is very easy:

A B (A → B)
F F T
F T T
T F F
T T T

So semantical necessesity derives from the above
table. Thats all you need to know about material
implication to judge something for being a tautology
or a semantic conclusion, written as:

T |= A

Which is by Gödels completness theorem equivalent:

T |- A

Whats your point Culio?

[Mostowski Collapse]

Now olcott wants something different from the
classical semantical necessesity. And he wants
a non-classical semantical necessisty where
the drinker paradox fails. He started with using

a new symbol combination, or is two symbols?

T ⊨□ A

Or maybe he means:

T ⊨ □A

Mostlikely this step doesn't change anything.
Since most modal logics have the rule of necessesity.
Namely this modal operator introduction rule:

|= A
----------- (Rule N)
|= □A

If we apply this to the drinker paradox we get:

|= ∃x(Dx → ∀yDy)
-------------------------------- (Rule N)
|= □∃x(Dx → ∀yDy)

So the Drinker Paradox is still generally valid.
Even Wolfgang Schartz tool, which also provides
modal logic, can verify it:

□∃x(Dx → ∀yDy) is valid.
https://www.umsu.de/trees/#~8~7x(Dx~5~6yDy)

So whats your point Olcott?

[olcott]

On 3/19/2023 1:32 AM, Julio Di Egidio wrote:
> On Saturday, 18 March 2023 at 23:24:07 UTC+1, olcott wrote:
>> On 3/18/2023 5:09 PM, Mostowski Collapse wrote:
>>> But according to semantical necessesity it is valid:
>>> The non-empty pub is just the domain of discourse:
>>>
>>> ∃x(Dx → ∀yDy) is valid.
>>> https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
>>>
>>> But there is no assumption that there is a drinker.
>>> According to semantical necessesity this is not derivable:
>
> Notice that the moron Burse is writing "semantical
> necessesity" (sic) while talking of *material implication*,
> and that indeed has less than zero to do with semantics,
> which is the whole point with these seeming paradoxes!
>
>> If the Moon is made from green cheese then it is semantically necessary
>> that the Moon is made from cheese.
>
> Yeah, sort of. The relevant notion in Logic actually
> is called (logical) entailment, and a more appropriate
> example is: "(to be a) bachelor" entails "(to be) not
> married", by the meaning of "bachelor". Whence it
> is self-contradictor to say "married bachelor".
>
> Incidentally, semantics has to do with meaning, not
> the other way round. I.e. understanding language is
> and remains a *pre*requisite to the whole endeavour.
>

Semantic Necessity operator: ⊨□
Because my foundation of correct reasoning supersedes overrides and
replaces every aspect of other logic systems that contradict it I
created a brand new logical operator.

"There is someone in the pub such that, if he or she is drinking, then
everyone in the pub is drinking."

⊨□ there is only one person in the pub.

>> "There is someone in the pub such that, if he or she is drinking, then
>> everyone in the pub is drinking."
>
> In natural language it goes like this:
>
> By the law of excluded middle, we can assume
> that either everybody is drinking or someone is
> not drinking. We then proceed by case analysis:
>
> In case everybody is drinking, the statement is
> trivially true.
>
> In case someone is not drinking, pick anyone who
> is not drinking, call them x. Use x as the witness
> for the statement in question, such that the
> statement becomes "if x is drinking, then everyone
> in the pub is drinking." And now consider that x is
> in fact *not* drinking, whence, by ex falso quodlibet,
> the conclusion holds.

ex falso quodlibet, is a bogus kludge that my foundations of correct
reasoning abolishes.

FALSE ⊨□ FALSE
(A & ~A) ⊨□ FALSE

>
> It does use LEM plus some choice principle, but the
> whole thing can be reformulated constructively over
> some decidable types. What is essential to this
> "paradox", to reiterate what I have said initially, is
> *(material) implication* and how very little it has to
> do with logical consequence/entailment.
>
> Julio

[Mostowski Collapse]

If you want to make the Drinker Paradox fail,
you don't need to change consequence relation
|=, try changing the implication itself ->,

this will possibly give you what is described here,
if you have made the strides to learn how strict
implication can be modelled in modal logic:

The Drinker Paradox and its Dual - Louis Warren et al., 2018
https://ir.canterbury.ac.nz/bitstream/handle/10092/16234/1805.06216v1.pdf

As a start you can try a simpler problem.
For example is this here non-classically valid?

(A -> B) v (B -> A)

Or an exacble with A,B which show little
relevance to each other:

if the moon is made of cheese
then pigs can fly or
if pigs can fly then the moon is
made of cheese

Classical logic would say the above is a tautology.

(A→B) ∨ (B→A) is valid.
https://www.umsu.de/trees/#(A~5B)~2(B~5A)

[olcott]

On 3/19/2023 9:11 AM, Mostowski Collapse wrote:
> Well material implication expresses semantical
> necessesity. You can give it a semantical meaning,
> not only a syntactic meaning by some inference rules.
> The semantical meaning is very easy:
>
> A B (A → B)
> F F T
> F T T
> T F F

Logical implication
p q p ⇒ q
F F T
If the Moon is made from Green cheese then the Moon is made from cheese

F T T
If the Moon is made from Green cheese then the Moon is made from something

T F F
If the Moon is made from dirt and rock then the Moon is made from green
cheese

T T T
If the Moon orbits the Earth then the Earth is orbited by the Moon

[olcott]

I have had more time to think about this.
Semantic Necessity operator: ⊨□

"There is someone in the pub such that, if he or she is drinking, then
everyone in the pub is drinking."

The above semantically entails that there is only one person in the pub.
∃x(Dx → ∀yDy) ∴ ∀y = x

>

[olcott]

On 3/19/2023 9:23 AM, Mostowski Collapse wrote:
> If you want to make the Drinker Paradox fail,
> you don't need to change consequence relation
> |=, try changing the implication itself ->,
>
> this will possibly give you what is described here,
> if you have made the strides to learn how strict
> implication can be modelled in modal logic:
>
> The Drinker Paradox and its Dual - Louis Warren et al., 2018
> https://ir.canterbury.ac.nz/bitstream/handle/10092/16234/1805.06216v1.pdf
>
> As a start you can try a simpler problem.
> For example is this here non-classically valid?
>
> (A -> B) v (B -> A)
>
> Or an exacble with A,B which show little
> relevance to each other:
>
> if the moon is made of cheese
> then pigs can fly or
> if pigs can fly then the moon is
> made of cheese
>
> Classical logic would say the above is a tautology.
>

The lack of semantic connection makes it bogus.

Socrates is a man
all men are mortal
∴ Socrates likes to watch soccer on TV

The foundation of correct reasoning restores the semantic connection of
the syllogism.

[Dan Christensen]

On Sunday, March 19, 2023 at 4:00:02 AM UTC-4, Julio Di Egidio wrote:
> On Sunday, 19 March 2023 at 04:18:12 UTC+1, Dan Christensen wrote:
> > On Sunday, March 5, 2023 at 6:03:51 AM UTC-5, Julio Di Egidio wrote:
> > > I am learning Coq (which is based on constructive logic), so
> > > I thought let's look at the Barber's Paradox, i.e. let's see if I can
> > > get a "contradiction"
> >
> > [snip]
> >
> > Can this result be obtained in Coq:
> >
> > 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):[a in m => [(barber,a) in s <=> ~(a,a) in s]] <=> ~barber in m]]
> >
> > where
> >
> > v = the set of all village residents
> > m = the set of men living in the village
> > s = the shaving relation on v such that (x,y) in s means the x shaves y
> > http://www.dcproof.com/BP12.htm

> I should play with it, but it is not the barber paradox

You might think of it as an attempt to get at what might be called the "root cause" of the problem. It is not the existence of the barber that is problematic, but the gender of the barber. The use of set theory seems inevitable in proving that, "in an village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves IF AND ONLY IF that barber is not a man."

> and possibly not even a variant of it: for one thing,
> in the original formulation, "shaves" is *any* binary
> relation on the domain set (on v in your case), so I
> should first ask why EXIST(s) in that nested scope
> instead of ALL(s) in an outer scope?
>

See lines 18-29. There I construct, i.e. prove the existence of the set of ordered pairs s using my Cartesian Product Axiom on line 18, and Subset Axiom on line 26.

[Julio Di Egidio]

On Sunday, 19 March 2023 at 16:18:04 UTC+1, Dan Christensen wrote:
> On Sunday, March 19, 2023 at 4:00:02 AM UTC-4, Julio Di Egidio wrote:
> > On Sunday, 19 March 2023 at 04:18:12 UTC+1, Dan Christensen wrote:
> > > On Sunday, March 5, 2023 at 6:03:51 AM UTC-5, Julio Di Egidio wrote:
> > > > I am learning Coq (which is based on constructive logic), so
> > > > I thought let's look at the Barber's Paradox, i.e. let's see if I can
> > > > get a "contradiction"
> > >
> > > [snip]
> > >
> > > Can this result be obtained in Coq:
> > >
> > > 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):[a in m => [(barber,a) in s <=> ~(a,a) in s]] <=> ~barber in m]]
> > >
> > > where
> > > v = the set of all village residents
> > > m = the set of men living in the village
> > > s = the shaving relation on v such that (x,y) in s means the x shaves y
> > > http://www.dcproof.com/BP12.htm
>
> > I should play with it, but it is not the barber paradox
>
> You might think of it as an attempt to get at what might be called the "root cause" of the problem. It is not the existence of the barber that is problematic, but the gender of the barber. The use of set theory seems inevitable in proving that, "in an village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves IF AND ONLY IF that barber is not a man."

Which makes of it simply a variant of the original problem,
since it is a theorem of (constructive) logic, that I have shown
initially in this thread (in Coq), that *there is no such barber*,
and what you do is enlarge the domain of discourse and rather
place the barber outside the original domain. And I am not
even sure how is that supposed to type-check, the 's' relation
in particular...

But indeed, even before that, I am still not sure what you are
actually proving, especially since, as I have pointed out, the
original theorem is about *any* binary relation on the domain
of discourse (which is what makes it interesting beyond any
"contingencies") while you bring into existence a specific
one... and you haven't addressed that point at all.

Julio