Prev: matching of arcs on pseudosphere with sphere #400 Correcting Math
Next: most likely candidate arc of tractrix and circle that are equal (proofs??) #403 Correcting Math
From: Jan Burse on 7 Feb 2010 14:30
Dear All

I am struggling with terminology. First of all I want to go
fully proof theoretical, so I don't agree when I find
on answer.com:

Beth Theorem
"It therefore connects the proof theory of
such a logic to its model theory."

Is there no connection of proof theory and model theory possible
for those logics that do not allow the "Beth Theorem".

Having said this, the proof theoretical cast I am using is as
follows. Lets say we want to define a predicate x.

An explicit definition is just a formula (often used
as axiom) of the following form:

forall u1 ... un((x u1 ... un) <-> D)

where x does not occur free in D

and the variables of D are among the parameters z1 ... zn

An implicit definition is just a formula (often used as axiom)
of arbitrary form E such that:

The variables of E are among the predicate x
and the parameters z1 ... zn

Uniqueness: Let y be a fresh predicate variable, then
E, E[x/y] |-
forall u1 ... un((x u1 ... un) <-> (y u1 ... un))

Unrestricted Existence:
|- exists x E

In an appropriate logic explicit definitions are automatically
unique and do unrestrictedly exist. So these two properties are
necessary conditions that an implicit definition ensues an
explicit definition. Question is whether they are sufficient.

I did not find so much mention of the unrestricted existence property
for an implicit definition in the literature. Maybe reason is that
it is not needed for the beth property. The beth property says that
from uniqueness it follows that:

Beth Property: If a definition E is unique, then
there exists an explicit definition F such that:
E |- F

So bottom line is that uniqueness is a sufficient condition for
the direction E |- F. What about the other direction F |- E. From
what I have read the Beth theorem is the larger statement that
E |- F and F |- E holds.

Anybody pointers to expositions of the other direction F |- E?
It seems to me that the unrestricted existence condition *together*
with the uniqueness is sufficient for the other direction. But I
have not so much found about it.

Best Regards
From: Jan Burse on 7 Feb 2010 14:32
Jan Burse schrieb:

> Is there no connection of proof theory and model theory possible
> for those logics that do not allow the "Beth Theorem".
Oops, question mark missing.
I actually doubt that the Beth Theorem gives the link.
 | 
Pages: 1
Prev: matching of arcs on pseudosphere with sphere #400 Correcting Math
Next: most likely candidate arc of tractrix and circle that are equal (proofs??) #403 Correcting Math