coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Formalization of the syntax of first-order logic: binders

From: Ian Shillito <Ian.Shillito AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Formalization of the syntax of first-order logic: binders
Date: Mon, 11 Oct 2021 08:41:22 +0000
Accept-language: en-AU, en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=Cu10nI9HeKzx/9cLNNIE63Vjqf9DT7zp7lRlb75MRWY=; b=VldB2XmEDowwEu8prMO7l+L3VkGl93JwvFvW9QDEKx+3MyO6TjUp2kqE/TBafYpJGm1pHezsHqT4rGKEeW4nPsKAs06CsZOaypaBT0E2kWTwnlzz5Ox2Vu/UB6JtihX71+mx9kBnrSaDTky7bFCN0oJCXct7+J2hdKQ95JQ+oEAhlm5l5KDsJGndB/3wSA5dgFggWblDVRpJH9atTq53gGjD753qhzGxGI2UJ67rmWiWOOhugkpDP9g822YfxMYWuy2zLNGiBBR2y2G2ELsWbD/hhLLjhwp29ZyMGvG76xIJdvqJM4t5608cElc6jKN+6We4QONyxxqDgUSBBtzowA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=DJVF1tpT3/FbdgXe5snVdrGD+h8Mew1+H8EZoN7tReoW53xRvo7g5nd2js71WsdfLJOO/xi5e6R1a01qI0d8Lwq6XzAJSsv5D2VjLgEd5FWY3ZH5oMzDsXqAoEqkMXTNHBMZMeCGomIWYKox3tAqUy8p7O/nAqb41GI1VER2LnQzlpVJyV+yiy+DfbQ98R4Q0RYxPBEMeYqpXR2b5hJvM/ybeNDVUm7LzIyCYDYKPyzmAKDZwys2AW5NsDzRnJDIFxCLd9HaSzPeHAt50jw/Zv8J2B16cA5vMF+Mb7VTfP6gZN/CFvwbHYb2aSe8C/Td5CCoRm4SC71rNT1Hz0CL6g==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Ian.Shillito AT anu.edu.au; spf=Pass smtp.mailfrom=Ian.Shillito AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME3-obe.outbound.protection.outlook.com
Ironport-hdrordr: A9a23:gtnvj6EwUBhpFmempLqFtJLXdLJyesId70hD6qkvc3Fom52j/fxGws5x6fatskd2ZJhSo6H4BEDgewKXyXcR2+Us1NiZLW3bUQeTTb2KjrGSjgEIeReOkdK1vJ0IG8cRNDSaNykYsS+O2njcLz9W+qjkzEnHv4fj5kYoaTsvR7Br7g9/BAreOFZxXhN6CZ0wE4fZztZbphK7EE5nIfiTNz0gZazuttfLnJXpbVotHBg88jSDijuu9frTDwWY5BEDSDlCqI1Sv1Qt0jaJp5lLgcvLiSM05FWjrai+X+GRj+erMfb8yvT97A+czjpAKr4RHIFq9wpF2N1HoGxa6+Uk5S1Qc/ibokmhA12duwfi1QX7zToi3Xf+1FeTgH/uptHOXj4hEcpGgrRYf3LimjAdlcA52rlK1WSC3qAnfS/ojWDz4cPFWAptkVfxqX0+kfQLh3gaSocGbqRNxLZvin+9Pa1waB4S0rpXZ9WGzfuslcp+YBefdTTUr2NvyNujUjA6GQqHWFELvoiQ3yJNlH50wkMEzIhH901wvK4VWt1B/aDJI65onLZBQosfar98Hv4IRY+yBnbWSRzBPWqOKRDsFb0BOXjKt5nriY9Frd2CadgN1t8/iZ7BWFRXuSo7fF/vE9SH2NlR/hXEUAyGLEHQIwFllupEU5jHNfHW2AG4OS8Tevqb0oYi65fgKoqO0bptcoHeEVc=
Ironport-phdr: A9a23:HO5xrRZK/ERu+NWiINqj+eL/LTF514qcDmcuAnoPtbtCf+yZ8oj4OwSHvLMx1gePDNyQtq0MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5YHfbx9MiTagbr9/LBe7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+TbxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspXzmp8qVlRwLyiCofNzA37nzZitB+gqxYvB2uqAdyzJTIbI2JLvdyYr/Rcc4cSGFcXshRTStBAoakYoUMFeUBO/tToZT9p1sPqRu+AQisBP/oyjRVgXL43rc10+I7HQ/b3AwgHtYOsHDVrNXpM6cfSvq6zK/VzTnZcfxZxCr95JLSfRA8uPyBW697fsXNx0c1DQzFkkmQppL/PzOTzukArWiV4ulkWO+uhWMqtx99rzmyyskihYfHiYwYx1HZ+Chn3Yo4IcG1RUFnbNOlH5ZdqTyWOoprTs88QmxluCk3x7sbspC1eygKzY4oxx/Za/GfboiI5BPjWP+KIThinn1lYra/iAy08Ue90OHzS9e73E5FripEjtnMtm0N2AfJ5sebTft9+0Gs0iuM2QDL8uxJLlw4mbDGJ5I9wLM8jIcfvVjAEyPshUn6krKael069uWp9+jqbLDrqoKAO4BoiwzzN7kiltC6DOglMgUBQm2W9OGh2LDt+0DyXa9EgecskqbDtZDXPcQbqbC9Aw9Syosu9xiwASq63NgFhHUJK11LdRyeg4juIF7BPur0DfCig1SwizhrwO3GPrv8DZnXNnjDirDhfapj5EFA1AozzNdf55ROBrEGPfLzRkvxtNvfDh86KQC73+HnCNBl2oMfX2KAHLOZPbvdvFOU/O4jPvWAaY0PtDrgN/Qo5OTigWInlVMAZaWp2IEYaHG8HvRoOUWZZn/sj88CH2gQuAoyVvHkiF2DUT5XY3ayXr485jYgBY28C4fDW5qhj6Kc0yemBJFZfH1GBkiWEXj0b4WER+sMaCWKL8B9lTwETKGtRJMl1RGzrwD30KFnL+rR+i0Ar53vztl15+vJlREz7zN4Fcqd03veB11zyykDQCZz16Riq2R8zE2C2O52mbYQQddU/rZCVhowHZ/a1e1zTd7oDFHvZNCMHXevRJ2dATA1StMtxJdaQk97Xe6ijxTH3jatK7YTivqGCIFy+7+KjCu5HNp013uTjPpptFIhWMYabQVOaYZ28RWVCoLU1UyExf/CnUE01SjQsmqP0CyHoRMAOOaReYz4ZihGI2779pH+7E6ESKKyA7M6NAcH0dSFNqZBdtzuixNBWevnP9PdJWm2njXpbSs=
Suggested_attachment_session_id: 4eac8104-a0f6-00c7-ab83-8b924c7ad1b2

Hi all,

I am about to start the formalisation of a proof of completeness for an extension of first-order intuitionistic logic. As a consequence I need to find a way to formalise the quantifiers of the FO syntax, and thus formalise binders.

It seems that there are already some approaches in the literature using:

de Bruijn indices (https://www.ps.uni-saarland.de/autosubst/ put in action in https://www.ps.uni-saarland.de/extras/fol-completeness/)
locally nameless (https://github.com/plclub/lngen could be used here?)

Are there arguments for using the one over the other? Are there other approaches? Do you have any experience to share about the formalisation of FO syntax?

Thanks in advance for your comments and thoughts!

Best,

Ian

[Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/11/2021
- Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Wilayat Khan, 10/11/2021
  - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Pierre Courtieu, 10/11/2021
    - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Carlos Olarte, 10/11/2021
      - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/12/2021
        
        RE: [Coq-Club] Formalization of the syntax of first-order logic: binders, Jason Hu, 10/12/2021
        
        RE: [Coq-Club] Formalization of the syntax of first-order logic: binders, Alan Schmitt, 10/12/2021
        
        Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Dominik Kirst, 10/12/2021
        Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/14/2021