4 replies to this topic

[Zeref]

Hi guys
I just joined this forum, and since end the end of last year my Interest in artificial intellegence and robotics has shot up.

I was just reading a book called paradim shift (forgot the author) and he explains what formal systems are.

I just wanted to know whether its possible to code the basics of a language( symbols, rules) to a computer and then allow the computer to deduce what kind of words and sentances it can construct based on those rules.
The understanding of these sentences will of course be other issue.

[Mihail121]

I doubt you have any idea what you are talking about (keep reading, read a LOT), but yes, it is quite possible to specify a language to a computer for it to deduce all words and sentences. In fact, the main computation model (by Alan Turing) is bound to a class of certain class of languages. Each language of that class is enumerable by a printer. But I don't want to get into the details of language theory here. Get the following book:

The Bible

It is a standard reference on the topic and will answer all your questions. Be sure you're good in maths.

[EricTheRed]

I would recommend Artificial Intelligence: A Modern Approach. It also covers formal languages among many other topics. You may want to expand your search to expert systems as well.

[Klatten]

've been reading up on formal systems and Gödel's incompleteness theorem, and I'm pretty sure I understand them both very well.

Something that has been bothering me though... It seems like it should be possible to create complete and consistent formal systems with an infinite number of axioms. It would, of course, be equivalent to the halting problem to enumerate the first n axioms of such a system, since we would define axiom n as the first statement (given by some arbitrary "alphabetical" order, the definition of which would also define the system) which cannot be proved nor disproved given the first n-1 axioms.

Indeed, we couldn't program a computer to use this system, but... What could we learn from considering such a system?

Or more practically, what could we learn from systems that are complete and consistent "locally" (for lack of a better term)? i.e. formal systems which only allow a limited number of inferences? (In this case, there are well-defined procedures to determine if a given statement is a theorem) Do non-trivial systems of this type even exist?

If anyone knows of literature on these kinds of systems (or e.g. a name for them for me to put into Google), I would love to know about it

[Reedbeta]

Actually, systems with infinitely many axioms are quite well known; even some of the most common formal systems technically have infinitely many axioms. The usual way to implement this is with an axiom schema, i.e. a template for generating axioms. The key here is that it must be computably decidable whether a given formula is an axiom (fits any of the schemas).

And there are systems that are complete and consistent, such as Euclidean geometry and the propositional calculus, IIRC. Of course in these systems you cannot represent natural numbers (and compute with them), since then they would be subject to the incompleteness theorems. So these systems are of necessity limited in expressiveness, but I would not think that they are trivial.

As for your idea of creating a system by repeatedly adding some undecidable proposition to the axioms, that sounds interesting but I don't know where there might be any literature on that. It's not clear that it's a well-defined formal system since one usually requires the set of axioms to be computably decidable, but I think in your case it would only be computably enumerable.