Arithmetic calculations in ZF

13 views
Skip to first unread message

Victor Porton

unread,
Mar 6, 2009, 2:05:35 PM3/6/09
to vdash
It seems that ZF does not understand "arith" proof method.

How I should prove "1 + 1 = 2" theorem?

P.S. I just installed Isabelle and Proof General and have the first
experience.

Slawomir Kolodynski

unread,
Mar 6, 2009, 6:32:34 PM3/6/09
to vd...@googlegroups.com

> How I should prove "1 + 1 = 2" theorem?
>

Look at Arith.thy in the standard library. Note that addition of natural numbers is denoted "#+" . 1 = succ(0) and 2 = succ(1).

You might want to ask questions like this on the Isabelle mailing list.

Slawekk


Reply all
Reply to author
Forward
0 new messages