Re: Foundations of Constructive Mathematics
- From: Jan Burse <janburse@xxxxxxxxxxx>
- Date: Mon, 05 Jan 2009 01:00:51 +0100
John Jones schrieb:
Frank J. Lhota wrote:
> Constructive mathematics asserts that the existence of a mathematical
> entity can only be proved only by providing a method for constructing
> that entity.
What's wrong with that sentence? What entity exists prior to its proof? and if it doesn't exist prior to it's proof then are you saying that something can be proved into existence? Is 'proof' the right word to use?
No there is nothing wrong with the above sentence.
When my background theory stipulates the existence of
objects that exist by mere stipulation, without giving
a method of constuction, than I can prove from this
background theory their existence.
And example of such a background theory is ZFC. It
for example stiplulates the existence of the power
set for all given sets. And one might wonder what
the (finite) method of construction would be, when
the given set is countable infinite.
If we drop ZFC and if we work with another background
theory, then the objects that can be proven to exist
might look totally different. For example all our
sets might be recursively enumerable.
An object is said to be proven to exist (uniquely),
when we have a formula A(x), and when we can prove
the following two facts:
- Existence: exists x A(x)
- Uniqueness: forall x,y A(x) & A(y) -> x=y
For example the empty set can be proven to exist
uniquely in ZFC by means of the following
formula:
A(x) :<=> forall y ~(y in x)
Proof:
- Existence: Follows directly from the axiom of
empty set in ZFC. Which reads:
exists x forall y ~(y in x)
The existence claim exists x A(x) is just an instance
of this axiom.
- Uniqueness: Follows from the axiom of extensionality
in ZFC. Which reads:
forall x,y(forall z(z in x <-> z in y) -> x=y)
Lets assume A(x) and A(y), then we have
forall z ~(z in x) and forall z ~(z in y). But
from this it follows logically forall z(~(z in x) <->
~(z in y)). And from this it follows logically
forall z((z in x) <-> (z in y)), and hence x=y.
The most simplest bottom line of this all is the following.
A background theory might use a certain vocabulary of
symbols. But neither the individual constant symbols
nor the combination of constant symbols and function
symbols span the objects that are implied by the background
theory.
This is even not in contradiction with the henkin term
model construction. Because there we dynamically add
new constants for new implied objects. Because the
initial term model is not exhaustive enough.
Best Regards
.
- Prev by Date: johnreed take 26 - An Astonishing Fact?
- Next by Date: TMFCS-09 call for papers
- Previous by thread: johnreed take 26 - An Astonishing Fact?
- Next by thread: Re: Foundations of Constructive Mathematics
- Index(es):
Relevant Pages
|
