What makes you think (A > (~A > B)) should be
derivable for a counterfactual conditional?

Dan Christensen schrieb am Mittwoch, 1. Februar 2023 um 04:28:36 UTC+1:
> See my reply just now to your identical posting at sci.logic
>
> Dan
> On Tuesday, January 31, 2023 at 7:56:58 PM UTC-5, Mostowski Collapse wrote:
> > And could you solve the riddle why counterfactual conditional
> > differs from material implication? Not only they are different
> > names, they also refer to different inference rules.
> >
> [snip]

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

Dan

On Wednesday, February 1, 2023 at 5:20:04 AM UTC-5, Mostowski Collapse wrote:
> What makes you think (A > (~A > B)) should be
> derivable for a counterfactual conditional?

Still clueless what counterfactuals conditionals are?

Lets say you tell your girlfriend:
If we take the tube to piccadilly we can go to a chines restaurant.

Then your girlfriend responds:
No, at piccadilly we could go to a cinema.

Poor Dan-O-Matik will not understand his girlfriend.

LoL

Dan Christensen schrieb am Mittwoch, 1. Februar 2023 um 15:24:30 UTC+1:
> See my reply just now to your identical posting at sci.logic
>
> Dan
> On Wednesday, February 1, 2023 at 5:20:04 AM UTC-5, Mostowski Collapse wrote:
> > What makes you think (A > (~A > B)) should be
> > derivable for a counterfactual conditional?

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

Dan

On Wednesday, February 1, 2023 at 12:25:08 PM UTC-5, Mostowski Collapse wrote:
> Still clueless what counterfactuals conditionals are?
>
> Lets say you tell your girlfriend:
> If we take the tube to piccadilly we can go to a chines restaurant.
>
> Then your girlfriend responds:
> No, at piccadilly we could go to a cinema.
>
[snip]

How would you formalize:

"piccadilly circus is not actually a circus"

Just joking. LoL

Dan Christensen schrieb am Mittwoch, 1. Februar 2023 um 22:52:33 UTC+1:
> See my reply just now to your identical posting at sci.logic.
>
> Dan
> On Wednesday, February 1, 2023 at 12:25:08 PM UTC-5, Mostowski Collapse wrote:
> > Still clueless what counterfactuals conditionals are?
> >
> > Lets say you tell your girlfriend:
> > If we take the tube to piccadilly we can go to a chines restaurant.
> >
> > Then your girlfriend responds:
> > No, at piccadilly we could go to a cinema.
> >
> [snip]

After a longwinding train of thought Dan-O-Matik
evacuated via his keyboard to the ethernal noone
sphere of the internet:

Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 01:43:21 UTC+1:
> "Counterfactual conditionals are used to speculate
or opine about what MIGHT have been."
https://groups.google.com/g/sci.logic/c/K18874J-4JE/m/WATxzs1RJwAJ

Not only, this here is terminological knowledge:

"piccadilly circus is not actually a circus"

Not some speculation.

And this here is also not a speculation, but a communicated
intention. Forming of a joint plan. Its not about speculating
whether Hilbert hotels exists. LoL:

> > > > Lets say you tell your girlfriend:
> > > > If we take the tube to piccadilly we can go to a chines restaurant.
> > > > Then your girlfriend responds:
> > > > No, at piccadilly we could go to a cinema.

You confuse speculation with intention. What do
you want to speculate about, whether the chines
restaurant or the cinema exists? Whether the

tube works and some can walk the ramaining
distance? You are hilarious Dan-O-Matik. Also I
guess you confuse the goals of logic. Like you

postulate that logic serves "insight" on the objects
the logic talk about. You can do this also informally.
Many people see logic as a way to get "insight" on

the meta level, how language works.
Thats why Carnap wrote this:

Meaning and Necessity: A Study in Semantics and Modal Logic
https://en.wikipedia.org/wiki/Meaning_and_Necessity

I guess it is not about elicidating some set theory
theorems with the help of logic, rather applying some
concepts to better understand semantics of modal logic,

which has other use cases than only mathematics.

Sorry

