Jan Brosius writes:
> I must put this in the good way;
>
> [forall x . alpha(x)] => alpha(x) is True
Yes, by instantiation.
> 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.
> So if alpha(x) is TRUE then [forall x. alpha(x) ]<=> alpha(x)
This does not follow. It is truth-equivalent to:
[forall x. alpha(x)] <=> True
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. A free variable behaves like a constant. 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, 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)
> > "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?
--
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
