info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
What is the truth value of f(x)=y if x is outside the domain of the function f?
214 views
Skip to first unread message
Dan Christensen
Dec 5, 2021, 11:13:09 PM12/5/21
to
This is actually a point of controversy to some here. A related question might be, given an array of 10 Boolean variables, what is the truth value of the 11th one? It seems to me that in both cases, the truth value is undefined. Your comments?
Dan
Dan
Mostowski Collapse
Dec 6, 2021, 2:32:37 AM12/6/21
to
Check wikipedia, F : P -> Q, requires necessarely F ⊆ P x Q:
ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)]
Now take contraposition you get:
ALL(a):ALL(b):[~P(a) | ~Q(b) => ~F(a,b)]
Or in words, if (a,b) is outside of the domain and co-domain, then F is false.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)]
Now take contraposition you get:
ALL(a):ALL(b):[~P(a) | ~Q(b) => ~F(a,b)]
Or in words, if (a,b) is outside of the domain and co-domain, then F is false.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
FredJeffries
Dec 6, 2021, 11:47:15 AM12/6/21
to
On Sunday, December 5, 2021 at 8:13:09 PM UTC-8, Dan Christensen wrote:
> This is actually a point of controversy to some here. A related question might be, given an array of 10 Boolean variables, what is the truth value of the 11th one? It seems to me that in both cases, the truth value is undefined. Your comments?
so you've abandoned your silly claim that two-valued Boolean logic is sufficient for all 'usual-textbook mathematics'
> This is actually a point of controversy to some here. A related question might be, given an array of 10 Boolean variables, what is the truth value of the 11th one? It seems to me that in both cases, the truth value is undefined. Your comments?
Mostowski Collapse
Dec 6, 2021, 12:53:02 PM12/6/21
to
It would explain why contraposition shouldn't hold. But to the
best of my knowledge, classically A => B and ~B => ~A share
the same truth table:
p q (p → q)
F F T
F T T
T F F
T T T
p q (¬q → ¬p)
F F T
F T T
T F F
T T T
But Dan-O-Matik did not refer to bivalance with his boolean
example. He rather asked what happens with F(10)
when F : {0,..,9} -> {0,1}. But the answer is clear:
~F(10,0), ~F(10,1), ~F(10, pink unicorn), etc...
Thats what the declaration F : {0,..,9} -> {0,1} implies.
best of my knowledge, classically A => B and ~B => ~A share
the same truth table:
p q (p → q)
F F T
F T T
T F F
T T T
p q (¬q → ¬p)
F F T
F T T
T F F
T T T
But Dan-O-Matik did not refer to bivalance with his boolean
example. He rather asked what happens with F(10)
when F : {0,..,9} -> {0,1}. But the answer is clear:
~F(10,0), ~F(10,1), ~F(10, pink unicorn), etc...
Thats what the declaration F : {0,..,9} -> {0,1} implies.
Mostowski Collapse
Dec 6, 2021, 12:57:05 PM12/6/21
to
Dan Christensen
Dec 6, 2021, 2:19:31 PM12/6/21
to
On Monday, December 6, 2021 at 2:32:37 AM UTC-5, Mostowski Collapse wrote:
> Check wikipedia, F : P -> Q, requires necessarely F ⊆ P x Q:
>
> ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)]
>
> Now take contraposition you get:
>
> ALL(a):ALL(b):[~P(a) | ~Q(b) => ~F(a,b)]
>
> Or in words, if (a,b) is outside of the domain and co-domain, then F is false.
>
This seems to be a weird artifact of the representation of a function that you have chosen. Thanks for bringing it to our attention, but AFAIK you cannot obtain this wonky result with the more standard representation: ALL(a):[a in P => F(a) in Q]
> Check wikipedia, F : P -> Q, requires necessarely F ⊆ P x Q:
>
> ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)]
>
> Now take contraposition you get:
>
> ALL(a):ALL(b):[~P(a) | ~Q(b) => ~F(a,b)]
>
> Or in words, if (a,b) is outside of the domain and co-domain, then F is false.
>
In group theory, for example, we can have at a subgroup H < G such that:
(1) ALL(a): ALL(b):[a in G & b in G => a*b in G]
(2) ALL(a): ALL(b):[a in H & b in H => a*b in H]
By your reasoning: x not in H would imply that x*y=z would be false for every y and z. An obvious non-starter.
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
Dan Christensen
Dec 6, 2021, 2:27:20 PM12/6/21
to
On Monday, December 6, 2021 at 12:53:02 PM UTC-5, Mostowski Collapse wrote:
> It would explain why contraposition shouldn't hold.
Nothing is wrong with contraposition. Here is a formal proof
> It would explain why contraposition shouldn't hold.
1 A => B
Premise
2 ~B
Premise
3 A
Premise
4 B
Detach, 1, 3
5 ~B & B
Join, 2, 4
6 ~A
Conclusion, 3
7 ~B => ~A
Conclusion, 2
8 A => B => [~B => ~A]
Conclusion, 1
Mostowski Collapse
Dec 6, 2021, 2:57:59 PM12/6/21
to
For the 1000-th time, its not my reasoning, read the fucking wiki:
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
A group is defined as a tripple <G,*,-1>, where
* : G x G -> G, -1 : G -> G
And the above are like in the wiki X -> Y definition. Now you can see that
your DC Proof axioms are utter nonsense.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
A group is defined as a tripple <G,*,-1>, where
* : G x G -> G, -1 : G -> G
And the above are like in the wiki X -> Y definition. Now you can see that
your DC Proof axioms are utter nonsense.
Mostowski Collapse
Dec 6, 2021, 3:06:05 PM12/6/21
to
Dang you are stupid. A sub group is the smaller multiplication
table, on not simply the larger multiplication plus some
hand waving. This multiplication table is also classical closed
and doesn't have some dark booleans outside.
To understand the forming of subgroups, you first might
start understanding the forming of restriction of a function
F : X -> Y to a sub domain Z.
You get a new object!! This new object is usually denoted
by F|Z, called the restriction of F to Z. For gods sake read
a beginner book before you start writing axioms.
You find all this in this booklet, and you don't need to get
much past the first chapter. Its really easy!!
Basic Set Theory - Azriel Levy
https://www.amazon.de/dp/0486420795
Its only 20 bucks or so.
table, on not simply the larger multiplication plus some
hand waving. This multiplication table is also classical closed
and doesn't have some dark booleans outside.
To understand the forming of subgroups, you first might
start understanding the forming of restriction of a function
F : X -> Y to a sub domain Z.
You get a new object!! This new object is usually denoted
by F|Z, called the restriction of F to Z. For gods sake read
a beginner book before you start writing axioms.
You find all this in this booklet, and you don't need to get
much past the first chapter. Its really easy!!
Basic Set Theory - Azriel Levy
https://www.amazon.de/dp/0486420795
Its only 20 bucks or so.
Mostowski Collapse
Dec 6, 2021, 6:32:12 PM12/6/21
to
Try proving with your nonsense axioms:
An operator * : G x G -> G is finite, if its extension is finite.
For example this operator * : {0,1} x {0,1} -> {0,1}:
* | 0 1
------------
0 | 0 1
1 | 1 1
Is finite, it is only 4 pairs. On the other hand
* : R x R -> R is infinite. You will possibly be able
to prove something. But you will not be able to
make a definition:
Finite(S) <=> ....
Where somebody can plug-in the operator *, and then
ask Finite(*). You solution will be something where
you have to carry around further attributes, instead
of using the proper F : X -> Y function spaces,
as define on wikipedia. Not using the proper
function spaces as on wikipedia is non-standard
and leads to clumsy proofs. Its not what is found
in today text books when we talk about a mathematical
structure such as a group.
Dan Christensen schrieb:
An operator * : G x G -> G is finite, if its extension is finite.
For example this operator * : {0,1} x {0,1} -> {0,1}:
* | 0 1
------------
0 | 0 1
1 | 1 1
Is finite, it is only 4 pairs. On the other hand
* : R x R -> R is infinite. You will possibly be able
to prove something. But you will not be able to
make a definition:
Finite(S) <=> ....
Where somebody can plug-in the operator *, and then
ask Finite(*). You solution will be something where
you have to carry around further attributes, instead
of using the proper F : X -> Y function spaces,
as define on wikipedia. Not using the proper
function spaces as on wikipedia is non-standard
and leads to clumsy proofs. Its not what is found
in today text books when we talk about a mathematical
structure such as a group.
Dan Christensen schrieb:
> On Monday, December 6, 2021 at 3:06:05 PM UTC-5, Mostowski Collapse wrote:
>
>> To understand the forming of subgroups, you first might
>> start understanding the forming of restriction of a function
>> F : X -> Y to a sub domain Z.
>>
>> You get a new object!!
>
> Not really. You get a binary function * on the subgroup that must be consistent with that on the entire group. They can't differ. You would lose that essential property with your representation of a function. Group theory would blow up. Thanks, but no thanks, Jan Burse!
>
>> To understand the forming of subgroups, you first might
>> start understanding the forming of restriction of a function
>> F : X -> Y to a sub domain Z.
>>
>> You get a new object!!
>
Mostowski Collapse
Dec 6, 2021, 7:28:24 PM12/6/21
to
Now you say it correctly for the first time:
> (The operator in the subgroup)1 must be consistent
> with (that defined in the entire group)2
There are two operators. If you have two monoids:
𝔊=<G,m,z> with m : G x G -> G, z : G
and ℌ=<H,k,e> with k : H x H -> H, e : G
Then the second monoid is a submonoid of the first monoid if:
1) H subset G
2) ALL(a):ALL(b):[H(a) & H(b) => k(a,b) = m(a,b)]
3) e = z
Obviously then k is the restriction of m. I didn't
say restriction implements closure, I only said
we have two copies:
k : (The operator in the subgroup)1
m : (that defined in the entire group)2
k = m | HxH
Lets say we denoted submonoid by ℌ < 𝔊. When using
a common operator you cannot work with so easily.
Lets say you have:
~(ℌ < 𝔊)
Such that k ≠ m | HxH. The usual approach to
represent mathematical structures in modern Proof
assistants is to use so called sigma types:
https://en.wikipedia.org/wiki/Dependent_type#%CE%A3_type
Have Fun!
Dan Christensen schrieb:
> On Monday, December 6, 2021 at 3:06:05 PM UTC-5, Mostowski Collapse wrote:
>
>>
> (The operator in the subgroup)1 must be consistent
> with (that defined in the entire group)2
There are two operators. If you have two monoids:
𝔊=<G,m,z> with m : G x G -> G, z : G
and ℌ=<H,k,e> with k : H x H -> H, e : G
Then the second monoid is a submonoid of the first monoid if:
1) H subset G
2) ALL(a):ALL(b):[H(a) & H(b) => k(a,b) = m(a,b)]
3) e = z
Obviously then k is the restriction of m. I didn't
say restriction implements closure, I only said
we have two copies:
k : (The operator in the subgroup)1
m : (that defined in the entire group)2
k = m | HxH
Lets say we denoted submonoid by ℌ < 𝔊. When using
a common operator you cannot work with so easily.
Lets say you have:
~(ℌ < 𝔊)
Such that k ≠ m | HxH. The usual approach to
represent mathematical structures in modern Proof
assistants is to use so called sigma types:
https://en.wikipedia.org/wiki/Dependent_type#%CE%A3_type
Have Fun!
Dan Christensen schrieb:
> On Monday, December 6, 2021 at 3:06:05 PM UTC-5, Mostowski Collapse wrote:
>
>>
>> To understand the forming of subgroups, you first might
>> start understanding the forming of restriction of a function
>> F : X -> Y to a sub domain Z.
>>
>> You get a new object!!
>
> Not really. The operator in the subgroup must be consistent with that defined in the entire group. Using your representation of a function, this requirement of consistency is lost. Group theory blows up! Thanks but no thanks, Jan Burse.
>> start understanding the forming of restriction of a function
>> F : X -> Y to a sub domain Z.
>>
>> You get a new object!!
>
Mostowski Collapse
Dec 6, 2021, 7:39:12 PM12/6/21
to
What implements closure is the declaration k : H x H -> H.
Why does restriction not implement closure.
Because restriction leaves more or less open what the
range of a function will be. If you have a function
F : X -> Y, and a domain Z, then F|Z can practically
have any range (smallest co-domain). There is no law
from the outside that would say what range (smallest
co-domain) F|Z would have, from the signature F : X -> Y alone.
Got it?
Just read this booklet please:
Basic Set Theory - Ariel Levy
https://www.amazon.de/dp/0486420795
Mostowski Collapse schrieb:
>
> Here is a sigma type monoid example in Arend:
> https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Monoid.ard
>
> Mostowski Collapse schrieb:
Why does restriction not implement closure.
Because restriction leaves more or less open what the
range of a function will be. If you have a function
F : X -> Y, and a domain Z, then F|Z can practically
have any range (smallest co-domain). There is no law
from the outside that would say what range (smallest
co-domain) F|Z would have, from the signature F : X -> Y alone.
Got it?
Just read this booklet please:
Basic Set Theory - Ariel Levy
https://www.amazon.de/dp/0486420795
Mostowski Collapse schrieb:
>
> Here is a sigma type monoid example in Arend:
> https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Monoid.ard
>
> Mostowski Collapse schrieb:
Dan Christensen
Dec 6, 2021, 7:46:04 PM12/6/21
to
On Monday, December 6, 2021 at 6:32:12 PM UTC-5, Mostowski Collapse wrote:
> But you will not be able to
>
> make a definition:
>
> Finite(S) <=> ....
>
Liar. See https://dcproof.wordpress.com/2014/09/17/infinity-the-story-so-far/
> But you will not be able to
>
> make a definition:
>
> Finite(S) <=> ....
>
Mostowski Collapse
Dec 6, 2021, 8:02:14 PM12/6/21
to
An easy corrolar of doing it properly is that if G is finite,
then * and -1 are both also finite. You claimed to know what is
finite somewhere else, by invoking Dedekind.
Can you absolutely prove, that if the object G is finite,
and <G,*,-1> is a group that then * is finite and -1 is finite?
I doubt that you can prove that with your nonsense.
In your nonsense world * can belong to the group G
or to some super group G', if the group G is finite the
super group G' might be nevertheless infinite,
so that * is both finite and infinite, or what? LoL Yikes,
and here we have it again, dark booleans, and
now dark groups.
then * and -1 are both also finite. You claimed to know what is
finite somewhere else, by invoking Dedekind.
Can you absolutely prove, that if the object G is finite,
and <G,*,-1> is a group that then * is finite and -1 is finite?
I doubt that you can prove that with your nonsense.
In your nonsense world * can belong to the group G
or to some super group G', if the group G is finite the
super group G' might be nevertheless infinite,
so that * is both finite and infinite, or what? LoL Yikes,
and here we have it again, dark booleans, and
now dark groups.
Message has been deleted
Mostowski Collapse
Dec 6, 2021, 8:03:51 PM12/6/21
to
Here is a sigma type monoid example in Arend:
https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Monoid.ard
Mostowski Collapse schrieb:
Message has been deleted
Dan Christensen
Dec 6, 2021, 8:12:09 PM12/6/21
to
On Monday, December 6, 2021 at 3:06:05 PM UTC-5, Mostowski Collapse wrote:
> To understand the forming of subgroups, you first might
> start understanding the forming of restriction of a function
> F : X -> Y to a sub domain Z.
>
> You get a new object!!
> start understanding the forming of restriction of a function
> F : X -> Y to a sub domain Z.
>
> You get a new object!!
Not really. You get a binary function * on the subgroup that must be consistent with that on the entire group. They can't differ. You would lose that essential property with your representation of a function. Group theory would blow up. Thanks, but no thanks, Jan Burse!
Mostowski Collapse
Dec 6, 2021, 8:13:50 PM12/6/21
to
Ok take two monoids 𝔊 and ℌ, with ℌ < 𝔊,
model them with your common operator approach,
and please tell us how the formalization of:
Finite((The operator in the subgroup)1)
Finite((that defined in the entire group)2)
If you have additional parameters than only the operator,
then you did obviously something wrong.
Dan Christensen schrieb:
Message has been deleted
Message has been deleted
Dan Christensen
Dec 7, 2021, 12:58:33 AM12/7/21
to
(Correction)
On Monday, December 6, 2021 at 2:32:37 AM UTC-5, Mostowski Collapse wrote:
Define a set of ordered pairs F such that ALL(a):[a in P => EXIST(b):[b in Q & (a,b) in F & ALL(c):[c in Q => [(a,c) in F => c=b]]]].
Note that this does NOT require that ALL(a):ALL(b):[(a, b) in F => a in P & b in Q]. The is does NOT rule out other terms in F.
Comments?
On Monday, December 6, 2021 at 2:32:37 AM UTC-5, Mostowski Collapse wrote:
> Check wikipedia, F : P -> Q, requires necessarely F ⊆ P x Q:
>
> ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)]
>
> Now take contraposition you get:
>
> ALL(a):ALL(b):[~P(a) | ~Q(b) => ~F(a,b)]
>
> Or in words, if (a,b) is outside of the domain and co-domain, then F is false.
>
> https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
Rethinking the notion of a function just a bit...
>
> ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)]
>
> Now take contraposition you get:
>
> ALL(a):ALL(b):[~P(a) | ~Q(b) => ~F(a,b)]
>
> Or in words, if (a,b) is outside of the domain and co-domain, then F is false.
>
> https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
Define a set of ordered pairs F such that ALL(a):[a in P => EXIST(b):[b in Q & (a,b) in F & ALL(c):[c in Q => [(a,c) in F => c=b]]]].
Note that this does NOT require that ALL(a):ALL(b):[(a, b) in F => a in P & b in Q]. The is does NOT rule out other terms in F.
Comments?
Mostowski Collapse
Dec 7, 2021, 3:14:10 AM12/7/21
to
STUDENTS BEWARE Dan-O-Matik didn't take his medication,
sweeping under the rug parts of a definitions. Lets recap:
1) Wikipedia definition of a function:
a binary relation F ⊆ P x Q, serial on P,Q and functional on P,Q
2) Dan-O-Matiks psychotic definition:
serial on P,Q and functional on P,Q
Do you see any differents dear students?
sweeping under the rug parts of a definitions. Lets recap:
1) Wikipedia definition of a function:
a binary relation F ⊆ P x Q, serial on P,Q and functional on P,Q
2) Dan-O-Matiks psychotic definition:
serial on P,Q and functional on P,Q
Do you see any differents dear students?
Mostowski Collapse
Dec 7, 2021, 9:38:28 AM12/7/21
to
This barber riddle is for Dan-O-Matik, I am pretty sure he will be able
to prove that Fritz Klein is indeterminate, some dark boolean, because
the function do something (mathematical) F : M -> T, where M are
mathematicians and T are topics, can have of course, according
to Dan-O-Matik, also some values outside of mathematics.
"Es gäbe zwei Klassen von Mathematikern in Göttingen.
Zur ersten Klasse gehören die, die täten, was Felix Klein wollte, was ihnen
aber nicht gefiel. Zur zweiten Klasse gehörten diejenigen, die täten,
was ihnen gefiel, was aber Felix Klein nicht gefiel. Zu welcher
Klasse gehört Felix Klein? Als die Studenten stumm blieben,
meinte er, die Antwort wäre furchtbar einfach:
Felix Klein wäre gar kein Mathematiker"
"There are two classes of mathematicians in Göttingen. The first
class includes those who do what Felix Klein wanted but didn't
like. The second class included those who did what they liked
but didn't like Felix Klein. What class does Felix Klein belong to?
When the students remained silent, he said the answer would be
terribly simple: Felix Klein wouldn't be a mathematician at all"
Try it with Dan-O-Matik functions! LoL
to prove that Fritz Klein is indeterminate, some dark boolean, because
the function do something (mathematical) F : M -> T, where M are
mathematicians and T are topics, can have of course, according
to Dan-O-Matik, also some values outside of mathematics.
"Es gäbe zwei Klassen von Mathematikern in Göttingen.
Zur ersten Klasse gehören die, die täten, was Felix Klein wollte, was ihnen
aber nicht gefiel. Zur zweiten Klasse gehörten diejenigen, die täten,
was ihnen gefiel, was aber Felix Klein nicht gefiel. Zu welcher
Klasse gehört Felix Klein? Als die Studenten stumm blieben,
meinte er, die Antwort wäre furchtbar einfach:
Felix Klein wäre gar kein Mathematiker"
"There are two classes of mathematicians in Göttingen. The first
class includes those who do what Felix Klein wanted but didn't
like. The second class included those who did what they liked
but didn't like Felix Klein. What class does Felix Klein belong to?
When the students remained silent, he said the answer would be
terribly simple: Felix Klein wouldn't be a mathematician at all"
Try it with Dan-O-Matik functions! LoL
Mostowski Collapse
Dec 7, 2021, 9:39:42 AM12/7/21
to
Source of the riddle by way of Wolfgang Pauli it seems:
https://de.wikipedia.org/wiki/Ernst_Zermelo#Sonstiges
https://de.wikipedia.org/wiki/Ernst_Zermelo#Sonstiges
Mostowski Collapse
Dec 7, 2021, 12:07:28 PM12/7/21
to
How can a grown up talk so much nonsense!
Its not tweaking the usual notion of a function as a set of ordered pairs.
It is the usual notion of a function as a set of ordered pairs.
Lets get back to F : {0} -> {0}, the only function is F = {(0,0)} a singleton
set of an ordered pair. This implies ~F(1,0) because:
~ (1,0) e {(0,0)}
Try proving ~F(1,0) from your definition, which is not a closed set
of ordered pairs. Your "prefered" incorrect definition leaves pretty open
what happens outside of the domain. You could even have elements that
are not ordered pair in F, outside of the domain and co-domain?
Dan Christensen schrieb am Dienstag, 7. Dezember 2021 um 16:49:20 UTC+1:
> There's just a minor technical problem with that approach, as you yourself pointed out: It enables to you assign truth values to functional expressions of the form (a, b) in F outside the domain P. It's a kind of paradox that is resolved as above by tweaking the usual notion of a function as a set of ordered pairs. Or you could just start with the standard functional notation by stating: ALL(a):[a in P => f(a) in Q. That it is my preference.
> Dan
Its not tweaking the usual notion of a function as a set of ordered pairs.
It is the usual notion of a function as a set of ordered pairs.
Lets get back to F : {0} -> {0}, the only function is F = {(0,0)} a singleton
set of an ordered pair. This implies ~F(1,0) because:
~ (1,0) e {(0,0)}
Try proving ~F(1,0) from your definition, which is not a closed set
of ordered pairs. Your "prefered" incorrect definition leaves pretty open
what happens outside of the domain. You could even have elements that
are not ordered pair in F, outside of the domain and co-domain?
Dan Christensen schrieb am Dienstag, 7. Dezember 2021 um 16:49:20 UTC+1:
> There's just a minor technical problem with that approach, as you yourself pointed out: It enables to you assign truth values to functional expressions of the form (a, b) in F outside the domain P. It's a kind of paradox that is resolved as above by tweaking the usual notion of a function as a set of ordered pairs. Or you could just start with the standard functional notation by stating: ALL(a):[a in P => f(a) in Q. That it is my preference.
> Dan
Mostowski Collapse
Dec 7, 2021, 12:14:49 PM12/7/21
to
If you do your nonsensical ALL(a):[a in P => f(a) in Q] , which
is not the f ⊆ P x Q, with a set f:
/* Dan-O-Matiks Nonsense */
1) ALL(a):[a in P => EXIST(b):[(a,b) e f & b in Q]]
You can not only not prove ~(a,b) e f outside of P x Q, you can
also not assure that outside of P x Q the elements, if they exist,
as you possibly have with your indeterminism,
that they are then ordered pairs, if some exist. This means based
on your prefered incorrect definition 1), you cannot prove:
/* Not Provable */
2) ALL(z):[z e f => EXIST(x):EXIST(y):[z = (x,y)]]
is not the f ⊆ P x Q, with a set f:
/* Dan-O-Matiks Nonsense */
1) ALL(a):[a in P => EXIST(b):[(a,b) e f & b in Q]]
You can not only not prove ~(a,b) e f outside of P x Q, you can
also not assure that outside of P x Q the elements, if they exist,
as you possibly have with your indeterminism,
that they are then ordered pairs, if some exist. This means based
on your prefered incorrect definition 1), you cannot prove:
/* Not Provable */
2) ALL(z):[z e f => EXIST(x):EXIST(y):[z = (x,y)]]
Mostowski Collapse
Dec 7, 2021, 12:25:43 PM12/7/21
to
Here is a proof of ALL(z):[z e f => EXIST(x):EXIST(y):[z = (x,y)]] from f ⊆ P x Q:
/* Exy for x in y, and o(x,y) for (x,y) */
∀z(Ezf → ∃x∃y(z=o(x,y) ∧ (Exp ∧ Eyq))) → ∀z(Ezf → ∃x∃yz=o(x,y)) is valid.
https://www.umsu.de/trees/#~6z%28Ezf~5~7x~7y%28z=o%28x,y%29~1Exp~1Eyq%29%29~5~6z%28Ezf~5~7x~7y%28z=o%28x,y%29%29%29
And here is evidence that it is not provable from ALL(a):[a in P => EXIST(b):[(a,b) e f & b in Q]]:
∀a(Eap → ∃b(Eo(a,b)f ∧ Ebq)) → ∀z(Ezf → ∃x∃yz=o(x,y)) is invalid.
https://www.umsu.de/trees/#~6a%28Eap~5~7b%28Eo%28a,b%29f~1Ebq%29%29~5~6z%28Ezf~5~7x~7y%28z=o%28x,y%29%29%29
/* Exy for x in y, and o(x,y) for (x,y) */
∀z(Ezf → ∃x∃y(z=o(x,y) ∧ (Exp ∧ Eyq))) → ∀z(Ezf → ∃x∃yz=o(x,y)) is valid.
https://www.umsu.de/trees/#~6z%28Ezf~5~7x~7y%28z=o%28x,y%29~1Exp~1Eyq%29%29~5~6z%28Ezf~5~7x~7y%28z=o%28x,y%29%29%29
And here is evidence that it is not provable from ALL(a):[a in P => EXIST(b):[(a,b) e f & b in Q]]:
∀a(Eap → ∃b(Eo(a,b)f ∧ Ebq)) → ∀z(Ezf → ∃x∃yz=o(x,y)) is invalid.
https://www.umsu.de/trees/#~6a%28Eap~5~7b%28Eo%28a,b%29f~1Ebq%29%29~5~6z%28Ezf~5~7x~7y%28z=o%28x,y%29%29%29
Mostowski Collapse
Dec 7, 2021, 12:29:56 PM12/7/21
to
Its even worse, when P and Q are the universal class V, then
it also does not assure that f is a set of ordered paris:
∀a∃bEo(a,b)f → ∀z(Ezf → ∃x∃yz=o(x,y)) is invalid.
https://www.umsu.de/trees/#~6a~7bEo%28a,b%29f~5~6z%28Ezf~5~7x~7y%28z=o%28x,y%29%29%29
Your ∀∃ combination is an edifice of imbecility. So there
is something fundamentally wrong in dropping the
assumption f ⊆ P x Q. Its just a ticket to hells kitchen.
it also does not assure that f is a set of ordered paris:
∀a∃bEo(a,b)f → ∀z(Ezf → ∃x∃yz=o(x,y)) is invalid.
https://www.umsu.de/trees/#~6a~7bEo%28a,b%29f~5~6z%28Ezf~5~7x~7y%28z=o%28x,y%29%29%29
Your ∀∃ combination is an edifice of imbecility. So there
is something fundamentally wrong in dropping the
assumption f ⊆ P x Q. Its just a ticket to hells kitchen.
Mostowski Collapse
Dec 7, 2021, 12:39:40 PM12/7/21
to
I wouldn't recommend house painting for Dan-O-Matik.
If you say paint this house, he might also paint the neighbour
house as well, since it was indeterminate what should happen
to the neighbour house. Dan-O-Matik as a painter might
cost you some extra paint and insurance incidents. Dan-O-Matik
with his fluffy function definition just created a new commedy
genre, called anti-occams razor mathematics.
💀 of Math and ☠️ of Physics Archimedes "Putin's Stooge" Plutonium
<plutonium....@gmail.com> blithered:
> > So, get out of sci.math, get out of academics. Go back to house painting...
If you say paint this house, he might also paint the neighbour
house as well, since it was indeterminate what should happen
to the neighbour house. Dan-O-Matik as a painter might
cost you some extra paint and insurance incidents. Dan-O-Matik
with his fluffy function definition just created a new commedy
genre, called anti-occams razor mathematics.
💀 of Math and ☠️ of Physics Archimedes "Putin's Stooge" Plutonium
<plutonium....@gmail.com> blithered:
> > So, get out of sci.math, get out of academics. Go back to house painting...
Dan Christensen
Dec 7, 2021, 2:17:27 PM12/7/21
to
On Tuesday, December 7, 2021 at 12:07:28 PM UTC-5, Mostowski Collapse wrote:
> Lets get back to F : {0} -> {0}, the only function is F = {(0,0)} a singleton
> set of an ordered pair. This implies ~F(1,0) because:
>
> ~ (1,0) e {(0,0)}
>
Thanks again for bringing this to our attention, but I see it as problematic -- a paradox that needs to be resolved. You probably need an axiom or theorem to the effect that, for all x, there exists a set S such that x in S, other elements not being ruled out. Apply it for (0, 0) to obtain (0, 0) in F. You could not then infer that (x, y) in F => x in {0) & y in {0}. Problem solved!
> Lets get back to F : {0} -> {0}, the only function is F = {(0,0)} a singleton
> set of an ordered pair. This implies ~F(1,0) because:
>
> ~ (1,0) e {(0,0)}
>
Mostowski Collapse
Dec 9, 2021, 6:53:41 PM12/9/21
to
Its very easy to prove that (x,y) e f is false outside of the domain.
But you cannot prove that f(x)=y is false outside of the domain.
Because in FOL the f in f(x) denotes a function f : V -> V, a second
order object, whereas the f in (x,y) e f denotes an element f : V a
first order object. The problem with your axiom:
ALL(x):[x in A => f(x) in B]
It talks about a second order object f, which is anyway f : V -> V.
You cannot coerce it to a smaller domain. You can always
prove the following:
ALL(x):EXIST(y):f(x)=y
If you would add a binary relation axiom, as per wiki f ⊆ P x Q,
but in wiki f is a first order object or a class, but not a second order
object. If you add this axiom:
(**) ALL(x):ALL(y):[f(x)=y -> P(x) & Q(y)]
You get an inconsistent system. Try adding (**), you will be
able to derive false in DC Proof. Thats relatively simple.
But you cannot prove that f(x)=y is false outside of the domain.
Because in FOL the f in f(x) denotes a function f : V -> V, a second
order object, whereas the f in (x,y) e f denotes an element f : V a
first order object. The problem with your axiom:
ALL(x):[x in A => f(x) in B]
It talks about a second order object f, which is anyway f : V -> V.
You cannot coerce it to a smaller domain. You can always
prove the following:
ALL(x):EXIST(y):f(x)=y
If you would add a binary relation axiom, as per wiki f ⊆ P x Q,
but in wiki f is a first order object or a class, but not a second order
object. If you add this axiom:
(**) ALL(x):ALL(y):[f(x)=y -> P(x) & Q(y)]
You get an inconsistent system. Try adding (**), you will be
able to derive false in DC Proof. Thats relatively simple.
Mostowski Collapse
Dec 9, 2021, 7:01:50 PM12/9/21
to
Here is the inconsistency proved:
(∃x¬Px ∧ ∀x∀y(f(x)=y → (Px ∧ Qy))) → (R∧¬R) is valid.
https://www.umsu.de/trees/#~7x~3Px~1~6x~6y%28f%28x%29=y~5Px~1Qy%29~5R~1~3R
In ZFC if P is set-like, you can always prove ∃x¬Px.
And any class P different from V, as also a separating element.
(∃x¬Px ∧ ∀x∀y(f(x)=y → (Px ∧ Qy))) → (R∧¬R) is valid.
https://www.umsu.de/trees/#~7x~3Px~1~6x~6y%28f%28x%29=y~5Px~1Qy%29~5R~1~3R
In ZFC if P is set-like, you can always prove ∃x¬Px.
And any class P different from V, as also a separating element.
Mostowski Collapse
Dec 9, 2021, 7:38:44 PM12/9/21
to
Pitty, I guess, the tree tool has a bug:
∀x∀y(f(x)=y → (Px ∧ Qy)) → (R∧¬R) is invalid.
https://www.umsu.de/trees/#~6x~6y%28f%28x%29=y~5Px~1Qy%29~5R~1~3R
Domain: | { 0 }
-- | --
f: | { }
P: | { 0 }
Q: | { 0 }
R: | false
It seems to me that the counter model is not a first oder model.
What is an empty function f = {} ? Looks rather like a partial function
to me. On the other hand the same system can prove the following,
saying f is total:
∀x∃yf(x)=y is valid.
https://www.umsu.de/trees/#~6x~7yf%28x%29=y
∀x∀y(f(x)=y → (Px ∧ Qy)) → (R∧¬R) is invalid.
https://www.umsu.de/trees/#~6x~6y%28f%28x%29=y~5Px~1Qy%29~5R~1~3R
Domain: | { 0 }
-- | --
f: | { }
P: | { 0 }
Q: | { 0 }
R: | false
It seems to me that the counter model is not a first oder model.
What is an empty function f = {} ? Looks rather like a partial function
to me. On the other hand the same system can prove the following,
saying f is total:
∀x∃yf(x)=y is valid.
https://www.umsu.de/trees/#~6x~7yf%28x%29=y
Dan Christensen
Dec 9, 2021, 11:13:17 PM12/9/21
to
On Thursday, December 9, 2021 at 6:53:41 PM UTC-5, Mostowski Collapse wrote:
> Its very easy to prove that (x,y) e f is false outside of the domain.
I thinks it's called Burse's Paradox. You really must find some way around it, Jan Burse. Somehow, you must go from a set of ordered pairs to an actual function which is undefined outside of its domain set. Here is how it is done in DC Proof: For functions of one variable, we have an axiom (from the Sets menu):
> Its very easy to prove that (x,y) e f is false outside of the domain.
1 ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
=> [ALL(a1):ALL(b):[(a1,b) in f => a1 in dom & b in cod]
& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
=> [(a1,b1) in f & (a1,b2) in f => b1=b2]]
=> ALL(a1):ALL(b):[a1 in dom & b in cod => [f(a1)=b <=> (a1,b) in f]]]]
Function
You would use this axiom to construct, i.e. prove the existence of a particular function. You start with the sets f, dom and cod, prove they have certain properties expected of a function. Then you will be able to prove:
ALL(x):[x in dom => f(x) in cod]
Sorry, but you will NOT be able to prove f(x)=/=y for any x not in dom. You will not be able to infer anything about f(x) if x is not in the domain of f, because, well, it's undefined there. Just like in almost every math textbook on the planet.
If you just want to introduce an arbitrary function, you can skip all the above and simply state from the start:
ALL(x):[x in dom => f(x) in cod]
As above, you will not be able to make any inference about f(x) if x is not in the domain of f.
I hope this helps you deal with your paradox, Jan Burse.
Mostowski Collapse
Dec 10, 2021, 9:23:10 AM12/10/21
to
You can call it whatever you want. You can also
snip of my posts whatever you want.
But I wrote:
> Its very easy to prove that (x,y) e f is false outside of the domain.
> But you cannot prove that f(x)=y is false outside of the domain.
Try adding these axioms:
1) ∃x¬Px
P is not the universal class.
2) ∀x∀y(f(x)=y → (Px ∧ Qy))
f is a binary relation
You can derive an inconsistency. You should be also able to dervie
an inconistency in DC Proof. Should I do it for you?
BTW: Meanwhile Wolfgang Schwartz fixed his model finder,
it doesn't show the f={} anomaly anymore.
https://github.com/wo/tpg/issues/8
snip of my posts whatever you want.
But I wrote:
> Its very easy to prove that (x,y) e f is false outside of the domain.
Try adding these axioms:
1) ∃x¬Px
P is not the universal class.
2) ∀x∀y(f(x)=y → (Px ∧ Qy))
f is a binary relation
You can derive an inconsistency. You should be also able to dervie
an inconistency in DC Proof. Should I do it for you?
BTW: Meanwhile Wolfgang Schwartz fixed his model finder,
it doesn't show the f={} anomaly anymore.
https://github.com/wo/tpg/issues/8
Mostowski Collapse
Dec 10, 2021, 9:29:43 AM12/10/21
to
Proving inconsistency means deriving false from 1) and 2).
You can derive false from 1) and 2):
(∃x¬Px ∧ ∀x∀y(f(x)=y → (Px ∧ Qy))) → (R∧¬R) is valid.
https://www.umsu.de/trees/#~7x~3Px~1~6x~6y%28f%28x%29=y~5Px~1Qy%29~5R~1~3R
But since in classical logic ~A and A -> f are the same,
we can also prove the following:
¬(∃x¬Px ∧ ∀x∀y(f(x)=y → (Px ∧ Qy))) is valid.
https://www.umsu.de/trees/#~3%28~7x~3Px~1~6x~6y%28f%28x%29=y~5Px~1Qy%29%29
Its only 9 proof lines. How many lines will it be in DC Proof?
You can derive false from 1) and 2):
(∃x¬Px ∧ ∀x∀y(f(x)=y → (Px ∧ Qy))) → (R∧¬R) is valid.
https://www.umsu.de/trees/#~7x~3Px~1~6x~6y%28f%28x%29=y~5Px~1Qy%29~5R~1~3R
we can also prove the following:
¬(∃x¬Px ∧ ∀x∀y(f(x)=y → (Px ∧ Qy))) is valid.
https://www.umsu.de/trees/#~3%28~7x~3Px~1~6x~6y%28f%28x%29=y~5Px~1Qy%29%29
Its only 9 proof lines. How many lines will it be in DC Proof?
Mostowski Collapse
Dec 10, 2021, 10:37:35 AM12/10/21
to
Thats a nice strenghening:
∀x(Px → ∃y(Qy ∧ f(x)=y)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
https://www.umsu.de/trees/#~6x%28Px~5~7y%28Qy~1f%28x%29=y%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29
LoL
∀x(Px → ∃y(Qy ∧ f(x)=y)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
https://www.umsu.de/trees/#~6x%28Px~5~7y%28Qy~1f%28x%29=y%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29
LoL
Dan Christensen
Dec 10, 2021, 10:50:16 AM12/10/21
to
See my reply just now to you identical posting at sci.math.
Dan
Dan
Mostowski Collapse
Dec 10, 2021, 1:08:47 PM12/10/21
to
Dan-O-Matik halucinated:
> "f(x)" makes no sense if you have not specified a domain for x.
I have specified a domain, it is P. What is wrong with you?
The strenghening of the inconsistency is:
> ∀x(Px → ∃y(Qy ∧ f(x)=y)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
https://www.umsu.de/trees/#~6x%28Px~5~7y%28Qy~1f%28x%29=y%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29
∀x(Px → ∃y(Qy ∧ f(x)=y)) is "serial", Dan-O-Matiks favorite
∀x∀y(f(x)=y → (Px ∧ Qy)) is "binary relation",
∀xPx is universal class
For "serial" and "binary relation" see wiki:
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
> "f(x)" makes no sense if you have not specified a domain for x.
I have specified a domain, it is P. What is wrong with you?
The strenghening of the inconsistency is:
> ∀x(Px → ∃y(Qy ∧ f(x)=y)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
https://www.umsu.de/trees/#~6x%28Px~5~7y%28Qy~1f%28x%29=y%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29
∀x∀y(f(x)=y → (Px ∧ Qy)) is "binary relation",
∀xPx is universal class
For "serial" and "binary relation" see wiki:
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
Mostowski Collapse
Dec 10, 2021, 1:11:04 PM12/10/21
to
Works also like this, simplifying ∀x(Px → ∃y(Qy ∧ f(x)=y))
into ∀x(Px → Qf(x)), same inconsistency:
∀x(Px → Qf(x)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
https://www.umsu.de/trees/#~6x%28Px~5Qf%28x%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29
into ∀x(Px → Qf(x)), same inconsistency:
∀x(Px → Qf(x)) → (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx) is valid.
https://www.umsu.de/trees/#~6x%28Px~5Qf%28x%29%29~5%28~6x~6y%28f%28x%29=y~5Px~1Qy%29~4~6xPx%29
Mostowski Collapse
Dec 10, 2021, 1:15:33 PM12/10/21
to
Or in words (Dan-O-Matik function = serial function):
A Dan-O-Matik function is a binary relation iff the domain is the universal class
A Dan-O-Matik function is a binary relation iff the domain is the universal class
Dan Christensen
Dec 10, 2021, 5:50:01 PM12/10/21
to
See my reply just now to your identical posting at sci.math
Mostowski Collapse
Dec 10, 2021, 6:30:46 PM12/10/21
to
I nowhere wrote inconsistency "in DC Proof" in this thread.
Whats wrong with you? What I wrote is this:
> Try adding these axioms:
>
> 1) ∃x¬Px
> P is not the universal class.
>
> 2) ∀x∀y(f(x)=y → (Px ∧ Qy))
> f is a binary relation
>
> You can derive an inconsistency.
The tree tool can do it:
∃x¬Px, ∀x∀y(f(x)=y → (Px ∧ Qy)) entails R∧¬R.
https://www.umsu.de/trees/#~7x~3Px,~6x~6y%28f%28x%29=y~5Px~1Qy%29|=R~1~3R
Whats wrong with you? What I wrote is this:
> Try adding these axioms:
>
> 1) ∃x¬Px
> P is not the universal class.
>
> 2) ∀x∀y(f(x)=y → (Px ∧ Qy))
> f is a binary relation
>
> You can derive an inconsistency.
∃x¬Px, ∀x∀y(f(x)=y → (Px ∧ Qy)) entails R∧¬R.
https://www.umsu.de/trees/#~7x~3Px,~6x~6y%28f%28x%29=y~5Px~1Qy%29|=R~1~3R
Mostowski Collapse
Dec 10, 2021, 6:41:08 PM12/10/21
to
But you can also add an axiom, as you often do,
in your blog post proof:
(*) ∀x(Px → Qf(x))
And then derive from it:
(**) (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx)
I called it also "inconsisteny", because its a similar
idea. But the statement us now:
A Dan-O-Matik function is a binary relation iff the domain is the universal class.
in your blog post proof:
(*) ∀x(Px → Qf(x))
And then derive from it:
(**) (∀x∀y(f(x)=y → (Px ∧ Qy)) ↔ ∀xPx)
I called it also "inconsisteny", because its a similar
idea. But the statement us now:
A Dan-O-Matik function is a binary relation iff the domain is the universal class.
Mostowski Collapse
Dec 10, 2021, 6:57:50 PM12/10/21
to
This probably explains why many HOL systems are also
type systems. A HOL system allows quantifying second order
objects, such as functions. So like in DC Proof, in a HOL system
one can do ALL(f) or EXIST(f). One explanation why one has
type systems, is then to avoid paradoxes of self application.
But another explanation could also be that the
functions subject to ALL(f) or EXIST(f) are a little inflexible,
if they are borrowd from FOL, i.e. if the HOL is extension of
FOL, then these function symbols are f : V -> V, and one
cannot coerce them to smaller domains and codomains,
as the inconsistency shows. On the other hand a HOL system
with product types would have types such as function space A -> B.
type systems. A HOL system allows quantifying second order
objects, such as functions. So like in DC Proof, in a HOL system
one can do ALL(f) or EXIST(f). One explanation why one has
type systems, is then to avoid paradoxes of self application.
But another explanation could also be that the
functions subject to ALL(f) or EXIST(f) are a little inflexible,
if they are borrowd from FOL, i.e. if the HOL is extension of
FOL, then these function symbols are f : V -> V, and one
cannot coerce them to smaller domains and codomains,
as the inconsistency shows. On the other hand a HOL system
with product types would have types such as function space A -> B.
Julio Di Egidio
Dec 10, 2021, 7:38:56 PM12/10/21
to
On Monday, 6 December 2021 at 05:13:09 UTC+1, Dan Christensen wrote:
> This is actually a point of controversy to some here. A related question might be,
> given an array of 10 Boolean variables, what is the truth value of the 11th one? It
> seems to me that in both cases, the truth value is undefined. Your comments?
Not per chance "domain" of a function is short for "domain of definition"...
HTH,
Julio
> This is actually a point of controversy to some here. A related question might be,
> given an array of 10 Boolean variables, what is the truth value of the 11th one? It
> seems to me that in both cases, the truth value is undefined. Your comments?
Not per chance "domain" of a function is short for "domain of definition"...
HTH,
Julio
Dan Christensen
Dec 11, 2021, 12:50:47 AM12/11/21
to
See my reply just now to your identical posting at sci.math
Dan
Mostowski Collapse
Dec 11, 2021, 2:55:45 AM12/11/21
to
Its not a prof that says anything about the notion "binary relation",
which is the subject matter of this thread. You know the thread
asks the following:
"What is the truth value of f(x)=y if x is outside the domain of the function f?"
Where do you prove something about f ⊆ x x y ? You proof doesn't
end with a formula that contains f ⊆ x x y. But we can prove the
following. From:
(*) ALL(a):[a in x => f(a) in y]
We can derive f ⊆ x x y iff x=V:
(**) ALL(a):ALL(b):[f(a)=b => a in x & b in y] <=> ALL(a):[a in x]]
Good luck with finding a set such that ALL(a):[a in x], If you
combine the above with your proof of impossiblity of the
universal set, you can prove:
(***) ~ALL(a):ALL(b):[f(a)=b => a in x & b in y]
P.S.: Here is a mechanized proof of (*) -> (**), I am using E__ for _ in _:
∀a(Eax → Ef(a)y) entails ∀a∀b(f(a)=b → (Eax ∧ Eby)) ↔ ∀aEax.
https://www.umsu.de/trees/#~6a%28Eax~5Ef%28a%29y%29|=%28~6a~6b%28f%28a%29=b~5Eax~1Eby%29~4~6aEax%29
Dan Christensen halucinated:
>> 13 ALL(a):[a in x => EXIST(b):[b in y & b=f(a) & ALL(c):[c in y => [c=f(a) => c=b]]]]
> Conclusion, 2
which is the subject matter of this thread. You know the thread
asks the following:
"What is the truth value of f(x)=y if x is outside the domain of the function f?"
Where do you prove something about f ⊆ x x y ? You proof doesn't
end with a formula that contains f ⊆ x x y. But we can prove the
following. From:
(*) ALL(a):[a in x => f(a) in y]
We can derive f ⊆ x x y iff x=V:
(**) ALL(a):ALL(b):[f(a)=b => a in x & b in y] <=> ALL(a):[a in x]]
Good luck with finding a set such that ALL(a):[a in x], If you
combine the above with your proof of impossiblity of the
universal set, you can prove:
(***) ~ALL(a):ALL(b):[f(a)=b => a in x & b in y]
P.S.: Here is a mechanized proof of (*) -> (**), I am using E__ for _ in _:
∀a(Eax → Ef(a)y) entails ∀a∀b(f(a)=b → (Eax ∧ Eby)) ↔ ∀aEax.
https://www.umsu.de/trees/#~6a%28Eax~5Ef%28a%29y%29|=%28~6a~6b%28f%28a%29=b~5Eax~1Eby%29~4~6aEax%29
Dan Christensen halucinated:
>> 13 ALL(a):[a in x => EXIST(b):[b in y & b=f(a) & ALL(c):[c in y => [c=f(a) => c=b]]]]
> Conclusion, 2
Mostowski Collapse
Dec 11, 2021, 6:12:23 PM12/11/21
to
I don't say that your approach is totally wrong. At least
the classical notion f : A -> B also obeys ∀x(x e A -> f(x) e B).
But the classical notion implies more, for example you can
prove with the classical notion where A={0,...,n-1} and B={0,1} that:
/* Provable */
|{ f | f : A -> B }| = 2^n
But you cannot prove:
/* Not Provable */
|{ f | ∀x(x e A -> f(x) e B) }| = 2^n
So if you would ask a mathematics teacher, whether
∀x(x e A -> f(x) e B) is the right translation of f : A -> B,
he would say no.
You would not pass an exam with this translation. Its
the same with Russels "the X is Y", wrong is wrong.
Twice wrong doesn't give right.
the classical notion f : A -> B also obeys ∀x(x e A -> f(x) e B).
But the classical notion implies more, for example you can
prove with the classical notion where A={0,...,n-1} and B={0,1} that:
/* Provable */
|{ f | f : A -> B }| = 2^n
But you cannot prove:
/* Not Provable */
|{ f | ∀x(x e A -> f(x) e B) }| = 2^n
So if you would ask a mathematics teacher, whether
∀x(x e A -> f(x) e B) is the right translation of f : A -> B,
he would say no.
You would not pass an exam with this translation. Its
the same with Russels "the X is Y", wrong is wrong.
Twice wrong doesn't give right.
Dan Christensen
Dec 11, 2021, 10:28:43 PM12/11/21
to
See my reply just now to your identical posting at sci.math
Dan
Dan
Mostowski Collapse
Dec 12, 2021, 4:14:47 AM12/12/21
to
Your Dan-O-Matik nonsense would be correct if Terrence Taos
would have somewhere a phrase an "arbitrary property P(x, y)".
But he expressis verbis says "P(x, y) be a property pertaining to
an object x ∈ X and an object y ∈ Y". Your Dan-O-Matik nonsense
does not get right in anyway. Two times wrong doesn't give right.
would have somewhere a phrase an "arbitrary property P(x, y)".
But he expressis verbis says "P(x, y) be a property pertaining to
an object x ∈ X and an object y ∈ Y". Your Dan-O-Matik nonsense
does not get right in anyway. Two times wrong doesn't give right.
Mostowski Collapse
Dec 12, 2021, 11:45:25 AM12/12/21
to
Hey Dan-O-Matik you have zero stamina. If you ask how high the
Mount Everest is, and nobody tells you, well then you have to climbe
the Mount Everest. Dont be a lazy ass. I didn't make up the question
myself, it comes from your own mouth. You even posted it on MSE:
asked Dec 6 at 3:00 Dan Christensen
> EDIT: A possibly related question: For an indexed array of 10
Boolean variables, what is the truth value of the 11th one?
https://math.stackexchange.com/q/4325129/1002973
I ask the same, I dont ask "what is", I ask how many.
So how many arrays of length 10 with values 0 and 1 are
there? Question is still, whether your ALL(a):[a e x => f(a) e y]
suffices for the cardinality task or not. What is your answer now?
Mount Everest is, and nobody tells you, well then you have to climbe
the Mount Everest. Dont be a lazy ass. I didn't make up the question
myself, it comes from your own mouth. You even posted it on MSE:
asked Dec 6 at 3:00 Dan Christensen
> EDIT: A possibly related question: For an indexed array of 10
Boolean variables, what is the truth value of the 11th one?
https://math.stackexchange.com/q/4325129/1002973
I ask the same, I dont ask "what is", I ask how many.
So how many arrays of length 10 with values 0 and 1 are
there? Question is still, whether your ALL(a):[a e x => f(a) e y]
suffices for the cardinality task or not. What is your answer now?
Mostowski Collapse
Dec 12, 2021, 2:59:19 PM12/12/21
to
The zero or one object test works if you use undefined ⊥.
So instead of only modelling f : A -> B as follows:
ALL(x):[x in A => f(x) in B]
We would model it as follows:
ALL(x):[x in A => f(x) in B] & ALL(x):[~x in A => f(x)=⊥]
Now the zero or one object test works, we can prove f ⊆ g,
by a similar proof we can also prove g ⊆ f, and hence f = g:
/* Encoding z=0, u=⊥ */
∀a(a=z → f(a)=z), ∀a(¬a=z → f(a)=u),
∀a(a=z → g(a)=z), ∀a(¬a=z → g(a)=u)
entails ∀a∀b(f(a)=b → g(a)=b).
https://www.umsu.de/trees/#~6a%28a=z~5f%28a%29=z%29,~6a%28~3a=z~5f%28a%29=u%29,~6a%28a=z~5g%28a%29=z%29,~6a%28~3a=z~5g%28a%29=u%29|=~6a~6b%28f%28a%29=b~5g%28a%29=b%29
Now its "entails" and not anymore "does not entail".
So instead of only modelling f : A -> B as follows:
ALL(x):[x in A => f(x) in B]
ALL(x):[x in A => f(x) in B] & ALL(x):[~x in A => f(x)=⊥]
Now the zero or one object test works, we can prove f ⊆ g,
by a similar proof we can also prove g ⊆ f, and hence f = g:
/* Encoding z=0, u=⊥ */
∀a(a=z → f(a)=z), ∀a(¬a=z → f(a)=u),
∀a(a=z → g(a)=z), ∀a(¬a=z → g(a)=u)
entails ∀a∀b(f(a)=b → g(a)=b).
https://www.umsu.de/trees/#~6a%28a=z~5f%28a%29=z%29,~6a%28~3a=z~5f%28a%29=u%29,~6a%28a=z~5g%28a%29=z%29,~6a%28~3a=z~5g%28a%29=u%29|=~6a~6b%28f%28a%29=b~5g%28a%29=b%29
Now its "entails" and not anymore "does not entail".
Mostowski Collapse
Dec 12, 2021, 3:00:15 PM12/12/21
to
Dan-O-Matik you had the chance to climb the Mount Everest first.
I even was waiting and waiting, and asking myself, will he move
his lazy ass, or continue calling me bad names. Now I did it, because
you didn't move any of your braincells out of your comfort zone.
I even was waiting and waiting, and asking myself, will he move
his lazy ass, or continue calling me bad names. Now I did it, because
you didn't move any of your braincells out of your comfort zone.
Mostowski Collapse
Dec 13, 2021, 8:08:00 AM12/13/21
to
You even dont get Terence Tao right. I don't remember him
using the symbol f twice? Overloading is all play and fun,
until you introduce quantifiers. Take this example from algebra:
ALL(-):EXIST(-):[x - y = x + (-y)]
What should this even mean?
- For every subtraction there is a minus. (false)
- For every minus there is a substraction. (true)
- What else?
Your conclusion is not accepted based on well formed
formula by the criteria of first order logic as implemented
by the Wolfgang Schwartz tree tool:
∀a∀b(Eax ∧ Eby → (f(a)=b ↔ Ep(a,b)f))
https://www.umsu.de/trees/#~6a~6b%28Eax~1Eby~5%28f%28a%29=b~4Ep%28a,b%29f%29%29
Don't use 'f' as both 1-ary function symbol and individual constant.
(I'm assuming 'Ep(a,b)f' is meant to be an atomic formula with predicate 'E'.)
In as far if you would then produce a proof ALL(a):ALL(b):[a inx
& b in y => [b=f(a) <=> P(a,b)]] based on your illformed formula,
this wouldn't consist a proof in FOL.
Twice wrong doesn't give right.
Dan Christensen schrieb am Sonntag, 12. Dezember 2021 um 16:30:23 UTC+1:
> We have 3 preconditions here for the functionality of f:
> 21 ALL(a1):ALL(b):[(a1,b) in f => a1 in x & b in y]
> & ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in f]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
> Detach, 18, 20
using the symbol f twice? Overloading is all play and fun,
until you introduce quantifiers. Take this example from algebra:
ALL(-):EXIST(-):[x - y = x + (-y)]
What should this even mean?
- For every subtraction there is a minus. (false)
- For every minus there is a substraction. (true)
- What else?
Your conclusion is not accepted based on well formed
formula by the criteria of first order logic as implemented
by the Wolfgang Schwartz tree tool:
∀a∀b(Eax ∧ Eby → (f(a)=b ↔ Ep(a,b)f))
https://www.umsu.de/trees/#~6a~6b%28Eax~1Eby~5%28f%28a%29=b~4Ep%28a,b%29f%29%29
Don't use 'f' as both 1-ary function symbol and individual constant.
(I'm assuming 'Ep(a,b)f' is meant to be an atomic formula with predicate 'E'.)
In as far if you would then produce a proof ALL(a):ALL(b):[a inx
& b in y => [b=f(a) <=> P(a,b)]] based on your illformed formula,
this wouldn't consist a proof in FOL.
Twice wrong doesn't give right.
> We have 3 preconditions here for the functionality of f:
> 21 ALL(a1):ALL(b):[(a1,b) in f => a1 in x & b in y]
> & ALL(a1):[a1 in x => EXIST(b):[b in y & (a1,b) in f]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in x & b1 in y & b2 in y
> => [(a1,b1) in f & (a1,b2) in f => b1=b2]]
> => ALL(a1):ALL(b):[a1 in x & b in y => [f(a1)=b <=> (a1,b) in f]]
> Detach, 18, 20
0 new messages