Mostowski Collapse schrieb am Donnerstag, 2. Februar 2023 um 01:03:52 UTC+1:
> How would you formalize:
>
> "piccadilly circus is not actually a circus"
>
> Just joking. LoL
> Dan Christensen schrieb am Mittwoch, 1. Februar 2023 um 22:52:33 UTC+1:
> > See my reply just now to your identical posting at sci.logic.
> >
> > Dan
> > On Wednesday, February 1, 2023 at 12:25:08 PM UTC-5, Mostowski Collapse wrote:
> > > Still clueless what counterfactuals conditionals are?
> > >
> > > Lets say you tell your girlfriend:
> > > If we take the tube to piccadilly we can go to a chines restaurant.
> > >
> > > Then your girlfriend responds:
> > > No, at piccadilly we could go to a cinema.
> > >
> > [snip]

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

Dan

On Thursday, February 2, 2023 at 4:38:31 AM UTC-5, Mostowski Collapse wrote:
> After a longwinding train of thought Dan-O-Matik
> evacuated via his keyboard to the ethernal noone
> sphere of the internet:
>
> Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 01:43:21 UTC+1:
> > "Counterfactual conditionals are used to speculate
> or opine about what MIGHT have been."

[snip]

Thats why its not called "counter fact", but "counterfactual":

factual: adjective
- actually occurring.
"cases mentioned are factual"

Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 18:17:32 UTC+1:
> See my reply just now to your identical posting at sci.logic.
>
> Dan
> On Thursday, February 2, 2023 at 4:38:31 AM UTC-5, Mostowski Collapse wrote:
> > After a longwinding train of thought Dan-O-Matik
> > evacuated via his keyboard to the ethernal noone
> > sphere of the internet:
> >
> > Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 01:43:21 UTC+1:
> > > "Counterfactual conditionals are used to speculate
> > or opine about what MIGHT have been."
> [snip]

French:

Synonyme : réel, attesté, observable
Contraire : imaginaire, inobservable

Do you deny that this is imaginaire at the moment it is uttered:

> > > > Then your girlfriend responds:
> > > > No, at piccadilly we could go to a cinema.

The only problem is that material implication can also
deal with the imaginaire. For example take Dan O
Matiks definition of Odd() [See evenodd thread]:

ALL(a):[Odd(a) <=> ~Even(a)]

We can then deduce:

ALL(a):[Unicorn(a) => Odd(a) | Even(a)]

Quite imaginary theorem. Or do you claim its vacously true?
If it were vacuously true, you would be able to prove
this here, but you cannot prove this here:

~EXIST(a):Unicorn(a)

LoL

Mostowski Collapse schrieb am Donnerstag, 2. Februar 2023 um 19:42:30 UTC+1:
> Thats why its not called "counter fact", but "counterfactual":
>
> factual: adjective
> - actually occurring.
> "cases mentioned are factual"
> Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 18:17:32 UTC+1:
> > See my reply just now to your identical posting at sci.logic.
> >
> > Dan
> > On Thursday, February 2, 2023 at 4:38:31 AM UTC-5, Mostowski Collapse wrote:
> > > After a longwinding train of thought Dan-O-Matik
> > > evacuated via his keyboard to the ethernal noone
> > > sphere of the internet:
> > >
> > > Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 01:43:21 UTC+1:
> > > > "Counterfactual conditionals are used to speculate
> > > or opine about what MIGHT have been."
> > [snip]

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

Dan

On Thursday, February 2, 2023 at 1:42:30 PM UTC-5, Mostowski Collapse wrote:
> Thats why its not called "counter fact", but "counterfactual":
>
> factual: adjective
> - actually occurring.
> "cases mentioned are factual"
> Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 18:17:32 UTC+1:
> > See my reply just now to your identical posting at sci.logic.
> >
> > Dan
> > On Thursday, February 2, 2023 at 4:38:31 AM UTC-5, Mostowski Collapse wrote:
> > > After a longwinding train of thought Dan-O-Matik
> > > evacuated via his keyboard to the ethernal noone
> > > sphere of the internet:
> > >
> > > Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 01:43:21 UTC+1:
> > > > "Counterfactual conditionals are used to speculate
> > > or opine about what MIGHT have been."
> > [snip]

