You could prove this one:

Dan(clown) |- ALL(quack):[Dan(quack) => quack=clown]

if Dan were a Russell Definite Description. But just
assuming a Dedekind Infinite Function and Set is not
a Russell Definite Description of some sort.

But thats anyway not my point, when I ask for an
alternative to your assumption of a Dedekind Infinite
Function and Set. Do you even read what I write?

I am asking for an existence proof of a Peano Structure
that doesn't start with a Dedekind Infinite Function and
Set. Since this is to close to a Peano Structure already,

doesn't make much sense such a proof. Also for
a Peano Structure <N,S,0> you need to be able
to show that we have:

Set(S)

Namely an element from the function space:

S : N -> N

Where do you show Set(S), the the successor function
is set-like. You nowhere show that?

Mostowski Collapse schrieb am Montag, 27. Februar 2023 um 20:55:18 UTC+1:
> Do you mean whether I understand this inference:
>
> /* See Proof below */
> Dan(clown) |- EXIST(quack):Dan(quack)
>
> Yes, why do you ask? Here is a proof in DC Poop:
>
> BTW: You can also proof:
>
> /* Provable */
> Dan(clown) |- EXIST(quack):[Dan(clown) & quack=clown]
>
> Of course you cannot prove:
>
> /* Not Provable */
> Dan(clown) |- ALL(quack):[Dan(quack) => quack=clown]
>
> ---------- begin proof ------
>
> 1 Dan(clown)
> Axiom
>
> 2 EXIST(quack):Dan(quack)
> E Gen, 1
>
> ---------- begin proof ------
> > Do pay attention, Mr. Collapse! On line 109, f is a FREE variable (a function)
> introduced in the axiom on line 2. s is the corresponding BOUND variable
> introduced by existential generalization on line 110 . Do you understand
> the difference? Didn't think so. Oh, well...

On Monday, February 27, 2023 at 3:01:33 PM UTC-5, Mostowski Collapse wrote:
> You could prove this one:
> Dan(clown) |- ALL(quack):[Dan(quack) => quack=clown]

Makes no sense, Mr. Collapse. Try again.
> if Dan were a Russell Definite Description. But just
> assuming a Dedekind Infinite Function and Set is not
> a Russell Definite Description of some sort.
>

Likewise.

> But thats anyway not my point, when I ask for an
> alternative to your assumption of a Dedekind Infinite
> Function and Set. Do you even read what I write?
>
> I am asking for an existence proof of a Peano Structure
> that doesn't start with a Dedekind Infinite Function and
> Set.

What's wrong with starting by postulating the existence of an infinite set? That is essentially how the natural numbers are constructed in ZFC theory.

Since this is to close to a Peano Structure already,
>
> doesn't make much sense such a proof. Also for
> a Peano Structure <N,S,0> you need to be able
> to show that we have:
>
> Set(S)
>
> Namely an element from the function space:
>
> S : N -> N
>
No function space here. Just function f: x --> x restricted to subset n of x.

108. x0 in n

& ALL(a):[a in n => f(a) in n] <----------------------------------- f: n --> n

& ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
& ALL(a):[a in n => ~f(a)=x0]
& ALL(p):[Set(p) & ALL(c):[c in p => c in n]
=> [x0 in p & ALL(c):[c in p => f(c) in p] => ALL(a):[a in n => a in p]]]

Join, 107, 104

[...]

Generalizing...

111. EXIST(n):EXIST(s):EXIST(0):[0 in n

& ALL(a):[a in n => s(a) in n] <------------------------------------- s: n --> n

& ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
& ALL(a):[a in n => ~s(a)=0]
& ALL(p):[Set(p) & ALL(c):[c in p => c in n]
=> [0 in p & ALL(c):[c in p => s(c) in p] => ALL(a):[a in n => a in p]]]]

E Gen, 110

> Where do you show Set(S), the the successor function
> is set-like.

Not necessary here. We started by assuming f: x --> x, then restricted f to a subset n of x, then generalized to get s: n --> n.

Dan

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

I am not interested in glorifying your prove which
is based on the assumption of a Dedekind Infinite
Set and Function and doesn't prove a Peano Structure.

