Definition talk:Formal Language

From ProofWiki
Jump to navigation Jump to search

Definition is weird

Hm, this is not how I learnt the definition of a formal language. Currently this reads:

A formal language is a structure which contains:

The third bullet point seems to me extraneous. By my reckoning, a formal language consists of:

  • a set $S$ (the alphabet) and
  • a set of words $W \subseteq \left\{ { \left({ x_1, x_2, ..., x_n }\right) : \forall i, x_i \in S}\right\}$

As I understand it, a grammar is a way to construct a set such as $W$ and thus to define a language; what use is it to include a grammar and a set of words in the definition of a formal language? — Timwi (talk) 22:36, 18 December 2012 (UTC)

I think this is done from an algorithmic perspective. Both the words and the formal grammar can be more easily realized in a computational context than the arbitrary set $W$ you propose. It seems to explain how in general formal languages are constructed (giving a grammar of WFFs); as such I think the current page is adequate and links well to most sources on the subject (though more general than most texts bother to define things). --Lord_Farin (talk) 22:44, 18 December 2012 (UTC)

Further broadening of perspective

Ben-Ari in his work that I have started covering defines a formula to be a labelled (rooted) tree (with ordering of child nodes). Given the conceptual simplicity that results (a subformula is a subtree) and in general the appeal of graphics representing things (often much more intuitive to process, e.g. commutative diagrams) I don't see a reason to restrict to words in specifying a formal language - it could equally well be a graphical language. It's a nice generalisation that Ben-Ari provides a source for. It will also come in handy to describe (eventually) proofs as labelled trees satisfying restrictions.

Explicitly, I'd like to (wherever such is appropriate) replace instances of "word" with the more general "expression" (as Definition:Expression isn't anything meaningful atm). If we are to pursue the aim of covering all (published or otherwise verifiably practised) approaches to a concept then I think this step will be inevitable. Thoughts? --Lord_Farin (talk) 11:30, 16 February 2013 (UTC)

It's not the only such source: 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability takes a similar approach, although they start with the definition of a formal system in the conventional way and then exhibit (more or less informally) an isomorphism between such a system and a rooted tree.
In my understanding the term "expression" is narrower that "word": the latter is any arbitrary string of symbols, an expression is a well-formed word. As long as the distinction is held in mind, and that both concepts are recognised, it doesn't matter what we call them as long as we register all the variant definitions.
Also worth disambiguating between "expression" and "mathematical expression" as the latter is used informally through maths, being implicitly understood and rarely defined rigorously.
To mix metaphors horrendously, you're currently treading on the same soft ground, thin ice and booby-trapped minefield that I retreat from every time I approach this area. Each work has its own separate approach, but I have been unable to create a synthesis. But if we can find that sweet spot that merges all approaches, we'll have created something seriously worth while. --prime mover (talk) 12:31, 16 February 2013 (UTC)
You are quite correct on "expression". The next words coming to mind are "arrangement" and "collation". I'd rather not redefine "word" to include pictures. Contemplating it a bit longer, I start to like "collation" more and more. You? --Lord_Farin (talk) 13:01, 16 February 2013 (UTC)
Never heard it used outside the context of catering - but I see it's a term in computer science loosely isomorphic to "ordering".
As always. If what you're adding is supported by your text sources then go for it. --prime mover (talk) 13:54, 16 February 2013 (UTC)

Clarification on "structure"

What is a structure and what does it mean for a structure to contain something? I would assume that in the meta-theory, this is a tuple, no? --Dfeuer (talk) 23:42, 6 September 2013 (UTC)

In defining a formal language, we can practically only talk in natural language (for no other language has been specified yet). To enforce a "tuple" as the carrying structure is not necessary at this point. We just need something, anything, that consists of these three parts and has them distinguishable.
I have changed "contains" to "comprises" to emphasize that there is nothing else in this structure. By all means, feel free to think of the structure as a tuple -- the intuition remains the same. — Lord_Farin (talk) 09:21, 7 September 2013 (UTC)
One of the initial challenges I had when I first started posting up the fundamentals of maths was: how not to be circular. An ordered tuple is defined as a set with a particular structure. A set is defined via ZFC or whichever axiomatic structure. ZFC itself contains an axiom which accepts a concept derived from logic. In order to define that logic rigorously, we need to specify some sort of formal language so to do. The rigorous definition of that formal language requires, in this page, the use of the definition of "ordered tuple".
I broke this chain by starting with the axioms of natural deduction as the "most fundamental" truths (notwithstanding Euclid), and my initial analysis used nothing more than reasoning based on that. A more rigorous treatment is required (as has been pointed out a few times), but such a treatment does require machinery of mathematics which is not, at that level, available. In particular, the step from propositional to predicate logic needs the concept of infinity to be able to justify.
In the work which I originally wrote (back in 2003 -- 2005) I used a double-pass (and indeed triple-pass) approach, where the original proplog theory was revisited with just enough of the concepts of basic number theory / abstract algebra having been deduced so as to be able to discuss set theoretical / proplogical concepts allowing the concepts of enumeration.
This to a certain extent mirrors the approach taken by 1965: Seth Warner: Modern Algebra, where the concept of a general cartesian product of sets (and consequently set union / intersection) are not even raised (for more than a binary operation) until chapter 18, that is, after the natural numbers have been introduced in chapter 16 (which are brought in via the mechanism of the naturally ordered semigroup). --prime mover (talk) 09:59, 7 September 2013 (UTC)
Oh, and in answer to the initial question, could we replace "structure" by "object"? I was the one who originally used the word "structure". Apologies. It had not occurred to me that it would need defining. Should we define "structure"? "A structure is an object with internal structure." (Hell, that ain't the blues ...) --prime mover (talk) 10:03, 7 September 2013 (UTC)
I trust in the ability of the reader's mind to intuitively grasp things at this level. We have to start somewhere. We could just as well have written "anything that consists of three identifiable parts" and I contend that "structure" sounds better. Everybody knows what we mean anyway (and here I write "know" in the sense of "deep down, intuitive knowledge"). — Lord_Farin (talk) 11:22, 7 September 2013 (UTC)