Lessness (Aug 02 2022 at 15:14): Lessness (Aug 02 2022 at 15:14):I have the FOL formulas with arbitrary functions, relations etc. and I want to prove that formulas are countable.
The only way I can imagine is:
(1) prove that countable union of finite sets are countable;
(2) prove using (1) that finite strings/lists of finite alphabet are countable;
(3) make function that transforms formula into corresponding string/list;
(4) prove it's injective;
(5) profit!
Is this the only way? Or, maybe, there are other ways too?
My definition of formulas can be found here if necessary.
Lessness (Aug 02 2022 at 15:16):Hmm, I could try proving that formulas with specific size makes finite set, too. And then use (1).
Pierre Castéran (Aug 02 2022 at 15:34):You may have a look at Russel's paper at https://arxiv.org/pdf/cs/0505034.pdf (there is an encoding of PA). Note that we maintain his work on coq-community: https://github.com/coq-community/goedel
On MathComp's side, there is a tool for making a countable type out of a tree data type (using generic trees)
https://math-comp.github.io/htmldoc_1_14_0/mathcomp.ssreflect.choice.html
Yannick Forster (Aug 03 2022 at 07:20):You can check out the Coq code of this paper, we have a proof of countability of formulas there if I remember correctly. We need it to prove enumerability of FOL probability: https://www.ps.uni-saarland.de/extras/fol-completeness-ext/
Last updated: Sep 23 2023 at 15:01 UTC