There is no difference in real/imaginary between material
implication and couterfactual conditional, they can both
do hypothetical reasoning. You don't believe me, right?

Here some hypothetical reasoning about Unicorns with
material implication only. I am using your "arithmetic
axiom" that your praised so much in the past:

1 ALL(a):[Odd(a) <=> ~Even(a)]
Axiom
https://dcproof.com/EvenNextOdd.htm

Now we can prove, doesn't look real to me:

23 ALL(a):[Unicorn(a) => Odd(a) | Even(a)]
Rem DNeg, 22

-------------------------------------- begin proof ------------------------------------

1 ALL(a):[Odd(a) <=> ~Even(a)]
Axiom

2 ~ALL(a):[Unicorn(a) => Odd(a) | Even(a)]
Premise

3 ~~EXIST(a):~[Unicorn(a) => Odd(a) | Even(a)]
Quant, 2

4 EXIST(a):~[Unicorn(a) => Odd(a) | Even(a)]
Rem DNeg, 3

5 ~[Unicorn(u) => Odd(u) | Even(u)]
E Spec, 4

6 ~[~Unicorn(u) | [Odd(u) | Even(u)]]
Imply-Or, 5

7 ~~[~~Unicorn(u) & ~[Odd(u) | Even(u)]]
DeMorgan, 6

8 ~~[Unicorn(u) & ~[Odd(u) | Even(u)]]
Rem DNeg, 7

9 Unicorn(u) & ~[Odd(u) | Even(u)]
Rem DNeg, 8

10 Unicorn(u)
Split, 9

11 ~[Odd(u) | Even(u)]
Split, 9

12 ~~[~Odd(u) & ~Even(u)]
DeMorgan, 11

13 ~Odd(u) & ~Even(u)
Rem DNeg, 12

14 ~Odd(u)
Split, 13

15 ~Even(u)
Split, 13

16 Odd(u) <=> ~Even(u)
U Spec, 1

17 [Odd(u) => ~Even(u)] & [~Even(u) => Odd(u)]
Iff-And, 16

18 Odd(u) => ~Even(u)
Split, 17

19 ~Even(u) => Odd(u)
Split, 17

20 Odd(u)
Detach, 19, 15

21 ~Odd(u) & Odd(u)
Join, 14, 20

22 ~~ALL(a):[Unicorn(a) => Odd(a) | Even(a)]
Conclusion, 2

23 ALL(a):[Unicorn(a) => Odd(a) | Even(a)]
Rem DNeg, 22

-------------------------------------- end proof ------------------------------------

Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 20:58:49 UTC+1:
> See my reply just now to your identical posting at sci.logic
> Dan
> On Thursday, February 2, 2023 at 1:42:30 PM UTC-5, Mostowski Collapse wrote:
> > Thats why its not called "counter fact", but "counterfactual":
> >
> > factual: adjective
> > - actually occurring.
> > "cases mentioned are factual"
> > Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 18:17:32 UTC+1:
> > > See my reply just now to your identical posting at sci.logic.
> > >
> > > Dan
> > > On Thursday, February 2, 2023 at 4:38:31 AM UTC-5, Mostowski Collapse wrote:
> > > > After a longwinding train of thought Dan-O-Matik
> > > > evacuated via his keyboard to the ethernal noone
> > > > sphere of the internet:
> > > >
> > > > Dan Christensen schrieb am Donnerstag, 2. Februar 2023 um 01:43:21 UTC+1:
> > > > > "Counterfactual conditionals are used to speculate
> > > > or opine about what MIGHT have been."
> > > [snip]

See my reply just now to you identical posting at sci.logic

Dan

On Thursday, February 2, 2023 at 4:53:15 PM UTC-5, Mostowski Collapse wrote:
> There is no difference in real/imaginary between material
> implication and couterfactual conditional, they can both
> do hypothetical reasoning.
[snip]

It looks your DC Proof material implication is also
a counterfactual conditional. Why can I prove this
alternate theory:

23 ALL(a):[Unicorn(a) => Odd(a) | Even(a)]
Rem DNeg, 22

That is counterfactual, there are no Unicorns around.
Or do you see some Unicorn? What is an Odd Unicorn,
a Unicorn with an odd number of legs? What

