Note that I was talking about second order logic, and not first order logic. A closure can be defined in second order logic. But I will read your answer more carefully tomorow.

Interesting, that even after a bonus, I didn't get an answer. This means that most logicians don't know how to do some simple math in FOL + PA. I have to verify if everything is right. I have ordered the book suggested.

Thanks for the comment. But I don't think it is that easy, because you might need to choose a new p. But I will take a look at the book you referenced earlier. But I am a little bit surprised that this is not some kind of standard result, which worries me, about how much we actually know about FOL + PA.

Thanks for the answer. Interesting that Peirce was already busy with these kind of things.

Thanks for the answer. I don't follow everything, but I read things that are somewhat similar to my own thoughts.

Thanks for the clear answer. I always wonder why logicians don't answer in a more formal way. This is clear positive exception.

I want to add that in principle you want to avoid "definition" when using a logic, because it can make your logic inconsistent. For making your inductive definition (without adding just rules to your logic), you can not use a fixed point definition, because for that you need second order logic. To do it in FOL + PA, you have to use a transitive reflexive closure. Which is possible in FOL + PA but quite tricky and not to be found in a standard book of logic. To my opinion a great gap in education!

I don't want to start from scratch. Existing verifiers should become part of the framework. However, current verifiers are designed to act in solo. Cooperation with other verifiers has never been a requirement. So, it might be necessary to adapt them, to make it possible that they can cooperate with other verifiers. I will look at the paper. But note, it doesn't go fast, because it is not my job to think about these things.

Vijay, I have looked at the verifiers. The Pex doesn't contain information about the algorithms it uses. I also have the Pratical Logic and Automated Reasoning from John Harrison. I have made 2 observation. First observation, if verifiers start cooperate, you need(\Pi^0_2) sentences in the arithmetic hierarchy to pass from one verifier to another. Halting problems are insufficient. Second observation, for daily reasoning about programs, all intermediate results can be expresses as (\Pi^0_2) problem. So, my ideas do have a rational.

Vijay, one of the things I am researching, is to design a framework for automatic provers. In such way that the different provers can cooperate with each other to solve a problem. Because, I don't believe in a single method. The difficulty is how the different provers communicate with each other. Communicating with Halting problems won't work, because that is not expressive enough. However, higher order logic, becomes too complicated. That is one of the reasons, I use transitive closures.

I meant the closure of a relation. I see now that it requires more rewriting of the original program, then using fixed point. However, as I said before, it has the advantage that it keeps things mostly within first order logic. My goal is to show how things can be build up from a simple system, such as (but not necessarily) FOL + PA. The article I intend to write is to represent the formulas in a graphical form, without using variables. And finally, my idea is that common reasoning about programs (with all intermediate results) stays within (\Pi^0_2) complexity.

Ah! I see now the difference. Thanks, I learned something again. The disadvantage of rewriting it in a fixed point, is that you need to use higher order logic. The Functor is a second order logical element. While the method I intended in my question stays within first order logic. The loops can be converted to FOL + PA, while you can't do that with fixed point induction.

Vijay. Thanks for your comments. But I don't agree with your second sentence. In my opinion, modern logic should be automatically verified. Otherwise, I call it just mathematics (nothing wrong with that). There are still plenty of possibilities to make automatic verifiable logic better suitable for humans. Goedel numbers are just the bits in the computer. You don't need to confront humans with it.

Andreas, I am not familiar with Coq, but I know a little ZFC and HOL Light. As far I know, if one has to transform a computerprogram with a loop to a logical expression in one of those systems, then you end up in making a closure operator somewhere. So, when explaining how programs and systems like ZFC and HOL light are related, then I think you have to start that. From there, one can go to fixed point theorems. I am an outsider, because I do not work on an university. But graduates that start to work in my company, are not capable of defining a mathematical problem in a formal system.

Andrej, I am reading the tutorial of Minlog. On page 12, they do add-global-assumption. These kind of things you want to avoid, because this way you can introduce inconsistencies in your system. The way I define the predicate in my question is 'safe', because it is a single definition. Taking the transitive reflexive closure is also 'safe'. So, I define the Fibonacci numbers in a safe way, while the tutorial in Minlog isn't.

Thanks for the answer. The idea that I have is to make a FOL extended with transitive closure, with some axioms for it. The advantage is that it stays rather simple. You don't need an induction axiom anymore, because that can be derived from the axioms of the closure (similar to the Axiom of Infinity). By the way, if you represent graphs as (Godel) numbers, then you can define reachability in FOL + PA. Of course, the graphs must be finite in such case. But you are right, that you can't define reachability if the graph is represented as predicate.