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?

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?

@Cody Roux how is that different from a function `nat -> Prop`

that generates the axiom

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.

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

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

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

and in fact you can prove false from it

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

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

[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! ]

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

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!)

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: Feb 05 2023 at 07:03 UTC