Erroneous conclusions from applying material conditionals?

[Dan Christensen]

What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present? (Hint: None?)

Dan

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

[Ross Finlayson]

How do you define "time"? How about "eternity"?

If it's false that time exists, isn't according to material implication it's forever?

Demonstrate any one true thing, that is only true and provable,
only by material implication, or otherwise give any reason why
material implication is a "necessity" and not just a "oxymoronic
non-conditional in a world of connectives of conditionals of the causal",
then for example that "in non-trivial theories with a modality of time,
show that anything that ever changes from false to true or correspondingly
its negation, invalidates what all were the 'material implications' that always
get constructed by expansion of comprehension in where otherwise,
according to expansion of comprehension, any that can does exist".


"All Cretans are liars?" "Yeah, the last one just died."

[Dan Christensen]

On Saturday, May 27, 2023 at 4:25:14 PM UTC-4, Ross Finlayson wrote:
> On Saturday, May 27, 2023 at 12:04:05 PM UTC-7, Dan Christensen wrote:
> > What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present? (Hint: None?)
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> How do you define "time"? How about "eternity"?
>
> If it's false that time exists, isn't according to material implication it's forever?
>

"Time exists" is not an unambiguously either true or false proposition in the present. Likewise, "It's forever."

> Demonstrate any one true thing, that is only true and provable,
> only by material implication, or otherwise give any reason why
> material implication is a "necessity" and not just a "oxymoronic
> non-conditional in a world of connectives of conditionals of the causal",
> then for example that "in non-trivial theories with a modality of time,
> show that anything that ever changes from false to true or correspondingly
> its negation, invalidates what all were the 'material implications' that always
> get constructed by expansion of comprehension in where otherwise,
> according to expansion of comprehension, any that can does exist".
>
> "All Cretans are liars?" "Yeah, the last one just died."

Ummm... It take you cannot give an example of even a single erroneous conclusion that might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present. Thanks anyway.

[Mild Shock]

The Generalized Drinker Paradox, like here:

ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

Its shows that the material implication can be quite challenging.

[Dan Christensen]

On Sunday, May 28, 2023 at 11:39:07 AM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Samstag, 27. Mai 2023 um 21:04:05 UTC+2:
> > What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present? (Hint: None?)

> The Generalized Drinker Paradox, like here:
>
> ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
> http://www.dcproof.com/STGeneralizedDrinkersThm.htm
>
> Its shows that the material implication can be quite challenging.

"Challenging?" Can you be more specific? Nowhere, for example, is the principle of vacuous truth invoked (the Arbitrary Consequent Rule, Arb Cons: P => (~P => Q)). Likewise the Arbitrary Antecedent Rule (Arb Ant: P => (Q => P)).

[Mild Shock]

This here uses Rem DNeg a couple of times:
http://www.dcproof.com/UniversalSet.htm

This here uses Rem DNeg once:
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

An intuitionistic proof would not use ~~A -> A.
But searching for intuitionistic proofs is much harder

than searching for classical proofs.

[Mild Shock]

Material implication is critizised for obeying two laws,
because it is seen as (A => B) == (~A v B):

Law of noncontradiction (LNC)
Formally this is expressed as the tautology ¬(p ∧ ¬p).
https://en.wikipedia.org/wiki/Law_of_noncontradiction

Law of excluded middle (LEM)
precise statement of the law of excluded middle, P ∨ ~P
https://en.wikipedia.org/wiki/Law_of_excluded_middle

Intuitionistic Logic accepts LNC, but rejects LEM.
~~A -> A needs both LNC and LEM. But it fails in
intuitionistic logic, because intuitionistic logic

rejects LEM. But as long as you accept ~~A -> A,
you are swimming in the pool of material implication.
And this pool is affected by some anomalies due to

LEM, such as the existence of this paradox:

Banach–Tarski paradox
https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox

In this case, the issue is that the entire concept of partitions
and equivalence classes, which underlies the usual proof of
he Banach-Tarski paradox, behaves very differently in constructive systems.
https://math.stackexchange.com/questions/175675/intuitionistic-banach-tarski-paradox

[Mild Shock]

Of course if you have ~~A -> A available you can
show LNC = LEM, by using de Morgan and Rem DNeg:

/* LNC = LEM */
¬(p ∧ ¬p) = ¬p ∨ ¬¬p = ¬p ∨ p

The last step uses Rem DNeg, i.e. ~~A -> A. If
Rem DNeg is not available, then LNC and LEM are

not the automatically the same as shown above.

Mild Shock schrieb am Sonntag, 28. Mai 2023 um 22:57:23 UTC+2:
> Material implication is critizised for obeying two laws,
> because it is seen as (A => B) == (~A v B):
>
> Law of noncontradiction (LNC)
> Formally this is expressed as the tautology ¬(p ∧ ¬p).
> https://en.wikipedia.org/wiki/Law_of_noncontradiction
>
> Law of excluded middle (LEM)

> precise statement of the law of excluded middle, p ∨ ¬p

[olcott]

On 5/28/2023 3:57 PM, Mild Shock wrote:
> Material implication is critizised for obeying two laws,
> because it is seen as (A => B) == (~A v B):
>
> Law of noncontradiction (LNC)
> Formally this is expressed as the tautology ¬(p ∧ ¬p).
> https://en.wikipedia.org/wiki/Law_of_noncontradiction
>
> Law of excluded middle (LEM)
> precise statement of the law of excluded middle, P ∨ ~P
> https://en.wikipedia.org/wiki/Law_of_excluded_middle
>
> Intuitionistic Logic accepts LNC, but rejects LEM.
> ~~A -> A needs both LNC and LEM. But it fails in
> intuitionistic logic, because intuitionistic logic
>
> rejects LEM. But as long as you accept ~~A -> A,
> you are swimming in the pool of material implication.
> And this pool is affected by some anomalies due to
>
> LEM, such as the existence of this paradox:
>
> Banach–Tarski paradox
> https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox

*Here is my take on that*
When you reconstruct a pair of spheres from one sphere they are no
longer perfectly spherical in that they are now comprised of line
segments of infinitesimal length.

>
> In this case, the issue is that the entire concept of partitions
> and equivalence classes, which underlies the usual proof of
> he Banach-Tarski paradox, behaves very differently in constructive systems.
> https://math.stackexchange.com/questions/175675/intuitionistic-banach-tarski-paradox
>
> Mild Shock schrieb am Sonntag, 28. Mai 2023 um 22:47:33 UTC+2:
>> This here uses Rem DNeg a couple of times:
>> http://www.dcproof.com/UniversalSet.htm
>>
>> This here uses Rem DNeg once:
>> http://www.dcproof.com/STGeneralizedDrinkersThm.htm
>>
>> An intuitionistic proof would not use ~~A -> A.
>> But searching for intuitionistic proofs is much harder
>>
>> than searching for classical proofs.
>> Dan Christensen schrieb am Sonntag, 28. Mai 2023 um 21:01:54 UTC+2:
>>> On Sunday, May 28, 2023 at 11:39:07 AM UTC-4, Mild Shock wrote:
>>>
>>>> Dan Christensen schrieb am Samstag, 27. Mai 2023 um 21:04:05 UTC+2:
>>>>> What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present? (Hint: None?)
>>>
>>>> The Generalized Drinker Paradox, like here:
>>>>
>>>> ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
>>>> http://www.dcproof.com/STGeneralizedDrinkersThm.htm
>>>>
>>>> Its shows that the material implication can be quite challenging.
>>> "Challenging?" Can you be more specific? Nowhere, for example, is the principle of vacuous truth invoked (the Arbitrary Consequent Rule, Arb Cons: P => (~P => Q)). Likewise the Arbitrary Antecedent Rule (Arb Ant: P => (Q => P)).
>>> Dan
>>>
>>> Download my DC Proof 2.0 freeware at http://www.dcproof.com
>>> Visit my Math Blog at http://www.dcproof.wordpress.com

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

[Dan Christensen]

On Sunday, May 28, 2023 at 4:47:33 PM UTC-4, Mild Shock wrote:


> Dan Christensen schrieb am Sonntag, 28. Mai 2023 um 21:01:54 UTC+2:
> > On Sunday, May 28, 2023 at 11:39:07 AM UTC-4, Mild Shock wrote:
> >
> > > Dan Christensen schrieb am Samstag, 27. Mai 2023 um 21:04:05 UTC+2:
> > > > What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present? (Hint: None?)


> > > The Generalized Drinker Paradox, like here:
> > >
> > > ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
> > > http://www.dcproof.com/STGeneralizedDrinkersThm.htm
> > >
> > > Its shows that the material implication can be quite challenging.

> > "Challenging?" Can you be more specific? Nowhere, for example, is the principle of vacuous truth invoked (the Arbitrary Consequent Rule, Arb Cons: P => (~P => Q)). Likewise the Arbitrary Antecedent Rule (Arb Ant: P => (Q => P)).

> This here uses Rem DNeg a couple of times:
> http://www.dcproof.com/UniversalSet.htm
>
> This here uses Rem DNeg once:
> http://www.dcproof.com/STGeneralizedDrinkersThm.htm
>

[snip]

So what? Removing '~~' is a widely accepted method of proof.

Anyway, this does not answer my question: What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present?

[Dan Christensen]

On Sunday, May 28, 2023 at 4:57:23 PM UTC-4, Mild Shock wrote:

> > Dan Christensen schrieb am Sonntag, 28. Mai 2023 um 21:01:54 UTC+2:
> > > On Sunday, May 28, 2023 at 11:39:07 AM UTC-4, Mild Shock wrote:
> > >
> > > > Dan Christensen schrieb am Samstag, 27. Mai 2023 um 21:04:05 UTC+2:
> > > > > What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present? (Hint: None?)
> > >
> > > > The Generalized Drinker Paradox, like here:
> > > >
> > > > ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
> > > > http://www.dcproof.com/STGeneralizedDrinkersThm.htm
> > > >
> > > > Its shows that the material implication can be quite challenging.
> > > "Challenging?" Can you be more specific? Nowhere, for example, is the principle of vacuous truth invoked (the Arbitrary Consequent Rule, Arb Cons: P => (~P => Q)). Likewise the Arbitrary Antecedent Rule (Arb Ant: P => (Q => P)).

