I also think it is hopeless , but I still want to try again
*----- Original Message -----
*From: Frank Atanassow <[EMAIL PROTECTED]>
*To: Jan Brosius <[EMAIL PROTECTED]>
*Cc: Frank Atanassow <[EMAIL PROTECTED]>; <[EMAIL PROTECTED]>
*Sent: Friday, May 19, 2000 12:59 PM
*Subject: Re: more detailed explanation about forall in Haskell
*Jan Brosius writes:
* > > > I must put this in the good way;
* > > >
* > > > [forall x . alpha(x)] => alpha(x) is True
* > >
* > > Yes, by instantiation.
* >
* > I disagree.
*You disagree with my agreeing with you?
About what do you agree with me?
* > > > If alpha(x) is TRUE then the following is true : alpha(x) => [forall x.
* > > > alpha(x)]
* > >
* > > No, alpha(x) only asserts that some element named x satisfies alpha. It
* > does
* > > not follow that therefore every other element also satisfies alpha.
*>
* > No the variable x means that it can be substituted by any term. That is the
* > real meaning of a variable
* > (at least in classical logic).
*Only when the variable is bound by a forall. It is exactly the same situation
*as with lambda-calculus and lambda. The term "x" denotes a fixed element of
*its type. When I bind it, as in "\x -> x", I'm saying that that x may range
*over any element in the type. Once I've said that, yes, I can substitute any
*element for x in the body.
* (\x -> P(x)) t = P(x) [t/x]
* > Consider e.g. Carl Witty's formula : prime(x) == x is a prime number.
* > Then prime(2) == (2|x) prime(x) is true , and prime (4) is false
* >
* > Take something else alpha(x) == prime(x) AND ¬ prime(x) ( ¬ signifies
* > not)
* >
*> then alpha(x) is a false formula and you have ¬ [exists x. alpha(x)]
*>
* > On the contrary beta(x) == ¬ alpha(x) is true for any x
*Yes, because x is bound in the body of beta.
I have seen what you mean by bound.
Clearly you are talking about something else than quantified logic
* beta := \x -> not(alpha(x))
You are talking about lambda calculus where I am talking about quantified logic
*BTW, I don't understand your "(2|x)" notation. Is this a substitution?
Yes
* > > > So if alpha(x) is TRUE then [forall x. alpha(x) ]<=> alpha(x)
* > >
* > > This does not follow. It is truth-equivalent to:
* >
* > Sorry, I disagree
*Well, you certainly have the right to disagree. But you are disagreeing with
*every logician since Gentzen.
I disagree with you Frank , the rest is your imagination.
* > > [forall x. alpha(x)] <=> True
* >
* > ( In the above you should at the very least not forget to mention that
* > [forall x. alpha(x)] must be true )
*Isn't that what I wrote?
Of course not , what you wrote down is FALSE stated like that. Don't you see that?
* > > I repeat: you do not understand the difference between bound and free
* > variables.
* >
* > I disagree a free variable is not a constant.
*> > A free variable behaves like a constant.
* >
* > No a constant is always the same constant, it is never substituted by
* > something else, it is "immutable".
* >
* > A variable is a placeholder for a Term ( a constant is a special term)
*I see where you are heading. In the reduction laws, you substitute for free
*variables. This is true, but you can only substitute for a free variable if it
*was bound in an outer scope, and you are stripping off the binding, as in the
*beta-equality for lambda-calculus, which I will repeat:
I am not talking about reduction laws
* (\x -> P(x)) t = P(x) [t/x]
*You cannot simply substitute any value you please for an arbitrary free
*variable and expect the new term to be equal to the old one. For example in
*Haskell, fst :: (a,b) -> a is a free variable in every term (where it's not
*shadowed). Now if I have the term
* fst p
*and I substitute snd for fst:
* (fst p) [snd/fst] = snd p
*but
* fst p /= snd p
*which demonstrates that substitution on free variables is not sound in
*general.
No you still don't understand me
* This is the reason for abstraction: it asserts that a free variable
*in the scope of the abstraction can range over the whole domain, so any
*substitution will preserve equality. It is exactly the same with forall.
* > >It is not "implicitly"
* > > quantified in any way, because it denotes a specific element. The only
* > > difference between a constant and a free variable is syntactic: a free
*> > variable can be bound in an outer scope,
* >
* > No the real role of a variable say x in a formula alpha(x) or a term T(x)
* > is a PLACEHOLDER ready to be substituted by a Term (e.g. constant or a
* > parameterized term)
* >
* > And that's the reason why I should find it weird if In Haskell 98+ one
* > would distinguish between
* >
* > a -> a and [forall a. a -> a]
* >
* > >while a constant cannot.
* > >
* > > > > The sentence "alpha(x)" asserts that there is a _distinguished_
* > element
* > > > > named
* > > >
* > > > NO , saying that there is a distinguished element T that satisfies
* > alpha
* > > > implies
* > > >
* > > > that exists x. alpha(x) is true
* > >
* > > Yes, it also implies this fact, because it can be derived by
* > extensionality:
* > >
*> > alpha(x) => exists y. alpha(y)
* > >
* > > However, existential quantification hides the identity of the element in
* > > question. The fact that we know _which_ element it is that satisifies
* > alpha
* > > permits us to say more. This is why:
* > >
* > > exists x. alpha(x),
* > > alpha(x),
* > >
* > > and
* > >
* > > forall x. alpha(x)
* > >
* > > are not truth-equivalent. Rather we have:
* > >
* > > forall y. alpha(y) => alpha(x) and alpha (x) => exists z. alpha(z)
* >
* > AND if alpha(x) is a TRUE formula then alpha(x) => forall x. alpha(x)
*No. It is meaningless to say that alpha(x) is TRUE unless you give a
*truth-value for x. It seems to me that you want alpha(x) to mean, "any value
*of x satisfies alpha". But that is simply not what it means in all extant
*presentations of logic. For that meaning, we use the term
*"forall x. alpha(x)".
look at this example:
alpha(x) == x is_an Integer => x^2 > -1
this is an example of a formula that is true
*If you want to come up with your own logic, where alpha(x) is equivalent to
*forall x. alpha(x), then that's fine.
No, if alpha(x) is a true formula then forall x. alpha(x) is again a true assertion
*I don't think you will manage it, but
*perhaps it is possible. However, that is _not_ the logic that we use in the
*Curry-Howard isomoporphism. Also, it is not the logic devised by Gentzen or
*Tarski and you will not find it, I assure you, in any modern text describing
*logic. (I have not read Bourbaki, so I can't comment on it, although I imagine
*you are misreading it if you find any assertion to the contrary.)
This is irrelevant
* > A better way to express this is
* >
* > Rule of genaralization:
* >
* > alpha(x ) is True (and x is a variable)
* > ********************
* > forall x . alpha(x ) is true
*This rule assumes that there are no constraints on x. You cannot _by
*definition_ (!!) give a denotation to a term unless you also give a denotation
*to all its variables. Therefore, to give a denotation to alpha(x) you must
*give a denotation x. If you give a denotation for x, it is constrained, and
*this rule becomes unsound.
* > I repeat that my use of true or false is not really the way it is expressed
* > in Bourbaki , I used it
* > in order to be understood by everybody (and in this discussion it doesn'
* > hurt).
* >
* > >
* > > > > "x" in the domain of your model, and that that element, at least,
* > > > satisfies
* > > >
* > > > x is a variable ; no domain ; no model
* > >
* > > A model must assign an element in the domain to each free variable. You
* > need a
* > > model to determine the truth-value of a first-order proposition which is
* > not
* > > tautological. We are trying to establish the truth-value of a proposition
* > with
* > > a free variable; therefore we need a model. A model needs a domain of
* > elements
* > > to draw from. Therefore we need a domain. OK?
* >
*This is absurd. You are trying to turn a simple discussion on free variables
*into a forum for your ideas of mathematical foundations.
What you say is irrelevant
*Fine. If you don't want to give a model for your logic, then I invite you to
*prove its consistency. Then publish it all, and we'll all see if it holds
*up. What I have tried to show you is completely standard, and you can find it
*in any beginner's book on formal logic. It has already been shown sound
*w.r.t. to Tarskian and other set-theoretic models. If you claim it is
*inconsistent, then you will need to show that set theory is inconsistent. Good
*luck.
This is really irrelevant
> The forall's used with domains, say e.g. N is the set of integers are in
> fact bounded forall's and
> one has e.g.
>
> forall x in N . prime(x) == forall x. x in N => prime(x)
>
> the left forall above is an example of a bounded forall where x must range
> over a constant set , here N.
*You have jumped from the meta-level to the object-level. We were discussing a
*term logic with simple parametric quantification.
I think I am discussing quantified logic and I think you don't
The rest what you say is irrelevant
*This is irrelevant. You can
*try to incorporate increasingly large parts of your metatheory into the object
*theory, but it will never become a closed system.
*--
*Frank Atanassow, Dept. of Computer Science, Utrecht University
*Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
*Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Friendly
Jan Brosius