about the horn of the Unicorn, do we count the legs
and the horn, or only the legs. Also DC Proof
is not able to prove this:

~EXIST(a):Unicorn(a)

So we can only conclude, according to the guidelines
of Dan Christensen, that the material implication
of DC Proof is also a couterfactual conditional?

LMAO!

Dan Christensen schrieb am Freitag, 3. Februar 2023 um 02:14:54 UTC+1:
> See my reply just now to you identical posting at sci.logic
>
> Dan
> On Thursday, February 2, 2023 at 4:53:15 PM UTC-5, Mostowski Collapse wrote:
> > There is no difference in real/imaginary between material
> > implication and couterfactual conditional, they can both
> > do hypothetical reasoning.
> [snip]

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

Dan

On Friday, February 3, 2023 at 6:35:51 AM UTC-5, Mostowski Collapse wrote:
> It looks your DC Proof material implication is also
> a counterfactual conditional. Why can I prove this
> alternate theory:
> 23 ALL(a):[Unicorn(a) => Odd(a) | Even(a)]
> Rem DNeg, 22
> That is counterfactual, there are no Unicorns around.
> Or do you see some Unicorn? What is an Odd Unicorn,
> a Unicorn with an odd number of legs? What
>
[snip]

Dan Christensen wrote:
> Where is your "counterfactual???"

I ddn't say there is a couterfactual in my example. Where
did you see me saying there is a counterfactual.
I literally wrote:

> There is no difference in real/imaginary between material
> implication and couterfactual conditional, they can both
> do hypothetical reasoning. You don't believe me, right?

And I produced some hypothetical reasoning with
material implication. In as far material implication
and couterfactual conditional are the same,

they both make an assumption.

Dan Christensen schrieb am Freitag, 3. Februar 2023 um 16:49:14 UTC+1:
> See my reply just now to your identical posting at sci.logic
>
> Dan
> On Friday, February 3, 2023 at 6:35:51 AM UTC-5, Mostowski Collapse wrote:
> > It looks your DC Proof material implication is also
> > a counterfactual conditional. Why can I prove this
> > alternate theory:
> > 23 ALL(a):[Unicorn(a) => Odd(a) | Even(a)]
> > Rem DNeg, 22
> > That is counterfactual, there are no Unicorns around.
> > Or do you see some Unicorn? What is an Odd Unicorn,
> > a Unicorn with an odd number of legs? What
> >
> [snip]

Yes I wrote "It looks your DC Proof material implication
is also a counterfactual conditional." , concerning the
aspect of making an assumption.

You copied it already, but here it is again:

> And I produced some hypothetical reasoning with
> material implication. In as far material implication
> and couterfactual conditional are the same,
>
> they both make an assumption.

You need to read the full post, not only the beginnings.

Ha Ha, you are assuming stable truths in a discourse.

Because natural language uses conterfactuals you
cannot read the meaning of a paragraph without
reading it holistically. So if you have a paragraph

A, B, C it might not say A. Depends what the composition
of A, B, C gives. So basically for non-counterfactual
conditional we find the following useful identity:

/* Material Implication */
(A & B => C) <=> (A => (B => C))

For counterfactual conditional there is also an identity:

/* Counterfactual Conditional */
(A x B => C) <=> (A > (B > C))

Only x is not symmetric. See also here:

"Classical and intuitionistic logics deal with stable truths :
if A and A ⇒ B, then B, but A still holds. This is perfect in mathematics,
but wrong in real life, since real implication is causal."
https://girard.perso.math.cnrs.fr/Synsem.pdf

Mostowski Collapse schrieb am Freitag, 3. Februar 2023 um 17:28:06 UTC+1:
> Yes I wrote "It looks your DC Proof material implication
> is also a counterfactual conditional." , concerning the
> aspect of making an assumption.
>
> You copied it already, but here it is again:
> > And I produced some hypothetical reasoning with
> > material implication. In as far material implication
> > and couterfactual conditional are the same,
> >
> > they both make an assumption.
> You need to read the full post, not only the beginnings.

Whats a rather trivial thing is this sentence removing
DC Proof, and saying material implication is a
counterfactual conditional.

