[FOM] What is a proof?

[John T. Baldwin]

Stephen G Simpson wrote:

>
>Concerning Angus Macintyre's recent paper in the BSL:
>  
>
Baldwin wrote

> > I, for instance, found the recent BSL piece by Angus largely
> > off-base.  It proposes an interesting new project and solely for
> > propaganda purposes labels it as model theory.
>  
>
Stephen G Simpson wrote:

This is news to me. When I read the paper, I didn't see any specific

>proposal for a new project, other than a devaluation of set theory,
>and some interesting applications of model theory to algebra, of the
>kind we have already seen.
>
Baldwin writes:  I don't have the paper at hand but Macintyre called for 
a model theory that is adequate to
understand sheaf theoretic methods in algebraic geometry.  He seems to 
feel that this would involve
abandoning the notions of models as sets and such fundamental model 
theoretic notions as Tarski's truth definition.

If he finds away to find logical foundations for contemporary algebraic 
geometry as good as contemporary model theory
gives foundations for 50's model theory, more power to him.  If he 
abandons the notion of model to do so, let him give
at another name.

By as good as: e.g.

Weil's algebraic geometry as expounded in e,.g. Lang's little `Algebraic 
Geometry' gives an almost mystical account of the
notion of  `a generic point of a variety V over an algebraically closed 
field k'. A clear concrete explication is: a generic point of
V is an element of an elementary extension of k which satisfies every 
equation over k satisfied by all elements of V and no more.


> By the way, you never replied to my
>earlier query (FOM, 9 Jul 2003):
>
>  Does anyone know of an alternative way to set up model theory using
>  some approach other than the familiar one, which is overtly
>  set-theoretical?
>
I didn't reply because I don't know any.

>
>  
>