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;
Is this the only way? Or, maybe, there are other ways too?
My definition of formulas can be found here if necessary.
Hmm, I could try proving that formulas with specific size makes finite set, too. And then use (1).
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)
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