To prove existence of a Peano Structure, you need to
prove existence of a Triple <N,S,0> and guess what each
member of the Triple is a Set or an element of Set:

0 e N
S e N -> N
Set(N)
Set(S)

If you have N and s not yet a set. But some function
symbol, its relatively easy to get a set-like function in
ZFC. Just use the axiom schema of replacement and

construct this set:

S = { (x,y) | x e N & s(x)=y }
https://en.wikipedia.org/wiki/Axiom_schema_of_replacement

In DC Poop we would not write Set(S), but rather Set'(S),
since it has a separate predicate for Sets that are Sets of
Pairs. But I do not find a proof of Set'(S) so far.

So there is no proof of a Peano Structure P = <N,S,0> yet.
And I don't know whether its possible in DC Poop to
also show Set''(P) ? Since it is a triple?

Dan Christensen schrieb am Montag, 27. Februar 2023 um 21:58:53 UTC+1:
> On Monday, February 27, 2023 at 3:01:33 PM UTC-5, Mostowski Collapse wrote:
> > You could prove this one:
> > Dan(clown) |- ALL(quack):[Dan(quack) => quack=clown]
> Makes no sense, Mr. Collapse. Try again.
> > if Dan were a Russell Definite Description. But just
> > assuming a Dedekind Infinite Function and Set is not
> > a Russell Definite Description of some sort.
> >
> Likewise.
> > But thats anyway not my point, when I ask for an
> > alternative to your assumption of a Dedekind Infinite
> > Function and Set. Do you even read what I write?
> >
> > I am asking for an existence proof of a Peano Structure
> > that doesn't start with a Dedekind Infinite Function and
> > Set.
> What's wrong with starting by postulating the existence of an infinite set? That is essentially how the natural numbers are constructed in ZFC theory.
> Since this is to close to a Peano Structure already,
> >
> > doesn't make much sense such a proof. Also for
> > a Peano Structure <N,S,0> you need to be able
> > to show that we have:
> >
> > Set(S)
> >
> > Namely an element from the function space:
> >
> > S : N -> N
> >
> No function space here. Just function f: x --> x restricted to subset n of x.
>
> 108. x0 in n
>
> & ALL(a):[a in n => f(a) in n] <----------------------------------- f: n --> n
>
> & ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
> & ALL(a):[a in n => ~f(a)=x0]
> & ALL(p):[Set(p) & ALL(c):[c in p => c in n]
> => [x0 in p & ALL(c):[c in p => f(c) in p] => ALL(a):[a in n => a in p]]]
>
> Join, 107, 104
>
> [...]
>
> Generalizing...
>
> 111. EXIST(n):EXIST(s):EXIST(0):[0 in n
>
> & ALL(a):[a in n => s(a) in n] <------------------------------------- s: n --> n
>
> & ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> & ALL(a):[a in n => ~s(a)=0]
> & ALL(p):[Set(p) & ALL(c):[c in p => c in n]
> => [0 in p & ALL(c):[c in p => s(c) in p] => ALL(a):[a in n => a in p]]]]
>
> E Gen, 110
> > Where do you show Set(S), the the successor function
> > is set-like.
> Not necessary here. We started by assuming f: x --> x, then restricted f to a subset n of x, then generalized to get s: n --> n.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Well Set''(P) wouldn't work. Rather Set''(Q) where
Q is the set of all structures <N,S,0> with:

Set(N)
Set'(S)
0 e N
S e N -> N

And then a Peano structure P would have P e Q. You
can check yourself what a structure is:

https://en.wikipedia.org/wiki/Structure_(mathematical_logic)

In universal algebra and in model theory, a structure
consists of a set D along with a collection of finitary
operations and relations that are defined on it.

Whereby finitary doesn't mean finite, it means with
finite arity. And each operation and relation is from
the function or relation space over the set D

from the structure:

f e D^n -> D for an n-ary operations
r ⊆ D^n for an n-ary relation

Such a set based structure, where each finitary
operation and relation is again set-like, can be shown
to be a set itself if the set theory has some ordered

