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?
> > > 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.
beta := \x -> not(alpha(x))
BTW, I don't understand your "(2|x)" notation. Is this a substitution?
> > > 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.
> > [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?
> In principle True is a sloppy expression for saying that [forall x .
> alpha(x)] is a theorem of some mathematical theory. I have used True because
> discussing mathematical theories would have lead the discussion
> out of the scope of the discussion.
>
> For instance let "T=" denote a mathematical theory with equality
>
> then one has "T=" -| x = x
>
> that is the formula x = x is a theorem in "T=" . More sloppy the formula
> x=x is TRUE in "T="
This has no bearing on the discussion.
> > which is equivalent to:
> >
> > forall x. alpha(x)
> >
> > which is only true when every element satisifies alpha; so it is not a
> > tautology.
> >
> > I repeat: you do not understand the difference between bound and free
> variables.
>
> I disagree a free variable is not a constant.
I didn't say it _was_ a constant. I said it behaved like a constant, but that
they are syntactically distinct because you cannot bind a constant.
> A bound variable is a variable tied to a quantifier. In principle a bound
> variable is not visibly.
> This is best illustrated by Bourbaki's approach where they first define :
>
> exists x . alpha(x) == (`t x (alpha)| x) alpha
>
> where if e.g. alpha(x) == x = x then
>
> `t x (alpha) == `t ( `sq = `sq ) where `sq denotes a small square and
> where here both `sq are tied to `t by a line
> In this way I can really say that in [existx x. x = x] the variable x has
> disappeared.
>
> Finally Bourbaki defines forall x . alpha(x) == ¬ [exists x . ¬ alpha(x)]
Sorry, I don't understand your notation, or what relevance this has.
> I repeat : there are no domains in propositional calculus , but I am aware
> that in some text books about
> propositional calculus one speaks about it , I regard this as cheating :
> introducing a concept that one is going to define later. I remember my
> prof, in logic in 1 cand. math - physics where his first lesson began by
> writing
> on the blackboard : p V ¬ p and he only said " p or not p " " tertium
> non datur" " a third possibility is not given "
> His whole course was as formally as possible, and variables were not
> supposed to range about a domain.
I don't understand what relevance this has.
> > 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:
(\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. 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)".
If you want to come up with your own logic, where alpha(x) is equivalent to
forall x. alpha(x), then that's fine. 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.)
> 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?
>
> No, you don't need a model for (formal ) logic . If at this stage
> (propositional calculus) you would
> talk about a domain or set then you are introducing "domain" before you
> have discussed what
> a domain is. If you are using a model than you are implicitly accepting the
> fact that the whole
> of mathematical set theory is at your disposition. Since mathematical set
> theory is based on propositional calculus a variable x in propositional
> calculus is really a variable which is equivalent to saying that it
> can be used for substitution no more,no less.
This is absurd. You are trying to turn a simple discussion on free variables
into a forum for your ideas of mathematical foundations.
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.
> 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. 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.
> However more complicated bounded forall's can be considered.
> In general let alpha(x) be a formula about a variable x then
>
> [forall alpha(x) . prime(x)] == [forall x. alpha(x) => prime(x)]
--
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
