[FOM] Fwd: Concerning definition of formulas

[Kaveh Ghasemloo]

For doing mathematics formally, there is a primitive need for some
intuitively clear concepts. Without them, it would be strange to be
able to do formalism. Even Hilbert and Bernays accepted some finitary
mathematics as a base for their work. Obviously we can not define
everything, because definitions define new concepts in terms of
previously understood concepts. To understand a definition we need to
be able to translate it in finite time to concepts we understand
directly.

A problem with finite, which is implied in the other replies is that
we have two meanings for it. One is an informal intuitive which is
real finiteness, easily understandable by what one can actually do,
but not definable, and one formal finite, which is defined inside some
theory like PA or ZFC. The difference is similar to what Nelson uses
in his "Predicative Arithmetic", chapter 18:

"Take a strong theory T    containing 0 and S, say any extension by
definition of PA or even ZFC. Let T* be the theory obtained by
adjoining a unary predicate symbol $\phi$ and the axiom"

"Fin. $\phi(0) \land (\phi(x) \rightarrow \phi(Sx))$"

"This adjunction does not increase the power of the theory in any way;
we can for example interpret $\phi(x)$ by x=x. If T is an
axiomatization of arithmetic, say an extension by definition of PA,
then by a  specific number    we mean a variable free term b of T; if
T is an extension by definition of ZFC containing constant $\omega$
denoting the set of all natural numbers, then by a specific number we
mean a variable-free term b of T such that $T \vdash b \in \omega$. We
say that a specific number is a  finite number in case that $T* \vdash
\phi(b)$."

Using non-standard models we see that these two concepts, specific and
finite, are distinct.
A finite number in this sense is completely understoond, although not
completely defined, by what we can actually do in principle (It's
different from what Nelson writes in that we think of doing "in
principle", where he thinks of "actually" doing), what we can prove.

So supposing that there are not many ultra-finitists around, we can
consider concept of finite number as something clearly understandable
intuitively, even for first year undergraduates. Without this
assumption, we will run into problems anyway we choose to go about
foundations, since, a far as I know, we do not yet have a considerable
development of ultra-finitism. When we take  finite number   as a
concept understood clearly by intuition (and some simple operations on
them), the problems about defining formulas disappear.

p.s. Concerning Tarski's definition of truth, here is something
interesting again from Girard, Locus Solum, Page 164:

"Tarskian Semantics
This is a theory of truth:
* $A \land B$ is true when A is true and B is true.
* $A \lor B$ is true when A is true or B is true.
* $\lnot A$ is true when A is  not true.
* $\forall x A[x]" is true when A[c] is true for all c.
and so on... In other terms, truth is the quality of what is true. The
first time one hears this nonsense, one finds it stupid, but after one
learns about a subtle point, namely the distinction between $\land"
and  and:<<you know, and    is meta>>; truth of A is no longer A, it
is in fact meta-A. Tarskian semantics is exciting like a carrot
diet... But after a few weeks of such diet, nothing tastes better than
carrot: you get addicted, and you dispraise the vulgar minds that say
that the King is naked... Tarski's semantics represents the most
unimaginative expression of Western rationalism, in sharp contrast to
Brouwer's approach. The usual schizophrenic presentation of logic must
be ascribed to his influence."

Page 94:

"Broccoli Logics
....
By the way Tarski is not (fully) responsible for this abusive
extension of his paradigm..., originally restricted to classical
logic(for which one can say that the paradigm is not wrong, if not
very useful), with the idea of one solid reality.
..."

-- 
Best
Kaveh Ghasemloo