Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] The chicken or the egg problem in the foundation of mathematics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] The chicken or the egg problem in the foundation of mathematics


Chronological Thread 
  • From: Marco Servetto <marco.servetto AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] The chicken or the egg problem in the foundation of mathematics
  • Date: Fri, 16 May 2025 06:53:14 +1200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=marco.servetto AT gmail.com; spf=Pass smtp.mailfrom=marco.servetto AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f169.google.com
  • Ironport-data: A9a23:TG2U66jQfTtPVsWO+9N6nqyoX161yxQKZh0ujC45NGQN5FlHY01je htvC2vUOvfeamqgfo9wPojg8h9VuZfVydZnGgFp/Cs8Fi5jpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDtJg06/gEk35qmq5WpF5gdWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGFxtuIKkh5sNNJjtqr t4ZFQIOLSDbiLfjqF67YrEEasULKcDqOMYOsCglw2iHXLApRpfMR6iM7thdtNsyrpoWTLCOO oxDMGspNUqRC/FMEg9/5JYWme6yjX65aDBCtl+Jua0f7G3azQg327/oWDbQUoXTG5oNzxvB+ Qoq+UzgAEoDBeWS0waB/1KojNbsjSXgH7odQejQGvlC2wDKnjNCVnX6T2CTqv6gz0W6Rth3M F0R4iNorK4o9UXtQMOVYvGjiHuNvxpZStAJVuNjtlDLxa3T7AKUQGMDS1atdeDKquctH2Q38 maVuunOXxg0kryoe3Hexu+b+Gba1TcuEUcOYioNTA0g6tbloZ0ugh+ncjqFOP7l5jESMWGgq w1mvBQDa6MvYdnnPphXEHjCijOo44nDF0s7v1uGGG2i6Qx9aciuYInABbnnARRofNfxorqp5 Sdsdy2iAAYmU8vleMulHr9lIV1Rz6zZWAAweHY2d3Xbyxyj+mS4Yadb6yxkKUFiP64sIGC1P xWP5l4MvMMNYxNGiJObharhW6zGKoCwRbzYugz8NIUmjmVZLV/epX43Pxb4M57Fyxl3yvlkU XtkTSpcJS1HUPw4nWTeqxY13rgsySQzjWLVTtaT8vhU+ev2WZJhcp9caAHmRrlhvMus+VyJm /4BbZfi40sEC4XWPHKHmbP/2HhTcxDX87iv9JQPLoZu42NORAkcNhMm6eJ/I9A7xvwKy48lP BiVAydl9bY2vlWfQS3iV5ypQOqHsU9X9CpgYX4fLhyz1mI9YI2iyq4aetFlNfMk7eFvh7o8B fUMZ8zKULwFRyXl6gYtS8D3jLVjUxC32iOIHS6uOwYkc7BaGgfmx97DfynUzhcoMBaZj8UEn uCf5lvpeqZbHwVGJ+TKWc2r1GK07CQ8mvotfk7mIetzWUTL8apsIRPflvUcfsMGc03C4hC41 A+mJwgSiseQgo0y8fjP3bulqaXwGcRAP0NqJUvpxpfoCjv7p02I3p1lfNuTWwzkREfY2fmHd PpE6fPRK9gFlwt6iJV9GLNV0q4O3dvjiLtExABCHn+QTVCUJp5/A3uBz+9dn7Zsw+JHhA6IR U6/wNlWFrGXMsfDElRKBg4EbPyG5M4EiAvp8vU5D0Xr1hBZpIPdfx1pACCNryhBIJ9eEoAvm 74hsfFLzT2PsEMhN9Legx1E82iJEGc7bJwmkZMnG67utBsgzwBTQJ7bCxKu2qq1Vfd3DhAIL AOX1Y34vJYN4mrZcnE2K2rB4voFu7QKpyJx7QEjI3anp4P7o8EZjTxr3xY5dAB39il88vlSP zFrPnJlJK/V8DZPgtNCbl+WGApAJUO4/0Dt+mQNj0ncaVeibU3WDWgHIe3W1lsow2FdWTl6/ b+j12fuVwjxTvzxxicfXU1EqeTpaN5Mqinuvd+BJNvcObUXeh/njb2KSUtSjiD4EOUjgEHjj st7ztZaMKHUG3YZnPwmNtO8y78VdiGhGEVDZvNEp4YiAmDWfWCJ6wikckyeVJtEGK3XzBWeF cdrG8NoUia+3gaoqhQwJ/YFA51wrc4TyOsyQJHZDk9YjOLHtRtsiozayQbmjmxyQ9lOr9c0G rmMSx28SF6vlVlmsE6TivJbO1iIQ8gOPyz9++GXzN8nNbw+tMNUTEVj9Yfs4lu0NlN88gO2r THzQfbc79ZfxLRGm6ruFaR+BDuIF+7jadTQ8C6PnoRPSfjtLfbxsxgkrwi7HgZOYpoUdddFt ZWMl9/VwHL6uK0SY2TYvqLYEox11JiWWeZJOJj7N0thwCmIApftxzAh+GmID4NDv/0Ax8ugR iq+MNCRc/xMUfhj5XRlUQpsODdDNLbScYHhunmbvdmXLxogjTz8M9Ks8EH2YVFhdiMnP4P0D in2sa2M4u90gZttBhheId1bGL59fUHeXJU5e+3LtTW3CneihnWAsODAkTsi8TT6NWmWIv3l4 J7qRgnMSzrqgfvmlOpmio1VugEbKF1fguNqJ0IUxINQugCAVWUDKbwQDIUCBpRqiRfN7ZDfZ gzWTW4cGC74DCVlcxL93YzZZT2hJNcyY/X3Gj942HmvSXaGNNvVSv8pvCJt+Gx/dTbf3fmqY 4NWsGH5Oh+qhIplX6AP7/i8mv1q3e7e2mlOw03mjsjuGFwLNN3mDpC68NZlDkQr0v0hlXkn4 UAwTGFABVCxEAv/SJgxPXFSHx4dsXXkyDBAgeJjBjrAk93z8QGC4KSX1yLPPnkrY8EDJbpIT nTyL4dIy37DwWQd4MPFpPpw6ZKZypu38gySI6rqRAlUlKa1goji0wXuggJXJPwfFMVj/58xW 9ViD7XSxKhIFayJ5ICr9A==
  • Ironport-hdrordr: A9a23:ywycRq+kdC2XOLTZN9luk+AHI+orL9Y04lQ7vn2ZLiYlCPBw9v re58jzsCWftN9/YgBFpTntAtjkfZqYz+8W3WBzB9eftWvdyQ2VxehZhOOI/9SjIVycygc379 YYT0ERMqyJMXFKyej/pCa1G8s929WcmZrY4tv2/jNCSUVFZchbgDuRyTz2LqS1fmR77FYCeq Z0L/Anmwad
  • Ironport-phdr: A9a23:Rvhs5R1N57Ykr4UAsmDOyw0yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeFo601xwSQBduBo9t/yMPo8InYGlY8qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebgtWiDanfb9+M Bq6oAvMusUKgIZuNLs6xwfUrHdPZ+lZymRkKE6JkRr7+sm+4oNo/T5Ku/Im+c5AUKH6cLo9Q LdFEjkoMH076dPyuxXbQgSB+nUTUmMNkhpVGAfF9w31Xo3wsiThqOVw3jSRMNDsQrA1XTSi6 LprSAPthSwaOTM17H3bh8pth69dvRmvpQFww5TMbY6aOvpxfKPTc90ZS2RcQMheSyNPD5igb 4sWFecNIfpUo5X/qlYIsBCwBROsBOTqyjJQgXH5x7c63PgmEQrbwQIvAcgOsGrKo9XpKKcSV v2+wa7NzTrZdfNZxTD95JLTch8/u/GMQ6x/cdbNyUkoDA7FgVCQppbkPzORzOgCr2+b7+95W O+plmUopB1/rCK1yccwlonGmJgVylbc+Ch43Ys5OcG1RUp6bNOrHpZdtj+XOYV2TM0iQ2xmt yg0x7wHtJKnfCUHx5AqywPBZvCab4WF4xDuWeSfLzp8mn5ofq+0iRi18Uil0OL8V8+03U5Rr iVZldnMqmwN2AbJ5cidTft9+Fyh2TGJ1wzJ9u5EJkU0mbLBJJ47zb8wl4QTvV7EHi/sl0X7i rKdeEY8+uWw9ejrfrHrqoWfOoJ0kA3yLLkil8ilDeglMwUDW26W8vmi2b3n4E35W6lKgeMsk qfEsZDbJNoUq7alDwJTz40t8QywDy2839QdhXQHLExKeBaAj4XxPlHBOvH4DfOmj1Wsizhn2 unKPrP8DpjMKnXPirjhfbF6605TzAo808pT6I5TCrEEOP7zW0nxu8LEDhIhLQC43+LqBM9+2 44eQ26DHLKVPafIvVOV5+8iJ/GAZIoPtzb8L/gl6eTujXg8mVIFeKmmx4EXZ2y/Hvh8OEWWf 2DsgskfHmcWogo+S/fniFKHUTFJZnayW7gw6S08CIKjFYvDQJuij6Sb3CinBp1WenxGCleUH Hv1b4mEQesDaDqOIs99lTwJTaSuS4g41R23qAD6z6dnIfHP9y0DtZPj0cB16PfJmREz8zx0F cWd3HuXQ2F6hGNbDwMxiat4uAl2zkqJ+al+mf1RU9JJtN1TVQJvEJfGxOsyMN3oRA/dYtDBH FOvWN6hRyo8VMw838MJS0l4EtSmyBvE2nz5UPcui7WXCclsoern1H/rKpMlo56n/Kwojl19B 9BKKXXjnalnsQ7aG4/OlUyd0aesb6UVmiDXpy+Y1WTbmkZeXUZrVLndG2gFbx7TpM7y4QXZQ qWwBKg7NSNOzMeDLu1Bbdi6xU5eSqLbMc/FK3m0h3/2AB+Jwr2Wa4+/fmwH1yKbE0UejQ0P4 XGuOg03ByPnqGXbX3R1DVy6RUTq/KFlrW+jCE85ywbfd0p6y7+84QIYn9SZQvIXm6MO4WIv8 mslWlm62N3SBpyLoA8JkLx0R9Q77R8H0GvYs1c4JZm8N+V5gUZYdQ1rvkTo3hExC4NakMFso ml4hAx1YbmV1l9MbVb6ldj5J6HXJ2/u/Ruud7+e21fQ18yT87sO7/JwokvqvQWgHE4vu3t91 Nwd33yZ75TMRA0cNPC5GkM+7RN94arXeDcw+5/T/XJpOKiw9DTF3pNhBecozAqhY8YKKLmNR 2qQW4URA8mjLvBvmkD8NEpVerAPsvRtboX/KarVvczjdPxtlz+nk2ldtYV000bXsjF5VvaNx JEdhfeRwgqAUT74ylanqMH+345eNlRwViKyzzbpAIlJa+h8Z4EOXC2rKte8wZNlioTzVmJE8 3asAloH3Imifh/YPDmflUVAkF8ap3Cqg37yyjVumDZvtaeFwiHS3+PKex8OO2oNT25nxwSJQ 8D8n5URW06maBIsnR2u6BPhxqRVk694KnHaXUZCeyWew3hKaqKrrfLCZsdO7MhtqiBLSKGnZ kjcTLfhohwc2ielHm1ExTl9eSv48pn+mhV7jiqaIhMR5DLccNt7wlHE6cbCSOJN2RIJQSB5j X/cAV30M9Sy/NqSnovOqajkDzPnBsAVK3C6i9re5WOy/ggISVWnkuq2m8H7HARyyiL929RwF G3JoBv6foj3xvG/OONjcFNvAQyZiYIyEYV/n40swZAIjCJC19PFoDxdyDa1aIsKisecJDIXS DUGwsDY+l3g0UxndTeSwp7hE26a2o1nbsW7ZWUf3mQ86dpLAeGa9u8h/2M9r1ymoAbWefU4k C0azK5k7XcAiOZPowc30CiBHrc6EkxRPCiqnBONpYPbzu0fdCO0fL682VAr19WoFrqF5BpRQ mj0ZoslNSB158R7dlnL1Tegj+OsMMmVZtUVuBqOlh7GhOUAM5M9mM0Bgi9/MH78t3komKYry AZj1pagsM2bOn1gqeinVwVAOGS/NKZxsnn9yLxTlcGM08WzE4V9T38VCYDwQ6vgESpO56+6c V/fSHtm9ijdQf2FQUee8Bs08S6JScvwcSjJfD9BiowzIXvVbE1H3FJKAnNjxsR/Tkbyg5a5O EZhumJPuBii9koKmroub16lCi/evFv6NW1yEcTZdUsMqFkFvhewU4TW7/ovTX4EuMT78UrVb DTcPloADHlVCBXcVxa6YebotZ+YtLLBTuumc6mXPu7I8L0CEa/OndX2jO4Et36NLpndZCEzS a1mnBMZDTYhXJ2G0zQXF35NznyLMp7d/UbmvHUw95H38ey3Cli2u83VUOoUao8po1fv0MLhf 6aGjSJ9Y160z7sqwnnFgPga1V8W0GR1ciW1VK8HrWjLRb7RnaleC1gabTlyPY1G9fB02A4FI sPdht7vs9wwxvcoF1dIU0DgkcC1dIQLJW+6LlbOGEeMMvyPOzTKx8j9Za70R6dXia1YsBi5u DDTFEGGXHzLjz7ySxWmKv1BlgmeNR1a/ZC3K1NjUDayCt3hbRK/PZl8ijh3ibw4i3XWNHINZ Dhxd0Qey9/YpShcg/h5BylA9i8/dbjCy3vftbCJbM9I4KgOYGw8je9R7XUkxqEA6ShFQKcwg y7Otpt1pEnglOCTyz1hWR4IqzBRhYvNs18xXMeRvpRGR3vA+woAqGuKDBFf7d5sENbo/btd0 MbCiL70ADhH+tPQu8AbAoKHTaDPeGpkKhfvFDPOWUEdSiW3MGjEm0FHuPSb93nQv5Jj75a1x stIRbhcW1g4UPgdDw42eb5KaIcyVTQin7mBiccO7nfrtxjdSvJRuZXfX+6TC/HiQN58pbZBb hoMh7j/KNZLXmUU80NnY1h+2o/NHhiJNTisiihobwtxsU8UtXYnEDx11EXiZQegpnQUEKzs9 iM=
  • Ironport-sdr: 68263827_AhwprVP3VwrwiMuDYK57IFRfOAIhiM/XUoFVqEsIdI2R5bN AY7GaeLj1PRcubil6OCOgAfnbX/hDIeWAKv3LOw==

Dear Laroslav,
If I understand your ideas, you really need to read
The Busy Beaver Frontier
https://www.scottaaronson.com/papers/bb.pdf
That discusses the work
A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory
https://arxiv.org/abs/1605.04343

Basically, if you know a big enough BB, you can, conceptually, beat
Goodell, in the sense of arithmetical Platonism.

Disclaimer, I'm not a big expert so I may be misrepresenting stuff.

On Mon, 12 May 2025 at 19:09, Iaroslav Baranov <kciray8 AT gmail.com> wrote:
>
> Hi!
>
> I know that all math can be reduced to type theory (calculus of
> constructions). Type theory rules can then be implemented using Turing
> Machine so we can have perfect math machine which decices the correctness
> of any mathwork. This seems astonishing and I love it. It seems to be the
> lowest level of foundation of everything.
>
> Hovewer, the turing machine and the type theory can be expressed inside
> themselves using set theory and logic. It seems like some kind of loop.
> When I think about it, it seems very interesting. Has anyone thought about
> it? Have any researchers tried to pin down this loop, extract it out and
> formalize?
>
> Best regards,
>
> Iaroslav Baranov, Java Software Engineer
>
> kciray8 AT gmail.comtyp



Archive powered by MHonArc 2.6.19+.

Top of Page