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.

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)

https://math-comp.github.io/htmldoc_1_14_0/mathcomp.ssreflect.choice.html

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: Feb 04 2023 at 22:29 UTC