Definition talk:Word

From ProofWiki
Jump to navigation Jump to search

I am having a problem here at the moment. Awodey says:

"Let $A$ be an alphabet, that is, a set $A = \left\{{a, b, c, \ldots}\right\}$. A word over $A$ is a finite sequence of letters."

It seems not to fit in either of the definitions currently up, while it is intimately connected to both. It pertains to the same stuff Jshflynn has been putting on his user domain. Should I just add another definition for it? If so, what to call it? Maybe introduce a new category 'Finite Sequences' so that we in passing have a place for Jshflynn's stuff to move in due time? My def would become Definition:Word (Finite Sequences) in that case. Thoughts? --Lord_Farin 14:04, 15 August 2012 (UTC)

Hi L_F. If you wish to do so you may quote: Introduction to Formal Language Theory by M.A.Harrison. There is still plenty of work to be done for anyone who is interested. Just see Chapter 2 of the following book which is freely available on Google Books: [1]. I will continue contributing as soon I have finished writing up some other unrelated document. --Jshflynn 15:34, 15 August 2012 (UTC)
In what way is it different from the definition as in Definition:Word (Formal Systems)? In my eyes it's the same. Again, am I missing something? Except for some reason Definition:Finite String has been redirected to Definition:Word: what was that all about? --prime mover 16:35, 15 August 2012 (UTC)
Instead of alphabet being defined as some specified collection of symbols pertaining to a formal language, it is just a set. Thus, the formal language def is an instance of the one purported by me, Jshflynn, Harrison and Awodey (in no particular order). It would be unfitting to add it there since it does not pertain to formal languages. --Lord_Farin 16:50, 15 August 2012 (UTC)

If an alphabet is just a set, then why not just say "set"? From what I understand, an "alphabet" is a set which is nested in a formal language. In the same way, if a "word" is just a sequence of elements of a set, then why not just use the word "sequence?" Otherwise you have multiple words for the same thing, the only difference being the label on the category of mathematics that the definition is made in.--prime mover 18:09, 15 August 2012 (UTC)


An alphabet is a finite non-empty set from the definitions I've seen. Words are finite sequences over an alphabet. I dislike synonyms in mathematics as well. It's unfortunate there's no W3C like organisation for mathematics :) --Jshflynn 18:22, 15 August 2012 (UTC)
yes-but-yes-but ... the only reason for calling it an "alphabet" is to use it in the context of a formal language. --prime mover 18:30, 15 August 2012 (UTC)
Okay... (what the heck does "yes-but-yes-but" mean?). It's probably restricted to being a finite non-empty set because they are used in computing by finite automata. I haven't looked so far into it yet. I'll just go along with whatever wording you guys see as most fitting. After all, it's important that the most potent contributors of the site are most comfortable with the vocabulary of the site. Peace. --Jshflynn 18:50, 15 August 2012 (UTC)


Fair enough. I will amend existing pages as appropriate. Apologies for generated confusion. --Lord_Farin 18:12, 15 August 2012 (UTC)
OK - I will swing by again when I revisit the source works to define their linear flow. --prime mover 18:15, 15 August 2012 (UTC)

Definition loop

finite string and word are defined circularly. Nowhere does it tell me how to make or recognize a finite string. Dfeuer (talk) 19:22, 19 December 2012 (UTC)

That help? Thanks for noticing. --Lord_Farin (talk) 19:27, 19 December 2012 (UTC)
Better, but not good. Finite string redirects to word, which is a disambiguation page containing a link to finite string. The whole thing is a mess because the definition of word invokes the formal system containing it, which is broken. Another difficulty is that formal languages are used to formalize things like logic and set theory, and our definition of finite sequence depends on the notions of "mapping" and "natural numbers". --Dfeuer (talk) 20:31, 19 December 2012 (UTC)
Agreed. I have tried to remove such circularities on Definition:Word (Formal Systems). I think we can descend to the next level, Definition:Alphabet (Formal Language). --Lord_Farin (talk) 20:43, 19 December 2012 (UTC)
Definition of alphabet is not fundamentally circular. I deem the issue resolved. --Lord_Farin (talk) 20:57, 19 December 2012 (UTC)
Also fixed the link from Definition:Finite String which was a remnant from earlier refactoring. --Lord_Farin (talk) 20:43, 19 December 2012 (UTC)

circularity is implicit

In order to formalise mathematics, you need to start somewhere. That somewhere is usually logic: prepositional based on natural deduction or truth-table analysis, then predicate. Then we use predicate logic in the specification of the axioms of set theory. Having got there, we now have numbers, ordered tuples, sequences and mappings, etc. all based on constructs from these basic starting blocks.

Now, having established mathematics, we then go back and formalise logic and set theory by means of construction of formal languages. But guess what folks - in order to specify the language in which mathematics is written, you need mathematics. To adequately define a word in a formal language, as a finite string of letters in that language, first you need the concept of a sequence (or, more accurately, an ordered tuple). But you need the formal language to specify the constructs from which the ordered tuple itself is defined. Of course it's circular.

I don't see it as a problem. You construct the language of mathematics with an implicit understanding of logic, and based on this you can (rigorously) create the axioms of set theory. And after you've done that, you create a formal system from which you then prove that the logical framework upon which you created your framework on is actually valid. If because of this fundamental truth about the universe and its creation proves that "the whole thing is a mess" then you're right, it's not worth carrying on. Maybe mathematics is a complete waste of time and effort after all. A bit like life, really. --prime mover (talk) 22:38, 19 December 2012 (UTC)

Precisely. You start with "implicit understanding". That is why I replaced the rigorous definitions with some natural language. We aren't specifying what everything is, because we have to start somewhere, and somewhere partially includes this page (I like to think e.g. the definition of $=$ is implicit as well). That's different from being circular IMO. True, one can take understanding of some mathematics implicit and then "do all of mathematics inside a formalised universe" (e.g. a model for set theory or via category theory) but this always seems to me like an unnecessary layer of extra premises (which have the admitted trait of being completely explicit). The virtue of the approach that I like to take is that it doesn't collapse into nothingness if some theory is shown inconsistent (which I hope all of us agree wouldn't invalidate mathematics; we'd simply find new theories). --Lord_Farin (talk) 22:56, 19 December 2012 (UTC)
Yes, starting with a concept as "understood" and building a theory from that, you can then also prove that you can construct a model of the concept within the theory, but you have to take care to note that this is indeed what you are doing and to avoid true circularity. Side note: when I first read of formal logic and started thinking about these very matters, I imagined a mathematician walking to the edge of a cliff and then proceeding to walk right over it through the air, with nothing below. This, I think, is more fundamental a matter of faith than such classic ones as "ZF is consistent".Dfeuer (talk) 00:09, 20 December 2012 (UTC)