info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Justifying the truth table for the IMPLIES-operator
317 views
Skip to first unread message
Message has been deleted
Dan Christensen
Sep 21, 2022, 1:22:18 AM9/21/22
to
Here is the truth table for the IMPLIES-operator:
A B A=>B
T T T
T F F
F T T
F F T
Judging by frequent questions at MSE (at least once every day) on this topic, there seems to be much confusion about this one, simple table.
This table is often used to "define" the IMPLIES-operator in introductory textbooks. No real explanation is usually given, just a few examples. There is a good reason for this, namely that to truly understand why it works, you must understand some basic methods of proof, i.e. the following rules of inference in propositional logic:
1. Premise
2. Conclusion (intro =>, intro ~)
3. Join (intro &)
4. Split (elim &)
5. Detachment (elim =>)
6. Remove ~~
(For an excellent introduction to these rules of inference, you need only work your way through only the first 3 (of 13) examples in the DC Proof tutorial.)
The above truth table is really just a table of the following 4 theorems in propositional logic:
1. A & B => [A => B]
2. A & ~B => ~[A => B]
3. ~A & B => [A => B]
4. ~A & ~B => [A => B]
*****************************************************************
Thm 1: A & B => [A => B]
1. A & B
Premise
2. A
Premise
3. B
Split, 1
4. A => B
Conclusion, 2
5. A & B => [A => B]
Conclusion, 1
*****************************************************************
Thm 2: A & ~B => ~[A => B]
1. A & ~B
Premise
2. A => B
Premise
3. A
Split, 1
4. ~B
Split, 1
5. B
Detach, 2, 3
6. ~B & B
Join, 4, 5
7. ~[A => B]
Conclusion, 2
8. A & ~B => ~[A => B]
Conclusion, 1
*****************************************************************
Thm 3: ~A & B => [A => B]
1. ~A & B
Premise
2. A
Premise
3. B
Split, 1
4. A => B
Conclusion, 2
5. ~A & B => [A => B]
Conclusion, 1
*****************************************************************
Thm 4: ~A & ~B => [A => B]
1. ~A & ~B
Premise
2. A
Premise
3. ~B
Premise
4. ~A
Split, 1
5. A & ~A
Join, 2, 4
6. ~~B
Conclusion, 3
7. B
Rem DNeg, 6
8. A => B
Conclusion, 2
9. ~A & ~B => [A => B]
Conclusion, 1
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
A B A=>B
T T T
T F F
F T T
F F T
Judging by frequent questions at MSE (at least once every day) on this topic, there seems to be much confusion about this one, simple table.
This table is often used to "define" the IMPLIES-operator in introductory textbooks. No real explanation is usually given, just a few examples. There is a good reason for this, namely that to truly understand why it works, you must understand some basic methods of proof, i.e. the following rules of inference in propositional logic:
1. Premise
2. Conclusion (intro =>, intro ~)
3. Join (intro &)
4. Split (elim &)
5. Detachment (elim =>)
6. Remove ~~
(For an excellent introduction to these rules of inference, you need only work your way through only the first 3 (of 13) examples in the DC Proof tutorial.)
The above truth table is really just a table of the following 4 theorems in propositional logic:
1. A & B => [A => B]
2. A & ~B => ~[A => B]
3. ~A & B => [A => B]
4. ~A & ~B => [A => B]
*****************************************************************
Thm 1: A & B => [A => B]
1. A & B
Premise
2. A
Premise
3. B
Split, 1
4. A => B
Conclusion, 2
5. A & B => [A => B]
Conclusion, 1
*****************************************************************
Thm 2: A & ~B => ~[A => B]
1. A & ~B
Premise
2. A => B
Premise
3. A
Split, 1
4. ~B
Split, 1
5. B
Detach, 2, 3
6. ~B & B
Join, 4, 5
7. ~[A => B]
Conclusion, 2
8. A & ~B => ~[A => B]
Conclusion, 1
*****************************************************************
Thm 3: ~A & B => [A => B]
1. ~A & B
Premise
2. A
Premise
3. B
Split, 1
4. A => B
Conclusion, 2
5. ~A & B => [A => B]
Conclusion, 1
*****************************************************************
Thm 4: ~A & ~B => [A => B]
1. ~A & ~B
Premise
2. A
Premise
3. ~B
Premise
4. ~A
Split, 1
5. A & ~A
Join, 2, 4
6. ~~B
Conclusion, 3
7. B
Rem DNeg, 6
8. A => B
Conclusion, 2
9. ~A & ~B => [A => B]
Conclusion, 1
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
Mostowski Collapse
Sep 21, 2022, 3:04:48 AM9/21/22
to
If you know how material implications works, why do you write
nonsense like this here:
> > y=\=x => ~Bijection(id_y,x,x)
> Not true in general. What is your point, Jan Burse?
Do you have a pair y,x where the above statement
y=\=x => ~Bijection(id_y,x,x) is not true?
Hint: Must be a statement of the second row:
A B A=>B
T F F
nonsense like this here:
> > y=\=x => ~Bijection(id_y,x,x)
> Not true in general. What is your point, Jan Burse?
Do you have a pair y,x where the above statement
y=\=x => ~Bijection(id_y,x,x) is not true?
Hint: Must be a statement of the second row:
A B A=>B
T F F
Dan Christensen
Sep 21, 2022, 9:56:33 AM9/21/22
to
> If you know how material implications works, why do you write
> nonsense like this here:
>
> > > y=\=x => ~Bijection(id_y,x,x)
> > Not true in general. What is your point, Jan Burse?
>
> Do you have a pair y,x where the above statement
> y=\=x => ~Bijection(id_y,x,x) is not true?
>
Suppose x = {0} and y = {0, 1}. Then x=/=y and for all z in x, id_y(z) =z, i.e. id_y is a bijection on set x.
> nonsense like this here:
>
> > > y=\=x => ~Bijection(id_y,x,x)
> > Not true in general. What is your point, Jan Burse?
>
> Do you have a pair y,x where the above statement
> y=\=x => ~Bijection(id_y,x,x) is not true?
>
Ross A. Finlayson
Sep 21, 2022, 11:47:39 AM9/21/22
to
Message has been deleted
Fritz Feldhase
Sep 21, 2022, 12:08:55 PM9/21/22
to
On Wednesday, September 21, 2022 at 5:47:39 PM UTC+2, Ross A. Finlayson wrote:
> What's 0^0 again?
1 .
By two different definitions:
a.) ^ defined recursively on IN:
Let m e IN:
m^0 = 1
m^(n+1) = m^n * m (for all n e IN)
b.) "set-theoretically" on IN (where IN is defined due to von Neumann):
m^n = card({f : n --> m}) (for all n, m e IN)
> What's 0^0 again?
1 .
By two different definitions:
a.) ^ defined recursively on IN:
Let m e IN:
m^0 = 1
m^(n+1) = m^n * m (for all n e IN)
b.) "set-theoretically" on IN (where IN is defined due to von Neumann):
m^n = card({f : n --> m}) (for all n, m e IN)
Dan Christensen
Sep 21, 2022, 1:28:57 PM9/21/22
to
On Wednesday, September 21, 2022 at 1:22:18 AM UTC-4, Dan Christensen wrote:
> Here is the truth table for the IMPLIES-operator:
>
> A B A=>B
> T T T
> T F F
> F T T
> F F T
>
> Judging by frequent questions at MSE (at least once every day) on this topic, there seems to be much confusion about this one, simple table.
>
> This table is often used to "define" the IMPLIES-operator in introductory textbooks. No real explanation is usually given, just a few examples. There is a good reason for this, namely that to truly understand why it works, you must understand some basic methods of proof, i.e. the following rules of inference in propositional logic:
>
> 1. Premise
> 2. Conclusion (intro =>, intro ~)
> 3. Join (intro &)
> 4. Split (elim &)
> 5. Detachment (elim =>)
> 6. Remove ~~
>
> (For an excellent introduction to these rules of inference, you need only work your way through only the first 3 (of 13) examples in the DC Proof tutorial.)
>
> The above truth table is really just a table of the following 4 theorems in propositional logic:
>
> 1. A & B => [A => B]
>
> 2. A & ~B => ~[A => B]
>
> 3. ~A & B => [A => B]
>
> 4. ~A & ~B => [A => B]
>
Started working on an update to the DC Proof tutorial to include these theorems as exercises with hints and full solutions. Should have thought of this years ago! The perfect proofs for the beginner--no more than 9 lines each and you don't even need that much logic. And IMHO quite profound when taken as a whole.
> Here is the truth table for the IMPLIES-operator:
>
> A B A=>B
> T T T
> T F F
> F T T
> F F T
>
> Judging by frequent questions at MSE (at least once every day) on this topic, there seems to be much confusion about this one, simple table.
>
> This table is often used to "define" the IMPLIES-operator in introductory textbooks. No real explanation is usually given, just a few examples. There is a good reason for this, namely that to truly understand why it works, you must understand some basic methods of proof, i.e. the following rules of inference in propositional logic:
>
> 1. Premise
> 2. Conclusion (intro =>, intro ~)
> 3. Join (intro &)
> 4. Split (elim &)
> 5. Detachment (elim =>)
> 6. Remove ~~
>
> (For an excellent introduction to these rules of inference, you need only work your way through only the first 3 (of 13) examples in the DC Proof tutorial.)
>
> The above truth table is really just a table of the following 4 theorems in propositional logic:
>
> 1. A & B => [A => B]
>
> 2. A & ~B => ~[A => B]
>
> 3. ~A & B => [A => B]
>
> 4. ~A & ~B => [A => B]
>
Dan Christensen
Sep 21, 2022, 2:01:08 PM9/21/22
to
On Wednesday, September 21, 2022 at 11:47:39 AM UTC-4, Ross A. Finlayson wrote:
[snip]
> What's 0^0 again?
Huh? Oh, I see... You would rather change the subject. Can't blame you, really.
See: https://dcproof.wordpress.com/2013/10/09/oh-the-ambiguity-2/
Start a new thread if you want to rehash it after all these years. Could be fun.
[snip]
> What's 0^0 again?
Huh? Oh, I see... You would rather change the subject. Can't blame you, really.
See: https://dcproof.wordpress.com/2013/10/09/oh-the-ambiguity-2/
Start a new thread if you want to rehash it after all these years. Could be fun.
Dan Christensen
Sep 21, 2022, 7:55:31 PM9/21/22
to
On Wednesday, September 21, 2022 at 1:28:57 PM UTC-4, Dan Christensen wrote:
> On Wednesday, September 21, 2022 at 1:22:18 AM UTC-4, Dan Christensen wrote:
> > Here is the truth table for the IMPLIES-operator:
> >
> > A B A=>B
> > T T T
> > T F F
> > F T T
> > F F T
> >
> > Judging by frequent questions at MSE (at least once every day) on this topic, there seems to be much confusion about this one, simple table.
> >
> > This table is often used to "define" the IMPLIES-operator in introductory textbooks. No real explanation is usually given, just a few examples. There is a good reason for this, namely that to truly understand why it works, you must understand some basic methods of proof, i.e. the following rules of inference in propositional logic:
> >
> > 1. Premise
> > 2. Conclusion (intro =>, intro ~)
> > 3. Join (intro &)
> > 4. Split (elim &)
> > 5. Detachment (elim =>)
> > 6. Remove ~~
> >
> > (For an excellent introduction to these rules of inference, you need only work your way through only the first 3 (of 13) examples in the DC Proof tutorial.)
> >
> > The above truth table is really just a table of the following 4 theorems in propositional logic:
> >
> > 1. A & B => [A => B]
> >
> > 2. A & ~B => ~[A => B]
> >
> > 3. ~A & B => [A => B]
> >
> > 4. ~A & ~B => [A => B]
> >
> Started working on an update to the DC Proof tutorial to include these theorems as exercises with hints and full solutions. Should have thought of this years ago! The perfect proofs for the beginner--no more than 9 lines each and you don't even need that much logic. And IMHO quite profound when taken as a whole.
Now available at my homepage.
> On Wednesday, September 21, 2022 at 1:22:18 AM UTC-4, Dan Christensen wrote:
> > Here is the truth table for the IMPLIES-operator:
> >
> > A B A=>B
> > T T T
> > T F F
> > F T T
> > F F T
> >
> > Judging by frequent questions at MSE (at least once every day) on this topic, there seems to be much confusion about this one, simple table.
> >
> > This table is often used to "define" the IMPLIES-operator in introductory textbooks. No real explanation is usually given, just a few examples. There is a good reason for this, namely that to truly understand why it works, you must understand some basic methods of proof, i.e. the following rules of inference in propositional logic:
> >
> > 1. Premise
> > 2. Conclusion (intro =>, intro ~)
> > 3. Join (intro &)
> > 4. Split (elim &)
> > 5. Detachment (elim =>)
> > 6. Remove ~~
> >
> > (For an excellent introduction to these rules of inference, you need only work your way through only the first 3 (of 13) examples in the DC Proof tutorial.)
> >
> > The above truth table is really just a table of the following 4 theorems in propositional logic:
> >
> > 1. A & B => [A => B]
> >
> > 2. A & ~B => ~[A => B]
> >
> > 3. ~A & B => [A => B]
> >
> > 4. ~A & ~B => [A => B]
> >
> Started working on an update to the DC Proof tutorial to include these theorems as exercises with hints and full solutions. Should have thought of this years ago! The perfect proofs for the beginner--no more than 9 lines each and you don't even need that much logic. And IMHO quite profound when taken as a whole.
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com <------- Here
Fritz Feldhase
Sep 21, 2022, 8:00:20 PM9/21/22
to
Let n, m e IN. Then
n + m = card(n x {0} u m x {1}) ,
n * m = card(n x m) ,
n ^ m = card({f | f : m --> n}) .
n = 0 and/or m = 0 is no "special case" here.
Actually, we would "artificially" have to treat 0^0 as a special case to "avoid" the result 1. But there is absolutely no reason to do so (in this context).
Ross A. Finlayson
Sep 21, 2022, 9:54:01 PM9/21/22
to
just pointing out that your stipulations and
"showing your work" about fail given alternatives.
I know you "have to have it your way", but when it comes
to usual set-theoretic disambiguation, you're just a usual
shill and fool.
Showing that now your "implies is inference" also fails
your other failings about the maintenance of the truth-valued
in truth tables and no "false antecedents",
you false antecedent.
Just change the order of stipulations of your proofs they
change what they say. Don't you think inference should
be a little more reliable than assuming what you set out to prove?
No offense, it's a little "show your work" tool for some reasoning,
but it's weak and compounded by "false antecedents in a world
of truth tables", it's further "garbage-in garbage-out".
Then, really I do not care what you think "0^0" is,
just pointing out that you think you do,
but there's more than one answer, so,
one of yours must be wrong.
Dan Christensen
Sep 21, 2022, 10:37:33 PM9/21/22
to
On Wednesday, September 21, 2022 at 9:54:01 PM UTC-4, Ross A. Finlayson wrote:
> On Wednesday, September 21, 2022 at 11:01:08 AM UTC-7, Dan Christensen wrote:
> > On Wednesday, September 21, 2022 at 11:47:39 AM UTC-4, Ross A. Finlayson wrote:
> >
> > [snip]
> >
> > > What's 0^0 again?
> >
> > Huh? Oh, I see... You would rather change the subject. Can't blame you, really.
> >
> > See: https://dcproof.wordpress.com/2013/10/09/oh-the-ambiguity-2/
> >
> > Start a new thread if you want to rehash it after all these years. Could be fun.
[snip]
> On Wednesday, September 21, 2022 at 11:01:08 AM UTC-7, Dan Christensen wrote:
> > On Wednesday, September 21, 2022 at 11:47:39 AM UTC-4, Ross A. Finlayson wrote:
> >
> > [snip]
> >
> > > What's 0^0 again?
> >
> > Huh? Oh, I see... You would rather change the subject. Can't blame you, really.
> >
> > See: https://dcproof.wordpress.com/2013/10/09/oh-the-ambiguity-2/
> >
> > Start a new thread if you want to rehash it after all these years. Could be fun.
So, you would rather not. Very wise.
> Don't you think inference should
> be a little more reliable than assuming what you set out to prove?
>
Where do you imagine that I assume ~A & B => [A => B] ?
Here again is my proof:
1. ~A & B
Premise
2. A
Premise
3. B
Split, 1
4. A => B
Conclusion, 2
5. ~A & B => [A => B]
Conclusion, 1
Ross A. Finlayson
Sep 22, 2022, 11:30:55 AM9/22/22
to
For example, A as "A is premise 1", i.e. whether A or not A,
then "A is premise 2", it's an example of a generic premise
that according to its introduction, and what so follows,
doesn't admit false antecedents, at all.
What otherwise you have there as a template for "wrong".
Ross A. Finlayson
Sep 22, 2022, 11:59:57 AM9/22/22
to
all these guns that shoot backward.
Then you forget which ones you put where, and none of them are safe.
You got no reliable reverse "material" implication.
What you've written there is "not-A not-implies-B", not, "not-A not not-implies-not-B",
that a false antecedent is always "not implies".
Which is not necessarily "implies".
Leave "material" "implication" out of things, direct implication only. It's about
one of the stupidest kinds of notational laziness.
Don't you have any kind of object in your theory that changes?
Can't a _change_ even possibly be an object in your little theory?
Then it's like you say "whu all these are constants" then it's like
"you mean your variables, ...".
Mostowski Collapse
Sep 22, 2022, 12:42:51 PM9/22/22
to
Nope, id_y isn't a bijection x -> x, it has missing
dom(id_y) = x
id_y is not member of this function space:
{ f : x -> x | f bijective }
Whats wrong with you?
dom(id_y) = x
id_y is not member of this function space:
{ f : x -> x | f bijective }
Whats wrong with you?
Dan Christensen
Sep 22, 2022, 12:47:29 PM9/22/22
to
On Thursday, September 22, 2022 at 11:30:55 AM UTC-4, Ross A. Finlayson wrote:
> On Wednesday, September 21, 2022 at 7:37:33 PM UTC-7, Dan Christensen wrote:
> > On Wednesday, September 21, 2022 at 9:54:01 PM UTC-4, Ross A. Finlayson wrote:
> > > On Wednesday, September 21, 2022 at 11:01:08 AM UTC-7, Dan Christensen wrote:
> > > > On Wednesday, September 21, 2022 at 11:47:39 AM UTC-4, Ross A. Finlayson wrote:
> > > >
> > > > [snip]
> > > >
> > > > > What's 0^0 again?
> > > >
> > > > Huh? Oh, I see... You would rather change the subject. Can't blame you, really.
> > > >
> > > > See: https://dcproof.wordpress.com/2013/10/09/oh-the-ambiguity-2/
> > > >
> > > > Start a new thread if you want to rehash it after all these years. Could be fun.
> > [snip]
> >
> > So, you would rather not. Very wise.
> > > Don't you think inference should
> > > be a little more reliable than assuming what you set out to prove?
> > >
> > [snip]
> >
> > Where do you imagine that I assume ~A & B => [A => B] ?
> >
No comment?
> On Wednesday, September 21, 2022 at 7:37:33 PM UTC-7, Dan Christensen wrote:
> > On Wednesday, September 21, 2022 at 9:54:01 PM UTC-4, Ross A. Finlayson wrote:
> > > On Wednesday, September 21, 2022 at 11:01:08 AM UTC-7, Dan Christensen wrote:
> > > > On Wednesday, September 21, 2022 at 11:47:39 AM UTC-4, Ross A. Finlayson wrote:
> > > >
> > > > [snip]
> > > >
> > > > > What's 0^0 again?
> > > >
> > > > Huh? Oh, I see... You would rather change the subject. Can't blame you, really.
> > > >
> > > > See: https://dcproof.wordpress.com/2013/10/09/oh-the-ambiguity-2/
> > > >
> > > > Start a new thread if you want to rehash it after all these years. Could be fun.
> > [snip]
> >
> > So, you would rather not. Very wise.
> > > Don't you think inference should
> > > be a little more reliable than assuming what you set out to prove?
> > >
> > [snip]
> >
> > Where do you imagine that I assume ~A & B => [A => B] ?
> >
> > Here again is my proof:
> > 1. ~A & B
> > Premise
> >
> > 2. A
> > Premise
> >
> > 3. B
> > Split, 1
> >
> > 4. A => B
> > Conclusion, 2
> >
> > 5. ~A & B => [A => B]
> > Conclusion, 1
> You have no concept of time, the modal, or change.
>
I am looking the state of "the world" at some instant in time (usually the present). A snapshot. It may sound limiting, but it turns out to be extremely useful in the real world and in mathematics.
>
The statement, "If it is raining then it is cloudy" means only that, at present, it is not both raining and not cloudy. It does NOT mean that rain causes cloudiness. Or that, historically, whenever it was raining it was also cloudy.
> For example, A as "A is premise 1", i.e. whether A or not A,
> then "A is premise 2", it's an example of a generic premise
> that according to its introduction, and what so follows,
> doesn't admit false antecedents, at all.
>
EXAMPLE
1 A & ~A
Premise
2 ~[A & ~A]
Mostowski Collapse
Sep 22, 2022, 12:49:00 PM9/22/22
to
Usually in set theory this here should hold for product function spaces:
Definition: 4.2.6 The Exponentiation Axiom (abbreviated Exp) postulates
that for sets a; b the class of all functions from a to b forms a set:
∀a∀b∃c ∀f(f e c <-> (f : a -> b))
https://www1.maths.leeds.ac.uk/~rathjen/book.pdf
You can even strengthen it to ∃!c. Now it seems in
DC Spoiled, the notion of product function space is
shape shifting, and so are function spaces that are
subset of the product function space, like this here:
{ f : x -> x | f bijective }
If id_y is element of the above function space, this
would imply that x -> x and y -> y are not disjoint,
for x =\= y. But usually they are disjoint, even in the
set theoretic approach, and also in the Bourbaki approach.
LMAO!
Definition: 4.2.6 The Exponentiation Axiom (abbreviated Exp) postulates
that for sets a; b the class of all functions from a to b forms a set:
∀a∀b∃c ∀f(f e c <-> (f : a -> b))
https://www1.maths.leeds.ac.uk/~rathjen/book.pdf
You can even strengthen it to ∃!c. Now it seems in
DC Spoiled, the notion of product function space is
shape shifting, and so are function spaces that are
subset of the product function space, like this here:
{ f : x -> x | f bijective }
would imply that x -> x and y -> y are not disjoint,
for x =\= y. But usually they are disjoint, even in the
set theoretic approach, and also in the Bourbaki approach.
LMAO!
Dan Christensen
Sep 22, 2022, 1:13:28 PM9/22/22
to
> What you've written there is "not-A not-implies-B", not, "not-A not not-implies-not-B",
> that a false antecedent is always "not implies".
>
> Which is not necessarily "implies".
>
> Leave "material" "implication" out of things, direct implication only. It's about
> one of the stupidest kinds of notational laziness.
>
1. Premise
2. Conclusion (intro =>, intro ~)
3. Join (intro &)
4. Split (elim &)
5. Detachment (elim =>)
6. Remove ~~
> Don't you have any kind of object in your theory that changes?
You could interpret some independent variable t as time with different values of t corresponding to different points in space if that's what you mean? But that's getting into the realm of science.
Dan Christensen
Sep 22, 2022, 1:29:14 PM9/22/22
to
On Thursday, September 22, 2022 at 12:49:00 PM UTC-4, Mostowski Collapse wrote:
[snip]
> Usually in set theory this here should hold for product function spaces:
>
> Definition: 4.2.6 The Exponentiation Axiom (abbreviated Exp) postulates
> that for sets a; b the class of all functions from a to b forms a set:
> ∀a∀b∃c ∀f(f e c <-> (f : a -> b))
> https://www1.maths.leeds.ac.uk/~rathjen/book.pdf
>
Not unlike the DC Proof Function Space axiom:
ALL(dom):ALL(cod):[Set(dom) & Set(cod)
=> EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> Function(f,dom,cod) & ALL(a1):[a1 in dom => f(a1) in cod]]]]
> You can even strengthen it to ∃!c. Now it seems in
> DC Proof, the notion of product function space is
[snip]
> Usually in set theory this here should hold for product function spaces:
>
> Definition: 4.2.6 The Exponentiation Axiom (abbreviated Exp) postulates
> that for sets a; b the class of all functions from a to b forms a set:
> ∀a∀b∃c ∀f(f e c <-> (f : a -> b))
> https://www1.maths.leeds.ac.uk/~rathjen/book.pdf
>
ALL(dom):ALL(cod):[Set(dom) & Set(cod)
=> EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> Function(f,dom,cod) & ALL(a1):[a1 in dom => f(a1) in cod]]]]
> You can even strengthen it to ∃!c. Now it seems in
> shape shifting, and so are function spaces that are
> subset of the product function space, like this here:
> { f : x -> x | f bijective }
> If id_y is element of the above function space, this
> would imply that x -> x and y -> y are not disjoint,
> for x =\= y.
If, however, x is a proper subset of y, we can say that id_y (the identity function on set y) is also a bijection on set x .
> subset of the product function space, like this here:
> { f : x -> x | f bijective }
> If id_y is element of the above function space, this
> would imply that x -> x and y -> y are not disjoint,
> for x =\= y.
Mostowski Collapse
Sep 22, 2022, 4:06:24 PM9/22/22
to
Dan Christensen halucinated on Thursday, 22. September 2022:
What does exist in mathematics, is the operation restriction:
f | A = { (x,y) e f | x e A }
And you can for example say:
id_X = id_Y | X
for X ⊆ Y. And subsequetly you can also say id_Y | X is a X -> X bijection.
This is all explained in the very first chapters here:
Basic Set Theory (Dover Books on Mathematics)
Azriel Levy - Revised Edition (13. August 2002)
https://www.amazon.com/dp/0486420795
Or read wikipedia:
In mathematics, the restriction of a function f is a new function, denoted f | A
https://en.wikipedia.org/wiki/Restriction_%28mathematics%29
> If, however, x is a proper subset of y, we can say that id_y (the identity function on set y) is also a bijection on set x .
No you cannot say that. People don't say that.
What does exist in mathematics, is the operation restriction:
f | A = { (x,y) e f | x e A }
And you can for example say:
id_X = id_Y | X
for X ⊆ Y. And subsequetly you can also say id_Y | X is a X -> X bijection.
This is all explained in the very first chapters here:
Basic Set Theory (Dover Books on Mathematics)
Azriel Levy - Revised Edition (13. August 2002)
https://www.amazon.com/dp/0486420795
Or read wikipedia:
In mathematics, the restriction of a function f is a new function, denoted f | A
https://en.wikipedia.org/wiki/Restriction_%28mathematics%29
Dan Christensen
Sep 22, 2022, 5:09:31 PM9/22/22
to
On Thursday, September 22, 2022 at 4:06:24 PM UTC-4, Mostowski Collapse wrote:
> > If, however, x is a proper subset of y, we can say that id_y (the identity function on set y) is also a bijection on set x .
> No you cannot say that. People don't say that.
>
> What does exist in mathematics, is the operation restriction:
>
> f | A = { (x,y) e f | x e A }
>
> And you can for example say:
>
> id_X = id_Y | X
>
> for X ⊆ Y. And subsequetly you can also say id_Y | X is a X -> X bijection.
>
In other words, like I said, "id_y is a bijection on set x."
> > If, however, x is a proper subset of y, we can say that id_y (the identity function on set y) is also a bijection on set x .
> No you cannot say that. People don't say that.
>
> What does exist in mathematics, is the operation restriction:
>
> f | A = { (x,y) e f | x e A }
>
> And you can for example say:
>
> id_X = id_Y | X
>
> for X ⊆ Y. And subsequetly you can also say id_Y | X is a X -> X bijection.
>
Thanks for clearing that up, Jan Burse. (Hee, hee!)
Mostowski Collapse
Sep 22, 2022, 5:32:17 PM9/22/22
to
Nope, id_y | x is a bijection on x.
id_y isn't a bijection on x.
Whats wrong with you?
Dan Christensen schrieb:
id_y isn't a bijection on x.
Whats wrong with you?
Dan Christensen schrieb:
Dan Christensen
Sep 22, 2022, 6:56:36 PM9/22/22
to
On Thursday, September 22, 2022 at 5:32:17 PM UTC-4, Mostowski Collapse wrote:
> Nope, id_y | x is a bijection on x.
> id_y isn't a bijection on x.
>
It is. Deal with it, Jan Burse.
> Nope, id_y | x is a bijection on x.
> id_y isn't a bijection on x.
>
Mostowski Collapse
Sep 22, 2022, 8:12:35 PM9/22/22
to
Not in math text books. Did your mama
notice that you are brain damaged?
The word "is a" translates to membership,
so the two sentences translate to:
id_y | x e { f : x -> x | f bijective }
id_y e { f : x -> x | f bijective }
For x ⊆ y & x =\= y only the first membership
is true, the second membership is false.
Dan Christensen schrieb:
Dan Christensen
Sep 22, 2022, 10:30:51 PM9/22/22
to
On Thursday, September 22, 2022 at 8:12:35 PM UTC-4, Mostowski Collapse wrote:
> For x ⊆ y & x =\= y only the first membership
> is true, the second membership is false.
>
> Dan Christensen schrieb:
> > On Thursday, September 22, 2022 at 5:32:17 PM UTC-4, Mostowski Collapse wrote:
> >> Nope, id_y | x is a bijection on x.
> >> id_y isn't a bijection on x.
> >>
> >
> > It is. Deal with it, Jan Burse.
> >
> For x ⊆ y & x =\= y only the first membership
> is true, the second membership is false.
>
> Dan Christensen schrieb:
> > On Thursday, September 22, 2022 at 5:32:17 PM UTC-4, Mostowski Collapse wrote:
> >> Nope, id_y | x is a bijection on x.
> >> id_y isn't a bijection on x.
> >>
> >
> > It is. Deal with it, Jan Burse.
> >
> Not in math text books.
[snip childish abuse]
>
> The word "is a" translates to membership,
> so the two sentences translate to:
>
> id_y | x e { f : x -> x | f bijective }
> id_y e { f : x -> x | f bijective }
>
Here is a the usual definition/abbreviation for the bijectivity predicate:
ALL(f):ALL(a):ALL(b):[Bijective(f,a,b) <=>
[ALL(c):ALL(d):[c in a & d in a => [f(c)=f(d) => c=d]] & ALL(c):[c in b => EXIST(d):[d in a & f(d)=c]]]
It's use is optional. It is used only to improve readability. Instead of writing the abbreviation Bijective(f,a,b), you could write it out in full as:
ALL(c):ALL(d):[c in a & d in a => [f(c)=f(d) => c=d]] & ALL(c):[c in b => EXIST(d):[d in a & f(d)=c]]
From the definitions of x, y and id_y above, we have Bijective(id_y,x,x). Deal with it, Jan Burse. Just admit you were wrong.
Fritz Feldhase
Sep 22, 2022, 11:27:42 PM9/22/22
to
On Friday, September 23, 2022 at 4:30:51 AM UTC+2, Dan Christensen wrote:
> Here is a
nonsensical
> definition/abbreviation for the bijectivity predicate:
>
> ALL(f):ALL(a):ALL(b):[Bijective(f,a,b) <=>
> [ALL(c):ALL(d):[c in a & d in a => [f(c)=f(d) => c=d]] & ALL(c):[c in b => EXIST(d):[d in a & f(d)=c]]]
Yeah, it's nonsense.
> Here is a
nonsensical
> definition/abbreviation for the bijectivity predicate:
>
> ALL(f):ALL(a):ALL(b):[Bijective(f,a,b) <=>
> [ALL(c):ALL(d):[c in a & d in a => [f(c)=f(d) => c=d]] & ALL(c):[c in b => EXIST(d):[d in a & f(d)=c]]]
Dan Christensen
Sep 22, 2022, 11:50:47 PM9/22/22
to
On Thursday, September 22, 2022 at 11:27:42 PM UTC-4, Fritz Feldhase wrote:
> On Friday, September 23, 2022 at 4:30:51 AM UTC+2, Dan Christensen wrote:
>
> > Here is definition/abbreviation for the bijectivity predicate:
> On Friday, September 23, 2022 at 4:30:51 AM UTC+2, Dan Christensen wrote:
>
> >
> > ALL(f):ALL(a):ALL(b):[Bijective(f,a,b) <=>
> > [ALL(c):ALL(d):[c in a & d in a => [f(c)=f(d) => c=d]] & ALL(c):[c in b => EXIST(d):[d in a & f(d)=c]]]
> Yeah, it's nonsense.
Oh, really? How do YOU define Bijective(f,a,b), Fritz?
> > ALL(f):ALL(a):ALL(b):[Bijective(f,a,b) <=>
> > [ALL(c):ALL(d):[c in a & d in a => [f(c)=f(d) => c=d]] & ALL(c):[c in b => EXIST(d):[d in a & f(d)=c]]]
> Yeah, it's nonsense.
Ross A. Finlayson
Oct 6, 2022, 9:49:48 PM10/6/22
to
And, for any b in B, there exists unique a in A such that F^-1(b) = a.
There exists F.
Here the unique part of course means for-any a, exists b, not exists
c =/= b, s.t. F(a) = c, and vice versa.
These days often set theorists are lazy and let Cantor/Schroeder/Bernstein thm.
work out there "exists" such an F, while of course it must result the above.
Ross A. Finlayson
Oct 6, 2022, 9:52:44 PM10/6/22
to
and it's pretty clear the rules are absolutely arbitrary.
Ross A. Finlayson
Oct 6, 2022, 10:56:08 PM10/6/22
to
You did say "function", right?
You got DesCartes, and for DesCartes, it was the time of geometry defining function.
So, the Cartesian function, it's the space of all the single value mappings from domain
to codomain. (Domain, image, domain, range, domain, codomain, image.)
This is where in geometry the only "space" is supports here is a line in geometry. According
to, "Euclid", the line is what exists and there are points on it. So, that's "not" a Cartesian function.
(I.e. functions like it without otherwise the multivalent are "discontinuous" functions.)
Which among them are series, ....
Ross A. Finlayson
Oct 6, 2022, 11:25:02 PM10/6/22
to
extra conditions will never reverse on me when taken the wrong way".
Also called "science".
Yeah, why don't you put "science" first in all your theorems.
The "science": part is only for the "non-logical",
the "logical" is already "logical".
Of course there's syllogism, where words are abstract non-logically.
Mostly "fulfills question words with respect to is or has".
Ross A. Finlayson
Oct 6, 2022, 11:31:29 PM10/6/22
to
Dan Christensen
Oct 6, 2022, 11:59:38 PM10/6/22
to
>
> Yeah, why don't you put "science" first in all your theorems.
>
Can you give even a single example of an actual error in science, engineering or any other human endeavour arising strictly from the application of faulty rules of logic that you imagine? What were the consequences? How many lives were lost or ruined, etc.
Ross A. Finlayson
Oct 7, 2022, 12:05:40 AM10/7/22
to
It's about the shortest way to say it, ....
(... insert Wiki ....)
Dan Christensen
Oct 7, 2022, 12:18:15 AM10/7/22
to
On Friday, October 7, 2022 at 12:05:40 AM UTC-4, Ross A. Finlayson wrote:
> >
> > Can you give even a single example of an actual error in science, engineering or any other human endeavour arising strictly from the application of faulty rules of logic that you imagine? What were the consequences? How many lives were lost or ruined, etc.
> >
> > Can you give even a single example of an actual error in science, engineering or any other human endeavour arising strictly from the application of faulty rules of logic that you imagine? What were the consequences? How many lives were lost or ruined, etc.
> If you ever forget that I'd feel sorry for you.
>
> It's about the shortest way to say it, ....
>
>
>
> (... insert Wiki ....)
So, not a single example. A tempest in a teacup, then. Whew!
>
> It's about the shortest way to say it, ....
>
>
>
> (... insert Wiki ....)
Dan
Ross A. Finlayson
Oct 7, 2022, 12:19:23 AM10/7/22
to
Dan Christensen
Oct 7, 2022, 12:49:04 AM10/7/22
to
> You did say function, right?
Get to the point, Ross.
Dan
Ross A. Finlayson
Oct 7, 2022, 2:41:55 AM10/7/22
to
Mostowski Collapse
Oct 7, 2022, 7:42:46 PM10/7/22
to
Maybe should launch a basic class in logic that
explains domain of discourse. Wonky man has
absolute no clue what it means for the Drinker Paradox
to deal with this issue:
"This proof illustrates several properties of classical
predicate logic which do not always agree with
ordinary language.
Non-Empty Domain"
https://paradox.fandom.com/wiki/Drinker_paradox
He still thinks some Russel Paradox and juggling with
sets is behind the Drinker Paradox. A complete
hopleless case wonky man aka Dan Christensen,
once a crank always a crank.
LMAO!
explains domain of discourse. Wonky man has
absolute no clue what it means for the Drinker Paradox
to deal with this issue:
"This proof illustrates several properties of classical
predicate logic which do not always agree with
ordinary language.
Non-Empty Domain"
https://paradox.fandom.com/wiki/Drinker_paradox
He still thinks some Russel Paradox and juggling with
sets is behind the Drinker Paradox. A complete
hopleless case wonky man aka Dan Christensen,
once a crank always a crank.
LMAO!
Mostowski Collapse
Oct 7, 2022, 7:55:02 PM10/7/22
to
Thats a recuring problem with wonky man, if you tell
him, that you work in the natural numbers, he starts
fiddling with this here:
x e N
Introducing another level, sets of natural numbers.
He is just plain crazy and doesn't understand elementary
wordings like these:
- Drinker Paradox: The people in a pub ...
- Liar Paradox: The people on an island ...
- Number Theory: The natural numbers ...
-
If mathematicians or logicians really want to quantify
over other stuff, they say so initially, like they mention sets
or functions, or they say they go higher order and not
first order. But if somebody say "The Natural Numbers",
then its not x e N, then its the domain of discourse is the
natural numbers. And you cannot have a set which is
the unversal set. If you introduce a first class object N,
and if it is a set, it cannot be the domain of discourse.
You can prove that with DC Spoiled itself, that introducing
N destroys the idea of working with natural numbers:
/* Previous Result http://www.dcproof.com/UniversalSet.htm */
1 ALL(s):[Set(s) => EXIST(a):~a ε s]
Axiom
2 Set(nat)
Axiom
3 Set(nat) => EXIST(a):~a ε nat
U Spec, 1
4 EXIST(a):~a ε nat
Detach, 3, 2
Oopsi, what is this thing outside of N?
LoL
him, that you work in the natural numbers, he starts
fiddling with this here:
x e N
Introducing another level, sets of natural numbers.
He is just plain crazy and doesn't understand elementary
wordings like these:
- Drinker Paradox: The people in a pub ...
- Liar Paradox: The people on an island ...
- Number Theory: The natural numbers ...
-
If mathematicians or logicians really want to quantify
over other stuff, they say so initially, like they mention sets
or functions, or they say they go higher order and not
first order. But if somebody say "The Natural Numbers",
then its not x e N, then its the domain of discourse is the
natural numbers. And you cannot have a set which is
the unversal set. If you introduce a first class object N,
and if it is a set, it cannot be the domain of discourse.
You can prove that with DC Spoiled itself, that introducing
N destroys the idea of working with natural numbers:
/* Previous Result http://www.dcproof.com/UniversalSet.htm */
1 ALL(s):[Set(s) => EXIST(a):~a ε s]
Axiom
2 Set(nat)
Axiom
3 Set(nat) => EXIST(a):~a ε nat
U Spec, 1
4 EXIST(a):~a ε nat
Detach, 3, 2
Oopsi, what is this thing outside of N?
LoL
Dan Christensen
Oct 7, 2022, 8:24:50 PM10/7/22
to
On Friday, October 7, 2022 at 7:42:46 PM UTC-4, Mostowski Collapse wrote:
> Maybe should launch a basic class in logic that
> explains domain of discourse.
Be sure to invite most mathematicians. There is no such thing in mathematics. For the most part, that it is in the domain of philosophers. Must be frustrating as hell for you,
> Maybe should launch a basic class in logic that
> explains domain of discourse.
> [snip childish abuse] has
> absolute no clue what it means for the Drinker Paradox
>
Jan Burse is still in denial. He should know better by now that, from ordinary set theory and logic, we know that for any set S and proposition Q (be it true or false), we have:
>
EXIST(x):[x in S => Q]
See my proof at the above link.
If S = the set of all drinkers, and Q is the proposition that all people in a given pub are drinkers, then we have the a set-theoretic version of the Drinker's Paradox. Deal with it, Jan Burse. Just admit your were wrong.
Mostowski Collapse
Oct 8, 2022, 4:57:04 PM10/8/22
to
The problem is you don't know what FOL is. Your
DC Spoiled is not FOL. And you cannot prove this
FOL theorem, namely the Drinker Paradox:
/* Not Provable in DC Spoiled, but Provable in FOL */
∃x(D(x) => ∀yD(y))
FOL is a modern development between 1900 - 1950.
In this periods a couple of publications appeared which
started classifying logics more clearly. One booklet
was Hilbert & Ackermann, Grundzüge der Theoretischen
Logik, which defined more clearly what FOL is. But you
find it also here in Gödels lecture, the simplest logics are:
1.1 Propositional logic
1.2 Predicate logic
Logic Lectures: Gödel's Basic Logic Course at Notre Dame
https://arxiv.org/abs/1705.02601
Neither of them can quatify function symbols as
DC Spoiled does. His lecture has a critical tone, and
you find sections like "Failure of traditional logic". First
thing Gödel does is this here:
1.2.5 Theorems and derived rules of the system for predicate logic
[74] ∀xPhi(x) ⊃ ∃xPhi(x) Syllogism
Which doesn't work in empty domain.
LoL
DC Spoiled is not FOL. And you cannot prove this
FOL theorem, namely the Drinker Paradox:
/* Not Provable in DC Spoiled, but Provable in FOL */
∃x(D(x) => ∀yD(y))
FOL is a modern development between 1900 - 1950.
In this periods a couple of publications appeared which
started classifying logics more clearly. One booklet
was Hilbert & Ackermann, Grundzüge der Theoretischen
Logik, which defined more clearly what FOL is. But you
find it also here in Gödels lecture, the simplest logics are:
1.1 Propositional logic
1.2 Predicate logic
Logic Lectures: Gödel's Basic Logic Course at Notre Dame
https://arxiv.org/abs/1705.02601
Neither of them can quatify function symbols as
DC Spoiled does. His lecture has a critical tone, and
you find sections like "Failure of traditional logic". First
thing Gödel does is this here:
1.2.5 Theorems and derived rules of the system for predicate logic
[74] ∀xPhi(x) ⊃ ∃xPhi(x) Syllogism
Which doesn't work in empty domain.
LoL
Dan Christensen
Oct 8, 2022, 6:27:42 PM10/8/22
to
See my reply just now to your identical posting at sci.math
Dan
On Saturday, October 8, 2022 at 4:57:04 PM UTC-4, Mostowski Collapse wrote:
> The problem is you don't know what FOL is. Your
> DC Spoiled is not FOL. And you cannot prove this
> FOL theorem, namely the Drinker Paradox:
>
[snip]
Dan
On Saturday, October 8, 2022 at 4:57:04 PM UTC-4, Mostowski Collapse wrote:
> The problem is you don't know what FOL is. Your
> DC Spoiled is not FOL. And you cannot prove this
> FOL theorem, namely the Drinker Paradox:
>
Fritz Feldhase
Oct 9, 2022, 12:22:53 AM10/9/22
to
On Saturday, October 8, 2022 at 2:24:50 AM UTC+2, Dan Christensen wrote:
> from ordinary set theory and logic, we know that for any set S and proposition Q (be it true or false), we have:
>
> EXIST(x):[x in S => Q]
So what?A rather trivial observation.
> from ordinary set theory and logic, we know that for any set S and proposition Q (be it true or false), we have:
>
> EXIST(x):[x in S => Q]
Hint: In ZF(C) ~(S in S) for any set S due to the axiom of foundation.
Hence
S in S -> Q
for any proposition Q (since "ex falso quodlibet").
Hence
Ex(x in S -> Q).
No "paradox" at all. No need to refer to Russell's Paradox.
Has nothing to do with the Drinker Paradox.
Mostowski Collapse
Oct 9, 2022, 5:28:45 AM10/9/22
to
Dan Christensen is the uber-crank. He not only beats John Gabriel,
he is on par with "John Gabriel: look I reinvented calculus, here is
new calculus", in that he has "Dan Christensen: look I reinvented
logic, here is DC Proof". He also beats Archimedes Plutonium,
in that he has more Alzheimer than Archimedes Plutonium. You
can talk to Dan Christensen and he doesn't understand acronyms:
FOL = first order logic
FOL+SET = first order logic plus his Subset axiom schema
And he doesn't know facts like:
Drinker Paradox is a FOL Paradox
Drinker Paradox is not a FOL+SET Paradox
Russell Paradox is not a FOL Paradox
Russell Paradox is a FOL+SET Paradox
Please wonky many, show as the Drinker Paradox in FOL
only? What is FOL only? It is not FOL+SET!
he is on par with "John Gabriel: look I reinvented calculus, here is
new calculus", in that he has "Dan Christensen: look I reinvented
logic, here is DC Proof". He also beats Archimedes Plutonium,
in that he has more Alzheimer than Archimedes Plutonium. You
can talk to Dan Christensen and he doesn't understand acronyms:
FOL = first order logic
FOL+SET = first order logic plus his Subset axiom schema
And he doesn't know facts like:
Drinker Paradox is a FOL Paradox
Drinker Paradox is not a FOL+SET Paradox
Russell Paradox is not a FOL Paradox
Russell Paradox is a FOL+SET Paradox
Please wonky many, show as the Drinker Paradox in FOL
only? What is FOL only? It is not FOL+SET!
Mostowski Collapse
Oct 9, 2022, 5:53:35 AM10/9/22
to
Why is the Russell Paradox viewed as an application of the
Diagonal Argument? He he, Alzheimer wonky man, so you don't
remember? Your brains totally blank, eaten by Corona Virus?
Because one can prove the Russell Paradox from a particular
instance of the Subset axiom schema:
∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a¬Eas) is valid.
https://www.umsu.de/trees/#~6k~7u%28Su~1~6a%28Eau~4%28Eak~1~3Eaa%29%29%29~5~6s%28Ss~5~7a~3Eas%29
And this instance with ~Eaa corresponds to the construction
of an Anti-diagonal, as used in the Diagonal Argument. The
Regularity Axiom doesn't come into play, it is even not built-in
in DC Proof. See also here, similar Diagonal Argument used in Cantors Proof:
https://en.wikipedia.org/wiki/Cantor's_diagonal_argument#Uncountable_set
The Drinker Paradox doesn't need this argument. It
even doesn't need SET, and is also not supposed to use SET.
You can much more easily prove the Drinker Paradox
in FOL, by proof by cases:
"The proof begins by recognising it is true that either
everyone in the pub is drinking (in this particular round of drinks),
or at least one person in the pub isn't drinking."
https://paradox.fandom.com/wiki/Drinker_paradox
Diagonal Argument? He he, Alzheimer wonky man, so you don't
remember? Your brains totally blank, eaten by Corona Virus?
Because one can prove the Russell Paradox from a particular
instance of the Subset axiom schema:
∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a¬Eas) is valid.
https://www.umsu.de/trees/#~6k~7u%28Su~1~6a%28Eau~4%28Eak~1~3Eaa%29%29%29~5~6s%28Ss~5~7a~3Eas%29
And this instance with ~Eaa corresponds to the construction
of an Anti-diagonal, as used in the Diagonal Argument. The
Regularity Axiom doesn't come into play, it is even not built-in
in DC Proof. See also here, similar Diagonal Argument used in Cantors Proof:
https://en.wikipedia.org/wiki/Cantor's_diagonal_argument#Uncountable_set
The Drinker Paradox doesn't need this argument. It
even doesn't need SET, and is also not supposed to use SET.
You can much more easily prove the Drinker Paradox
in FOL, by proof by cases:
"The proof begins by recognising it is true that either
everyone in the pub is drinking (in this particular round of drinks),
or at least one person in the pub isn't drinking."
https://paradox.fandom.com/wiki/Drinker_paradox
Dan Christensen
Oct 9, 2022, 1:19:29 PM10/9/22
to
See my reply earlier today to your identical posting at sci.math
Dan
On Sunday, October 9, 2022 at 5:28:45 AM UTC-4, Mostowski Collapse wrote:
> Dan Christensen is the uber-crank. He not only beats John Gabriel,
> he is on par with "John Gabriel: look I reinvented calculus, here is
> new calculus", in that he has "Dan Christensen: look I reinvented
>
>[snip]
Dan
On Sunday, October 9, 2022 at 5:28:45 AM UTC-4, Mostowski Collapse wrote:
> Dan Christensen is the uber-crank. He not only beats John Gabriel,
> he is on par with "John Gabriel: look I reinvented calculus, here is
> new calculus", in that he has "Dan Christensen: look I reinvented
>
Mostowski Collapse
Oct 9, 2022, 4:31:54 PM10/9/22
to
I nowhere claimed that you cannot prove your nonsense.
But this still doesn't make it correct.
The formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is even
not the Drinker Paradox. It would be the drinker
paradox if x in s were D(x) and Q were ALL(y):D(y).
But this still doesn't make it correct.
The formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is even
not the Drinker Paradox. It would be the drinker
paradox if x in s were D(x) and Q were ALL(y):D(y).
Mostowski Collapse
Oct 9, 2022, 4:55:45 PM10/9/22
to
Why don't you ask here:
Mathematics Stack Exchange
https://math.stackexchange.com/
MathOverflow
https://mathoverflow.net/
Whether there is anybody on this planet that believes
that your formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]
is the Drinker Paradox. Could be fun!
Mathematics Stack Exchange
https://math.stackexchange.com/
MathOverflow
https://mathoverflow.net/
Whether there is anybody on this planet that believes
that your formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]
is the Drinker Paradox. Could be fun!
Dan Christensen
Oct 10, 2022, 12:21:49 AM10/10/22
to
On Sunday, October 9, 2022 at 4:31:54 PM UTC-4, Mostowski Collapse wrote:
[snip]
> The formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is even
> not the Drinker Paradox. It would be the drinker
> paradox if x in s were D(x) and Q were ALL(y):D(y).
[snip]
It can be formalized using either predicates or sets or a combination of both. At Wikipedia, these use a combination of both. Deal with it, Jan Burse.
[snip]
> The formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is even
> not the Drinker Paradox. It would be the drinker
> paradox if x in s were D(x) and Q were ALL(y):D(y).
It can be formalized using either predicates or sets or a combination of both. At Wikipedia, these use a combination of both. Deal with it, Jan Burse.
Message has been deleted
Dan Christensen
Oct 10, 2022, 1:20:32 AM10/10/22
to
On Sunday, October 9, 2022 at 4:55:45 PM UTC-4, Mostowski Collapse wrote:
> Why don't you ask here:
>
> Mathematics Stack Exchange
> https://math.stackexchange.com/
>
> MathOverflow
> https://mathoverflow.net/
>
> Whether there is anybody on this planet that believes
> that your formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]
>
> is the Drinker Paradox.
Do pay attention, Jan Burse! Once again, DP is special case of this theorem with s = the set of all drinkers, and Q = ALL(y):[y in P => y in s].
> Why don't you ask here:
>
> Mathematics Stack Exchange
> https://math.stackexchange.com/
>
> MathOverflow
> https://mathoverflow.net/
>
> Whether there is anybody on this planet that believes
> that your formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]
>
> is the Drinker Paradox.
Mostowski Collapse
Oct 10, 2022, 5:42:30 AM10/10/22
to
Do pay attention, Dan Christensen! DP is not
a special case of this theorem. DP is foremost a
kindergarden thought experiment concerning
the universal predicate. "The everybody is drinking"
in the pub is a metaphore for the universal predicate.
ALL(x):U(x)
But there is no universal set in set theory. So
DP is not a special of something in set theory.
You failed at a simple kindergarden thought
experiment posed by Raymond Smullyan.
Raymond Smullyan got you tricked!
LMAO!
a special case of this theorem. DP is foremost a
kindergarden thought experiment concerning
the universal predicate. "The everybody is drinking"
in the pub is a metaphore for the universal predicate.
ALL(x):U(x)
But there is no universal set in set theory. So
DP is not a special of something in set theory.
You failed at a simple kindergarden thought
experiment posed by Raymond Smullyan.
Raymond Smullyan got you tricked!
LMAO!
Mostowski Collapse
Oct 10, 2022, 5:45:24 AM10/10/22
to
Why don't you ask here:
Mathematics Stack Exchange
https://math.stackexchange.com/
MathOverflow
https://mathoverflow.net/
Whether there is anybody on this planet that believes
that your formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]
Mathematics Stack Exchange
https://math.stackexchange.com/
MathOverflow
https://mathoverflow.net/
Whether there is anybody on this planet that believes
that your formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]
is the Drinker Paradox. Could be fun!
Dan Christensen
Oct 10, 2022, 11:25:25 AM10/10/22
to
On Monday, October 10, 2022 at 5:42:30 AM UTC-4, Mostowski Collapse wrote:
[snip]
> > Do pay attention, Jan Burse! Once again, DP is special case of this theorem with s = the set of all drinkers, and Q = ALL(y):[y in P => y in s].
> DP is foremost a
> kindergarden thought experiment concerning
>
> the universal predicate. "The everybody is drinking"
> in the pub is a metaphore for the universal predicate.
>
> ALL(x):U(x)
>
> But there is no universal set in set theory.
Or equivalently, every set excludes something as I proved here.
First-order predicate logic is apparently insufficient for some problems, even for something as mundane as the Barber Paradox. See my blog posting at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/
[snip]
> > Do pay attention, Jan Burse! Once again, DP is special case of this theorem with s = the set of all drinkers, and Q = ALL(y):[y in P => y in s].
> Do pay attention, Dan Christensen! DP is not
> a special case of this theorem.
Wrong again, Jan Burse.
> a special case of this theorem.
> DP is foremost a
> kindergarden thought experiment concerning
>
> the universal predicate. "The everybody is drinking"
> in the pub is a metaphore for the universal predicate.
>
> ALL(x):U(x)
>
> But there is no universal set in set theory.
First-order predicate logic is apparently insufficient for some problems, even for something as mundane as the Barber Paradox. See my blog posting at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/
> DP is not a special of something in set theory.
> You failed at a simple kindergarden thought
>
> experiment posed by Raymond Smullyan.
> Raymond Smullyan got you tricked!
>
You got blinded by your stubbornness and bruised ego, Jan Burse. Deal with it.
> You failed at a simple kindergarden thought
>
> experiment posed by Raymond Smullyan.
> Raymond Smullyan got you tricked!
>
Mostowski Collapse
Oct 10, 2022, 2:55:26 PM10/10/22
to
Looks like you even don't understand the Barber Paradox.
You don't need sets. Its pretty easy in FOL:
¬∃x(Px ∧ ∀y(Py → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x%28Px~1~6y%28Py~5%28Sxy~4~3Syy%29%29%29
You don't need sets. Its pretty easy in FOL:
¬∃x(Px ∧ ∀y(Py → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x%28Px~1~6y%28Py~5%28Sxy~4~3Syy%29%29%29
Mostowski Collapse
Oct 10, 2022, 2:55:54 PM10/10/22
to
Thats just Russell Paradox with set builder, the Barber Paradox,
what you showed on your blog is an outside element. But you
get the outside element also without set theory. I posted this
already a few days ago, but you snipped it:
Mostowski Collapse schrieb am Sonntag, 9. Oktober 2022 um 13:13:52 UTC+2:
> ∃u∀a(Eau ↔ ¬Eaa) → ∀s∃a¬Eas is valid.
> https://www.umsu.de/trees/#~7u~6a%28Eau~4~3Eaa%29~5~6s~7a~3Eas
>
> But more shockingly for Frege, you can derive:
> ∀a(Eau ↔ ¬Eaa) → (Euu ∧ ¬Euu) is valid.
> https://www.umsu.de/trees/#~6a%28Eau~4~3Eaa%29~5Euu~1~3Euu
https://groups.google.com/g/sci.math/c/-OsA3VNX6yI/m/Pdv66TmmBQAJ
So its the same fallacy on your side wonky man. Only because
you obtained a FOL+SET proof, doesn't mean there is no FOL proof.
Whats wrong with you Dan Christensen?
Slow in the mind wonky man, He He?
what you showed on your blog is an outside element. But you
get the outside element also without set theory. I posted this
already a few days ago, but you snipped it:
Mostowski Collapse schrieb am Sonntag, 9. Oktober 2022 um 13:13:52 UTC+2:
> ∃u∀a(Eau ↔ ¬Eaa) → ∀s∃a¬Eas is valid.
> https://www.umsu.de/trees/#~7u~6a%28Eau~4~3Eaa%29~5~6s~7a~3Eas
>
> But more shockingly for Frege, you can derive:
> ∀a(Eau ↔ ¬Eaa) → (Euu ∧ ¬Euu) is valid.
> https://www.umsu.de/trees/#~6a%28Eau~4~3Eaa%29~5Euu~1~3Euu
https://groups.google.com/g/sci.math/c/-OsA3VNX6yI/m/Pdv66TmmBQAJ
So its the same fallacy on your side wonky man. Only because
you obtained a FOL+SET proof, doesn't mean there is no FOL proof.
Whats wrong with you Dan Christensen?
Slow in the mind wonky man, He He?
Mostowski Collapse
Oct 10, 2022, 2:56:25 PM10/10/22
to
Lets bring it into the form how you proved it on your
block with FOL+SET, but with FOL only:
∀a(Ma → (Sba ↔ ¬Saa)) → ¬Mb is valid.
https://www.umsu.de/trees/#~6a%28Ma~5%28Sba~4~3Saa%29%29~5~3Mb
M = the men in the village
S = the shaving relation
LMAO!
block with FOL+SET, but with FOL only:
∀a(Ma → (Sba ↔ ¬Saa)) → ¬Mb is valid.
https://www.umsu.de/trees/#~6a%28Ma~5%28Sba~4~3Saa%29%29~5~3Mb
M = the men in the village
S = the shaving relation
LMAO!
Mostowski Collapse
Oct 10, 2022, 3:07:33 PM10/10/22
to
The other direction works also wit FOL, no FOL+SET
needed, you have EXIST(s) in your blog, but we can make
it more constructively, just define some S, which works,
here is a proof:
¬Mb → (∀a(Ma → (¬Sba ∧ Saa)) → ∀a(Ma → (Sba ↔ ¬Saa))) is valid.
https://www.umsu.de/trees/#~3Mb~5~6a%28Ma~5~3Sba~1Saa%29~5~6a%28Ma~5%28Sba~4~3Saa%29%29
Have Fun!
needed, you have EXIST(s) in your blog, but we can make
it more constructively, just define some S, which works,
here is a proof:
¬Mb → (∀a(Ma → (¬Sba ∧ Saa)) → ∀a(Ma → (Sba ↔ ¬Saa))) is valid.
https://www.umsu.de/trees/#~3Mb~5~6a%28Ma~5~3Sba~1Saa%29~5~6a%28Ma~5%28Sba~4~3Saa%29%29
Have Fun!
Dan Christensen
Oct 10, 2022, 3:17:50 PM10/10/22
to
On Monday, October 10, 2022 at 2:55:26 PM UTC-4, Mostowski Collapse wrote:
> Looks like you even don't understand the Barber Paradox.
> You don't need sets.
To truly resolve BP, you must prove: 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.
> Looks like you even don't understand the Barber Paradox.
> You don't need sets.
Try to prove this with only first-order predicate logic. Good luck.
Mostowski Collapse
Oct 10, 2022, 3:34:40 PM10/10/22
to
I proved it already. You are late with responding.
But anyway thanks for the luck, but I didn't need it.
Fritz Feldhase
Oct 10, 2022, 3:47:13 PM10/10/22
to
On Monday, October 10, 2022 at 9:17:50 PM UTC+2, Dan Christensen wrote:
> To truly resolve BP <bla bla>
Time to quit wonky man.
Good bye!
> To truly resolve BP <bla bla>
Time to quit wonky man.
Good bye!
Mostowski Collapse
Oct 10, 2022, 8:53:26 PM10/10/22
to
Its not truly resolved by Dan Christensens blog post.
He proves EXIST(s) without any relation to what
the villagers can do. So what he proved is not very
natural, since it is disconnected from what the villagers
can do. I have to check his proof which s he even constructs.
At step 25 he has constructed V x V:
25 ALL(c1):ALL(c2):[(c1,c2) e v2 <=> c1 e v & c2 e v]
Split, 23
http://www.dcproof.com/BP12.htm
The he uses the subset axiom, and at step 29 he has
constructed s as follows:
29 ALL(a):ALL(b):[(a,b) e s <=> (a,b) e v2 & [a=barber & b e m]]
Split, 27
This means s is this set:
S = {barber} x M
One can verify that it satisfies another formula than
I gave, namely this formula:
∀a(Ma → (Sba ∧ ~Saa)
Dan Christensen proves the ~Saa part here:
47 ALL(a):[a e m => ~(a,a) e s]
4 Conclusion, 30
So basically he says something else than what I projected,
namely he says this here in his proof:
¬Mb → (∀a(Ma → (Sba ∧ ¬Saa)) → ∀a(Ma → (Sba ↔ ¬Saa))) is valid.
https://www.umsu.de/trees/#~3Mb~5~6a%28Ma~5Sba~1~3Saa%29~5~6a%28Ma~5%28Sba~4~3Saa%29%29
But now we have already two options S1, from my
∀a(Ma → (¬Sba ∧ Saa)) and S2 from his blog, which
is ∀a(Ma → (Sba ∧ ¬Saa)).
But what if the villagers have some people who can
shave themselves and some people who cannot shave
themselves. The construction S1 and S2 is purely
hypothetical, not related to the village. A theorem that
would show the existence of a shaving plan for the barber
from the capabilities of the villager would look totally different.
Such a proof could be considered a solution. But what
Dan Christensen proved in is blog is just unnaturally disconnected
from the villagers, and doesn't make much sense.
He proves EXIST(s) without any relation to what
the villagers can do. So what he proved is not very
natural, since it is disconnected from what the villagers
can do. I have to check his proof which s he even constructs.
At step 25 he has constructed V x V:
25 ALL(c1):ALL(c2):[(c1,c2) e v2 <=> c1 e v & c2 e v]
Split, 23
http://www.dcproof.com/BP12.htm
The he uses the subset axiom, and at step 29 he has
constructed s as follows:
29 ALL(a):ALL(b):[(a,b) e s <=> (a,b) e v2 & [a=barber & b e m]]
Split, 27
This means s is this set:
S = {barber} x M
One can verify that it satisfies another formula than
I gave, namely this formula:
∀a(Ma → (Sba ∧ ~Saa)
Dan Christensen proves the ~Saa part here:
47 ALL(a):[a e m => ~(a,a) e s]
4 Conclusion, 30
So basically he says something else than what I projected,
namely he says this here in his proof:
¬Mb → (∀a(Ma → (Sba ∧ ¬Saa)) → ∀a(Ma → (Sba ↔ ¬Saa))) is valid.
https://www.umsu.de/trees/#~3Mb~5~6a%28Ma~5Sba~1~3Saa%29~5~6a%28Ma~5%28Sba~4~3Saa%29%29
But now we have already two options S1, from my
∀a(Ma → (¬Sba ∧ Saa)) and S2 from his blog, which
is ∀a(Ma → (Sba ∧ ¬Saa)).
But what if the villagers have some people who can
shave themselves and some people who cannot shave
themselves. The construction S1 and S2 is purely
hypothetical, not related to the village. A theorem that
would show the existence of a shaving plan for the barber
from the capabilities of the villager would look totally different.
Such a proof could be considered a solution. But what
Dan Christensen proved in is blog is just unnaturally disconnected
from the villagers, and doesn't make much sense.
Dan Christensen
Oct 10, 2022, 9:15:42 PM10/10/22
to
On Monday, October 10, 2022 at 3:34:40 PM UTC-4, Mostowski Collapse wrote:
> > On Monday, October 10, 2022 at 2:55:26 PM UTC-4, Mostowski Collapse wrote:
> > > Looks like you even don't understand the Barber Paradox.
> > > You don't need sets.
> > To truly resolve BP, you must prove: 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.
> >
> > Try to prove this with only first-order predicate logic. Good luck.
> I proved it already.
> > On Monday, October 10, 2022 at 2:55:26 PM UTC-4, Mostowski Collapse wrote:
> > > Looks like you even don't understand the Barber Paradox.
> > > You don't need sets.
> > To truly resolve BP, you must prove: 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.
> >
> > Try to prove this with only first-order predicate logic. Good luck.
No, you didn't. Oh, well...
Dan
Mostowski Collapse
Oct 10, 2022, 9:27:57 PM10/10/22
to
Well its the same thing like yours, only with SET
and stripped from V. In FOL there is no need for V.
=> direction
also don't have an EXIST theorem for N from nothing. Nobody cares.
You can say S exists as much as your N, the set of natural numbers, exists.
In the same way as nobody knows formally so far in DC Proof, whether
for example this axiom here has a model:
4 ALL(a):[a ε n => ~a+1=1]
Axiom
5 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
Axiom
LoL
and stripped from V. In FOL there is no need for V.
=> direction
∀a(Ma → (Sba ↔ ¬Saa)) → ¬Mb is valid.
https://www.umsu.de/trees/#~6a%28Ma~5%28Sba~4~3Saa%29%29~5~3Mb
<= direction
https://www.umsu.de/trees/#~6a%28Ma~5%28Sba~4~3Saa%29%29~5~3Mb
¬Mb → (∀a(Ma → (Sba ∧ ¬Saa)) → ∀a(Ma → (Sba ↔ ¬Saa))) is valid.
https://www.umsu.de/trees/#~3Mb~5~6a%28Ma~5Sba~1~3Saa%29~5~6a%28Ma~5%28Sba~4~3Saa%29%29
It doesn't have an EXIST quantifier though. Well your Peano Axioms
https://www.umsu.de/trees/#~3Mb~5~6a%28Ma~5Sba~1~3Saa%29~5~6a%28Ma~5%28Sba~4~3Saa%29%29
also don't have an EXIST theorem for N from nothing. Nobody cares.
You can say S exists as much as your N, the set of natural numbers, exists.
In the same way as nobody knows formally so far in DC Proof, whether
for example this axiom here has a model:
4 ALL(a):[a ε n => ~a+1=1]
Axiom
5 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
Axiom
LoL
Mostowski Collapse
Oct 10, 2022, 9:50:37 PM10/10/22
to
A more natural proof, relating to what the villagers can do
in terms of Saa, would prove existence of T, such that we have:
¬Mb → ∀a(Ma → (Tba ↔ ¬Saa))))
can you prove that with DC Spoiled? Instead of fixing s to
∀a(Ma → (Sba ∧ ¬Saa)), which doesn't make any sense?
But this was never the intention of the Barber Paradox,
to go this far. The <= direction is not in the scope of
The Barber Paradox. The Barbar Paradox is done if you
can prove the following:
¬∃x(Mx ∧ ∀y(My → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x(Mx~1~6y(My~5(Sxy~4~3Syy)))
https://en.wikipedia.org/wiki/Barber_paradox#In_first-order_logic
Turning this into (your => direction):
∀x(∀y(My → (Sxy ↔ ¬Syy)) → ¬Mx) is valid.
https://www.umsu.de/trees/#~6x(~6y(My~5(Sxy~4~3Syy))~5~3Mx)
Is application of some simple transformation rules.
Transformation rule 1: ¬∃x = ∀x¬
∀x¬(Mx ∧ ∀y(My → (Sxy ↔ ¬Syy))) is valid.
Transformation rule 2: ¬(A∧B) = (A→¬B)
∀x(Mx → ¬∀y(My → (Sxy ↔ ¬Syy))) is valid.
Transformation rule 3: (A→¬B) = (B→¬A)
∀x(∀y(My → (Sxy ↔ ¬Syy)) → ¬Mx) is valid.
On the other hand your <= direction, is just bla bla, doesn't
solve the paradox in any way. Since the => direction is still
the original paradox. You didn't change the => direction,
you only pulled a <= direction out of your ass, and made
it a case in favor of SET theory. You could use a more
convincingly example to plead for SET theory, without
the crazy claim you solved the Barber Pradox. Nobody
cares about the <= direction? Nobody cares if the Barber is
not a man from the village? Its not anymore the Barber
Paradox if the Barber is not a man from the villag!
You can solve any Pradox if you introduce Pink Unicorns.
in terms of Saa, would prove existence of T, such that we have:
¬Mb → ∀a(Ma → (Tba ↔ ¬Saa))))
can you prove that with DC Spoiled? Instead of fixing s to
∀a(Ma → (Sba ∧ ¬Saa)), which doesn't make any sense?
But this was never the intention of the Barber Paradox,
to go this far. The <= direction is not in the scope of
The Barber Paradox. The Barbar Paradox is done if you
can prove the following:
¬∃x(Mx ∧ ∀y(My → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x(Mx~1~6y(My~5(Sxy~4~3Syy)))
https://en.wikipedia.org/wiki/Barber_paradox#In_first-order_logic
Turning this into (your => direction):
∀x(∀y(My → (Sxy ↔ ¬Syy)) → ¬Mx) is valid.
https://www.umsu.de/trees/#~6x(~6y(My~5(Sxy~4~3Syy))~5~3Mx)
Is application of some simple transformation rules.
Transformation rule 1: ¬∃x = ∀x¬
∀x¬(Mx ∧ ∀y(My → (Sxy ↔ ¬Syy))) is valid.
Transformation rule 2: ¬(A∧B) = (A→¬B)
∀x(Mx → ¬∀y(My → (Sxy ↔ ¬Syy))) is valid.
Transformation rule 3: (A→¬B) = (B→¬A)
∀x(∀y(My → (Sxy ↔ ¬Syy)) → ¬Mx) is valid.
On the other hand your <= direction, is just bla bla, doesn't
solve the paradox in any way. Since the => direction is still
the original paradox. You didn't change the => direction,
you only pulled a <= direction out of your ass, and made
it a case in favor of SET theory. You could use a more
convincingly example to plead for SET theory, without
the crazy claim you solved the Barber Pradox. Nobody
cares about the <= direction? Nobody cares if the Barber is
not a man from the village? Its not anymore the Barber
Paradox if the Barber is not a man from the villag!
You can solve any Pradox if you introduce Pink Unicorns.
Dan Christensen
Oct 10, 2022, 10:54:04 PM10/10/22
to
On Monday, October 10, 2022 at 8:53:26 PM UTC-4, Mostowski Collapse wrote:
> Fritz Feldhase schrieb am Montag, 10. Oktober 2022 um 21:47:13 UTC+2:
> > On Monday, October 10, 2022 at 9:17:50 PM UTC+2, Dan Christensen wrote:
> >
> Fritz Feldhase schrieb am Montag, 10. Oktober 2022 um 21:47:13 UTC+2:
> > On Monday, October 10, 2022 at 9:17:50 PM UTC+2, Dan Christensen wrote:
> >
> > > To truly resolve BP, you must prove: 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. Try to prove this with only first-order predicate logic. Good luck.
> Its not truly resolved by Dan Christensens blog post.
> He proves EXIST(s) without any relation to what
> the villagers can do.
[snip]
> He proves EXIST(s) without any relation to what
> the villagers can do.
You really don't get it, do you, Jan Burse? This is about what the BARBER can and cannot do. Once again we prove:
Theorem:
ALL(v):ALL(barber):ALL(m):[Set(v)
& barber in v
& Set(m)
& ALL(a):[a in m => a in v]
=> [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
& ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
<=> ~barber in m]]
where
v = the set of all villagers
m = the set of all men in the village
s = the shaving relation on v, a set of ordered pairs, (x,y) in s means x shaves y
Full text of proof: http://www.dcproof.com/BP12.htm
> So what he proved is not very
>
> natural, since it is disconnected from what the villagers
> can do.
Huh??? Pay attention, Jan Burse! In lines 6-14, we prove that if the barber is a man, then there can exist no shaving relation on the set of villagers such that for all men in the village, the barber shaves those and only those men who do not shave themselves:
14. barber in m
=> ~EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
& ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
Conclusion, 6
In lines 17-97, we prove that if the barber is NOT a man, then there does exist at least one shaving relation on the set of villagers such that for all men in the village, the barber shaves those and only those men who do not shave themselves (e.g. x shaves y iff x = the barber and y is a man in the village).
97. ~barber in m
=> EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
& ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
Conclusion, 17
From these conclusions and the initial assumptions on line 1, we have the above theorem as required:
100. ALL(v):ALL(barber):ALL(m):[Set(v)
& barber in v
& Set(m)
& ALL(a):[a in m => a in v]
=> [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
& ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
<=> ~barber in m]]
Conclusion, 1
Get it, Jan Burse??? Didn't think so. Oh, well...
Ross A. Finlayson
Oct 10, 2022, 11:43:29 PM10/10/22
to
Dan Christensen
Oct 11, 2022, 12:42:18 AM10/11/22
to
On Monday, October 10, 2022 at 9:50:37 PM UTC-4, Mostowski Collapse wrote:
> A more natural proof, relating to what the villagers can do
> in terms of Saa, would prove existence of T, such that we have:
>
> ¬Mb → ∀a(Ma → (Tba ↔ ¬Saa))))
>
> can you prove that with DC Spoiled? Instead of fixing s to
> ∀a(Ma → (Sba ∧ ¬Saa)), which doesn't make any sense?
> But this was never the intention of the Barber Paradox,
>
Nevertheless, using set theory, I have proven:
> A more natural proof, relating to what the villagers can do
> in terms of Saa, would prove existence of T, such that we have:
>
> ¬Mb → ∀a(Ma → (Tba ↔ ¬Saa))))
>
> can you prove that with DC Spoiled? Instead of fixing s to
> ∀a(Ma → (Sba ∧ ¬Saa)), which doesn't make any sense?
> But this was never the intention of the Barber Paradox,
>
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.
Jeff Barnett
Oct 11, 2022, 2:09:18 AM10/11/22
to
On 10/10/2022 10:42 PM, Dan Christensen wrote:
> On Monday, October 10, 2022 at 9:50:37 PM UTC-4, Mostowski Collapse wrote:
>> A more natural proof, relating to what the villagers can do
>> in terms of Saa, would prove existence of T, such that we have:
>>
>> ¬Mb → ∀a(Ma → (Tba ↔ ¬Saa))))
>>
>> can you prove that with DC Spoiled? Instead of fixing s to
>> ∀a(Ma → (Sba ∧ ¬Saa)), which doesn't make any sense?
>> But this was never the intention of the Barber Paradox,
>>
>
> Nevertheless, using set theory, I have proven:
>
> 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.
I see that you are now doing modal logic. If you said, instead, "that
> On Monday, October 10, 2022 at 9:50:37 PM UTC-4, Mostowski Collapse wrote:
>> A more natural proof, relating to what the villagers can do
>> in terms of Saa, would prove existence of T, such that we have:
>>
>> ¬Mb → ∀a(Ma → (Tba ↔ ¬Saa))))
>>
>> can you prove that with DC Spoiled? Instead of fixing s to
>> ∀a(Ma → (Sba ∧ ¬Saa)), which doesn't make any sense?
>> But this was never the intention of the Barber Paradox,
>>
>
> Nevertheless, using set theory, I have proven:
>
> 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.
the barber shaves those ... implies the barber is not a man" it's easy
to see what you had in mind and prove it. (Perhaps I'm giving what you
had in mind credit improperly.) With the "can" in there it says that
the barber not a man implies that the barber COULD do the shaving.
That's true but not expressible in a FOL that doesn't have builtin modal
operators as far as I know.
> If you have given up trying to prove both directions of the biconditional, just say so. There is only so much you can do using only first-order predicated logic. Why do you think set theory was invented?
Jeff Barnett
Mostowski Collapse
Oct 11, 2022, 3:24:13 AM10/11/22
to
Implying that there is really a barber who is not a man
of the village, would be fallacious. You don't need
modal logic for that, just find a classical counter model:
¬∃x(Lx ∧ Mx) → ∃x¬Mx is invalid.
https://www.umsu.de/trees/#~3~7x%28L%28x%29~1M%28x%29%29~5~7x~3M%28x%29
Dan Christensen doesn't explicitly imply it, but since he
uses a theorem of the form, he somehow implicitly
implies it, since he uses this phrasing:
(Lx ↔ ¬Mx)
can if and only if that barber is not a man.
http://www.dcproof.com/BP12.htm
But using ¬Mx, in his proof ~barber e m, suggest somehow
that he has this assumption. But every bi-implication can be
flipped, so instead using the form (A ↔ ¬B), he could also
use the form (¬A ↔ B), they are both logically equivalent, which
shows that he didn't solve the Barber Pradox, there is still
no barber as a man in the viallage, which can obey the law Lx,
every barber as a man in the village would break the law:
(¬Lx ↔ Mx)
cannot if and only if that barber is a man.
http://www.dcproof.com/BP12.htm
Dan Christensen
Oct 11, 2022, 10:15:42 AM10/11/22
to
On Tuesday, October 11, 2022 at 2:09:18 AM UTC-4, Jeff Barnett wrote:
> On 10/10/2022 10:42 PM, Dan Christensen wrote:
> > On Monday, October 10, 2022 at 9:50:37 PM UTC-4, Mostowski Collapse wrote:
> >> A more natural proof, relating to what the villagers can do
> >> in terms of Saa, would prove existence of T, such that we have:
> >>
> >> ¬Mb → ∀a(Ma → (Tba ↔ ¬Saa))))
> >>
> >> can you prove that with DC Spoiled? Instead of fixing s to
> >> ∀a(Ma → (Sba ∧ ¬Saa)), which doesn't make any sense?
> >> But this was never the intention of the Barber Paradox,
> >>
> >
> > Nevertheless, using set theory, I have proven:
> >
> > 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.
> I see that you are now doing modal logic.
Nope. Just good old-fashioned true-or-false logic as always.
> On 10/10/2022 10:42 PM, Dan Christensen wrote:
> > On Monday, October 10, 2022 at 9:50:37 PM UTC-4, Mostowski Collapse wrote:
> >> A more natural proof, relating to what the villagers can do
> >> in terms of Saa, would prove existence of T, such that we have:
> >>
> >> ¬Mb → ∀a(Ma → (Tba ↔ ¬Saa))))
> >>
> >> can you prove that with DC Spoiled? Instead of fixing s to
> >> ∀a(Ma → (Sba ∧ ¬Saa)), which doesn't make any sense?
> >> But this was never the intention of the Barber Paradox,
> >>
> >
> > Nevertheless, using set theory, I have proven:
> >
> > 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.
> I see that you are now doing modal logic.
> If you said, instead, "that
> the barber shaves those ... implies the barber is not a man" it's easy
> to see what you had in mind and prove it. (Perhaps I'm giving what you
> had in mind credit improperly.) With the "can" in there it says that
> the barber not a man implies that the barber COULD do the shaving.
ALL(v):ALL(barber):ALL(m):[Set(v)
& barber in v
& Set(m)
& ALL(a):[a in m => a in v]
=> [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
& ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
<=> ~barber in m]]
where
v = the set of all villagers
m = the set of all men in the village
See: http://www.dcproof.com/BP12.htm
I hope this helps.
Mostowski Collapse
Oct 11, 2022, 2:38:57 PM10/11/22
to
Not a smart move, trying to prove a loaded question.
You lost your mind already years ago wonky man.
Dan Christensen
Oct 11, 2022, 3:00:53 PM10/11/22
to
> Not a smart move, trying to prove a loaded question.
What question would that be, Jan Burse? I posted no question. You really seem to be losing it here.
Dan
Mostowski Collapse
Oct 11, 2022, 5:47:13 PM10/11/22
to
Be careful with the drugs, did you smoke meth
when writing the blog post? Since when can
the verb "shave" apply to woman and men?
ALL(a):ALL(b):[(a,b) e s => a e v & b e v]
http://www.dcproof.com/BP12.htm
Dan Christensen
Oct 11, 2022, 6:01:02 PM10/11/22
to
> Since when can
> the verb "shave" apply to woman and men?
>
Think before you write, Jan Burse.
Mostowski Collapse
Oct 12, 2022, 11:50:33 AM10/12/22
to
Is this some sort of new Pink Unicorn LGBT solution from an
USA university course on gender studies to the barber paradox.
Recall what a barber is:
Mostowski Collapse schrieb am Dienstag, 11. Oktober 2022 um 23:25:29 UTC+2:
> A barber is a person whose occupation is mainly
> to cut, dress, groom, style and shave **men's** and
> **boys'** hair or beards.
https://groups.google.com/g/sci.math/c/hEQjzBmQIIw/m/zgLGPMNkBgAJ
Anyway, you are completely nuts wonky man. You
got carried away by a loaded question. And you tried
some construal of a complete answer where a "EXIST(b)"
by using a constant barber. But the solution to the barber
paradox is quite simple, there is no barber, which you
cannot express when using a constant, the complete
solution is trivially "~EXIST(b)", you can prove it quite trivially:
/* With non-empty domain assumption, FOL proof */
¬∃x∀y(Sxy ↔ ¬Syy) is valid.
https://www.umsu.de/trees/#~3~7x~6y(Sxy~4~3Syy)
What does "¬∃x" say? It says there is no barber. It is even
immune to empty domains, works also for empty domains,
you can try yourself:
/* Without non-empty domain assumption, FOL proof */
¬∃x(Dx ∧ ∀y(Dx → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x(Dx~1~6y(Dx~5(Sxy~4~3Syy)))
This is unlike the Drinker Paradox, and hence shows a
difference to the Drinker Paradox, because the Drinker Paradox
requires a non-empty domain, the Barber Paradox and the
Russell Paradox do not require a non-empty domain.
USA university course on gender studies to the barber paradox.
Recall what a barber is:
Mostowski Collapse schrieb am Dienstag, 11. Oktober 2022 um 23:25:29 UTC+2:
> A barber is a person whose occupation is mainly
> to cut, dress, groom, style and shave **men's** and
> **boys'** hair or beards.
https://groups.google.com/g/sci.math/c/hEQjzBmQIIw/m/zgLGPMNkBgAJ
Anyway, you are completely nuts wonky man. You
got carried away by a loaded question. And you tried
some construal of a complete answer where a "EXIST(b)"
by using a constant barber. But the solution to the barber
paradox is quite simple, there is no barber, which you
cannot express when using a constant, the complete
solution is trivially "~EXIST(b)", you can prove it quite trivially:
/* With non-empty domain assumption, FOL proof */
¬∃x∀y(Sxy ↔ ¬Syy) is valid.
https://www.umsu.de/trees/#~3~7x~6y(Sxy~4~3Syy)
What does "¬∃x" say? It says there is no barber. It is even
immune to empty domains, works also for empty domains,
you can try yourself:
/* Without non-empty domain assumption, FOL proof */
¬∃x(Dx ∧ ∀y(Dx → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x(Dx~1~6y(Dx~5(Sxy~4~3Syy)))
This is unlike the Drinker Paradox, and hence shows a
difference to the Drinker Paradox, because the Drinker Paradox
requires a non-empty domain, the Barber Paradox and the
Russell Paradox do not require a non-empty domain.
Mostowski Collapse
Oct 12, 2022, 11:58:47 AM10/12/22
to
You can also try Edsger W. Dijkstra:
"Where is Russell's paradox? - EWD 923A, Austin, 22 May, 1985"
Conclusion: the village has no barber. Where is the paradox?"
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD09xx/EWD923a.html
Thats the COMPLETE SOLUTION you moron.
No need to invent Pink Unicorns wonky man,
only because the loaded question has EXIST(b).
The complete solution is ~EXIST(b). Whats wrong
with you? A little mellow in the brain, already years ago?
When did you write this nonsense, so that we can diagnose
how long you suffer from a severe case of Alzheimer
and USA wokeness and read some cringe prejudice and
discrimination into the Barber Paradox?
"if that barber is not a man"
http://www.dcproof.com/BP12.htm
LMAO!
"Where is Russell's paradox? - EWD 923A, Austin, 22 May, 1985"
Conclusion: the village has no barber. Where is the paradox?"
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD09xx/EWD923a.html
Thats the COMPLETE SOLUTION you moron.
No need to invent Pink Unicorns wonky man,
only because the loaded question has EXIST(b).
The complete solution is ~EXIST(b). Whats wrong
with you? A little mellow in the brain, already years ago?
When did you write this nonsense, so that we can diagnose
how long you suffer from a severe case of Alzheimer
and USA wokeness and read some cringe prejudice and
discrimination into the Barber Paradox?
"if that barber is not a man"
LMAO!
Mostowski Collapse
Oct 12, 2022, 12:12:51 PM10/12/22
to
Dan Christensen hallucinates:
> A shaving "solution" to BP would not exist if only a man could be the barber.
Well it exists, if there is no barber. For example if there are
3 villagers A, B and C, which do not have the profession of a
barber, and they are not subject to the law Sxy ↔ ¬Syy,
Then S = {(A,A), (A,B)} would be a solution. So villager
A would shave himself and villager B. Villager C would
not be shaved at all, he grows a beard indefinitely,
it would be automatically a village where such C
villagers are allowed. Kind of an Anarchistic Village,
with no Barber, you might like that wonky man.
> A shaving "solution" to BP would not exist if only a man could be the barber.
Well it exists, if there is no barber. For example if there are
3 villagers A, B and C, which do not have the profession of a
barber, and they are not subject to the law Sxy ↔ ¬Syy,
Then S = {(A,A), (A,B)} would be a solution. So villager
A would shave himself and villager B. Villager C would
not be shaved at all, he grows a beard indefinitely,
it would be automatically a village where such C
villagers are allowed. Kind of an Anarchistic Village,
with no Barber, you might like that wonky man.
Dan Christensen
Oct 12, 2022, 1:08:55 PM10/12/22
to
On Wednesday, October 12, 2022 at 12:12:51 PM UTC-4, Mostowski Collapse wrote:
> Dan Christensen hallucinates:
> > A shaving "solution" to BP would not exist if only a man could be the barber.
>
> Well it exists, if there is no barber.
[snip]
> Dan Christensen hallucinates:
> > A shaving "solution" to BP would not exist if only a man could be the barber.
>
> Well it exists, if there is no barber.
See my reply just now to your identical posting at sci.math.
Dan
Mostowski Collapse
Oct 12, 2022, 2:06:56 PM10/12/22
to
You invested so much into the barber paradox,
even did a power point, with a story where it is
pretended that the barber exists.
http://www.dcproof.com/BarberParadox.ppt
And you also make a teaching about sets
and stuff. I feel a little bit sorry, that is all
complete nonsense, its
based on the fallacy to believe the pretens.
After all the barber paradox is based on a
loaded questions:
"The question is a loaded question that assumes
the existence of the barber, which is false.
A loaded question is a form of complex question
that contains a controversial assumption"
https://en.wikipedia.org/wiki/Barber_paradox
https://en.wikipedia.org/wiki/Loaded_question
even did a power point, with a story where it is
pretended that the barber exists.
http://www.dcproof.com/BarberParadox.ppt
And you also make a teaching about sets
and stuff. I feel a little bit sorry, that is all
complete nonsense, its
based on the fallacy to believe the pretens.
After all the barber paradox is based on a
loaded questions:
"The question is a loaded question that assumes
the existence of the barber, which is false.
A loaded question is a form of complex question
that contains a controversial assumption"
https://en.wikipedia.org/wiki/Barber_paradox
https://en.wikipedia.org/wiki/Loaded_question
Mostowski Collapse
Oct 12, 2022, 2:14:13 PM10/12/22
to
Dan Christensen hallucinated:
> This would be vacuously true if there was
> no barber in the village, i.e. ~EXIST(barber):barber in v.
Well in the original take you can prove that
it is like this, its not only a "would be". Its
a "must be". You can check yourself:
/* With non-empty domain assumption, FOL proof */
¬∃x∀y(Sxy ↔ ¬Syy) is valid.
https://www.umsu.de/trees/#~3~7x~6y(Sxy~4~3Syy)
/* Without non-empty domain assumption, FOL proof */
¬∃x(Dx ∧ ∀y(Dx → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x(Dx~1~6y(Dx~5(Sxy~4~3Syy)))
No barber! Sorry.
¬∃x(Dx ∧ ∀y(Dx → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x(Dx~1~6y(Dx~5(Sxy~4~3Syy)))
Dan Christensen
Oct 12, 2022, 3:12:41 PM10/12/22
to
See my reply just now to your identical posting at sci.math
Dan
On Wednesday, October 12, 2022 at 2:06:56 PM UTC-4, Mostowski Collapse wrote:
> You invested so much into the barber paradox,
> even did a power point, with a story where it is
> pretended that the barber exists.
>
Mostowski Collapse
Oct 12, 2022, 5:10:46 PM10/12/22
to
See my reply just now to your identical posting at sci.math
[Snip]
Mostowski Collapse
Oct 12, 2022, 5:11:07 PM10/12/22
to
See my reply just now to your identical posting at sci.logic
[Snip]
[Snip]
Mostowski Collapse
Oct 16, 2022, 10:01:07 AM10/16/22
to
Wonky man aka Dan Christensen sophistry are typical
crank farts. When refering to the Russell Paradox we of
course refer to everything the Russell Paradox needs,
none of it is needed for the Drinker Paradox. Here is
another proof, again in FOL:
To add a proof in Fitch style, natural deduction:
19 | Ex(Px -> VyPy) 18 ~~ Elimination
https://math.stackexchange.com/a/807721
Not a single line towards Russell Paradox needed,
not as a theorem, not as something derived from it,
not any axiom from SET needed, its not a FOL+SET
proof, its simply a FOL proof. Something wonky man
aka Dan Christensen and his ant brain cannot grasp.
How is this possible he asks, since his crank tool
cannot do it. On the other hand his crank tool DC Spoiled
should be able to prove the following, this is also valid in an
empty domain. So why can wonky man not prove it
ALL(drinkers):EXIST(x):[x e drinkers => ALL(y):[y e drinkers]]
without resorting to the Russell Paradox and related stuff?
LMAO!
crank farts. When refering to the Russell Paradox we of
course refer to everything the Russell Paradox needs,
none of it is needed for the Drinker Paradox. Here is
another proof, again in FOL:
To add a proof in Fitch style, natural deduction:
19 | Ex(Px -> VyPy) 18 ~~ Elimination
https://math.stackexchange.com/a/807721
Not a single line towards Russell Paradox needed,
not as a theorem, not as something derived from it,
not any axiom from SET needed, its not a FOL+SET
proof, its simply a FOL proof. Something wonky man
aka Dan Christensen and his ant brain cannot grasp.
How is this possible he asks, since his crank tool
cannot do it. On the other hand his crank tool DC Spoiled
should be able to prove the following, this is also valid in an
empty domain. So why can wonky man not prove it
ALL(drinkers):EXIST(x):[x e drinkers => ALL(y):[y e drinkers]]
without resorting to the Russell Paradox and related stuff?
LMAO!
Mostowski Collapse
Oct 16, 2022, 10:12:00 AM10/16/22
to
Interesting other "dual" of the Drinker Paradox is this one,
again a pure FOL proof available, still no FOL+SET needed,
contrary to what Wonky Man aka Dan Christensen wants:
∃x(∃yQy → Qx) is valid.
https://www.umsu.de/trees/#~7x%28~7yQy~5Qx%29
Its even more intuitively true, without invoking the
Russell Paradox and related stuff. There are two cases:
case 1: ∃yQy, well modell theoretically we can take any
witness y0, which did Qy0 make true, and make the quantified
main sentence also true, ∃yQy → Qy0, which makes main
sentence also true, ∃x(∃yQy → Qx).
case 2: ~∃yQy, then ∃x(∃yQy → Qx) is vacuously true.
Credits: https://math.stackexchange.com/a/4225776
again a pure FOL proof available, still no FOL+SET needed,
contrary to what Wonky Man aka Dan Christensen wants:
∃x(∃yQy → Qx) is valid.
https://www.umsu.de/trees/#~7x%28~7yQy~5Qx%29
Its even more intuitively true, without invoking the
Russell Paradox and related stuff. There are two cases:
case 1: ∃yQy, well modell theoretically we can take any
witness y0, which did Qy0 make true, and make the quantified
main sentence also true, ∃yQy → Qy0, which makes main
sentence also true, ∃x(∃yQy → Qx).
case 2: ~∃yQy, then ∃x(∃yQy → Qx) is vacuously true.
Credits: https://math.stackexchange.com/a/4225776
Mostowski Collapse
Oct 17, 2022, 3:05:49 AM10/17/22
to
Since Dan-O-Matik aka Wonky Man believes in Wikipedia, this
could help cure his botched Drinker Paradox. Might he take a
closer look what he proved:
/* Wrong Formula */
EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
http://www.dcproof.com/DrinkersThm1.htm
And then what Wikipedia wants:
∃x e P [D(x) => ∀y e P D(y)]
https://en.wikipedia.org/wiki/Drinker_paradox
or expanding the bounded quantifier:
∃x[x e P & [D(x) => ∀x[x e P => D(y)]]
https://en.wikipedia.org/wiki/Bounded_quantifier#Bounded_quantifiers_in_set_theory
If we use y e drinkers for D(y), and z e pub for z e P, what
do we get. Correct a different formula:
/* Corrected Formula */
EXIST(x):[x e pub & [x e drinkers => ALL(a):[a e pub => a e drinkers]]]
Would he dare proving the above formula in DC Proof?
Can he do it without Russell Paradox?
could help cure his botched Drinker Paradox. Might he take a
closer look what he proved:
/* Wrong Formula */
EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
http://www.dcproof.com/DrinkersThm1.htm
And then what Wikipedia wants:
∃x e P [D(x) => ∀y e P D(y)]
https://en.wikipedia.org/wiki/Drinker_paradox
or expanding the bounded quantifier:
∃x[x e P & [D(x) => ∀x[x e P => D(y)]]
https://en.wikipedia.org/wiki/Bounded_quantifier#Bounded_quantifiers_in_set_theory
If we use y e drinkers for D(y), and z e pub for z e P, what
do we get. Correct a different formula:
/* Corrected Formula */
EXIST(x):[x e pub & [x e drinkers => ALL(a):[a e pub => a e drinkers]]]
Would he dare proving the above formula in DC Proof?
Can he do it without Russell Paradox?
Mostowski Collapse
Nov 23, 2022, 5:46:46 PM11/23/22
to
What kind of material implication is this:
> I have been unable to formally justify the without-loss-of-generality
claim. [...] It seems unlikely that the without-loss-of-generality claim
can be justified using the ordinary rules of logic found in most math
textbooks as has been used here.
https://groups.google.com/g/sci.logic/c/mU8PLvGDJQ8/m/Kb5H-uRCAQAJ
Implication of the existence of an alien mathematics from
the fifth dimension because of Wonky Mans inability?
LoL
> I have been unable to formally justify the without-loss-of-generality
claim. [...] It seems unlikely that the without-loss-of-generality claim
can be justified using the ordinary rules of logic found in most math
textbooks as has been used here.
https://groups.google.com/g/sci.logic/c/mU8PLvGDJQ8/m/Kb5H-uRCAQAJ
Implication of the existence of an alien mathematics from
the fifth dimension because of Wonky Mans inability?
LoL
Mostowski Collapse
Nov 23, 2022, 5:51:09 PM11/23/22
to
Come on, you can quantify over function symbols in DC Proof.
It should not be so difficult to prove for red blue colorings:
ALL(color):EXIST(color2):ALL(x):[
(color(x)=red => color2(x)=blue) &
(color(x)=blue => color2(x)=red)]
Eh voila you have found a Galois Connection that could
solve your WLOG problem. Isn't this a nice feature of DC Proof?
It should not be so difficult to prove for red blue colorings:
ALL(color):EXIST(color2):ALL(x):[
(color(x)=red => color2(x)=blue) &
(color(x)=blue => color2(x)=red)]
Eh voila you have found a Galois Connection that could
solve your WLOG problem. Isn't this a nice feature of DC Proof?
Dan Christensen
Nov 23, 2022, 7:52:29 PM11/23/22
to
On Wednesday, November 23, 2022 at 5:51:09 PM UTC-5, Mostowski Collapse wrote:
> Come on, you can quantify over function symbols in DC Proof.
> It should not be so difficult to prove for red blue colorings:
>
> ALL(color):EXIST(color2):ALL(x):[
> (color(x)=red => color2(x)=blue) &
> (color(x)=blue => color2(x)=red)]
>
[snip]
> Come on, you can quantify over function symbols in DC Proof.
> It should not be so difficult to prove for red blue colorings:
>
> ALL(color):EXIST(color2):ALL(x):[
> (color(x)=red => color2(x)=blue) &
> (color(x)=blue => color2(x)=red)]
>
So this the first line of your promised formal proof to find a formal mathematical shortcut? What rule did you apply to obtain it? What are the next 2 lines and the rules you used to obtain them. You don't have clue??? Oh, well...
Dan
Mostowski Collapse
Nov 24, 2022, 10:35:02 AM11/24/22
to
Its amazing that Galois Connection doesn't speek to you.
But you proved the Schröder-Bernstein-Cantor theorem,
where you have f : A → B injective and g : B → A injective.
What is the result after the pair (f,g) ? The conclusion
is that there is a bijection h : A → B. Now bijection doesn't
ring a bell? Its here on the WLOG wikipedia:
> On the other hand, if neither such a symmetry nor
> another form of **equivalence** can be established,
> https://en.wikipedia.org/wiki/Without_loss_of_generality
Still no brain cell moving in Wonky Mans big void?
Why would you claim WLOG isn't formalizable?
LMAO!
But you proved the Schröder-Bernstein-Cantor theorem,
where you have f : A → B injective and g : B → A injective.
What is the result after the pair (f,g) ? The conclusion
is that there is a bijection h : A → B. Now bijection doesn't
ring a bell? Its here on the WLOG wikipedia:
> On the other hand, if neither such a symmetry nor
> another form of **equivalence** can be established,
> https://en.wikipedia.org/wiki/Without_loss_of_generality
Still no brain cell moving in Wonky Mans big void?
Why would you claim WLOG isn't formalizable?
LMAO!
Mostowski Collapse
Nov 24, 2022, 10:49:56 AM11/24/22
to
Its relatively easy, if your space S can be partitioned
into two disjoint parts, R ∪ T, and there is a function,
not necessary a bijection, h : R → T , and if you have:
ALL(x):[R(x) => P(x)]
ALL(x):[R(x) & P(x) => P(h(x))]
Then you can of course conclude:
ALL(x):[T(x) => P(x)]
So without loss of generality, if you know ALL(x):[R(x) & P(x)
=> P(h(x))], you don't need to prove ALL(x):[T(x) => P(x)].
Even Wolfgang Schwartz tool can do, DC Proof can't?
(∀x(Rx → Th(x)) ∧ /* h : R → T */
(∀x(Rx → Px) ∧ /* ALL(x):[R(x) => P(x)] */
∀x((Rx ∧ Px) → Ph(x)))) → /* ALL(x):[R(x) & P(x) => P(h(x))] */
∀x(Tx → Px) is invalid. /* ALL(x):[T(x) => P(x)] */
https://www.umsu.de/trees/#~6x%28R%28x%29~5T%28h%28x%29%29%29~1~6x%28R%28x%29~5P%28x%29%29~1~6x%28R%28x%29~1P%28x%29~5P%28h%28x%29%29%29~5~6x%28T%28x%29~5P%28x%29%29
P:S.: Sometimes R ∪ T are not disjoint. Some symmetries
have a "diagonal", which is included in both R and T.
So you have a partition D ∪ R ∪ T, where S0 is the
Diagonal, and a bijection h : D ∪ R → D ∪ T. But
the result is the same, you can look at D ∪ R only. This
is a very common method to reduce search space
in combinatorial problems, and goes by the name
symmetry breaking. Example paper:
> Breaking Symmetries in Graph Search with Canonizing Sets
> Avraham Itzhakov, Michael Codish - 2015
> https://arxiv.org/abs/1511.08205
into two disjoint parts, R ∪ T, and there is a function,
not necessary a bijection, h : R → T , and if you have:
ALL(x):[R(x) => P(x)]
ALL(x):[R(x) & P(x) => P(h(x))]
Then you can of course conclude:
ALL(x):[T(x) => P(x)]
So without loss of generality, if you know ALL(x):[R(x) & P(x)
=> P(h(x))], you don't need to prove ALL(x):[T(x) => P(x)].
Even Wolfgang Schwartz tool can do, DC Proof can't?
(∀x(Rx → Th(x)) ∧ /* h : R → T */
(∀x(Rx → Px) ∧ /* ALL(x):[R(x) => P(x)] */
∀x((Rx ∧ Px) → Ph(x)))) → /* ALL(x):[R(x) & P(x) => P(h(x))] */
∀x(Tx → Px) is invalid. /* ALL(x):[T(x) => P(x)] */
https://www.umsu.de/trees/#~6x%28R%28x%29~5T%28h%28x%29%29%29~1~6x%28R%28x%29~5P%28x%29%29~1~6x%28R%28x%29~1P%28x%29~5P%28h%28x%29%29%29~5~6x%28T%28x%29~5P%28x%29%29
P:S.: Sometimes R ∪ T are not disjoint. Some symmetries
have a "diagonal", which is included in both R and T.
So you have a partition D ∪ R ∪ T, where S0 is the
Diagonal, and a bijection h : D ∪ R → D ∪ T. But
the result is the same, you can look at D ∪ R only. This
is a very common method to reduce search space
in combinatorial problems, and goes by the name
symmetry breaking. Example paper:
> Breaking Symmetries in Graph Search with Canonizing Sets
> Avraham Itzhakov, Michael Codish - 2015
> https://arxiv.org/abs/1511.08205
Dan Christensen
Nov 24, 2022, 10:55:43 AM11/24/22
to
Try to stay on topic, Jan Burse. See the thread, ""Without loss of generality" may not be formalizable"
Dan
On Thursday, November 24, 2022 at 10:35:02 AM UTC-5, Mostowski Collapse wrote:
> Its amazing that Galois Connection doesn't speek to you.
> But you proved the Schröder-Bernstein-Cantor theorem,
> where you have f : A → B injective and g : B → A injective.
>
> What is the result after the pair (f,g) ? The conclusion
> is that there is a bijection h : A → B. Now bijection doesn't
> ring a bell? Its here on the WLOG wikipedia:
>
> > On the other hand, if neither such a symmetry nor
> > another form of **equivalence** can be established,
> > https://en.wikipedia.org/wiki/Without_loss_of_generality
>
> Still no brain cell moving in Wonky Mans big void?
> Why would you claim WLOG isn't formalizable?
>
[snip]
Dan
On Thursday, November 24, 2022 at 10:35:02 AM UTC-5, Mostowski Collapse wrote:
> Its amazing that Galois Connection doesn't speek to you.
> But you proved the Schröder-Bernstein-Cantor theorem,
> where you have f : A → B injective and g : B → A injective.
>
> What is the result after the pair (f,g) ? The conclusion
> is that there is a bijection h : A → B. Now bijection doesn't
> ring a bell? Its here on the WLOG wikipedia:
>
> > On the other hand, if neither such a symmetry nor
> > another form of **equivalence** can be established,
> > https://en.wikipedia.org/wiki/Without_loss_of_generality
>
> Still no brain cell moving in Wonky Mans big void?
> Why would you claim WLOG isn't formalizable?
>
Mostowski Collapse
Nov 24, 2022, 11:22:54 AM11/24/22
to
I am totally on topic. Given this:
Dan Christensen schrieb am Montag, 21. November 2022 um 21:18:40 UTC+1:
> I have been unable to formally justify the without-loss-of-generality
claim. [...] It seems unlikely that the without-loss-of-generality claim
can be justified using the ordinary rules of logic found in most math
textbooks as has been used here.
https://groups.google.com/g/sci.logic/c/mU8PLvGDJQ8/m/Kb5H-uRCAQAJ
We are still waiting for your proof of the unprovability of symmetry breaking.
LoL
Dan Christensen schrieb am Montag, 21. November 2022 um 21:18:40 UTC+1:
> I have been unable to formally justify the without-loss-of-generality
claim. [...] It seems unlikely that the without-loss-of-generality claim
can be justified using the ordinary rules of logic found in most math
textbooks as has been used here.
https://groups.google.com/g/sci.logic/c/mU8PLvGDJQ8/m/Kb5H-uRCAQAJ
LoL
Dan Christensen
Nov 24, 2022, 12:49:30 PM11/24/22
to
On Thursday, November 24, 2022 at 11:22:54 AM UTC-5, Mostowski Collapse wrote:
> I am totally on topic. [snip]
Get a life, Jan Burse! The topic here is "Justifying the truth table for the IMPLIES-operator." See the thread "'Without loss of generality' may not be formalizable".
Dan
> I am totally on topic. [snip]
Get a life, Jan Burse! The topic here is "Justifying the truth table for the IMPLIES-operator." See the thread "'Without loss of generality' may not be formalizable".
Dan
Mostowski Collapse
Nov 24, 2022, 5:24:40 PM11/24/22
to
The swapping works also with SAT Solver version
of Pigeon principle, that is related to the WLOG example:
If we try to place 3 pigeons in 2 boxes, we get this
conjunctive normal form (CNF_1):
X11 v X12
X21 v X22
X31 v X32
~X11 v ~X21
~X11 v ~X31
~X21 v ~X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32
Now if we swap indices of the two boxes, we
get another conjunctive normal form (CNF_2):
X12 v X11
X22 v X21
X32 v X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32
~X11 v ~X21
~X11 v ~X31
~X21 v ~X31
But obviously CNF_1 => CNF_2, and of course
also CNF_1 => CNF_2, they are logically equivalent.
of Pigeon principle, that is related to the WLOG example:
If we try to place 3 pigeons in 2 boxes, we get this
conjunctive normal form (CNF_1):
X11 v X12
X21 v X22
X31 v X32
~X11 v ~X21
~X11 v ~X31
~X21 v ~X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32
Now if we swap indices of the two boxes, we
get another conjunctive normal form (CNF_2):
X12 v X11
X22 v X21
X32 v X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32
~X11 v ~X21
~X11 v ~X31
~X21 v ~X31
But obviously CNF_1 => CNF_2, and of course
also CNF_1 => CNF_2, they are logically equivalent.
Mostowski Collapse
Nov 24, 2022, 5:30:37 PM11/24/22
to
But I agree with Fritz that Wikipedia is a little nonsensical.
Since they write the following:
"Assume, without loss of generality, that the first object is red."
https://en.wikipedia.org/wiki/Without_loss_of_generality
This could be read as not only a choice of a color, but also a
choice of a pigeon. Its basically a DPLL step: Set x11 to true,
and see what happens, via unit propagation we get a reduced formula:
X21 v X22
X31 v X32
~X21
or another pigeon, or another color and another pigeon. The
problem is now that DPLL is not based on symmetry breaking,
as a next step it would try to set X11 to false. So there could
be indeed a problem, in that another reading of Wikipedia doesn't
show without loss of generality as we would wish.
It would only give an example of a kind of order independence,
which is a common phenomenon for many algorithms, even
if there is no symmetry breaking:
Davis–Putnam–Logemann–Loveland (DPLL) algorithm
https://en.wikipedia.org/wiki/DPLL_algorithm
Mostowski Collapse schrieb am Donnerstag,
24. November 2022 um 23:24:40 UTC+1:
Since they write the following:
"Assume, without loss of generality, that the first object is red."
https://en.wikipedia.org/wiki/Without_loss_of_generality
This could be read as not only a choice of a color, but also a
choice of a pigeon. Its basically a DPLL step: Set x11 to true,
and see what happens, via unit propagation we get a reduced formula:
X21 v X22
X31 v X32
~X31
~X21 v ~X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32
But we could also start with any other variable, an other color
~X21 v ~X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32
or another pigeon, or another color and another pigeon. The
problem is now that DPLL is not based on symmetry breaking,
as a next step it would try to set X11 to false. So there could
be indeed a problem, in that another reading of Wikipedia doesn't
show without loss of generality as we would wish.
It would only give an example of a kind of order independence,
which is a common phenomenon for many algorithms, even
if there is no symmetry breaking:
Davis–Putnam–Logemann–Loveland (DPLL) algorithm
https://en.wikipedia.org/wiki/DPLL_algorithm
Mostowski Collapse schrieb am Donnerstag,
24. November 2022 um 23:24:40 UTC+1:
Dan Christensen
Nov 24, 2022, 6:39:08 PM11/24/22
to
On Thursday, November 24, 2022 at 5:30:37 PM UTC-5, Mostowski Collapse wrote:
> But I agree with Fritz that Wikipedia is a little nonsensical.
> Since they write the following:
>
> "Assume, without loss of generality, that the first object is red."
> https://en.wikipedia.org/wiki/Without_loss_of_generality
>
> But I agree with Fritz that Wikipedia is a little nonsensical.
> Since they write the following:
>
> "Assume, without loss of generality, that the first object is red."
> https://en.wikipedia.org/wiki/Without_loss_of_generality
>
It is loading more messages.
0 new messages