Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?

poopdeville_at_gmail.com
Date: 02/04/05 

Date: 3 Feb 2005 20:11:11 -0800

Sorry for the late reply.

tchow@lsa.umich.edu wrote:
>
> >Yes! We need to know what symbols are, and what (the relevant)
> >syntactic rules are to do number theory. But the syntactic rules
> >demonstrably don't pick out a unique interpretation, which is
exactly
> >why we need to be careful when talking about truth.
>
> To respond to this let me skip forward a bit to:
>
> >If you can tell me what a set is, outside of a "collection" (the
> >more-or-less personal "mental picture") or "an element of a
collection
> >which satisfies the membership relation" (the public notion that
> >doesn't pick out one of these mental pictures), that'd be great.
:-)
>
> I'll tell you what a set is if you can tell me what a symbol is.

Glyphs on paper, words, sense data, representations of objects that
must be interpreted. Outside of that, I don't know what they are, but
I know we have much more immediate access to them than the things they
represent. (This is the point where you can justifiably accuse me of
being an extreme skeptic)

>
> By the way, historically, symbols were often thought of as being less
well
> understood than integers. The whole notion of Goedel numbering is,
in a
> sense, a symptom of the feeling that we know how to deal with
integers, so
> to convince ourselves that we know how to deal with symbols and
strings,
> let's convert symbols and strings to integers, so that we *really*
know
> what we're talking about.

This is interesting.

>
> But that's an aside. Let me take your argument about unique
interpretations
> and turn it against you. Logic, like any other branch of
mathematics, can
> be formalized and studied. In particular, we can develop a
first-order
> theory of syntax, which captures discourse about symbols and strings
and
> so forth. When we do this, we discover that sentences about symbols,
> strings, rules, and so forth admit nonstandard interpretations. We
might
> *think* we know what we mean by a proof of finite length, but lo and
behold,
> nonstandard models of axioms for syntax show us that "finite length"
proofs
> could be "nonstandardly finite," which is what most people would call
> infinite. Does this shake your belief that you know what symbols and
proofs
> are?

No. But then again, I was already familiar with logics in which some
theorems require infinite tableux to prove. And other various
non-classical logics, such as intuitionist logics. This only helps
make my point for me -- unless we specify in which logic we're working
with, we're not going to be able to understand each other (OK, so FOL
is the de facto standard. I have no quarrel with that. It's up to the
intuitionist to mention that he's working with a non-classical logic)

>
> >> The set of axioms for a group does not mimic the *discourse* of
group
> >> theorists.
> [...]
> >I had not thought of this distinction.
>
> Let me elaborate a bit because I think this exercise can be helpful.
> Suppose we try to express "every finite simple group is X" in the
> first-order language of groups. (I'm being lazy and not saying what
> X is, but as you'll see, we won't need to know anything about X other
> than that it's some property that groups might have.) As a first
step
> towards formalization we might try to rephrase:
>
> For all groups G, if G is finite and G is simple, then G is X.
>
> The problem is that we're quantifying over *groups* here ("for all
> groups G"), and in the first-order language of groups we can only
> quantify over *group elements*. (That's what "first-order" *means*.)
>
> Let's not give up just yet, though. If we could find a sentence
> "FiniteSimple" in the first-order language of groups such that
> "GroupAxioms & FiniteSimple" is satisfied by all and only the finite
> simple groups, then
>
> GroupAxioms & FiniteSimple -> X
>
> would be a tolerably good formalization. The problem, though, is
> the basic theorem of mathematical logic that any first-order sentence
> that is satisfiable by arbitrarily large finite structures is also
> satisfiable by some infinite structures. So we can't write down a
> sentence that captures "finite" in the sense we want.
>
> Problems also arise with "simple" because this means that there are
no
> nontrivial normal subgroups. A subgroup is a *subset* of the group,
> and again we can't talk directly about subsets in a first-order
> language, only about group elements.
>
> These limitations illustrate that when people study the first-order
> language of groups, they're *not* trying to mimic a large fraction of
> group-theoretic discourse; they're interested specifically in
*first-order
> properties of groups*, which is a very limited fraction of the
properties
> of groups that group theorists in general are interested in.
>
> In contrast, when people study ZFC, they are often investigating the
> foundations of mathematics as a whole, and it's important that most
of
> mathematical discourse can be mimicked more-or-less directly in the
> language. It's not that we're interested in---for lack of a better
> term---"universes" and we're trying to isolate the first-order
properties
> of universes for special scrutiny. We're actually trying to find
formal
> counterparts for all the kinds of statements that mathematicians
make.
>
> The two projects are quite different and the fact that the same tool
> (first-order logic) is being used in both cases does not mean that
> direct parallels between ZFC and the axioms for a group always make
> sense.

Agreed. Thanks for the great explanation.

'cid 'ooh

Relevant Pages

  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... >>syntactic rules are to do number theory. ... > strings, rules, and so forth admit nonstandard interpretations. ... I was already familiar with logics in which some ... > first-order language of groups. ...
    (sci.logic)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... >>syntactic rules are to do number theory. ... > strings, rules, and so forth admit nonstandard interpretations. ... I was already familiar with logics in which some ... > first-order language of groups. ...
    (sci.math)
  • Re: Semantics of First-Order Languages
    ... other logics than FOL to understand what this would mean. ... first-order ZFC to first-order PA. ... You cannot use a formal system in FOL ...
    (sci.logic)
  • Re: Run and hide you girls
    ... USE first-order logic. ... or IS false in all interpretations, then there IS a program that WILL ... we could not prove Golbach's Conjecture, ... some sufficiently strong first-order axiom-system approximating ...
    (sci.logic)
  • Re: Semantics of First-Order Languages
    ... least in principle, be completed. ... other logics than FOL to understand what this would mean. ... You cannot use a formal system in FOL ... enumerate the first-order truths about the natural numbers ...
    (sci.logic)