Re: Provability

On Oct 25, 11:38 am, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:
On Oct 25, 10:35 am, galathaea <galath...@xxxxxxxxx> wrote:
On Oct 25, 10:13 am, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:
On Oct 24, 8:58 pm, Michael Press <rub...@xxxxxxxxxxx> wrote:

A theorem is not a theorem until it is proven.

A sentence S is a theorem of a set of sentences G iff there is a proof
of S from G.

But what does "until" mean in this context?

constructivists almost universally seat properties in time

I'm not expert on the subject, but I recognize that certain
constructivists have notions that might be thought of, more or less
loosely, as temporal. However, it seems to me that in intuitionistic
mathematics, this can be formalized without a literal temporal
component.

anything that can be formalised
can be formalised in a completely meaningless game of symbols

constructivists
from before brouwer
have made the point that math is a physical process
and that any computation
calculation
application of rule sets in steps
exists temporally
and have argued that any description of mathematics
that is to have _meaning_
must likewise describe these temporal processes

brouwer made much of math being a mental phenomenon
and used kantian arguments to connect this process with time

later constructivists
have allowed mathematics any computational existence
abstracted from the mind
and have used the temporality of computation
to make the connection more operational

kripke models
the most common semantic setting for heyting algebras
are inherently temporal
for the same reason the semantic interpretation of "possibility"
is inherently temporal

i am sure you have seen BHK semantics
moe

Yes. Personally though (and I don't hold this to be controlling of
anyone else's understanding or even necessarily a permanent notion of
my own), I tend to view the BHK as an informal motivation that is then
formalized by actual mathematical semantics.

that has been a common description over the years
but it is much less true since the work of martin-lof and artemov

there are obstructions that make it impossible
for a full valuation to be treated in BHK
so it has been often assumed the semantics could only be informal
but that is an error in mistaken existentials

it is sufficient for semantics
that a skolemised realisation exist

this was the importance of artemov's theory
in completing the formalisation of BHK

do you understand why constructivists
reject ullrich's dichotomy?

Due to my own personal unfamiliarity with Ullrich's notation, I don't
opine on the example Ullrich gave. But more generally, are you saying
that there is a definitely articulated constructivst notion of
'algorithm' that includes that something is not an algorithm until
proven to be an algorithm? If so, would you recommend a book or
article that I can read about that?

i am unfamiliar with a specific singling out of "algorithm"
since constructivists tend to have strongly operational views
on all properties

for a good summary paper
that stresses in multiple places
the verificationist programme michael press has mentioned
see

http://www.cs.gc.cuny.edu/%7Esartemov/publications/RusMatSurveys.ps

almost any book on constructivism
though
will point out that constructivists do not accept

forAll sentences A
either A or not-A must be true
required by ullrich's construct

tertium datur

most references on constructivism will explain why this position is
taken

often
they will even use an example

old books sometimes used fermat's conjecture
many now use goldbach

there is a reason these examples are almost universally of this form
and why they will by nature change over the years

it has everything to do with time

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar

.