1
$\begingroup$

I am trying to understand FOL + PA, better.

With FOL + PA I mean, first order logic, with addition and multiplication predicate and induction axiom scheme.

The book I am reading explains how to construct transitive reflexive closure with these predicates. By encoding the sequence using a prime number, that is larger than any of the numbers in the sequence.

However, it is not directly clear to me, that the invariant of this closure can be derived from the induction axiom scheme (it is also not explained in the book). If there is a predicate R(x,y), one wants to be able to prove that for any $\phi$:

$(\forall x,y:(\phi(x) \land R(x,y)) \to \phi(y)) \to (\forall x,y:(\phi(x) \land R^*(x,y)) \to \phi(y))$

It is not obvious to me that this is possible. For using induction, you need to number the values in the sequence. However, I doubt if there is already enough prove power to do so.

Does any have resources where this is detailed out? If such invariant is not possible, then FOL + PA constructed this way is crippled.

Lucas

Edit, here the definition as in the book of John Harrison:

$R^*(x,y) ::= \exists m, p, Q: primepow(p,Q) \land x < p \land y < p \land$ $(\exists s: m = x + ps) \land$

$(\exists r: r < Q \land m = r + Qy) \land$

$\forall q: q < Q \to primepow(p,q) \to \exists r, a, b, s: m = r + q(a + p(b + ps)) \land r < q \land a < p \land b < p \land R(a,b)$

Improve this question
$\endgroup$
17
  • $\begingroup$ To clarify, is the displayed formula missing some quantifiers? Also, by FOL+PA do you just mean the usual Peano Arithmetic? $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Oct 28, 2010 at 20:16
  • $\begingroup$ I'm sorry, I do not understand. What is $R^*$? Also, what is the invariant (or invariance?) you mention? I also have Bjørn's question about whether this is PA or something else. Do you have definitional axioms for addition and multiplication, or only the symbols? Do you have a symbol for 0? A symbol for successor? Do you have axioms for them? Can you please explain better what is the encoding you refer to in paragraph 3? $\endgroup$
    – Andrés E. Caicedo
    Commented Oct 28, 2010 at 20:26
  • 1
    $\begingroup$ Well, I don't know what answer you expect, but yes, it seems quite clear that you can do it. As a good heuristic you can imagine that you're allowed to manipulate finite objects (finite lists of numbers, finite sets of finite lists of numbers, etc.) Then you can show the desired conclusion by induction on the length of the sequence that witnesses $R^{*}(x,y)$. $\endgroup$
    – Andrej Bauer
    Commented Oct 28, 2010 at 20:27
  • $\begingroup$ Is $R^*$ the transitive closure of $R$? (If yes, and you really mean Peano Arithmetic, the answer is yes, as mentioned by Andrej.) $\endgroup$
    – Andrés E. Caicedo
    Commented Oct 28, 2010 at 20:31
  • $\begingroup$ I added the quantifiers. For FOL + PA, you have a 0, a successor operator, an addition function and multiplication function. And the normal axioms for them. For the $R^*$ I use the definition given in a book from John Harrison (the creator of HOL-Light). Page 536 of his book automated reasoning. $\endgroup$
    – Lucas K.
    Commented Oct 28, 2010 at 20:31

1 Answer 1

Reset to default
1
$\begingroup$

The answer can be found here:

http://www.staff.science.uu.nl/~ooste110/syllabi/peanomoeder.pdf

Most important part, theorem 1.9 ii.

With this theorem you can have some kind of sequence for which you can prove that the sequence can be extended. This proof is given in PA. With the sequences the remaining part is trivial.

The suggested book Shoenfield's "Mathematical Logic", doesn't provide the answer. It only gives the proof in informal mathematics, but not in PA. Which is required here. The informal mathematics assumes sequences you haven't available yet.

Improve this answer
$\endgroup$
6
  • $\begingroup$ Shoenfield gives the proof in informal mathematics in Chapter 6, but in Chapter 8 he points out, in the fourth paragraph before the end of Section 8.1, that the proof can be formalized in PA. In fact, that is why the proof in chapter 6 is somewhat more awkward than what one might do if only an informal proof is wanted. The proof in Chapter 6 was designed to be easily formalizable in PA. (Of course, if you really want a fully formalized proof in PA, then that is not contained in Shoenfield's book --- for which I and probably many other readers are grateful.) $\endgroup$
    – Andreas Blass
    Commented Jan 13, 2013 at 21:26
  • $\begingroup$ I should add that the references in my preceding comment are to the 1967 edition of Shoenfield's "Mathematical Logic". I conjecture the newer version is reasonably similar if not identical. $\endgroup$
    – Andreas Blass
    Commented Jan 13, 2013 at 21:27
  • $\begingroup$ Andreas, I don't have the book by hand, because I am typing from a different location. But I do not agree with you that the proof was designed to be easily formalizable. The informal proof starts with an sequence. In the formal part, you are just trying to prove the basic properties of sequence. So, that is a no go. If you look to the reference I gave of Jaap van Oosten, you will see that the proof contains several non trivial induction step. You need to prove that a sequence can be extended. This is not trivial, when it is encoded with prime number, because you need to choose a new one. $\endgroup$
    – Lucas K.
    Commented Jan 19, 2013 at 23:08
  • $\begingroup$ Note, that the proof is not required for the remaining part of the book. It is necessary to show that you can do basic mathematics (whatever that is) in FOL+PA. The book only addresses that FOL+PA can define certain things, such as computable functions. Still, I consider it an omission. My question popped up, because I was looking at rather simple systems where you could do some real mathematics, without the complexity of ZFC or type theory. If you start with a closure operator and a successor operator, you don't need the + and x of PA and it is a better prequal to 2nd order logic. $\endgroup$
    – Lucas K.
    Commented Jan 19, 2013 at 23:15
  • $\begingroup$ I agree with you that a fully formal proof would make a book unreadable (although, in these times you can put it on the internet and give a reference in the book :-). However, one can adopt a style of writing, where it is very clear how theorems (so, not proofs) could be writtten formaly. The referenced piece of Jaap van Oosten follows this style, and leaves many proofs to the reader (which I consider okay). The Shoenfield book doesn't follow this style. The sequences pop up in informal mathematics, without proper link to the formal part. $\endgroup$
    – Lucas K.
    Commented Jan 19, 2013 at 23:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .