## Stream: Coq users

### Topic: How to prove countability of formulas?

#### 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: Jun 18 2024 at 10:02 UTC