> Material implication is critizised for obeying two laws,
> because it is seen as (A => B) == (~A v B):
>
> Law of noncontradiction (LNC)
> Formally this is expressed as the tautology ¬(p ∧ ¬p).
> https://en.wikipedia.org/wiki/Law_of_noncontradiction
>
> Law of excluded middle (LEM)
> precise statement of the law of excluded middle, P ∨ ~P
> https://en.wikipedia.org/wiki/Law_of_excluded_middle
>

[snip]

It would be even more widely criticized if material conditional did NOT obey those widely accepted methods of proof.

Again, you have not answered my question: What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present?

[Mild Shock]

Maybe pay more attention you blisteriung idiot. You
are a fucking Liar!. I wrote, what you willfully did hide in
your nonsense [snip], an example of a non-constructive proof:

Mild Shock schrieb am Sonntag, 28. Mai 2023 um 22:57:23 UTC+2:
> you are swimming in the pool of material implication.
> And this pool is affected by some anomalies due to
> LEM, such as the existence of this paradox:
>
> Banach–Tarski paradox
> https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox
>
> In this case, the issue is that the entire concept of partitions

> and equivalence classes, which underlies the usual proof of the

> Banach-Tarski paradox, behaves very differently
> in constructive systems.
> https://math.stackexchange.com/questions/175675/intuitionistic-banach-tarski-paradox

https://groups.google.com/g/sci.logic/c/UyUeW6187tw/m/jzZSSD1_AwAJ

Whats wrong with you? Why [snip] and then ask?

[Mild Shock]

There are like dozen or so theorems in real analysis
that mostly don't work in a constructive setting.
Just google it. Not that difficult to find.

Disclaimer: Constructive settings can slightly
vary. And also I have no sketch concerning the
Banach–Tarski paradox on a back of an envelope

what Carl Mummert is hinting at. Maybe the simplest
example where LEM leaves one puzzled is the
failure that a proof A v B, leads either to a proof of

A or a proof B. Which would be an ingredient of
"constructive", but which is not present in classical logic
and material implication, because it accepts LEM:

Constructive gem: irrational to the power of irrational that is rational
https://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/

[Mild Shock]

You find also a remark by Terrence Tao in the post by
Andrej Bauer. I guess Terrence Tao is already past the
question mark "what is material implication"?

Maybe you can learn about "material implication"
from Terence Tao? Although I don't know how prolific
he is in constructive math, maybe try a little Andrej Bauer.

[Mild Shock]

John Gabriel was prolific in avoiding the pitfalls of
material implication. He repeatedly claimed to posses
a "constructive" mean value theorem.

"(c) John Gabriel, Discoverer of the New Calculus.
The first constructive proof of the mean value
theorem was produced by me."
https://thenewcalculus.weebly.com/

Although we have:

"In constructive mathematics, the mean-value theorems
generally cannot be proved, since it may be impossible
to find the value c."
https://ncatlab.org/nlab/show/mean+value+theorem

[Dan Christensen]

On Sunday, May 28, 2023 at 6:56:38 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

> > Again, you have not answered my question: What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present?

[snip same old childish abuse]

> I wrote, what you willfully did hide in
> your nonsense [snip], an example of a non-constructive proof:

> Mild Shock schrieb am Sonntag, 28. Mai 2023 um 22:57:23 UTC+2:
> > you are swimming in the pool of material implication.
> > And this pool is affected by some anomalies due to
> > LEM, such as the existence of this paradox:
> >
> > Banach–Tarski paradox
> > https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox
> >

You were asked for an example of an erroneous conclusion that might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present. If you are going to claim that BTP is such a result, you have lot of work ahead of you. To get started, you must formally disprove BTP. Fame and fortune await, Mr. Collapse! (Hee, hee!)

[Mild Shock]

Dan Christensen halucinated:

> logical propositions that are unambiguously either true
> or false in the present

Define "present". Did you see a perfect unit circle
that satisfies this here:

x^2 + y^2 = 1

in the "present"? material implication has nothing to do
with truth in some "present".

Whats wrong with you? Material implication is not some
measurement device. If we have material implication as:

(A => B) == (~A v B)

What makes you think it can generate more than analytic
"truth", i.e. real "truth"?

The analytic–synthetic distinction is a semantic distinction, used
primarily in philosophy to distinguish between propositions (in
particular, statements that are affirmative subject–predicate judgments)
that are of two types: analytic propositions and synthetic propositions.
Analytic propositions are true or not true solely by virtue of their
meaning, whereas synthetic propositions' truth, if any, derives from how
their meaning relates to the world.
https://en.wikipedia.org/wiki/Analytic%E2%80%93synthetic_distinction

Dan Christensen schrieb:

[Mild Shock]

Although the name is "material implication", it
doesn't designate material truth which is
synonymous to synthetic propositions' truth.

"material implication" still belongs to formal
truth and is tied to the intricacies of having
a theory of the world. Roughly I guess it is the case:

In a construtive theory of the world:
The Banach Tarski construction possibly doesn't work.

In a non-constructive theory of the world:
The Banach Tarski construction possibly does work.

"material implication" is only the name of this identity:
(A=>B) = (~A v B)
Material implication (rule of inference)

But its not a license for material truth. I don't
know the ethymology of metarial implication right
now, why people call it that way.

Do you know?

Mild Shock schrieb:

[Mild Shock]

Of course if your world is simple, there is not
much choice of a constructive or non-constructive
modelling, like for example this here:

man(socrates)

Makes a nice world fact. But then already a rule like:

∀x(man(x) -> mortal(x))

Is not anymore "material truth". Where do you
see rules inscribed in the "present"?

So how do you want to know that there is no error here:

man(socrates), ∀x(man(x) -> mortal(x)) |- mortal(socrates)

Maybe John Gabriel resurrected and he is immortal
now, so that we have a counter example to

∀x(man(x) -> mortal(x)):

In the form of:

man(jg), ~mortal(jg)

LoL

Mild Shock schrieb:

[Dan Christensen]

On Sunday, May 28, 2023 at 8:27:11 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

[snip]

> Define "present".

[snip]

Every mathematical proposition can be thought as being in the present tense, e.g. 2 plus 2 equals 4 (present tense).

> Material implication is not some
> measurement device. If we have material implication as:
> (A => B) == (~A v B)

That would do, but I prefer the equivalent ~(A & ~B).

> What makes you think it can generate more than analytic
> "truth", i.e. real "truth"?
>

[snip]

Please answer the original question if you can: What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present?

[Mild Shock]

I already answered the question. The problem is you
don't pay attention. You don't listen. You are dumb. You
cannot think Here it is again a summary Banach-Tarski.

a) Take the proposition we have a sphere.
b) Take the conlusion we can chop it into 3 spheres.

Material implication makes a errorneous conclusion.
The proof goes usually like this:

Proof: That there is an error.
a) The sphere has volume V. b) the 3 spheres have
volume 3*V. Its not possible to constructively rearrange
matter so that the volume increases. All construcitive
operations preserve the volume.
Q.E.D.

[Dan Christensen]

On Sunday, May 28, 2023 at 8:45:09 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> Of course if your world is simple, there is not
> much choice of a constructive or non-constructive
> modelling, like for example this here:
>
> man(socrates)
>
> Makes a nice world fact. But then already a rule like:
>
> ∀x(man(x) -> mortal(x))
>

man(x) can be taken to mean that x is a man (present tense), etc.

> Is not anymore "material truth". Where do you
> see rules inscribed in the "present"?
>
> So how do you want to know that there is no error here:
>
> man(socrates), ∀x(man(x) -> mortal(x)) |- mortal(socrates)
>

Please answer the original question if you can: What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present?

[Mild Shock]

The argument assumes that the resulting sphere are the
same mass density as the original sphere, like all are from
the same glass, some marble toy, in room temperature.

How do you get more mass?

This would solve the world energy problem.

Hope this Helps!

[Mild Shock]

Ha Ha,

just visit Dan Christensen, ask him for a little
material implication, and peng everybody on the
planet is happy, infinite energy forever and ever!

Even for Putin it is now game over,
no more gas games during winter!

There is also a Dan Christensen patented
perpetuum mobile, called material implication
bicycle, and then something still in the

working, material implication Nuremberg
Funnel, it will make anybody smart, even the
dumbest nut head on this planet.

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

[Dan Christensen]

On Sunday, May 28, 2023 at 8:51:23 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

> Dan Christensen schrieb am Montag, 29. Mai 2023 um 02:46:21 UTC+2:
> > Please answer the original question if you can: What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present?

> I already answered the question. The problem is you
> don't pay attention. You don't listen. You are dumb. You
> cannot think Here it is again a summary Banach-Tarski.
>
> a) Take the proposition we have a sphere.
> b) Take the conlusion we can chop it into 3 spheres.
>
> Material implication makes a errorneous conclusion.
> The proof goes usually like this:
>
> Proof: That there is an error.
> a) The sphere has volume V. b) the 3 spheres have
> volume 3*V. Its not possible to constructively rearrange
> matter so that the volume increases. All construcitive
> operations preserve the volume.

That is your claim. Now formally prove it.

[Mild Shock]

It has a section proof:

> Proof: That there is an error.
> a) The sphere has volume V. b) the 3 spheres have
> volume 3*V. Its not possible to constructively rearrange

> matter so that the volume increases. All constructive
> operations preserve the volume.
> Q.E:D:

Whats wrong with you. The proof is V =\= 3*V.
Or simpler 1 =\= 3. You can use your Peano Axioms
in DC Proof for that.

[Dan Christensen]

On Sunday, May 28, 2023 at 9:12:05 PM UTC-4, Dan Christensen wrote:
> On Sunday, May 28, 2023 at 8:51:23 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
>
> > Dan Christensen schrieb am Montag, 29. Mai 2023 um 02:46:21 UTC+2:
> > > Please answer the original question if you can: What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present?
> > I already answered the question. The problem is you
> > don't pay attention. You don't listen. You are dumb. You
> > cannot think Here it is again a summary Banach-Tarski.
> >
> > a) Take the proposition we have a sphere.
> > b) Take the conlusion we can chop it into 3 spheres.
> >
> > Material implication makes a errorneous conclusion.
> > The proof goes usually like this:
> >
> > Proof: That there is an error.
> > a) The sphere has volume V. b) the 3 spheres have
> > volume 3*V. Its not possible to constructively rearrange
> > matter so that the volume increases. All construcitive
> > operations preserve the volume.
> That is your claim. Now formally prove it.

Alternatively, formalize the original proof of BTP and identify where it supposedly goes wrong.

[Mild Shock]

You have an attention span like a snail. Whats wrong with you.
I already wrote were it goes wrong. See the last section here,
I refering to a post by Carl Mummert:

> Material implication is critizised for obeying two laws,
> because it is seen as (A => B) == (~A v B):
>
> Law of noncontradiction (LNC)
> Formally this is expressed as the tautology ¬(p ∧ ¬p).
> https://en.wikipedia.org/wiki/Law_of_noncontradiction
>
> Law of excluded middle (LEM)
> precise statement of the law of excluded middle, P ∨ ~P
> https://en.wikipedia.org/wiki/Law_of_excluded_middle
>

> Intuitionistic Logic accepts LNC, but rejects LEM.
> ~~A -> A needs both LNC and LEM. But it fails in
> intuitionistic logic, because intuitionistic logic
>
> rejects LEM. But as long as you accept ~~A -> A,

> you are swimming in the pool of material implication.
> And this pool is affected by some anomalies due to
>
> LEM, such as the existence of this paradox:
>
> Banach–Tarski paradox
> https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox
>

> In this case, the issue is that the entire concept of partitions
> and equivalence classes, which underlies the usual proof of
> the Banach-Tarski paradox, behaves very differently in constructive systems.
> https://math.stackexchange.com/questions/175675/intuitionistic-banach-tarski-paradox

But you might try something simpler, like Vitali set
or somesuch. Don't know. I am only the conveyor of a message.
I already wrote as well:

> Disclaimer: Constructive settings can slightly
> vary. And also I have no sketch concerning the
> Banach–Tarski paradox on a back of an envelope
>
> what Carl Mummert is hinting at. Maybe the simplest
> example where LEM leaves one puzzled is the
> failure that a proof A v B, leads either to a proof of
>
> A or a proof B. Which would be an ingredient of
> "constructive", but which is not present in classical logic
> and material implication, because it accepts LEM:
>
> Constructive gem: irrational to the power of irrational that is rational
> https://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/

[Mild Shock]

The Nuremberg Funnel works as follows. It is just
an application of the Banach Tarski theorem. So if
somebody has only a brain with IQ 40.

You just apply the Banach Tarski theorem once,
and your brain sphere duplicates into 3 brain
spheres, eh voila you have IQ 120.

[Dan Christensen]

On Sunday, May 28, 2023 at 9:23:14 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
[snip childish abuse]

> I already wrote were it goes wrong. See the last section here,
> I refering to a post by Carl Mummert:
> > Material implication is critizised for obeying two laws,
> > because it is seen as (A => B) == (~A v B):
> >
> > Law of noncontradiction (LNC)
> > Formally this is expressed as the tautology ¬(p ∧ ¬p).
> > https://en.wikipedia.org/wiki/Law_of_noncontradiction
> >
> > Law of excluded middle (LEM)
> > precise statement of the law of excluded middle, P ∨ ~P
> > https://en.wikipedia.org/wiki/Law_of_excluded_middle
> >

Pay attention, Mr. Collapse! Again, these laws are legitimate methods of proof that are widely accepted by the vast majority of mathematicians. It is rejected only by a fringe element, the self-styled "constructionists." If you want your work to be widely accepted, this is probably the worst possible approach.

> > Banach–Tarski paradox
> > https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox
> >
> > In this case, the issue is that the entire concept of partitions
> > and equivalence classes, which underlies the usual proof of
> > the Banach-Tarski paradox, behaves very differently in constructive systems.

[snip]

You mean "constructive" (aka fringe) systems???

[Ross Finlayson]

Hey, you just learned there "exists" constructivism, it's not "fringe", it's a central effort
in _rigorous formalism for mathematics_.

I.e., some constructivists have the "non-constructive" is not even _sound_, and is at
best incomplete and not self-contradictory.

Then, about Banach-Tarski, what the Burse-bot there is doing is what's called
"talking out the ass", because it's just something you don't know, and whether
"the devil made you do it" is a sufficient "arbitrary consequent" or "arbitrary antecedent"
would suffice, something "you don't know".

About Banach-Tarski, there are two at-odds approaches, one's plainly geometric and
is for Vitali-Hausdorff. Another is plainly geometric and for, say, Micielski-Marczewski.

Here's a thread about "Banach-Tarski". Of course, I think what I write is most informative,
and I understand that's subjective.

https://groups.google.com/g/sci.logic/c/UFQub2CKXQo/m/eksBibcTAQAJ

One hopes that someday you might understand
that "ALGEBRAIC geometry" is not "algebraic GEOMETRY".



"So, you can see that "re-Vitali-ization" is ongoing in
mathematics writ large, and quite more accessibly these
days then that as the dust arises of the construction,
it all has to settle to the foundations again. Then,
looking to "re-Vitali-ize" measure as from some quite
fundamental notions as the spiral-space-filling curve
and unique properties of the equivalency function (in
continuity, analysis, differential analysis, singularity
theory, and probability theory) makes a neat course for
then laying out what are building up as these quite
immense structures in categorical algebra in descriptive
set theory, as somewhat neatly primitive (and accordingly
fundamental)."

"Too wordy?"



"It's a "spherical group".

One's geometry's, the other algebra's.

This is in "dynamical topology" in "descriptive set theory". "



"Now, why this relates to Marczewski-Dougherty-Foreman's
Banach-Tarski's is because the "group paradoxical action"
that was set under "decomposition paradoxical action"
(so they didn't look "stupid" or plain "wrong" or otherwise
have to defend another "paradox") is these days being disambiguated
from where they were framed together in the corresponding
systems together.

This arrives full-circle at Zeno. "



Of course you can always read Burse instead:
"Lol, banach-tarski-fication of herpes boy" - Burse.



Ross:

"This then is for such notions about
Szpilrajn that these days are framed
in notions of "transfer principle"
and "antitransfer principle", but
re-using the development without
re-seating the terms leaves a bit
of an inconsistency in the middle
that naive inference could work out
either way.

Informed inference though is rather
setting such notions in the first-class
where they belong and able to redress
such hand-waving abandonment of topology's
usual difference between results in union
and results in intersection about the
special or limit cases for the transfer
principle where such infinitary results
would be disambiguated to hold or not.


classical geometry -> "paradoxical" decompositions
algebraic geometry -> "paradoxical" group actions

"... as long as we have two copies here,
might as well just stop at the first
and call it the action, though we'll
frame it in the results of the second."

But, really it's that both meet in the middle
(and either way, under some ambiguous assumptions).

So, one might neatly consider a theory of
Banach-Tarski as independent of some usual
assumptions, here basically under topology
and of course as here about that being under
all these usual assumptions of measure, and
whether for example it's "area", as least
under the quadratic , or, "volume", as
under the sphere. "



"An anagram of Banach-Tarski's Paradox
is Marczewski-Swierczkowski's Banach-Tarski's Paradox".

"Here then Banach and Tarski's development
is Banach and Tarski's, vis-a-vis, variously,
Groot, Steinhaus, Swierczkowski, and
algebraic interpretations. "


"That appears to be among Hausdorff's theorems, there (and see above)."

[Ross Finlayson]

The original development of Banach and Tarski
is more "geometric" than "algebraic", more
about "congruences" than "generators", and
constructively.



Here, I wrote this:


Looking to Banach's and Tarski's paper:

http://matwbn.icm.edu.pl/ksiazki/fm/fm6/fm6127.pdf

With for example "Grace a une remarque due a M.Lindenbaum,
on peut enoncer un theoreme analogue au lemme precedent
pour les ensembles lineaires, in remplacant le term "segment"
par "point"."

Then it seems that Banach Tarski are using:
Vitali "we have non-measurable sets"
Lindenbaum "hi these are Veronese's"
Hausdorff "I spun Vitali's around for a 2-D analogue"
that Banach Tarski are coming across then
as "there's certainly enough here to find
some non-measurable ones then what
Hausdorff said holds and it doesn't matter
that our actual constructions don't add up
because they're non-measurable because
they're non-measurable there are uncountably
many to get them all and Vitali points out how
they double up".

So, the development on the Banach-Tarski wiki
is not Banach and Tarski's.

"Comme l' indique M.Hausdorff (en utilisant
une idee M.Vitali) on peut decompose tout
segment en une infinite nombrable de sous-
ensembles disjoints equivalents par decomposition
finite deux a deux. Soient: ..."

-- http://matwbn.icm.edu.pl/ksiazki/fm/fm6/fm6127.pdf

[Dan Christensen]

On Monday, May 29, 2023 at 12:51:51 AM UTC-4, Ross Finlayson wrote:

> > > > Material implication is critizised for obeying two laws,
> > > > because it is seen as (A => B) == (~A v B):
> > > >
> > > > Law of noncontradiction (LNC)
> > > > Formally this is expressed as the tautology ¬(p ∧ ¬p).
> > > > https://en.wikipedia.org/wiki/Law_of_noncontradiction
> > > >
> > > > Law of excluded middle (LEM)
> > > > precise statement of the law of excluded middle, P ∨ ~P
> > > > https://en.wikipedia.org/wiki/Law_of_excluded_middle
> > > >
> > Pay attention, Mr. Collapse! Again, these laws are legitimate methods of proof that are widely accepted by the vast majority of mathematicians. It is rejected only by a fringe element, the self-styled "constructionists." If you want your work to be widely accepted, this is probably the worst possible approach.
> > > > Banach–Tarski paradox
> > > > https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox
> > > >
> > > > In this case, the issue is that the entire concept of partitions
> > > > and equivalence classes, which underlies the usual proof of
> > > > the Banach-Tarski paradox, behaves very differently in constructive systems.
> > [snip]
> >
> > You mean "constructive" (aka fringe) systems???

> Hey, you just learned there "exists" constructivism, it's not "fringe", it's a central effort
> in _rigorous formalism for mathematics_.
>

[snip]

A really tough sell in mainstream mathematics by the looks of it. Don't expect a breakthrough any time soon.