pairs. So for example ZFC can talk about them. You
can then prove theorems about set-like structures
in ZFC itself. Sometimes structures are not set-like,

when for example the domain D is a class. This is also
possible to work with class based structures, and to
obtain class based results. Whereby Levy in his book

Basic Set Theory was a little bit paranoid about forming
the pair <V,V> where V is the universal class. He tried
to avoid that, but I don't remember exactly what can go wrong?

Mostowski Collapse schrieb am Montag, 27. Februar 2023 um 22:38:05 UTC+1:
> I am not interested in glorifying your prove which
> is based on the assumption of a Dedekind Infinite
> Set and Function and doesn't prove a Peano Structure.
>
> To prove existence of a Peano Structure, you need to
> prove existence of a Triple <N,S,0> and guess what each
> member of the Triple is a Set or an element of Set:
>
> 0 e N
> S e N -> N
> Set(N)
> Set(S)
>
> If you have N and s not yet a set. But some function
> symbol, its relatively easy to get a set-like function in
> ZFC. Just use the axiom schema of replacement and
>
> construct this set:
>
> S = { (x,y) | x e N & s(x)=y }
> https://en.wikipedia.org/wiki/Axiom_schema_of_replacement
>
> In DC Poop we would not write Set(S), but rather Set'(S),
> since it has a separate predicate for Sets that are Sets of
> Pairs. But I do not find a proof of Set'(S) so far.
>
> So there is no proof of a Peano Structure P = <N,S,0> yet.
> And I don't know whether its possible in DC Poop to
> also show Set''(P) ? Since it is a triple?
> Dan Christensen schrieb am Montag, 27. Februar 2023 um 21:58:53 UTC+1:
> > On Monday, February 27, 2023 at 3:01:33 PM UTC-5, Mostowski Collapse wrote:
> > > You could prove this one:
> > > Dan(clown) |- ALL(quack):[Dan(quack) => quack=clown]
> > Makes no sense, Mr. Collapse. Try again.
> > > if Dan were a Russell Definite Description. But just
> > > assuming a Dedekind Infinite Function and Set is not
> > > a Russell Definite Description of some sort.
> > >
> > Likewise.
> > > But thats anyway not my point, when I ask for an
> > > alternative to your assumption of a Dedekind Infinite
> > > Function and Set. Do you even read what I write?
> > >
> > > I am asking for an existence proof of a Peano Structure
> > > that doesn't start with a Dedekind Infinite Function and
> > > Set.
> > What's wrong with starting by postulating the existence of an infinite set? That is essentially how the natural numbers are constructed in ZFC theory.
> > Since this is to close to a Peano Structure already,
> > >
> > > doesn't make much sense such a proof. Also for
> > > a Peano Structure <N,S,0> you need to be able
> > > to show that we have:
> > >
> > > Set(S)
> > >
> > > Namely an element from the function space:
> > >
> > > S : N -> N
> > >
> > No function space here. Just function f: x --> x restricted to subset n of x.
> >
> > 108. x0 in n
> >
> > & ALL(a):[a in n => f(a) in n] <----------------------------------- f: n --> n
> >
> > & ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
> > & ALL(a):[a in n => ~f(a)=x0]
> > & ALL(p):[Set(p) & ALL(c):[c in p => c in n]
> > => [x0 in p & ALL(c):[c in p => f(c) in p] => ALL(a):[a in n => a in p]]]
> >
> > Join, 107, 104
> >
> > [...]
> >
> > Generalizing...
> >
> > 111. EXIST(n):EXIST(s):EXIST(0):[0 in n
> >
> > & ALL(a):[a in n => s(a) in n] <------------------------------------- s: n --> n
> >
> > & ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > & ALL(a):[a in n => ~s(a)=0]
> > & ALL(p):[Set(p) & ALL(c):[c in p => c in n]
> > => [0 in p & ALL(c):[c in p => s(c) in p] => ALL(a):[a in n => a in p]]]]
> >
> > E Gen, 110
> > > Where do you show Set(S), the the successor function
> > > is set-like.
> > Not necessary here. We started by assuming f: x --> x, then restricted f to a subset n of x, then generalized to get s: n --> n.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Monday, February 27, 2023 at 4:38:05 PM UTC-5, Mostowski Collapse wrote:
> I am not interested in glorifying your prove which
> is based on the assumption of a Dedekind Infinite
> Set and Function and doesn't prove a Peano Structure.
>
> To prove existence of a Peano Structure, you need to
> prove existence of a Triple <N,S,0> and guess what each
> member of the Triple is a Set or an element of Set:
>

