Re: arithmetic in ZF
- From: "Babylonian" <starofbabylon@xxxxxxxxx>
- Date: 28 Apr 2005 10:37:46 -0700
Bhupinder Singh Anand wrote:
>
> B>> That is merely a consequence of using the law of excluded middle
> over infinite sets ... <<B
>
> How so?
Classicaly, if we assume ~(Ex)Px and prove p&~p, we can infer (Ex)Px.
THIS inference leads to belief in objects whose existence is
"non-algorithmic and essentially unverifiable constructively", and it
is equivalent to adding LEM as an axiom.
>
> I am not familiar with intuitionistic truth. My impression is that it
> involves belief in a priori, absolute, mathematical truths.
A sentence p is nontrue until a proof of p is found, whereupon p
becomes true. ~p is the statement that there can never be a proof of p.
p is false if and only if ~p is true.
This states a time-dependence of truth in terms of the construction of
formal OR informal proofs, while your definitions appear to state
time-independence of truth in terms of nonconstructive existence of
*formal* proofs:
>
> However, I believe that such beliefs could inhibit effective
> communication of mathematically expressed concepts, and it should be
> possible to, alternatively, define semantic truth effectively, in an
> interpretation M of a formal system P, by linking it to
P-provability,
> say as follows:
>
> (i) Uniform (algorithmic) truth: A formula S of a formal system P is
> uniformly (algorithmically) true under an interpretation M if, and
only
> if, S is provable in P.
(ia) Then if S is (i)-true, there is an algorithm to prove it, but what
if S is NOT (i)-true? The set of (i)-true sentences is not decidable,
and others have pointed this out.
(ib) definition (i) makes vacuous reference to M; the (i)-truth of S
depends solely on the axioms and inferences of P.
>
> (ii) Individual truth: A formula S of a formal system P is
individually
> (instantiationally) true under an interpretation M if, and only if,
> every instantiation of its interpretation in M is the interpretation
of
> a formula that is provable in P.
(iia) If I understand this, S could have an infinite number of
instantiations under M; how do you determine if every such
instantiation is the interpretation of a P-provable formula; i.e. a
(i)-true formula?
>
> (iii) Truth: A formula S of a formal system P is true under an
> interpretation M if, and only if, it is either uniformly
> (algorithmically), or individually (instantiationally), true under
the
> interpretation M.
How can you say this defines truth "effectively"? You have defined
truth in terms of the existence of proofs, not the existence of
algorithms.
>
> Clearly, the Law of the Excluded Middle does not hold unequivocally,
> since the negation of 'S is true under the interpretation M' is not
'S
> is false under the interpretation M'. In this sense, the above
> definitions support the Intuitionistic objections to beliefs in an
> unrestricted applicability of the Law.
>
The negation of "S is true under M" is "S is not (i)-true and S is not
(ii)-true under M". Then there is no proof of S, and there is some
instantiation of S in M which is not the interpretation of a formula
that is provable in P.
Since you defined truth in terms of the existence of formal proofs, do
you not define falsehood in terms of non-existence of formal proofs?
> (Note that, for an interpreted proposition R in M, we may still have
> that either R is true or R is false provided there is some effective
> method for determining every proposition of M as either true or
false.)
>
Where did that come from? I ask again: where in your definitions is any
mention made of effective methods?
>
> B>> A "definition of truth" in the sense of Tarskian theory is
nothing
> more or less than a definition of meaning. So, (Ax)Rx is true in M if
> and only if, for all x in the domain of M, Rx. That's all Tarskian
> theory is. <<B
>
> True. That appears to be a widely accepted interpretation of Tarski's
> definitions of semantic truth. However, I find that Tarski's
> definitions, when applied to the semantic truth of the propositions
of
> a formal language under a well-defined interpretation, gain in
> significance if we interpret them as implicitly implying the
existence
> of some effective method for determining that 'for all x in the
domain
> of M, Rx'.
Then instead of (i), (ii), and (iii), why not just restate Tarski with
reference added to effective methods? What you have stated makes no
such reference.
>
> We can, then, extend them to distinguish further between uniform
> (algorithmic) effective methods, and individual (non-algorithmic)
> effective methods, as suggested above,
>
> B>> The Church-Turing thesis has nothing directly to do with
> determining the truth of arithmetic sentences.<<B
>
> You're right, not directly. However, Church's Thesis is that a
> number-theoretic function is computable if, and only if, it is
> recursive. Since every recursive function is, both, instantiationally
> computable and representable in a Peano Arithmetic, it follows that
> every number-theoretic proposition (in the common, standard,
> interpretation M of Arithmetic), when treated as a Boolean function,
is
> effectively decidable - either uniformly or individually -
Myself and others have shown this is not so. IIRC others have made
points along similar lines. We can determine if S is (i)-true
(independently of M!), but that does NOT mean (i)-truthhood is a
decidable predicate, and (ii)-truth is defined in terms of (i)-truth
(P-provability).
.
- Follow-Ups:
- Re: arithmetic in ZF
- From: george
- Re: arithmetic in ZF
- References:
- arithmetic in ZF
- From: H. Enderton
- Re: arithmetic in ZF
- From: george
- Re: arithmetic in ZF
- From: Bhupinder Singh Anand
- Re: arithmetic in ZF
- From: george
- Re: arithmetic in ZF
- From: Bhupinder Singh Anand
- Re: arithmetic in ZF
- From: george
- Re: arithmetic in ZF
- From: Bhupinder Singh Anand
- arithmetic in ZF
- Prev by Date: Re: arithmetic in ZF
- Next by Date: Re: Relation between sets and their elements
- Previous by thread: Re: arithmetic in ZF
- Next by thread: Re: arithmetic in ZF
- Index(es):
Relevant Pages
|