FOM: determinate truth values, coherent pragmatism

[Kanovei]

>Date: Tue, 5 Sep 2000 12:02:04 
>From: Harvey Friedman <friedman at math.ohio-state.edu>

>On the other hand, we already know how to meet the following challenge by
>the statistical method of repeated trials:

>CHALLENGE 3. Find a way to confirm or reject a Pi-0-1 sentence of the form
>"for most bit strings of length at most 1000, such and such feasibly
>testable property holds" other than finding a proof or refutation of that
>statement from accepted axioms.

Can you make it more clear what do you mean by 
"other than finding a proof ... from accepted axioms" ? 
Well, in some cases you can execute a computation that 
results in 0 or 1 and you interpret this as TRUE or FALSE 
(a given sentence is). 
Then (in fact, before) you have to demonstrate that this is 
just a true answer, which cannot be anything other than a 
mathematically rigorous "proof from accepted axioms", whatever 
simple set of axioms is sufficient for such a demonstration. 

Would you claim that SOME "accepted axioms", like e.g. m+n=n+m 
for natural numbers, are really not axioms but rather physically 
evident postulates which do not count as axioms in "CHALLENGE 3" ? 

Thanks,

V.Kanovei