It seems to me that one could use a Goedel type argument to show
that even intuitionists need to distiguish between provability,
in some fixed system, and something like ‘truth’. Has anybody
ever worked this out in some detail?
Peter
30
Nov
Intuitionism and provability
In article <14…@scott.ed.ac.uk> p…@cogsci.ed.ac.uk (Peter Ruhrberg) writes:
>It seems to me that one could use a Goedel type argument to show
>that even intuitionists need to distiguish between provability,
>in some fixed system, and something like ‘truth’.
Godel’s proof is intuitionistically valid. The concept of proof used
in intuitionistic foundations is not "proof in T" for any formal system
T.
In <14…@scott.ed.ac.uk> p…@cogsci.ed.ac.uk (Peter Ruhrberg) writes:
>It seems to me that one could use a Goedel type argument to show
>that even intuitionists need to distiguish between provability,
>in some fixed system, and something like ‘truth’. Has anybody
>ever worked this out in some detail?
I don’t know who got this discussion starting but intuitionists do distinguish
between truth and provability. The theory of Kripke models can be considered
as defining intuitionistic truth while something like IPC formalizes
provability. (Of course I am talking about `modern’ intuitionism and not
about what Brouwer and Bishop (a constructivist rather than an intuitionist,
btw) wrote in their times.
Now in Kripke models, A or not A is not necessarily true for every A.
But that it not to say that anything else that IS true in a Kripke model
should be provable. So a form of the Goedel results can still hold.
–
Annius V. Groenink — phone (private): +31 30 895261
Mathematics/Computer Science — e-mail (university): avgro…@cs.ruu.nl
University of Utrecht – groen…@math.ruu.nl
Netherland — ZFC Computing
In article <1993Jun21.135123.10…@cs.ruu.nl> avgro…@cs.ruu.nl
(Annius Groenink) writes:
>I don’t know who got this discussion starting but intuitionists do
>distinguish between truth and provability. The theory of Kripke models
>can be considered as defining intuitionistic truth while something
>like IPC formalizes provability.
Kripke semantics is indeed a model-theoretic characterization of
provability in intuitionistic predicate logic, but it is not at all
an intuitionistic definition of truth, or even of validity in predicate
logic.
>So a form of the Goedel results can still hold.
Godel’s theorem is perfectly valid intuitionistically.