|
|
Verifiable Mathematics
Posted:
Mar 27, 2012 7:41 AM
|
|
If T is a first order theory with n axioms A1,...,An, then Con(T) is
equivalent to saying that ~Ai is not a theorem of FOL+A1+...+Ai-1 for
i=1,...,n where A0 is a tautology.
Now the problem with proving consistency of a theory T is that there
might be a too long proof of ~Ai in FOL+A1+...+An, and since the
number of proofs in FOL and its extensions is infinite then we need a
way to prove that every m-long proof in FOL+A1+...+An do end up with
~Ai, but there is no guarantee that there is such a way.
Now if we work in a finite FOL, which is a subsystem of FOL where
there is an upper bound on the number of characters in a formula, now
if we symbolize this upper bound as i, then an iFOL have all the rules
of formation of formals of FOL with the added condition that the total
number of characters in a formula must not exceed i. Now we also
stipulate that there is a finite number of constant, variable,
function and predicate symbols, so the result is a FOL that has
finitely many formulas.
Now it is trivial to see that any theory T formalized in such finitary
logic system would have a proof of consistency or inconsistency which
is actually obtained by simply checking if ~Ai is not one of the
finitely many statements of jFOL+A1+...+Ai-1.
We can obtain a *complete* theory T in a finite FOL system, by
continually adding Ai axioms till no non derivable statements are
possible.
For every iFOL we can define the set of all consistent and complete
theories the extends it.
Now my point is that it is also trivial to see that the above can be
done for every finite i, because the whole process of proving
consistency and completeness depends on the feature of having an end,
i.e. EXHAUSTION. which is common to all finite naturals.
I think that we can do a lot of consistent formulations in those
rather extremely weak systems. I call them Verifiable mathematics.
I think verifiable mathematics can be used in most extra-mathematical
empirical fields ordinary mathematics is used in. So it may replace
ordinary mathematics for applied purposes.
By contrast known systems are involved with the concept of the
infinite, and if they are strong enough to formulate arithmetic then
they cannot be proved consistent, so their consistency is not provable
and one can only give informal reasons for why they ought to be
thought of being consistent, yet all of statements formulated within
them assumes that they are consistent, since if they were not then
there would be no meaning of stating them in those systems. This is
applicable to PA, 2nd order Arithmetic, Z,ZF,MK, etc... all are of non
provable consistency.
Now why we need to work with NEVER provable systems, systems that
cannot ever be proven consistent. Why we don't stick to something more
concrete and that is suitable for all applications of mathematics in
empirical sciences.
My question is about preference of systems, those that have a proof of
their consistency and even completeness in an unshakable manner and
those that cannot ever be proved consistent. The main problem is in
the "non provability" of the later systems, it is not the problem that
they are not proven yet, the problem is that they cannot ever be
proved consistent, while every result stemming from them is only of
importance if they were consistent.
Compare between:
Verifiable mathematics: Theories in can be: Provably Consistent,
Complete, Effectively generated, Categorical.
Ordinary mathematics: Theories in are: Not provably consistent, never
complete, not Categorical But effectively generated.
So why prefer the later to the former?
Zuhair
|
|