Dan

[Mild Shock]

Material Implication when given as: (A => B) == (~A v B),
can show that LEM is the same as I-Axiom, which is
admissible in Łukasiewicz's third axiom systems:

(A => A) = (~A v A)

But interestingly under the BHK interpretation, intuitionstic
logic can also do (A => A), its also a theorem in intuitionistic
logic, although it rejects LEM.

How is this possible. Well its possible since intuitionistic
logic it is rejected (A => B) == (~A v B). In intuitionistic logic
we have (A => B) =\= (~A v B).

This is quite amazing that we nevertheless have
(A => A) in intuitionistic logic, where the BHK interpretation
would say the function that sends proofs of A to

proofs of A is simply the identity function.

Mild Shock schrieb am Sonntag, 28. Mai 2023 um 17:39:07 UTC+2:
> The Generalized Drinker Paradox, like here:
>
> ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
> http://www.dcproof.com/STGeneralizedDrinkersThm.htm
>
> Its shows that the material implication can be quite challenging.

> Dan Christensen schrieb am Samstag, 27. Mai 2023 um 21:04:05 UTC+2:

> > What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present? (Hint: None?)

[Mild Shock]

The BHK interpretation is interesting, since it covers
the notion of proof in a new way different from material
implication. So to arrive from some premisses A

to some conclusion B, to have (A => B) valid, it does
not draw on the truth table of material implication, but
wants a justification in a form of a function f:

Justification of A => B, is a function f that sends
a proof of A to a proof of B.

This is the key to constructive mathematics, in the
sense that we have a notion of function in going from
premisses to conclusions, and we can restrict these

functions to be "constructive", like as the Greeks interpreted
constructive, Geometric constructions were constructive
when they used rule and compass a finite number of times.

In as far its quite conceivable that the Banach Tarksi theorem
might fail, if the "constructive" function set doesn't cover
making 3 spheres out of 1 sphere. Although Banach Tarski

tried everything to make it nevertheless that it is plausible
to have such a function, since they only use translation and
rotation, which usually preserves volume.

[Mild Shock]

The Drinker Paradox is not such an example where
a "constructive" way to go from premisse A to conclusion B
would be needed, since it doesn't deal with some "constructive"

doing. The generalized Drinker Paradox fails some other
tests of "fiction" in mathematics. Namely it fails the adequacy
of the premisses itself. A premisse:

Set(s)

Is not adequate for the Drinker Paradox, since there is no
U with s ⊆ U. If you write Set(s) as a premisse you postulate
that s comes from Cantors absolute infinite, which doesn't

contain some U such that s ⊆ U. But the drinkers are all from
the pub U. So premisse as follows is needed:

s ⊆ U

The fallacy of Dan Christensen is then exposed, in that
the conclusion is not anymore possible.

[Dan Christensen]

On Monday, May 29, 2023 at 6:03:46 AM UTC-4, Mild Shock wrote:
> The Drinker Paradox is not such an example where
> a "constructive" way to go from premisse A to conclusion B
> would be needed, since it doesn't deal with some "constructive"
>
> doing. The generalized Drinker Paradox

http://www.dcproof.com/STGeneralizedDrinkersThm.htm

> fails some other
> tests of "fiction" in mathematics. Namely it fails the adequacy
> of the premisses itself. A premisse:
>
> Set(s)
>
> Is not adequate for the Drinker Paradox, since there is no
> U with s ⊆ U. If you write Set(s) as a premisse you postulate
> that s comes from Cantors absolute infinite, which doesn't
>
> contain some U such that s ⊆ U. But the drinkers are all from
> the pub U. So premisse as follows is needed:
>
> s ⊆ U
>
> The fallacy of Dan Christensen is then exposed, in that
> the conclusion is not anymore possible.

Nonsense. While philosophers may not agree, from none other Terence Tao, we have:

"Among all the objects studied in mathematics, some of the objects happen to be sets; and if x is an object and A is a set, then either x ∈ A is true or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A undefined; for instance, we consider the statement 3 ∈ 4 to neither be true or false, but simply meaningless, since 4 is not a set.)"
--Terence Tao, "Analysis I," p.34

Note the use of the phrases, "A is set" and "A is not a set" suggesting a predicate Set(A) in a more formal setting.

In DC Proof, 'Set(s)', when introduced as premise, can be taken to mean: Let s be an object to which the axioms of set theory can be applied, e.g. that there exists a power set of s.

Example

Let s be a set

1. Set(s)
Axiom

Invoke the Powers Set Axiom

2. ALL(a):[Set(a) => EXIST(b):[Set(b) & ALL(c):[c in b <=> Set(c) & ALL(d):[d in c => d in a]]]]
Power Set

3. Set(s) => EXIST(b):[Set(b) & ALL(c):[c in b <=> Set(c) & ALL(d):[d in c => d in s]]]
U Spec, 2

4. EXIST(b):[Set(b) & ALL(c):[c in b <=> Set(c) & ALL(d):[d in c => d in s]]]
Detach, 3, 1

Define: p (the power set of s)

5. Set(p) & ALL(c):[c in p <=> Set(c) & ALL(d):[d in c => d in s]]
E Spec, 4

[Mild Shock]

Well while constructive logic might prevent that Unicorns
are created through some non-constructive implications.
You start right away with a Unicorn when you start with

the assumption, that the whole of the Drinkers is from Set(_):

Set(s)

This is of course not the case. The Drinkers are only from
the pub U, not from the absolute infinite, also known as
inconsistent multiplicity, see Cantor. A less Unicorn assumption

reflecting the "present" in your premisse would be that s ⊆ U.
If you use this assumption:

s ⊆ U

You cannot prove this nonsense, correcting another bug
about the "present", this time not in the premisse but
in the conclusion:

EXIST(x):[x e U & (x e s => Q(x,s))]

Try proving the above. LoL

[Mild Shock]

Already using this alone, where U represents the guests of the pub:

EXIST(x):[x e U & (x e s => Q(x,s))]

Prevents your errorneous conclusion. After all, Smullyan
talks about a man at the bar, the place inside a pub
where you usually order a drink. Not on venus or mars:

"A man was at a bar. He suddenly slammed down his
fist and said, " Gimme a drink, and give everyone elsch
a drink, caush when I drink, everybody drinksh!" So drinks
were happily passed around the house."
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

You know how a bar looks like. Its basically a kind
of alevated desk, that separates the kitchen etc.. from
the rest of the pub, where one side you find the bar tenders,

and on the other side the guests.

[Mild Shock]

Of course material implication cannot help errors
of this time, garbage in garbage out. Material implication
cannot validate premisses or conclusions, whether

they sensibly refer to the present or not. It can help
do so though. You can use material implication to
run validation test cases. But then you have to change

your premisses or conclusions. As long as they are
garbage, they are garbage.

[Ross Finlayson]

Well, it seems that we're arguing from "opposite perspectives".

So, what we're arguing out is actually among points of contention in the field,
and includes what has a name called the "qualification problem".

So, leafing through Russell and Norvig's book "Artificial Intelligence", there's
Chapter 7 is called "Logic Agents".

So, there's a notion of entailment and about the "worlds", and, the notion of "implication"
isn't connected to "causal implication" a.k.a. "direct implication", because it has a sort
of "little model of entailment", and, not having a universal model of the objects and rules.

Then the idea is that the overall entailment is transitive and makes up for sets of events
that are the "models", and I'll argue that they don't really reflect "model theory" because
there are unmodeled "rules" in what they "entail", the idea is that entailment then makes
it so a naive algorithm can accomplish various "derivations", with very simple rules,
in the context of the "search" of the digital development in their "goal-seeking",
and about what's "complete".

So, one might start with calling "material", "implication", instead, "material entailment".


Then, of course there's a totally different approach, or a sort of opposite, where
"implication" actually means "causal" and "direct" implication, and the contents of
the truth tables more reflect values of attributes, than the carriage of entailment,
then that changes in the conditions, can be applied to the entire truth-table.

So, there's a sort of disambiguation of what are "entailment tables" and "implication tables",
that "implication tables" have a more complete algebra about the negation and the modal
and so on, in terms of the piece-wise rows of the entailment tables, the column-wise
relations of the implication tables (the truth tables, "the tableau").


So, that said, what there is is a lot of ambiguity because this sort of style of entailment
is squatting on the domain of the definition of the good old classical propositional logic.

Clearly, what results is a deconstructive account that results a disambiguation of the terms
and their application: in this manner making it better an approach to the "qualification problem",
and making less primary the approach of "large, fast, and dumb".

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

Also, this sort of "squat ambiguity" is carried out from "monotonicity", there are basically
_conflicting definitions_ that need to get sorted out and built into a better thing.

Now, one way to approach this is to consider Lukasiewicz and the "multivalent", but really
instead of just introducing U for Uncertain after T for True and F for false, to introduce
constants of the NULL and UNIVERSAL. The idea then is to write implications so that
there are constants that

False -> Null
True -> Universal
Null -> False
Universal -> True

though, there are various considerations why there's only one of those constants or otherwise
what results for the "arithmetization" the properties of the "arithmetic identities and annihilators",
what values to assign those things, for example like

False -1
Null/Universal 0
True 1

that then, this entire situation can be improved, and, it can be pointed exactly what's wrong in
the _definitions_ and their _derivations_ from the _assumptions_ of the _models_.



So, most certainly, there is an entire school of "classical propositional logic" that
basically excludes the entire "model of worlds, OK it's just samples of events",m
approach, that peope like De Morgan and so on would find much more familiar,
when they find that usual of their derivation rules are not possible in such a system.

Anyways with this sort of disambiguation of vagaries of definition,
and basically separating the approach of "opportunistic goal-seeking"
from "tractable oversall verification", I will carry on like so thus that
both are put side-by-side, and their differences sorted, then to remove
what are the "squat ambiguities" thus that each has a proper, qualified,
language.

Then, again, the classical logic is much more about the
_causal_ and the _implicatory_ not the simplest algorithms
of a model based on "my block of data: the world", and,
the "truth tables" of "entailment tables" and "implication tables"
are , ..., different relations of binary and placeholder VALUES.

[Mild Shock]

If we follow Dan Christensens argumentation of generalization,
and take for example Euclids proof of the infinity of prime numbers,
and would say its formalized as follows:

T: Some number theory
A: The statement there are infinite prime numbers
T |- A

Then Dan Christensens "generalizations" approach would allow
to replace T by ⊥. After all it doesn't destroy the statement
that there are infinite prime numbers:

⊥: Generalized number theory
A: The statement there are infinite prime numbers
⊥ |- A

Woa! Perfect, we have found a generalization of number theory.
The only problem is we went a little bit too far, in that
we now have also:

⊥ |- ~A

The same here:
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

You can now prove:
EXIST(x):[x e s => ALL(x):x e s]]

And you can also prove:
EXIST(x):[x e s => ~ALL(x):x e s]]

So what went wrong? My hypothesis so far, neither Rossy Boy
nor Dan Christensen have any clue what went wrong. You need
to be able to dig into the whole history of set theory,

including Cantors discovery of absolute infinite respectively
inconsistent multiplicity, and how set theory is designed to be
used in mathematics, to understand whats going wrong.

Its not a problem of classical logic in any way. Its a problem of
set theory, and its practical use.

Ross Finlayson schrieb am Montag, 29. Mai 2023 um 18:01:43 UTC+2:
> .... Herpes Blister gibberish ...

[Mild Shock]

Concerning Dan Christensens over generalization blooper:

> Its not a problem of classical logic in any way. Its a problem of
set theory, and its practical use.

Hint: Mathematicians like to think in structures. They consider
working with a structure that has a carrier set or carrier class,
and a couple of relations and functions.

Whats the structure of the Drinker Paradox? And how does it
get modelled as formulas? Including the Drinker Paradox
statement itself?

[Mild Shock]

And why is this a blooper:

You can now prove:
EXIST(x):[x e s => ALL(x):x e s]]

And you can also prove:
EXIST(x):[x e s => ~ALL(x):x e s]]

You can try yourself, the FOL formulation doesn't have this defect:

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

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

[Dan Christensen]

On Monday, May 29, 2023 at 11:30:33 AM UTC-4, Mild Shock wrote:
> Already using this alone, where U represents the guests of the pub:
> EXIST(x):[x e U & (x e s => Q(x,s))]
> Prevents your errorneous conclusion. After all, Smullyan
> talks about a man at the bar, the place inside a pub
> where you usually order a drink. Not on venus or mars:
>
> "A man was at a bar. He suddenly slammed down his
> fist and said, " Gimme a drink, and give everyone elsch
> a drink, caush when I drink, everybody drinksh!" So drinks
> were happily passed around the house."

Smullyan's informal proof:

"Either it is true that everybody drinks or it isn't. Suppose it is true that everybody drinks. Then take any person--call him Jim. Since everybody drinks and Jim drinks, then it is true that if Jim drinks then everybody drinks. So, there is at least one person namely Jim-such that if he drinks then everybody drinks.

"Suppose, however, that it is not true that everybody drinks; what then? Well, in that case there is at least one person-call him Jim-who doesn't drink. Since it is false that Jim drinks, then it is true that if Jim drinks, everybody drinks. So again there is a person--namely Jim--such that if he drinks, everybody drinks."

--"What is the name of this book?" pp. 209-210

Hmmm.... No mention of any pub or and other location. In your "standard" FOL, Smullyan's Drinkers' Principle would be Ex(Dx => AyD(y)). Nothing corresponding to anything like a pub. What gives?

> https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf
>

For a set-theoretic variation of DP that includes explicit mention of a pub set p (unlike Smullyan's original version), see the thread, "Yet another set-theoretic variation of the Drinkers' Paradox." There, using ordinary set theory and basic logic, I prove:

ALL(d):ALL(p):[Set(d) & Set(p) => EXIST(x):[x in d => p=d]]

Where d could be thought of as the set of people drinking in given pub, and p as the set of all people in that pub. Note that d and p are arbitrary, possibly empty sets. Since these are arbitrary sets, this results holds whether or not d is a subset of p.

[Dan Christensen]

On Monday, May 29, 2023 at 12:35:10 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> And why is this a blooper:
> You can now prove:
> EXIST(x):[x e s => ALL(x):x e s]]
>
> And you can also prove:
> EXIST(x):[x e s => ~ALL(x):x e s]]

> You can try yourself, the FOL formulation doesn't have this defect:
>
> ∃x(Dx → ∀yDy) is valid.
> https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
>
> ∃x(Dx → ¬∀yDy) is invalid.
> https://www.umsu.de/trees/#~7x(Dx~5~3~6yDy)

Is your short-term memory already going, Mr. Collapse? Recall recently:

∃x¬Dx → ∃x(Dx → ¬∀yDy) is valid (in your "standard" FOL)

https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5~3~6yDy)

[Mild Shock]

What makes you think this is relevant:

> ∃x¬Dx → ∃x(Dx → ¬∀yDy) is valid (in your "standard" FOL)
> https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5~3~6yDy)

When this is invalid:

∃x¬Dx is invalid.
https://www.umsu.de/trees/#~7x~3Dx

Garbage in, Garbage out.

On Monday, May 29, 2023 at 12:35:10 PM UTC-4, Mild Shock (aka Mr.
Collapse) wrote:
> And why is this a blooper:
> You can now prove:
> EXIST(x):[x e s => ALL(x):x e s]]
>
> And you can also prove:
> EXIST(x):[x e s => ~ALL(x):x e s]]

> You can try yourself, the FOL formulation doesn't have this defect:
>
> ∃x(Dx → ∀yDy) is valid.
> https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
>
> ∃x(Dx → ¬∀yDy) is invalid.
> https://www.umsu.de/trees/#~7x(Dx~5~3~6yDy)

Is your short-term memory already going, Mr. Collapse? Recall recently:

∃x¬Dx → ∃x(Dx → ¬∀yDy) is valid (in your "standard" FOL)

https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5~3~6yDy)

[Ross Finlayson]

Yes, this sort of critical analysis of the approaches is a lot better than that
otherwise, without disambiguating all the assumptions that go into the
definitions of "derive" that there would simply otherwise only be conflict.

So, the "qualification problem" and "ramification problem" are parts of it,
but it also reflects that models of inclusion have corresponding duals as
models of exclusion. (...That are not "complete" with respect to each other,
but each is structural.)

For example, if you consider usual goal-finding and "greedy" algorithms,
vis-a-vis "easy" and "hard" problems, sometimes it's better to find what
combinations definitely force the system open, instead of what particulars
or Horn clauses or simple algorithms reduce it more closed, that what would
be pathological can be removed under combinations, or for an underlying graph
theory, and its interpretation, separating models and establishing where
they're incomplete and where they're incomplete. It's a fuller analysis.


So, there are some total vagaries in definition, that need to get dis-ambiguated,
making for a deconstructive account of a reconstructive analysis that makes
for both a "universal theory" and "a world where implication is causal",
combining the "rules" and the "values", contra a loose collection in sampling/event theory,
where basically "monotonicity" is used in two incompatible ways, in terms of
adding "samples" or adding "inferences".

This way it can be clear that "the logic" sorts out these kinds of "mutual dumbs",
then also to establish what are their compatible modes, models, thus that it
can result what are their relative strengths and weaknesses, besides the usual
sort of "algorithmics" that "greedy goal-finding search" has in its context,
that aren't overall relevant to "classical propositional logic" and its soundness,
validity, and so on.

Yes, it would make a lot less "mutual dumb" to sort out these "vagaries of definition"
and what are "squat ambiguities" and dis-ambiguate them and so on.

Anyways nobody needs "material implication" to do logic, but,
"causality" and "direct implication" are always unbreakable rules.
(In the logic, ..., what with regards to "logical paradoxes" are to be
resolved through quantifier disambiguation and modal quantifiers
and what makes for reconciling numbering and counting and so on,
about a logical foundation that's correct and dis-ambiguates the
definitions in the "entailment", "implication", "models", "rules",
"monotonicity", of the "inference".)

[Dan Christensen]

On Monday, May 29, 2023 at 1:58:44 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

> > And why is this a blooper:
> > You can now prove:
> > EXIST(x):[x e s => ALL(x):x e s]]
> >
> > And you can also prove:
> > EXIST(x):[x e s => ~ALL(x):x e s]]
>
> > You can try yourself, the FOL formulation doesn't have this defect:
> >
> > ∃x(Dx → ∀yDy) is valid.
> > https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
> >
> > ∃x(Dx → ¬∀yDy) is invalid.
> > https://www.umsu.de/trees/#~7x(Dx~5~3~6yDy)
>
> Is your short-term memory already going, Mr. Collapse? Recall recently:
>
> ∃x¬Dx → ∃x(Dx → ¬∀yDy) is valid (in your "standard" FOL)
>
> https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5~3~6yDy)

> What makes you think this is relevant:

> > ∃x¬Dx → ∃x(Dx → ¬∀yDy) is valid (in your "standard" FOL)
> > https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5~3~6yDy)

You have forgotten that, too??? Oh, my....

Once again, in ordinary set theory anyway, every set excludes some object. (EXIST(x):~Dx is the FOL equivalent.) Using this fact in set theory, we can obtain:

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

Also...

ALL(s):[Set(s) => EXIST(x):[x in s => ~ALL(y):[y in d]]]

In "standard" FOL:

∃x¬Dx → ∃x(Dx → ¬∀yDy)

I hope this helps.

> When this is invalid:
>
> ∃x¬Dx is invalid.
> https://www.umsu.de/trees/#~7x~3Dx
>

That just means it is not always true. In "standard" FOL, ALL(a):D(a) is not ruled out.

Again, in "standard" FOL we have:

∃x¬Dx → ∃x(Dx → ¬∀yDy)

[Mild Shock]

For a good natural intelligence you need to
distinguish Chihuahuas from Muffins.

Well if you can prove something which is the
analogue to ∃x¬Dx, then something went wrong
in your model. You did some over generalization,

or some other blooper. Basically before your over
generalization or other blooper, we had,
from D is a predicate assumption:

**Chihuahua:** ∃x(Dx → ∀yDy) is valid.
https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
**Muffin:** ∃x(Dx → ¬∀yDy) is invalid.
https://www.umsu.de/trees/#~7x(Dx~5~3~6yDy)

Now with your over generalization we have,
from Set(s) assumption:

**Chihuahua:** EXIST(x):[x in s => ALL(y):[y in d]]] is valid
http://www.dcproof.com/STGeneralizedDrinkersThm.htm
**Chihuahua:** EXIST(x):[x in s => ~ALL(y):[y in d]]] is valid
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

So suddently there are two Chihuahua, whereas we
had before one Chihuahua and one Muffin. The
second Chihuaha is usually called a false positive.

So what is the difference between predicates and
unrestricted sets, such as the absolute infinite?
Well in predicates we have:

**Muffin:** ∃x¬Dx is invalid.
https://www.umsu.de/trees/#~7x~3Dx

Whereas in sets we have:

**Chihuahua:** EXIST(x):[~x in s] is valid.
http://www.dcproof.com/UniversalSet.htm

So I guess your false positive happened because
in one place you replaced Muffin by Chihuahua.

[Mild Shock]

But your blooper is understandable, distinguishing
Chihuahuas from Muffins requires very good eye sight.
Artificial intelligence has similar struggles:

Chihuahua or muffin? My search for the best computer vision API
https://www.freecodecamp.org/news/chihuahua-or-muffin-my-search-for-the-best-computer-vision-api-cbda4d6b425d/

In the present case one needs eye sight to
see that we have "invalid" and "valid", two different
words already, even with opposite meaning:

> **Muffin:** ∃x¬Dx is invalid.
> https://www.umsu.de/trees/#~7x~3Dx

> **Chihuahua:** EXIST(x):[~x in s] is valid.
> http://www.dcproof.com/UniversalSet.htm

[Mild Shock]

Conclusion it requires more work, to go from predicates
to sets, than blindly replacing each predicate by a set
membership. It requires more when you want to

preserve validity and invalidity, i.e. when you want to
prevent false positives in the new formalization with sets.
Most mathematicians know how to do it.

[Dan Christensen]

> Conclusion it requires more work, to go from predicates
> to sets, than blindly replacing each predicate by a set
> membership.

I never claimed otherwise. In set theory, you have more tools at your disposal.

> It requires more when you want to
> preserve validity and invalidity, i.e. when you want to
> prevent false positives in the new formalization with sets.

[snip]

"False positives?" With more tools, you can supposedly prove things that you could not prove without them. Deal with it, Mr.Collapse.

[Mild Shock]

But the term "generalization" is wrongly applied. You didn't do
a generalization. A generalization doesn't have false positives
and only false positives. A generalization can be specialized,

so that the old result can be obtained. Take this example
from mathematics of a generalization. A real valued
matrice is a generalization of a single real number:

| a11 ... a1n |
... ....
| am1 ... amn |
https://en.wikipedia.org/wiki/Matrix_(mathematics)

In general matrices loose commutativity. For two square
matrices A and B, it is not necessary anymore the case
that their product commutes:

/* not provable anymore for square matrices n > 1 *
A*B = B*A

So in the generalization there is less provable. But you
have somewhere a lever so that you can still get the
special thingy. Namely square matrices of size 1,

behave like single real numbers:

/* provable for square matrices n = 1 *
A*B = B*A

Nothing of all this is found in your generalized Drinker Paradox.
It is rather a specialized Drinker Paradox, since it makes things
provable that werent provable before. And this is a one way

ticket. You have no lever to prove the original Drinker Paradox.
What would be your level to extract the original Drinker Paradox,
when you have, a muffin changed into a chihuahua:

> **Muffin:** ∃x¬Dx is invalid.
> https://www.umsu.de/trees/#~7x~3Dx

> **Chihuahua:** EXIST(x):[~x in s] is valid.
> http://www.dcproof.com/UniversalSet.htm

You went from general to special. You prove a special Drinker
Paradox, not a general Drinker Paradox.

[Dan Christensen]

See my reply just now to your identical posting elsewhere here at sci.logic.

Dan

On Monday, May 29, 2023 at 8:37:37 PM UTC-4, Mild Shock wrote:
> But the term "generalization" is wrongly applied. You didn't do
> a generalization. A generalization doesn't have false positives
> and only false positives. A generalization can be specialized,
>
> so that the old result can be obtained.

[snip]

[Ross Finlayson]

So, your wonderings about "is there something wrong with material implication?" can be deliberated
in an expansive sense by understanding that "the logics" you've been copying have a "the baggage"
that is about the algorithmics, the rules, whether there are multiple observers or parallel change,
and then other things that get into what are suitable systems for the evaluation of inference,
in what are "time-forward" systems and with monotonicity and modality.

I.e., the usual "monotonicity" you get is really "adding extra" not "making changes",
that there are for the derivations of classical propositional logic, making sure that
what results for values used for their derivations, that _all_ the classical derivations
follow, not excluding those (few..., but, some) that "material entailment" does not support.

So, this way, is for making it so to show _why_ there is that the "working data structures" of
various "simple, quite linear, means of computing inferences or rather the predicate test()",
are _not_ so necessarily fundamental as opportunistic, and, there are both higher level concerns,
and lower level concerns, which results why there's for making "normal truth tables",
for the monotonic and the modal, and "time-forward", and also "retro-active", but
that as exceptional and for again the "time-forward", or "self-healing", that the "truth tables"
are populated with values what make for that changes in inferences or rules, can get applied
in-place, for example, to the "truth-tables", vis-a-vis the time and space terms, of their algorithms.


So, "the baggage", here as expressed in part by the "qualification problem" and "ramification problem",
is largely the ramification problem, and is to reflect that "the baggage" of, "the logics", should
reflect fundamentally the scientific necessities, or, the overall closed algebraically, and the finite,
or, expert systems and what are cataloged axiomatics, in, a system overall where there's only
one world and only one model.

I.e., this can help explain why there's a difference between "various ad hoc and working theories",
and, "FOUNDATIONS", and help explain why some researchers in FOUNDATIONS, _reject_
"material implication" as, ..., "wrong", as well do various constructivists, as well do various
of those who associate implication only with causality (either shared or coincident).

This makes it so that "all the classical derivation rules are _entailed_", which you'll notice
that some with "the baggage" or "entailment, modern baggage: defined that vacuity brings
in false as any antecedent and true as any consequent of a _material implication_", as, an
un-used data structure that's _missing_ some of the derivation rules of the classical
propositional calculus.

Such "modern baggage" is _not_ considered classical, nor is it classically complete.

(Or, "facile est descensis averno".)

[Mild Shock]

What makes you think this is relevant:

> ∃x¬Dx → ∃x(Dx → ¬∀yDy) is valid (in your "standard" FOL)
> https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5~3~6yDy)

What this is invalid:

∃x¬Dx is invalid.
https://www.umsu.de/trees/#~7x~3Dx

Dan Christensen schrieb:

[Dan Christensen]

On Tuesday, May 30, 2023 at 5:27:06 AM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb:
> > On Monday, May 29, 2023 at 12:35:10 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> >> And why is this a blooper:
> >> You can now prove:
> >> EXIST(x):[x e s => ALL(x):x e s]]
> >>
> >> And you can also prove:
> >> EXIST(x):[x e s => ~ALL(x):x e s]]
> >
> >> You can try yourself, the FOL formulation doesn't have this defect:
> >>
> >> ∃x(Dx → ∀yDy) is valid.
> >> https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
> >>
> >> ∃x(Dx → ¬∀yDy) is invalid.
> >> https://www.umsu.de/trees/#~7x(Dx~5~3~6yDy)
> >
> > Is your short-term memory already going, Mr. Collapse? Recall recently:
> >
> > ∃x¬Dx → ∃x(Dx → ¬∀yDy) is valid (in your "standard" FOL)
> >
> > https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5~3~6yDy)
> >

> What makes you think this is relevant:

> > ∃x¬Dx → ∃x(Dx → ¬∀yDy) is valid (in your "standard" FOL)
> > https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5~3~6yDy)

> What this is invalid:
> ∃x¬Dx is invalid.
> https://www.umsu.de/trees/#~7x~3Dx

Again, ∃x¬Dx tells us only that D is not a universal predicate/set. It is a reasonable assumption in many cases, e.g. not everything is a drinker. Nevertheless, a universal predicate is not ruled out in your "standard" FOL, so ∃x¬Dx is NOT a theorem in that system. The non-existence of a universal set is, however, a theorem in ordinary set theory (see Russell's Paradox) allowing us to generalize. Introducing the equivalent assumption ∃x¬Dx in FOL would also allow us to generalize in FOL, e.g. ∃x¬Dx → ∃x(Dx → ¬∀yDy) . I hope this helps.

[Mild Shock]

See my response to your crazyness in "Why is model theory needed?"

[Ross Finlayson]

You might improve from reading Pascal's "Thoughts on Mind and Style".

[Ross Finlayson]

What you've been calling "classical" is really "computer-age" and follows only from a
"convention" that is an "opinion" of the data structure of "entailment" and about a
bounded fragment of a system that doesn't have symbolic universals.

Then, it's split apart the rules from the data structures, that being a very _flexible_
organization, is not "monotonic" in the usual sense of "apply _all_ the logics".

So, sorting out that there are other "opinions" and "conventions" make more general
that what you have as the "vacuous" is actually just a limitation of your data structure
(your "models" in your "world").

Then, this makes for what is a "monotonic" logic above that that quite more clearly
re-attaches "causality" to "implication" and is for dis-ambiguating the "conflicts of
collisions in definition" what makes for that "a data structure of a sampling space of
events in a bounded fragment" is just an application detail, while, the greater "logic"
has a truer "entailment" and its definitions are more natural in corresponding with
their natural meaning, "entailment" and "implication", a fuller and more natural language.

[Mild Shock]

The K stands for Komolgorov. Notably the BHK interpretation
does not automatically lead to a function that would
prove ex falso quodlibet:

⊥ => A

Such a function would need to send a proof of absurd ⊥,
to a proof of A. But ⊥ is considered unprovable? Kolmogorov
even rejected Ex Falso, as one can find documented here:

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

But intuitionistic logic accepts the above. Since when for example
if we define ~A = A => ⊥ it happens that ⊥ is provable by simple
modus ponens, from some premisses.

~A => (A => ⊥)

Provability is a notion that happens in some context. Can the
BHK interpretation be restored for intuitionistic logic. One way
to restore it is to assume that for every formula A, there

is a constant C_A, that sends a proof of absurd ⊥ to the a new
proof that proofs A. So C_A is the function for ⊥ => A.

[Mild Shock]

This leads to a constuctive proof of the Russell paradox,
at least the contradiction can be constructively reached:
See also:

Constructive logic and Russell's paradox
https://math.stackexchange.com/a/3923755

We define, where as mentioned below ~A = A => ⊥:

A := { x | ~(x ∈ x) },

We then get:

1. A ∈ A
Assumption
2. ~(A ∈ A)
Apply z ∈ { y | P(y) } gives P(z)
3. ⊥
Detachment 2,1 [You could use Join in DC Proof]
4. ~(A ∈ A)
Conclusion 1,3
5. A ∈ A
Apply P(z) gives z ∈ { y | P(y) }
6. ⊥
Detachment 4,5 [You could use Join in DC Proof]

[Mild Shock]

But mostlikely this result here is not anymore
constructive. Because constructive logic has often
an existence property, so when we can prove ∃xP(x) in

constructive logic, we can often extract a term t,
such that P(t). But this here has mostlikely no term t,
I guess it cannot be made constructive:

EXIST(a):[~a e s]
http://www.dcproof.com/UniversalSet.htm

At least in its present form, I guess its not constructive.
What is the existence property of constructive theories?
You can read here:

Disjunction and existence properties
In mathematical logic, the disjunction and existence
properties are the "hallmarks" of constructive theories
https://en.wikipedia.org/wiki/Disjunction_and_existence_properties

[Mild Shock]

In ZFC it can be made a kind of constructive. I
don't know whether this works also in DC Proof.
One can define Zermelo successor:

succ(A) = {A}

Or von Neumann successor:

succ(A) = A u {A}

You then need regularity axiom, and can show:

~succ(A) e A

So some existential witness term is succ(A). But
wellfounded sets are again more specialized than
sets in general as Dan Christensen uses Set(_).

The Russell Paradox works both for wellfounded sets,
and sets that do not subscribe to the regularity axiom.
But when you have a regularity axiom, you can

use succ(A) as an alternative road to show that there
is no universal set. Russell Paradox is not the only
road here to show that there is no universal set.

[Dan Christensen]

On Tuesday, May 30, 2023 at 1:53:36 AM UTC-4, Ross Finlayson wrote:

[snip]

> So, your wonderings about "is there something wrong with material implication?" can be deliberated
> in an expansive sense by understanding that "the logics" you've been copying have a "the baggage"
> that is about the algorithmics, the rules, whether there are multiple observers or parallel change,
> and then other things that get into what are suitable systems for the evaluation of inference,
> in what are "time-forward" systems and with monotonicity and modality.
>

[snip]

My concern is about conditional statements based on logical propositions that are unambiguously either true or false in the PRESENT--the case of false antecedents in particular. I take it you reject the notion that if proposition A is false, then the implication A=>B (but not necessarily B) must be true. ~A=>[A=>B]

My proof again:

1. ~A
Premise

2. A
Premise

3. ~B
Premise

4. ~A & A
Join, 1, 2

5. ~~B
Conclusion, 3

6. B
Rem DNeg, 5

7. A => B
Conclusion, 2

8. ~A => [A => B]
Conclusion, 1

Please explain why you take exception to this when, as you must know, the vast majority of mathematicians accept this method of proof to no ill effect, i.e. no logical inconsistencies or errors.

[Ross Finlayson]

There you just change the order of 1 and 2.



You're just fabricating any contradiction and using it to negate the next step
in the proof you've ordered: it's not logic, it's stipulation.

It seems just extended, capricious stipulation.

1) I don't need it to do logic.
2) It shouldn't be called "implication"
3) If it gets negated it loses what placement it has in chained and bi-conditionals
4) as a stipulation and a hypothetical it should just be excluded
5) it doesn't bear any truth value
6) it collides with "implication"

Then, the way you collect your premises, and when you get a contradiction,
just negating the next premise, I'd say it's disordered. I.e., A and ~A are
mutually contradictory. B is independent of them. So, when your premises
contradict each other then you pick one, it's rather that the consideration
was never included, because otherwise that's just writing whatever you
want and arguing what was un-related was related, so, actually that looks
pretty disordered, because otherwise your objects most include some properties
like "in a contradiction, what I say first wins", and, "after any contradiction, what
follows is contradicted", that you can always just stipulate contradiction in
front and cascade negations.

This goes back to my long-standing criticism of stipulations ina vacuum,
and not a "logic of a universe of logical objects", which goes back to a
long-running thread called "first principles and final causes" and
"elementary and axiomatic theories", besides that as above your derivation
rules, aren't recoverable with "exchange any two premises that negate
each other" and "premises with no common terms cannot negate each other".

Any premise X can be re-written ~Y.

Basically "premises with no common terms cannot negate each other".
In a sense that's called "monotonicity".

[Ross Finlayson]

Oh? How do you prove there _is_ a universal set and
what its properties, are?

I just apply Russell's directly to the finites and make an extra-ordinary in-finite.
(Which is, ..., "not Russell's".)

[Mild Shock]

Prove it without Rem DNeg. Hint: Its possible.
The theorem is intuitionistically valid. So whats the concern?

P.S.: If you get stuck with DC Proof doing intutionistic logic,
you can use this CharGPT template, you can ask for proofs without LEM:

ChatGPT does:

- Here's how you can translate the proof into natural deduction:
- Here's an alternative proof that does not rely on LEM:
- Here's the translation of the proof into Fitch-style natural deduction:
- Here's the translation of the proof into Gentzen's tree-style natural deduction:
- Here's the translation of the proof into sequent-style natural deduction:
https://chat.openai.com/share/79ae4f02-fd07-4786-800b-305bc9eed143

[Mild Shock]

Material implication is critizised for obeying two laws,
because it is seen as (A => B) == (~A v B):

Law of noncontradiction (LNC)
Formally this is expressed as the tautology ¬(p ∧ ¬p).
https://en.wikipedia.org/wiki/Law_of_noncontradiction

Law of excluded middle (LEM)
precise statement of the law of excluded middle, P ∨ ~P
https://en.wikipedia.org/wiki/Law_of_excluded_middle

If you want the theorem ~A => (A => B) not generally valid
you would need to reject LNC. LEM ist responsibe.
This is the reason why ~A => (A => B) is intuitionistically

valid, intuitionism rejects LEM, but does not reject LNC.
If you want to google the field of logics that reject
either LNC or LEM, here is little entry guide:
- A logic that rejects LEM is called para complete.
- A logic that rejects LNC is called para consistent.

The ChatGPT template below was not done by me. Credits
go to Joseph Vidal-Rosset. It contains a LEM rejection.
Maybe somebody can do a LNC rejection with ChatGPT

and share it here. That conversations and thus interaction
specific context and mini learnt model extensions can be
shared via share links seems to be a new feature of ChatGPT.

I saw this feature appear only yesterday in ChatGPT.

See also:
https://help.openai.com/en/articles/7925741-chatgpt-shared-links-faq

[Dan Christensen]

> There you just change the order of 1 and 2.
>
>
>
> You're just fabricating any contradiction and using it to negate the next step
> in the proof you've ordered: it's not logic, it's stipulation.
>

[snip]

Apparently you cannot point to any actual errors arising from the application these methods. We know they work.

[Mild Shock]

The application of ~A => [A => B] is usually considered an
error in linguistic. Since it violates "relevance". B can use
predicates that do not appear in A. And humans are supposed

to only communicate relevant matter. An example where one
sees that it produces nonsensical results is the generalized
drinker paradox by Dan Christensen. You find it here:

The Generalized Drinker Paradox, like here:

ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

Its shows that the material implication can be quite challenging.
It is quite challenging, because a mathematician should
communicate like a human, so it is expected that a mathematician

doesn't use blindly material implication, but also see to it
that there is some "relevance".

[Mild Shock]

The idea of "relevance" gave yet rise to another field
of logic. It has a little bit more complicated semantics
than only rejecting LNC. You find a SEP article here:

Relevance Logic
https://plato.stanford.edu/entries/logic-relevance/

The article lists also ~A => [A => B]:

"Among the paradoxes of material implication are the following:
p -> (q -> p)
~p -> (p -> q)
(p -> q) v (q -> r)"
https://plato.stanford.edu/entries/logic-relevance/

The rejection of the first is the surprise. It is the
rejection of weakening. The second is LNC and the
third is LEM again.

[Dan Christensen]

> Prove it without Rem DNeg.

[snip]

Not necessary as this is a widely used method of proof that is accepted by the vast majority of mathematicians. Maybe you can try to do math without ANY kind negation symbol and make mathematics more, umm... POSITIVE! (HA, HA!)

[Mild Shock]

You can do mathematics without Rem DNeg. Its
associated with so called constructive mathematics.
Maybe you have never heard about it?

Constructive mathematics is distinguished from its
traditional counterpart, classical mathematics, by the strict
interpretation of the phrase “there exists” as “we can construct”.
https://plato.stanford.edu/entries/mathematics-constructive/

Have Fun!

[Dan Christensen]

On Friday, June 2, 2023 at 12:23:41 AM UTC-4, Mild Shock wrote:
> The idea of "relevance" gave yet rise to another field
> of logic.

[snip]

Not a very popular or useful field by the looks of it. Maybe you will find a few devotees in philosophy, but not in mathematics, science or engineering. Like they say, if it ain't, don't fix it. Must be frustrating as hell for you.

[Mild Shock]

You see where non-constructive mathematics
ends. In utter nonsense like this here:

First this here. Its not wrong, but it is not constructive:

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

And then operating with something non-constructive:

ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

[Mild Shock]

The original Smullyan Drinker Parardox is also
not constructive. You find this elaborated here:

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

[Ross Finlayson]

I think that belongs to "natural deduction".

[Mild Shock]

The problem with Rossy Boys rants, he occasionally hits the
nails. He is a like a random number generator. He shoots
his load, and some of the seeds sometimes hit salient points.

Like Rossy Boy had:

> You're just fabricating any contradiction and using it to negate the next step
> in the proof you've ordered: it's not logic, it's stipulation.

I like that one. Ha Ha, you can stipulate whatever B you want
via ~A => (A => B). Very convenient in certain situations. Use
anacoluthon from ~A to A and get your argument B done.

LoL

[Ross Finlayson]

A stopped clock is, right twice a day.

About the most usual modal or temporal is day or night,
for something like "everything falls" there's "the sun also rises",
but at any given time it's A or ~A and 50:50 whether it's so.

So of course, with direct implication, you can plug in, according to
whether it's day or night, A or ~A respectively, to all the inferences,
that go into all the derivation rules, in all their completions,
what derives what's coincident and after what's causal, and
all such good of logic, results right, without, re-write,
while "material implication" would simply result having to
re-write all the derivations, and, toss the old ones,
and, any information contained in them as single point of definition,
would not exist, it would be, lost.

So, first, I don't need "material implication" for anything, _and neither
does anybody else_, except for a particular sort of data structure where it
makes entailment trivial for the monotonicity of concatenation, assuming
of course no two premises were ever introduced twice and discharged variously,
where, it's as well just left out in an equivalent data structure with a convention for
a null, for the very "absurdity" in its absence of implication.

That's convenient and a convention in a data structure in a space of
values, these days we're not quite so short bits and it's more relevant often
to update the structure besides reading it off, mand it's just as fast with
"direct implication" and making for "monotonicity of concatenation".
(Including for example discovering "non-monotinincity of concatenatation".)

Now, I can understand that's very widespread, but also that most people
have never gone into the derivations, where what would be the "completion",
brings in the necessity of an ontological commitment _in the derivation_ what
must be _in the logic_, to universal quantification and such. I.e. it breaks
there, like I said above.

Also, I can understand that's very widespread, but most people do not use
it at all, because to them it says "a lie implies my truth" which is not reasonable
to these people, and instead they use "really: classical propositional calculus".


Then, about the order of your premises, and their discharge,
why can't you re-order your premises? Is it because the order
you've declared them makes a stipulation with no common
terms another stipulation that they do have a common term
only being in the order you've declared them?


Are you suggesting that stipulations with no common terms are related?

It seems moreso that _you must stipulate it_ and then
it's up to you to show it non-contadictory, which is problematic,
when _you must also prove it implies the opposite_,
that _the both things it implies contradict each other_.

Though, I'd imagine you'd rather leave that out, ...,
then that in larger systems it gets more and more intractable
to maintain correctness when things change,
because "material" "implication" should be two
things: 1) direct implication, and 2) a placeholder under
the vacuous, that when someone adds columns to "the truth table"
with derived quantites expected to be used in the arithmetic
of the maintenance of data structure, because that's all the
way of this is for its "monotonic concatenation entailing entailment",
that part is "not an inference" just "keeping the projection in the space".


Are you suggesting that stipulations with no common terms are related,
and you can negate them capriciously just be stipulating a contradiction first?

Because, that's just stipulating "this is logical, now forget it",
really, I think best you can do is make "material implication"
a premise and then separate out the parts for direct implication
contra "vacuous placeholder".


So, I definitely point at "showing a contradiction in terms
negates an unrelated term" as _false_.

[Mild Shock]

Formulas such as of the form:

~A => (A => B)

Don't make a gas. You cannot write scientific paper:
"if the moon is made of cheese then ..."

On the other hand if you would have something else
at hand than material implication =>, namely counter
factual conditional ~>, then this here:
~A => (A ~> B)

Could make a gas. You can write scientific papers:
"Suppose the moon were made of cheese then ..."

[Mild Shock]

Very funny grammatically, this fake past, sounds like going
back into the past, "were" has past tense morphology,
but a counter factual points more into the future?

[Mild Shock]

You can write a paper:

Theorem 1:
"if the moon is made of cheese then Rossy Boy can fly"

With reference to the fact that the moon is not
made of cheese, the above theorem would be
even a correct therem.

[Mild Shock]

But I guess the paper wouldn't be accepted,
as showing something relevant.

[Dan Christensen]

On Friday, June 2, 2023 at 12:31:43 AM UTC-4, Mild Shock wrote:
> You see where non-constructive mathematics
> ends. In utter nonsense like this here:
>
> First this here. Its not wrong, but it is not constructive:
>

Not being "constructive" in this sense is simply not an issue to the vast majority of mathematicians.

> 28 ALL(s):[Set(s) => EXIST(a):~a e s]
> Rem DNeg, 27
> http://www.dcproof.com/UniversalSet.htm
>
> And then operating with something non-constructive:
> ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
> http://www.dcproof.com/STGeneralizedDrinkersThm.htm

[snip]

[Dan Christensen]

On Friday, June 2, 2023 at 1:02:45 AM UTC-4, Ross Finlayson wrote:

[snip]

> Now, I can understand that's very widespread, but also that most people
> have never gone into the derivations, where what would be the "completion",
> brings in the necessity of an ontological commitment _in the derivation_ what
> must be _in the logic_, to universal quantification and such. I.e. it breaks
> there, like I said above.
>

The truth table of logical (material) implication:

A B A=>B
T T T
T F F
F T T
F F T

In daily discourse about the present state of the world, the first two lines are routinely used. The last two are rarely if ever use. We don't usually give any consideration about implications with false antecedents (A). The last two lines are typically only used in very technical arguments, e.g. in mathematical proofs. They are, however, easily derivable from first principles (see my proof here).

> Also, I can understand that's very widespread, but most people do not use
> it at all, because to them it says "a lie implies my truth" which is not reasonable
> to these people, and instead they use "really: classical propositional calculus".
>

Again, if the antecedent A is false, then the implication A=>B (but not necessarily the consequent B) must be true.

>
> Then, about the order of your premises, and their discharge,
> why can't you re-order your premises?

[snip]

You could reorder your premises, but you will likely not obtain the same result. If you interchange the first two premises in my proof, you would get A=>[~A=>B] instead of ~A=>[A=>B].

> Because, that's just stipulating "this is logical, now forget it",
> really, I think best you can do is make "material implication"
> a premise and then separate out the parts for direct implication
> contra "vacuous placeholder".
>
> So, I definitely point at "showing a contradiction in terms
> negates an unrelated term" as _false_.

No errors or inconsistencies here. Try again.

[Dan Christensen]

On Friday, June 2, 2023 at 1:28:12 AM UTC-4, Mild Shock wrote:
> Formulas such as of the form:
> ~A => (A => B)
> Don't make a gas. You cannot write scientific paper:
> "if the moon is made of cheese then ..."
>

See my proof here. Also see https://dcproof.wordpress.com/2017/12/28/if-pigs-could-fly/

[Mild Shock]

And how would you formalize the criteria, that
such an irrelevant paper would not be accepted?

On Friday, June 2, 2023 at 1:28:12 AM UTC-4, Mild Shock wrote:
> Formulas such as of the form:
> ~A => (A => B)
> Don't make a gas. You cannot write scientific paper:
> "if the moon is made of cheese then ..."
>

See my proof here. Also see
https://dcproof.wordpress.com/2017/12/28/if-pigs-could-fly/

Dan Christensen schrieb:
> What erroneous conclusions might arise from applying material conditionals for logical propositions that are unambiguously either true or false in the present? (Hint: None?)

[Ross Finlayson]

1) "I'm conflicted"
2) "Whatever ..."

[Ross Finlayson]

I think you mean "irreverant".

[Mild Shock]

There is a certain idea behind the random mess that
Rossy Boy creates when he creates his boring texts.
To avoid that they look obviously random, he pickles

them with antagonistic pairs, like linear and non-linear,
inner anus radius and outer anus radius, etc.. etc.. So
he is copying some Bhagwan guru that preaches

ying and yang. Who does he want to impress with
his nonsense? Who teached him that this makes up
an interesting text, a pearl necklace of black and

white stones? I rather listen to John Gabriel.

Ross Finlayson schrieb am Freitag, 2. Juni 2023 um 18:42:40 UTC+2:
> I "think" <~~ There is a lot doubt here

[Mild Shock]

Maybe Rossy Boy never went to school. He should
know that antonyms or words that belong to an
enumeration or a measurement, often have a category

that combines the words into a domain. You find
these ideas already discussed in Aristoteles, he
provides a nice upper ontology for all that.

Example:
- female
- male

The category is:
- gender

So a grown up would summarize a topic much shorter,
in that we would say the book covers gender issues.
Only a little school boy would write the book covers

female and male issues. The later is kind of idiotic.

[Mild Shock]

Maybe we can ask ChatGPT to make a summary. A summary with
would join antonyms in their upper category. Usually its the job
of the lexicographer to collect word stems and make a little

glossary for each word stem, that then describes the word stem.
The knowledge engeiner can use these descriptions to weave a
semantic net, which puts the meaning behind the word stems

into relation. A publicitly available semantic net of this kind is
WordNet. We can for example query it online here:

WordNet Search - 3.1
http://wordnetweb.princeton.edu/perl/webwn

For example female has two meanings, this is from
the lexicographer level:

S: (n) female, female person (a person who belongs
to the sex that can have babies)
S: (adj) female (being the sex (of plant or animal) that
produces fertilizable gametes (ova) from which offspring
develop) "a female heir"; "female holly trees bear the berries"

Thats why the general category could be peoples or gender (sex).
You can now use the WordNet website and click on "S",
and you will see semantic net information. For example antonyms:

S: (n) female, female person (a person who belongs to the sex
that can have babies)
antonym
W: (n) male [Opposed to: female] (a person who belongs to
the sex that cannot have babies)

S: (adj) female (being the sex (of plant or animal) that
produces fertilizable gametes (ova) from which
offspring develop) "a female heir"; "female holly
trees bear the berries"
antonym
W: (adj) androgynous [Opposed to: female]
(having both male and female characteristics)
W: (adj) male [Opposed to: female] (being the sex
(of plant or animal) that produces gametes (spermatozoa)
that perform the fertilizing function in generation)
"a male infant"; "a male holly tree"

Concerning antonym, WordNet doesn't only spit out strict
opposites. If the domain D is multivalued, it spits out
D \ {s} which can have more than one member.

Ross Finlayson schrieb am Montag, 29. Mai 2023 um 06:51:51 UTC+2:
> ... galloping nonsense like: ...
> One hopes that someday you might understand
> that "ALGEBRAIC geometry" is not "algebraic GEOMETRY".