You don't actually have to prove the existence of a Peano Structure. You could legitimately use Peano's Axioms as an axiom of infinity. (My preference) The Axioms are sufficiently self-evident. Informally, we have:

1. 0 is a natural number
2. Every natural number has a unique successor that is also a natural number.
3. Different natural numbers have different successors.
4. 0 is not the success of any natural number.
5. Every natural number but 0 itself, can be be reached by a process repeated successor starting at 0.

Which of these do you believe is NOT self-evident, Mr. Collapse?

But if you insist on proving its existence, you will have to assume the existence of some other structure, as is done in ZFC theory with its own Axiom of Infinity. Are you familiar with it, Mr. Collapse? Ask you little buddy, AP, about his theory of infinity. (Sooooooo cute!!)

Dan

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

Can you formalize a quantifier ꟻxP(x):

Almost all:

ꟻxP(x) :<=> { x | ~P(x) } is finite

We can say inside a Peano structure this one must hold:

~ꟻx⏊

Yes or No?

Dan Christensen schrieb am Montag, 27. Februar 2023 um 23:37:16 UTC+1:
> On Monday, February 27, 2023 at 4:38:05 PM UTC-5, Mostowski Collapse wrote:
> > I am not interested in glorifying your prove which
> > is based on the assumption of a Dedekind Infinite
> > Set and Function and doesn't prove a Peano Structure.
> >
> > To prove existence of a Peano Structure, you need to
> > prove existence of a Triple <N,S,0> and guess what each
> > member of the Triple is a Set or an element of Set:
> >
> You don't actually have to prove the existence of a Peano Structure. You could legitimately use Peano's Axioms as an axiom of infinity. (My preference) The Axioms are sufficiently self-evident. Informally, we have:
>
> 1. 0 is a natural number
> 2. Every natural number has a unique successor that is also a natural number.
> 3. Different natural numbers have different successors.
> 4. 0 is not the success of any natural number.
> 5. Every natural number but 0 itself, can be be reached by a process repeated successor starting at 0.
>
> Which of these do you believe is NOT self-evident, Mr. Collapse?
>
> But if you insist on proving its existence, you will have to assume the existence of some other structure, as is done in ZFC theory with its own Axiom of Infinity. Are you familiar with it, Mr. Collapse? Ask you little buddy, AP, about his theory of infinity. (Sooooooo cute!!)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Is this the famous Kreisel Quantifier?
http://www.piergiorgioodifreddi.it/wp-content/uploads/2022/01/kreiseliana.pdf
If you have greater than or equal, its relatively easy:

ꟻxP(x) :<=> ∃z∀y(y ≥ z => P(y))

But it will not allow you to tell appart N+ and R+.
Same with your Dedekind Infinite set and function, it
could be also f : R+ -> R+ and f(x) = x + 1. Don't you

have some better axiomatics that shows existence
of a Peano Structure from the bottom up, and not top
down by reducing a Dedekind Infinite set and function?

