
Re: Whitehead & Russell on Reductio A.A. and when Constructivism is mainstream #200; 2nd ed; Correcting Math
Posted:
Oct 16, 2009 1:04 AM


On Oct 12, 3:35 pm, Nam Nguyen <namducngu...@shaw.ca> wrote: Basically is it possible that, e.g. arithmetically, ExPx is true without a concrete example? For instance, is it conceivable that ~GC is true without the need of citing one single example?
Making this into a precise question might take some work. Thinking constructively, an arithmetic claim of the form Ex P(x) just says that there exists an example, and being an integer it is concrete. Thinking classically, you could well prove the existence of an integer satisfying P without being able to prove that any specific integer satisfies P.
There's a metatheorem ensuring that if you can prove a statement of the form Ex P(x) where P(x) has all of its quantifiers bounded (so that whether P(x) is true is computable) (in a system S taken from some wide assortment of classical systems) then there is also a constructive proof (in a corresponding constructive system S+). Even without a metatheorem to help, though, one would usually reason (classically) that the existence of such an x means that we can find it by checking integers one by one.
If you have a more complicated predicate, there's no general guarantee. It's conceivable for example that one could prove (classically) that there are finitely many Fermat primes without being able to prove specifically how many there are.
BTW let's please set followups so that sci.physics doesn't have to put up with this discussion.
Keith Ramsay

