Stream: Miscellaneous

Topic: non standard integers


view this post on Zulip Cody Roux (Jun 03 2021 at 21:24):

My real question is this: is it bad form to talk about foundations on the Coq club? Years ago I left the FOM mailing list because it was a lot of bickering and it was getting pretty nasty. The crux was: ultimately these were philosophical arguments based on opinion, rather than something that can be settled with a couple lines of Gallina/Ltac.

However I quite enjoy these discussions, until they drag on or get heated. So: should I avoid them or not?

view this post on Zulip Cody Roux (Jun 03 2021 at 21:25):

Also: how would one actually generate an axioms of the form gt_n : c > S (....n_times... (S 0) ... ) for fixed but extensible n?

Is Ltac2 up to the task, or would I need something like MetaCoq?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 21:49):

@Cody Roux how is that different from a function nat -> Prop that generates the axiom

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 21:57):

But I think you are in trouble in any case, in order for the set of axioms to imply a non-standard model of N, you gotta add omega of them.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 21:58):

In FOL, thanks to compactness, the infinite extension has a model, as every finite subset has one.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 21:58):

However this is not the case in the logic of Coq [obviating co-fixpoints which I am not very familiar with]

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 21:58):

There is no meta-theorem that guarantees a model for your axiom set

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 21:58):

and in fact you can prove false from it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 21:59):

That being said, yes, you can use metaCoq to generate that, that is what I'd use.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 22:00):

Add a command to generate the number of axioms you want, but I am not sure I see the use case.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 22:01):

[By the way I dunno about if this kind of discussion is OK or not in Coq forums, but IMHO it is fine and I do enjoy it! ]

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2021 at 22:01):

But likely a good idea to continue on Zulip and for most of coq-club subscribers this may be spam.

view this post on Zulip Cody Roux (Jun 04 2021 at 01:07):

Yeah, of course, you can't axiomatize a non-standard integer.

I will note that your argument about HOL involves interpreting predicates like nat -> Prop as ranging over all possible "real" subsets of N, which usually is why you lose completeness.

A much more natural interpretation is the Henkin one, where you don't have a magic oracle to know if you have all subsets of nat, and you recover completeness, but lose categoricity of course (and so non-standard numbers come back!)

view this post on Zulip Cody Roux (Jun 04 2021 at 01:09):

But yes I agree that just having a function nat -> Prop would work, though it might be nice to have some Ltac state to increment the constant automatically.

I'm not sure why I'd like such a thing. Maybe just to make a philosophical point.


Last updated: Aug 14 2022 at 11:02 UTC