Non standard model!

Stream: lean4

[Cody Roux]

Hi all, I used the excellent Mathlib completeness theorem to build a little non-standard model! https://github.com/codyroux/compact-php/blob/43dd90a1ef52e6b95de0c590d4a910b00b918868/CompactPhp/Nonstandard.lean#L215

Not sure if it's been done before, though I feel like it is implicit in the work on independence of CH.

The only sad thing is that there is only constants and the < symbol, though adding + and × should be pretty trivial (but some tedium), and I think this gives the "usual" models.

Feedback is encouraged! Don't think I'm close to a Mathlib submission though.

[Andrés Goens]

cool! just curious, for context for someone (like myself) who doesn't know that much about logic, what's CH?

[Yaël Dillies]

Continuum Hypothesis