Mostowski Collapse schrieb am Dienstag, 28. Februar 2023 um 23:53:57 UTC+1:
> Can you formalize a quantifier ꟻxP(x):
>
> Almost all:
>
> ꟻxP(x) :<=> { x | ~P(x) } is finite
>
> We can say inside a Peano structure this one must hold:
>
> ~ꟻx⏊
>
> Yes or No?
> Dan Christensen schrieb am Montag, 27. Februar 2023 um 23:37:16 UTC+1:
> > On Monday, February 27, 2023 at 4:38:05 PM UTC-5, Mostowski Collapse wrote:
> > > I am not interested in glorifying your prove which
> > > is based on the assumption of a Dedekind Infinite
> > > Set and Function and doesn't prove a Peano Structure.
> > >
> > > To prove existence of a Peano Structure, you need to
> > > prove existence of a Triple <N,S,0> and guess what each
> > > member of the Triple is a Set or an element of Set:
> > >
> > You don't actually have to prove the existence of a Peano Structure. You could legitimately use Peano's Axioms as an axiom of infinity. (My preference) The Axioms are sufficiently self-evident. Informally, we have:
> >
> > 1. 0 is a natural number
> > 2. Every natural number has a unique successor that is also a natural number.
> > 3. Different natural numbers have different successors.
> > 4. 0 is not the success of any natural number.
> > 5. Every natural number but 0 itself, can be be reached by a process repeated successor starting at 0.
> >
> > Which of these do you believe is NOT self-evident, Mr. Collapse?
> >
> > But if you insist on proving its existence, you will have to assume the existence of some other structure, as is done in ZFC theory with its own Axiom of Infinity. Are you familiar with it, Mr. Collapse? Ask you little buddy, AP, about his theory of infinity. (Sooooooo cute!!)
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Spelunkies such as John Gabriel and Dan Christensen are
a real gold mine. While they were begging for food under
a bridge without an internet connection,

they came up of an idea of a narrow mathematics:

1) John Gabriel: He wants to base mathematics
on credos such as real numbers are not numbers.
Unfortunately all his KISS and revolutionizing mathematics
attempts have failed so far.
https://thenewcalculus.weebly.com/

2) Dan Christensen: He prefers to blindfold himself,
unless he gets a wakeup call from Terrence Tao. Usually
he annoys mathematicians by inventing barbers that
don't live on islands etc.. Typicall nonsense:
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

I guess its rather STDGeneralizedDriners, something
like sexually transmitted desease Drinker Paradox. So
what was the results of their approach to "narrow mathematics",

well they became a bunch of crying apes with internet connection.

Dan Christensen schrieb am Donnerstag, 9. Februar 2023 um 04:31:09 UTC+1:
> See my reply just now to your identical posting at sci.logic
>
> Dan
> On Wednesday, February 8, 2023 at 5:29:13 PM UTC-5, Mostowski Collapse wrote:
> > How do your formulas even give any information
> > that the table is single valued and not multi-valued.
> > For example where is it stated that not both:
> >
> > ~A => [A=>B]
> >
> > and
> >
> > ~A => ~[A=>B]
> >
> > hold. Where do you prove that only one of the two holds?
> > BTW: Its not unexpectedly that both could hold.
> [snip]

They are a gold mine, because they can make you happy,
since you didn't waste your lifetime on some narrow ideas
of mathematics, and they can also strengthen some

viewpoints, that show some breadth and wide range, some
viewpoints you might have not ascended that consciously,
and you only had presumed because you didn't start with

a narrow mathematics premis. Also interesting to see
and find new sources how Logicians dealt with these
problems. I guess you can never plough enough books

about second order logic? Why? Well real analysis can
be viewed as second order arithmetic:

"Because real numbers can be represented as (infinite)
sets of natural numbers in well-known ways, and because
second-order arithmetic allows quantification over such sets,
it is possible to formalize the real numbers in second-order arithmetic."
https://en.wikipedia.org/wiki/Second-order_arithmetic

