Prev: New Primitive Programming Language - Is it Turing Complete?
Next: The size of proper classes?
From: Marshall on 1 Dec 2009 10:22
It seems a common technique for working with the natural
numbers is to pick a set of axioms, such as Peano's,
show the naturals are a model of those axioms, and work
the axiomatic method from there. Can we go the other way?

What if we say, in something like Haskell,

data nat = zero | succ nat

and define operators via pattern matching

+ :: nat -> nat -> nat
x + 0 = x
x + succ y = succ x + y

(likewise for *)

This gives us a model for the natural numbers.

Is there a formal way for extracting axioms/theorems
from this model? How might we go about proving,
say, commutativity of + from this?

Can anyone recommend any books or search terms
for further reading?

Thanks,


Marshall
From: David C. Ullrich on 2 Dec 2009 09:48
On Tue, 1 Dec 2009 07:22:46 -0800 (PST), Marshall
<marshall.spight(a)gmail.com> wrote:

>It seems a common technique for working with the natural
>numbers is to pick a set of axioms, such as Peano's,
>show the naturals are a model of those axioms, and work
>the axiomatic method from there. Can we go the other way?
>
>What if we say, in something like Haskell,
>
>data nat = zero | succ nat
>
>and define operators via pattern matching
>
>+ :: nat -> nat -> nat
>x + 0 = x
>x + succ y = succ x + y
>
>(likewise for *)
>
>This gives us a model for the natural numbers.

Do you mean "model" in precisely the formal technical
sense as in logic? (If so I don't see how this gives us a
model. If you mean "model" more informally then fine.)

>Is there a formal way for extracting axioms/theorems
>from this model? How might we go about proving,
>say, commutativity of + from this?

Starting with something that formally translates
definitions like

data nat = zero | succ nat

into either a second-order

"0 in nat & (x in nat implies succ x in nat)
&(for all S 0 in S and (x in S implies succ x in S) implies nat
subset S)"

ot the analogous first-order scheme referring to definiable
properties instead of sets.

Which I guess amounts to saying I don't quite see the point
to the question - seems to me those bits of Haskell are
just reformulations of the Peano axioms...

>Can anyone recommend any books or search terms
>for further reading?
>
>Thanks,
>
>
>Marshall

David C. Ullrich

"Understanding Godel isn't about following his formal proof.
That would make a mockery of everything Godel was up to."
(John Jones, "My talk about Godel to the post-grads."
in sci.logic.)
From: Aatu Koskensilta on 2 Dec 2009 10:00
Marshall <marshall.spight(a)gmail.com> writes:

> Is there a formal way for extracting axioms/theorems from this model?

Sure. Have a look at any exposition of constructive type theory. For a
hands-on approach perfect for someone of a Haskell turn of mind, try
your hand at Agda!

> How might we go about proving, say, commutativity of + from this?

By structural induction, of course.

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Marshall on 11 Dec 2009 12:10
On Dec 2, 6:48 am, David C. Ullrich <dullr...(a)sprynet.com> wrote:
> On Tue, 1 Dec 2009 07:22:46 -0800 (PST), Marshall <marshall.spi...(a)gmail.com> wrote:
> >It seems a common technique for working with the natural
> >numbers is to pick a set of axioms, such as Peano's,
> >show the naturals are a model of those axioms, and work
> >the axiomatic method from there. Can we go the other way?
>
> >What if we say, in something like Haskell,
>
> >data nat = zero | succ nat
>
> >and define operators via pattern matching
>
> >+ :: nat -> nat -> nat
> >x + 0 = x
> >x + succ y = succ x + y
>
> >(likewise for *)
>
> >This gives us a model for the natural numbers.
>
> Do you mean "model" in precisely the formal technical
> sense as in logic? (If so I don't see how this gives us a
> model. If you mean "model" more informally then fine.)

I'm not very good with the terminology, but it seems like
my proposal (once you include the definition for *) gives
you:

a set of values (the type "nat")
a set of symbols and their arities: zero/0 succ/1 +/2 */2
executable code for each of the symbol

This is concrete executable computer code with resource
limits, rather than an unrealized abstraction, but it seems
to qualify at least in spirit to the formal definition of "model."

Yes?


> >Is there a formal way for extracting axioms/theorems
> >from this model? How might we go about proving,
> >say, commutativity of + from this?
>
> Starting with something that formally translates
> definitions like
>
> data nat = zero | succ nat
>
> into either a second-order
>
>   "0 in nat & (x in nat implies succ x in nat)
>     &(for all S 0 in S and (x in S implies succ x in S) implies nat
> subset S)"
>
> ot the analogous first-order scheme referring to definiable
> properties instead of sets.

Oh. That mostly went over my head. Can you suggest some
introductory text?


> Which I guess amounts to saying I don't quite see the point
> to the question - seems to me those bits of Haskell are
> just reformulations of the Peano axioms...

Um, that doesn't seem right to me. It satisfies the
Peano axioms, but it isn't equivalent to them, is it?
(If that's what you meant by "refomulations".) This
is an actual implementation of the arithmetic of the
naturals, and so it shouldn't have the incompleteness
that any axiomatization of such will be subject to.

Not sure, though.


> >Can anyone recommend any books or search terms
> >for further reading?
>
> >Thanks,
>
> >Marshall
>
> David C. Ullrich
>
> "Understanding Godel isn't about following his formal proof.
> That would make a mockery of everything Godel was up to."
> (John Jones, "My talk about Godel to the post-grads."
> in sci.logic.)

From: Arturo Magidin on 11 Dec 2009 12:50
On Dec 11, 11:10 am, Marshall <marshall.spi...(a)gmail.com> wrote:
> On Dec 2, 6:48 am, David C. Ullrich <dullr...(a)sprynet.com> wrote:

> > Which I guess amounts to saying I don't quite see the point
> > to the question - seems to me those bits of Haskell are
> > just reformulations of the Peano axioms...
>
> Um, that doesn't seem right to me. It satisfies the
> Peano axioms, but it isn't equivalent to them, is it?
> (If that's what you meant by "refomulations".)

No; "reformulation" here means "a different but equivalent form".

--
Arturo Magidin
 |  Next  |  Last
Pages: 1 2 3
Prev: New Primitive Programming Language - Is it Turing Complete?
Next: The size of proper classes?