Cody Roux (Jun 03 2021 at 21:24): 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?
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?
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
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.
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.
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]
Emilio Jesús Gallego Arias (Jun 03 2021 at 21:58):There is no meta-theorem that guarantees a model for your axiom set
Emilio Jesús Gallego Arias (Jun 03 2021 at 21:58):and in fact you can prove false from it
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.
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.
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! ]
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.
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!)
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: Jun 01 2023 at 11:01 UTC