coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] FOL or SOL formalization in Coq

From: roux cody <cody.roux AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] FOL or SOL formalization in Coq
Date: Mon, 17 Dec 2018 11:09:33 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cody.roux AT gmail.com; spf=Pass smtp.mailfrom=cody.roux AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f53.google.com
Ironport-phdr: 9a23:MJgD+hwlzSbkKg/XCy+O+j09IxM/srCxBDY+r6Qd1O0VIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRDnhicINT43/m/UhMJtkqxUvAmsqAZjz4POeoyZKOZyc6HbcNgHRWRBRMFRVylZD4OmaIsPEuUANvtEoIn6ulQPrQa1CA6wC+Po1zBJhmX63bc90+Q8HgDLxwMgH9cUv3TVqNX5LrsdUeewzKTRyzjIcv1Y2TD46IfScxAhp+mBUqhqccveyEkvCRnJjlKKqYzqJz+VzfgNvHKH4OpjS+2uhHIoqwFrrTipyccjlJPFiZ4SylDB7Sl5z4c1JcG4SE5metGoCodftyafN4ZwX8gsQHlotT4kxrEavZO3ZisHxZQ9yxLBdvCKcZKE7xLtWeuXPDx2nmhqeKiliBa36UWgyvPzVs2z0FtSqypKiNjMtnQU2xzN8ciLV+Jx/kmh1DuBzQzT5eZEIUc7larfNZEt2KI/lp0WsUjbHy/2nlv5jLOOe0k65uSl7/7rb7bmq5OGKYN4lwPzPr4ul8GxGeg4NxIBX2mf+eSyzr3j+kj5Ta1Wgf0xj6bYsIrWJd4cpq6kDA5YyYkj6xOlADen1NQUh2UILFVAeB6flYjmJ0nOIOzkDfe4m1mjjDBrx+nfMrL9BpXNM2PMnaz6fbd97k5c0BA8wcpe55JSELEBIej8VlX/tNzCXVcFNFm/xP+iA9Fg3KsfX3iOC+mXKvD8q1iNs/goPvnEb4gZqX6pIP8p9rj0imIpsVAYdKitm5AQbSbrTbxdP0yFbC+00Z86GmAQs19mFb24uBi5STdWIk2Kcec57zA/BpihCN6aFI+oib2Fmiy8G88PPzwUOhW3CX7tMr68dbIUcivLe51ulzUFUf6qTIpzjUjz5j+/8KJuK6/vwgNdtZ/n04IotejalBV36yctSsrAiCeCSGZ7mm5OTDgzjvhy

Hi Francisco,

There have been many such formalizations, as a few google searches will show. One of note would be O'Connor's proof of incompleteness: https://arxiv.org/pdf/cs/0505034.pdf

You might also take a look at this stackexchange answer: https://cstheory.stackexchange.com/a/10087/3984

Best,

Cody

On Mon, Dec 17, 2018 at 10:41 AM Francisco Trucco <franciscoctrucco AT gmail.com> wrote:

Hi all,

I was wondering if any of you knew of a first order logic or second order logic formalization in Coq. In particular, I am looking for something similar to Coq in Coq but with FOL or SOL.

Thanks a lot!

Francisco Trucco

[Coq-Club] FOL or SOL formalization in Coq, Francisco Trucco, 12/17/2018
- Re: [Coq-Club] FOL or SOL formalization in Coq, roux cody, 12/17/2018
  - Re: [Coq-Club] FOL or SOL formalization in Coq, Milad Ketabii, 12/17/2018
- Re: [Coq-Club] FOL or SOL formalization in Coq, Yannick Forster, 12/17/2018