[FOM] First Order Logic
silver_1 at mindspring.com
Mon Sep 2 14:04:37 EDT 2013
I reproduce below a (SNIPPED version of a) discussion that took place on FOM on Sept. 11th, 2000, between Matt Insall and Harvey Friedman. I believe this old exchange sums up the matter succinctly and accurately:
So in a sound and complete finitary deductive calculus, semantic
compactness is equivalent to strong completeness.
Yes, but the hypothesis of completeness is far too strong in the context of
SOL. The set of SOL validities is nowhere near even recursively enumerable.
SOL is well known not to be semantically compact, and also any complete
deductive system for SOL must be grossly unreasonable.
On Sep 2, 2013, at 10:20 AM, Carl Hewitt <hewitt at concurrency.biz> wrote:
> Dear Martin,
> The second-order axiomatization of the Peano Natural Numbers has been a great success since it has become the standard way for mathematicians to prove properties of the Natural Numbers.
> In fact, the axiomatization is basically the only way known to prove that some property is true of the Natural Numbers.
> However, it is computationally undecidable whether or not a sentence is a theorem of the second-order axiomatization of the Peano Natural Numbers.
> Consequently, there is some sentence that is neither provable nor disprovable using the second-order axiomatization of the Peano Natural Numbers.
> Should it be considered a defect of the second-order axiomatization of the Peano Natural Numbers that there is such a sentence?
> From: MartDowd at aol.com
> Sent: August 31, 2013
> To: Foundations of Mathematics
> [All] true statements [about the Natural Numbers] are not [provable using the second-order axiomatization of the Peano Natural Numbers].
> - Martin Dowd
> In a message to Foundations of Mathematics on August 30, 2014, Carl Hewitt wrote:
> I am having trouble understanding why the proponents of first-order logic think that second-order systems are unusable.
> [Dedekind 1888] and [Peano 1889] thought they had achieved success because they had presented axioms for natural numbers and real numbers such that models of these axioms are unique up to isomorphism with a unique isomorphism. And later generations of mathematicians were happy to use these axioms.
> The above axiomatizations bar many mathematical monsters that are created by the “first-order thesis” [Barwise 1985]. The articlehttp://arxiv.org/abs/0812.4852 presents a mathematical foundation for Computer Science that is an alternative to the first-order thesis.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM