Re: really basic problem with universal quantifier, free variables and generalisation.

DONKEY-BRAIN@xxxxxxxxxxxxx schrieb:
On Jul 12, 9:03 pm, "J. Burse" <janbu...@xxxxxxxxxxx> wrote:
OK but how do you construct a formal argument where x is not
arbrary....
i.e.
x is even -| x+1 is odd
There are also calculi which allow unbound variables
in the premisse and/or conclusion. Here is a reference:

Ebbinghaus, Heinz-Dieter; Flum, Jörg; Thomas, Wolfgang:
Einführung in die mathematische Logik. 4.
Aufl. - Heidelberg 1996.

Is this sort of thing not expressible in FOL?

For this book, Mathematical Logic means in this
case is mostly FOL, maybe some results about
SOL, Horn, etc.. as well.

But you can have FOL with or without unbound
variables in the premisse and/or conclusion.
There are various calculi for FOL. But its
still FOL.

They proof everything with a calculus that allows unbound
variables in this way.

For example the deduction theorem in such a calculus
is much easier, it is simply:

if G,B |- C then G |- B->C

Such a theorem is also known in calculi that are weaker
than classical calculi, and that allow also unbound
variables. See proof as types etc..

is this curry/howard?

Yep, to be precise:

Proof Lambda Expression
G |- C t_C within variables x_G
G\B |- B->C (lambda y_B.t_C)_B->C within variables x_G\y_B

Note in a calculus without unbound variables in the premisse
and conclusion, we have to make the provisio that B has no
unbound variables.

Concerning your question about the introduction of
the unversal quantifier. Your rule is wrong. The rule
is not:

F(x) |- Ax F(x)

You have given a counterexample by yourself. The rule
is as follows:

G |- F(u)
---------- u notin G Ax F(x)
G |- Ax F(x)

"u notin G Ax F(x)" ?

Yes, the side condition on u. It doesn't work when
for example u occurs in G.

u = 0 |- u = 0
--------------
u = 0 |- Ax (x=0)

Not a valid inference.

Thus you have first to proof |- F(u) by some premisses,
then you can conclude by the same premisses |- Ax F(x).

What you gave was not a rule, it would have been an
axiom schema. But you showed by yourself that this axiom is
wrong.

In a gentzen style calculus as above, the only axiom
schema that is needed is the following:

G, A |- A

The rest are rules as depicted above, where you go from
certain proofs, to new proofs.

Best Regards
.