Which is possibly not wrong Taking the Ramsey test,
where counterfactual conditional is realized as:

G x A |- B
----------------------
G |- A > B

Then material implication is a counterfactual conditional
where the believe revision operator G x A is the special
case of doing no revision at all, where it is the stable

truth operator so to speak, picking up a phrasing from
Jean-Yves Girard, so in material implication we have
G x A = G u {A}, with the drawback of a possible inconsistency

when A conflicts with G:

G u {A} |- B
----------------------
G |- A => B

But not withstanding material implication are the same as
counterfactual conditional, and it looks they are also the
same in DC Proof, in that matrial implication can exactly

make the above assumption G u {A}, similarly like
counterfactual conditional performs some assumption
G x A. So they are based on the same assumption mechanism,

more or less. Namely hypothesizing a situation G x A respectively
G u {A} to decide A > B respectively A => B. They are both
based on hypothetical reasoning:

"Aristotle refers briefly to hypothetical reasoning, but develops no
theory of it in any surviving texts. His successor Theophrastus (371–287 BC),
however, is reputed to have developed a theory of hypothetical syllogisms —
in modern terms, a theory of the conditional.

A History of The Connectives
Daniel Bonevac, Josh Dever
Handbook of the History of Logic
Volume 11, 2012, Pages 175-233

Mostowski Collapse schrieb am Freitag, 3. Februar 2023 um 17:34:09 UTC+1:
> Ha Ha, you are assuming stable truths in a discourse.
>
> Because natural language uses conterfactuals you
> cannot read the meaning of a paragraph without
> reading it holistically. So if you have a paragraph
>
> A, B, C it might not say A. Depends what the composition
> of A, B, C gives. So basically for non-counterfactual
> conditional we find the following useful identity:
>
> /* Material Implication */
> (A & B => C) <=> (A => (B => C))
>
> For counterfactual conditional there is also an identity:
>
> /* Counterfactual Conditional */
> (A x B => C) <=> (A > (B > C))
>
> Only x is not symmetric. See also here:
>
> "Classical and intuitionistic logics deal with stable truths :
> if A and A ⇒ B, then B, but A still holds. This is perfect in mathematics,
> but wrong in real life, since real implication is causal."
> https://girard.perso.math.cnrs.fr/Synsem.pdf
> Mostowski Collapse schrieb am Freitag, 3. Februar 2023 um 17:28:06 UTC+1:
> > Yes I wrote "It looks your DC Proof material implication
> > is also a counterfactual conditional." , concerning the
> > aspect of making an assumption.
> >
> > You copied it already, but here it is again:
> > > And I produced some hypothetical reasoning with
> > > material implication. In as far material implication
> > > and couterfactual conditional are the same,
> > >
> > > they both make an assumption.
> > You need to read the full post, not only the beginnings.

Chu Space have a charming counterfactual aspect.
Lets define the Set embedding as follows, where U is
the Herbrand Universe, a little diversion from the slides:

[X] = (X, U \ X)
https://bentnib.org/docs/datatypes-with-negation-20220623.pdf

This somehow explains the below non-monotonic example:

:- dynamic abnormal/1.
fly(X) :- bird(X), \+ abnormal(X).
bird(tweety).
?- fly(tweety).
true.

And then:

abnormal(tweety).
?- fly(tweety).
false.

Have Fun!

Dan Christensen schrieb am Freitag, 3. Februar 2023 um 18:21:16 UTC+1:
> See my reply just now to your identical posting at sci.logic
>
> Dan
> On Friday, February 3, 2023 at 11:34:09 AM UTC-5, Mostowski Collapse wrote:
> > Ha Ha, you are assuming stable truths in a discourse.
> >
> > Because natural language uses conterfactuals you
> > cannot read the meaning of a paragraph without
> > reading it holistically. So if you have a paragraph
> >
> > A, B, C it might not say A. Depends what the composition
> > of A, B, C gives. So basically for non-counterfactual
> > conditional we find the following useful identity:
> >
> [snip]

What can go wrong, when you represent a table
by "if" rules only, from input values to output values.
What about the other direction, making it an "iff"?

