Understanding where implicit assumptions enter Euclid's Proof.

[Sidharth Ghoshal]

I was exploring: https://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/euclidthm

Where part of the proof hinges on the fact $x_1 * x_2 * ... x_n > 1$. However I never saw in any part of the proof an assumption that $x_1 ... x_n$ are natural numbers. So how does that enter the proof? Also, what rigorously is "..." defined as? 

[Paul Merrell]

This part isn't explained very well on the web page, but each theorems we display on the web page each correspond to one part of a ".gh" file. In that file, we declare the variables, so x always represents a natural number within that file. (In fact in that file, the concept of integers, rationals, and real numbers isn't introduced until later, so all numbers are natural.)

Everything is very rigorously defined. The web page tries to put things in a human-readable format, so some of this isn't immediately obvious. There is a "notation help" button at the bottom of the theorem which helps explain what is going on here. The operation (<*> x) is displayed as $x_1 * x_2 * ... x_n$. Here x is a finite sequence of numbers and (<*> x) is defined as the product of the numbers in the sequence. This finite sequence is represented as a tuple. A tuple is defined in terms of ordered pairs. The tuple (A, B, C) is internally represented as (((A, B), C), 3). And then ordered pairs are defined in terms of basic arithmetic using triangular numbers. So we've been very careful here.

Paul

On Sat, Dec 8, 2018 at 9:28 PM 'Sidharth Ghoshal' via Ghilbert <ghil...@googlegroups.com> wrote:

I was exploring: https://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/euclidthm

Where part of the proof hinges on the fact $x_1 * x_2 * ... x_n > 1$. However I never saw in any part of the proof an assumption that $x_1 ... x_n$ are natural numbers. So how does that enter the proof? Also, what rigorously is "..." defined as? 

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Adam Bliss]

I clicked through to https://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/tupleproduct0 and it fails rendering with an error :

Expected x not free in (lambda x (_ A x))

Do we have a regression in the JS verifier?

[Adam Bliss]

It may also be worth noting that the important operations on Tuples, such as indexing, are defined using recursive functions; these recursive functions are not part of the base Peano axioms and were themselves defined in terms of Gödel's β function: 

https://en.m.wikipedia.org/wiki/Gödel's_β_function
https://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/df-beta

The development of the β function itself requires some theorems about prime numbers, all of which were proven from the original axioms without using recursion. E.g.:

https://ghilbert-app.appspot.com/edit/peano/peano_thms.gh/relprimex

On Sun, Dec 9, 2018, 01:58 Paul Merrell <pa...@merrells.org> wrote: