Stream: Coq users

Topic: How to prove countability of formulas?


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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: Feb 04 2023 at 22:29 UTC