Are the output values definite descriptions à la Russel,
if we use "if" rules only. Can we prove something
along this here, where R is the table relationsship:

ALL(x):EXISTUNIQUE(y):R(x, y)

Which would make R a function f. Maybe difficult to
formulate if x and y are propositional variables, since
in ordinary first order logic (FOL), and also in DC Proof,

one cannot quantify over propositional variables.

Mostowski Collapse schrieb am Mittwoch, 8. Februar 2023 um 23:08:50 UTC+1:
> What can go wrong, when you represent a table
> by "if" rules only, from input values to output values.
> What about the other direction, making it an "iff"?

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.
For example I get:

¬(p∨¬p) → ((p∨¬p) → q) is valid.
https://www.umsu.de/trees/#~3(p~2~3p)~5(p~2~3p~5q)

¬(p∨¬p) → ¬((p∨¬p) → q) is valid.
https://www.umsu.de/trees/#~3(p~2~3p)~5~3(p~2~3p~5q)

Now I am also a little perplexed. But I guess the
question is what does a capital variable A even mean?
Can we substitute it for any other formula.

Mostowski Collapse schrieb am Mittwoch, 8. Februar 2023 um 23:12:12 UTC+1:
> Are the output values definite descriptions à la Russel,
> if we use "if" rules only. Can we prove something
> along this here, where R is the table relationsship:
>
> ALL(x):EXISTUNIQUE(y):R(x, y)
>
> Which would make R a function f. Maybe difficult to
> formulate if x and y are propositional variables, since
> in ordinary first order logic (FOL), and also in DC Proof,
>
> one cannot quantify over propositional variables.
> Mostowski Collapse schrieb am Mittwoch, 8. Februar 2023 um 23:08:50 UTC+1:
> > What can go wrong, when you represent a table
> > by "if" rules only, from input values to output values.
> > What about the other direction, making it an "iff"?

Ha Ha, another waterloo for Dan Christensen.
He doesn't get it that here:
https://www.dcproof.com/ConstructPeanoNS0.htm

He can also deduce:
EXIST(s):[ .... & ALL(a):[a e n => f(a) = s(a)]]
So what did he prove? Nothing, f was assumed.

P.S.: The cheating renaming step is here, first its f then its s:

109 EXIST(0):[0 e n & ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=0]
& ALL(p):[Set(p) & ALL(c):[c e p => c e n]
=> [0 e p & ALL(c):[c e p => f(c) e p]
=> ALL(a):[a e n => a e p]]]]
E Gen, 108

110 EXIST(s):EXIST(0):[0 e n & ALL(a):[a e n => s(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
& ALL(a):[a e n => ~s(a)=0]
& ALL(p):[Set(p) & ALL(c):[c e p => c e n]
=> [0 e p & ALL(c):[c e p => s(c) e p]
=> ALL(a):[a e n => a e p]]]]
E Gen, 109

LoL

On Monday, February 27, 2023 at 5:21:07 AM UTC-5, Mostowski Collapse wrote:
> Ha Ha, another waterloo for Dan Christensen.
> He doesn't get it that here:
> https://www.dcproof.com/ConstructPeanoNS0.htm
>
> He can also deduce:
> EXIST(s):[ .... & ALL(a):[a e n => f(a) = s(a)]]
> So what did he prove? Nothing, f was assumed.
>
> P.S.: The cheating renaming step is here, first its f then its s:
>
> 109 EXIST(0):[0 e n & ALL(a):[a e n => f(a) e n]
> & ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
> & ALL(a):[a e n => ~f(a)=0]
> & ALL(p):[Set(p) & ALL(c):[c e p => c e n]
> => [0 e p & ALL(c):[c e p => f(c) e p]
> => ALL(a):[a e n => a e p]]]]
> E Gen, 108
>
> 110 EXIST(s):EXIST(0):[0 e n & ALL(a):[a e n => s(a) e n]
> & ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
> & ALL(a):[a e n => ~s(a)=0]
> & ALL(p):[Set(p) & ALL(c):[c e p => c e n]
> => [0 e p & ALL(c):[c e p => s(c) e p]
> => ALL(a):[a e n => a e p]]]]
> E Gen, 109
>

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...

Dan

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

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...