Mild Shock schrieb am Donnerstag, 8. Juni 2023 um 11:55:43 UTC+2:
> Spelunkies such as John Gabriel and Dan Christensen are
> a real gold mine. While they were begging for food under
> a bridge without an internet connection,
>
> they came up of an idea of a narrow mathematics:
>
> 1) John Gabriel: He wants to base mathematics
> on credos such as real numbers are not numbers.
> Unfortunately all his KISS and revolutionizing mathematics
> attempts have failed so far.
> https://thenewcalculus.weebly.com/
>
> 2) Dan Christensen: He prefers to blindfold himself,
> unless he gets a wakeup call from Terrence Tao. Usually
> he annoys mathematicians by inventing barbers that
> don't live on islands etc.. Typicall nonsense:
> http://www.dcproof.com/STGeneralizedDrinkersThm.htm
>
> I guess its rather STDGeneralizedDriners, something
> like sexually transmitted desease Drinker Paradox. So
> what was the results of their approach to "narrow mathematics",
>
> well they became a bunch of crying apes with internet connection.
> Dan Christensen schrieb am Donnerstag, 9. Februar 2023 um 04:31:09 UTC+1:
> > See my reply just now to your identical posting at sci.logic
> >
> > Dan
> > On Wednesday, February 8, 2023 at 5:29:13 PM UTC-5, Mostowski Collapse wrote:
> > > How do your formulas even give any information
> > > that the table is single valued and not multi-valued.
> > > For example where is it stated that not both:
> > >
> > > ~A => [A=>B]
> > >
> > > and
> > >
> > > ~A => ~[A=>B]
> > >
> > > hold. Where do you prove that only one of the two holds?
> > > BTW: Its not unexpectedly that both could hold.
> > [snip]

Ok, maybe for full real analysis functions over sets can
be helpful. Wikipedia has a section about Coding Mathematics.
Interestingly there are still publications in this area, like:

On the logical and computational properties of the Vitali covering theorem
DAG NORMANN AND SAM SANDERS - last revised 5 Apr 2022
https://arxiv.org/abs/1902.02756

Didn't read. Not sure whether will have time. Only picked
it up, to see whether the field is still alive.

Mild Shock schrieb am Donnerstag, 8. Juni 2023 um 11:57:00 UTC+2:
> They are a gold mine, because they can make you happy,
> since you didn't waste your lifetime on some narrow ideas
> of mathematics, and they can also strengthen some
>
> viewpoints, that show some breadth and wide range, some
> viewpoints you might have not ascended that consciously,
> and you only had presumed because you didn't start with
>
> a narrow mathematics premis. Also interesting to see
> and find new sources how Logicians dealt with these
> problems. I guess you can never plough enough books
>
> about second order logic? Why? Well real analysis can
> be viewed as second order arithmetic:
>
> "Because real numbers can be represented as (infinite)
> sets of natural numbers in well-known ways, and because
> second-order arithmetic allows quantification over such sets,
> it is possible to formalize the real numbers in second-order arithmetic."
> https://en.wikipedia.org/wiki/Second-order_arithmetic
> Mild Shock schrieb am Donnerstag, 8. Juni 2023 um 11:55:43 UTC+2:
> > Spelunkies such as John Gabriel and Dan Christensen are
> > a real gold mine. While they were begging for food under
> > a bridge without an internet connection,
> >
> > they came up of an idea of a narrow mathematics:
> >
> > 1) John Gabriel: He wants to base mathematics
> > on credos such as real numbers are not numbers.
> > Unfortunately all his KISS and revolutionizing mathematics
> > attempts have failed so far.
> > https://thenewcalculus.weebly.com/
> >
> > 2) Dan Christensen: He prefers to blindfold himself,
> > unless he gets a wakeup call from Terrence Tao. Usually
> > he annoys mathematicians by inventing barbers that
> > don't live on islands etc.. Typicall nonsense:
> > http://www.dcproof.com/STGeneralizedDrinkersThm.htm
> >
> > I guess its rather STDGeneralizedDriners, something
> > like sexually transmitted desease Drinker Paradox. So
> > what was the results of their approach to "narrow mathematics",
> >
> > well they became a bunch of crying apes with internet connection.
> > Dan Christensen schrieb am Donnerstag, 9. Februar 2023 um 04:31:09 UTC+1:
> > > See my reply just now to your identical posting at sci.logic
> > >
> > > Dan
> > > On Wednesday, February 8, 2023 at 5:29:13 PM UTC-5, Mostowski Collapse wrote:
> > > > How do your formulas even give any information
> > > > that the table is single valued and not multi-valued.
> > > > For example where is it stated that not both:
> > > >
> > > > ~A => [A=>B]
> > > >
> > > > and
> > > >
> > > > ~A => ~[A=>B]
> > > >
> > > > hold. Where do you prove that only one of the two holds?
> > > > BTW: Its not unexpectedly that both could hold.
> > > [snip]