coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Iaroslav Baranov <kciray8 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] The chicken or the egg problem in the foundation of mathematics
- Date: Fri, 9 May 2025 16:48:09 +0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kciray8 AT gmail.com; spf=Pass smtp.mailfrom=kciray8 AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f181.google.com
- Ironport-data: A9a23:1B6bi6reqMGb24PBirtDXM7UP2BeBmK5YRIvgKrLsJaIsI4StFCzt garIBmOO/uINGChKtx1aIqy9xsA75XRzoRmQAU5/CE2FSlGouPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKiefHoZqTZMEE8JkQhkl/MynrlmiN24BxLlk d7pqqUzAnf8s9JPGjxSsv/rRC9H5qyo5WtF5g1mP5ingXeH/5UrJMJHTU2OByCgKmVkNrbSb /rOyri/4lTY838FYj9yuuuTnuUiG9Y+DCDW4pZkc/DKbitq+kTe5p0G2M80Mi+7vdkmc+dZk 72hvbToIesg0zaldO41C3G0GAkmVUFKFSOuzdFSfqV/wmWfG0YAzcmCA2k4FIkf5ddlBltBr /AZcmsWbEC/t8GplefTpulE3qzPLeHuNYIb/2B/lHTXVKZ/B5/ERKrO6JlT2zJYasJmR66PI ZpEL2M1PFKZM0Qn1lQ/UPrSmM+rjXjleiwIgF2QrKszpWPUyWSd1ZC3aoOOIYXWGJk9ckCwq 23FrlvdOSkhO+fO5R2731S2h+DdtHauMG4VPOblr6Y10QP7KnYoIBYRTB6wpeSzolWvXspWb U0S4Csn66YonHFHVfH4Vhy85W+b51sSAooJVeI97w6Jx+zf5APx6nU4oiBpZvUis9AHVzsQ2 QWFnomyHj4/jI22VifInluLlg+aNS8QJG4EQCYLSwoZ/tXuyL3faDqfHr6P94bl3rXI9SHM/ tyckMQpa1wuYSMj0qy6+RXWnGvpqMGZF0g64QLYWm/j5QR8DGJEW2BKwQiLhRqjBN/GJrVkg JTis5bFhAzpJc/W/BFhuM1XQNmUCw+taVUwe2JHEZg77CiK8HW+Z41W6zwWDB42bphbI26wO RGK4l85CHpv0J2CPf8fj2WZW5RC8EQcPY61PhwpRoMeO8EuLVXflM2QTRXBhDu1yyDAbp3Ty b/ALJ/0UidEYUiW5DWxQOgZ3PcqwCt4rV4/triqpylLJYG2PSbPIZ9caAXmRrlgsMus/l+Jm /4BbJDi40sEAIXDjtz/q9J7waYidyVjXcieRg0+XrLrHzeK70l9U6SLmut+ItM190mX/8+Rl kyAtoZj4AKXrRX6xc+iMxiPsZu2Bc0n/0EodzchJ0ip0HUFaIOipvVXPZgucLVtsKQpwfdoR rNXM4+NE9ZeeAThoj49VJjaqJA9VRKJgQnVATGpTgJidLFdRivI2OTeQC3RyAc0ABGai+4Cs py79waCQZM8VwVoV8nXT/S0zmKOh3sWmcMsfk6RItBsZ1nhwIN6DxPAntgbDtw+c0Td9GGK0 yKTJwkSnsjWgooP6NKSr7u1n4SoNOpfH0RhAGjQ64itBxTa5maOxYxhUv6CWzLWREfY2fyFS 71O7vfeNPYnog57g7BkGew28ZNktsrdmbBK6y9FQlPJVg2PIZF9KCCk2cJviPV89oVBs1HrZ nPVq8hoApTXCsbLC1VLGREEaN6E3vQqmjX/y/Q5DUH5xS1v9oq8TkRgEEiQuRNZMYdKHtsp8 cU5tO4Szj6PuB4gH9KFryJTrkCnDHgLVYc5vZA7Xq7vrCcWyW95XJ+NMR+uvamzaOhNPHI6f R6Spq7J3IpHymT4LnEcKHnq3Mhmv6oohixk9lE4Ggm2qoL3vcNvhBx12hYrfztR1SRCgr5SO HA0FkhbJpeu3jZPhepFVV+CAwtqWR+ToBTw73Arl2TpaVaieUKQDW86OMeLpFs49UAFdBdl3 bio8kTXehe0Q9PQhwwZRlxAh8H4a+BI5inuuZyCDtuUOZsXeh/nifKeXnUJoB7ZHs8Bvk3Li u109uJWa6egFyovj4AkKoudx5ICYQulITFcfPRf4685J2HQVzWs0zyoKUrqWMdsJeTPwHCoG f5VOcNDeBSv5hmg9glBK/Y3HIZ1u/o16P4pWLDhfzcGuoTCiAtZisvb8yymiVI7R9lrr90GF brQUDC/CU2Vu2pfnj7cjctDO1fgW+I+Wi/H4LmX/tkKRrU5i8M9VWEp07CxgWeZDxs/wTKQo zH4RvH3y85M9N1SurXCQ4R5KSe6E9fRbNiz0RuSto1OZOzfMM2VuAIyrELmDjtsPrAQeopWk LiRgeHzx2fAmqg8aEHCupy7D6ISz96DbOlWFcPWLXdhgiqJXvH30SYD42yVLZ9okstXw8uaG y+UTdSWTsFMfftw31hXZDp6PzdHLp/of4HyoS+ZhNadOCg3iADoAouuyi70UDt9aCQNBazbN ib1nPSLvfVzs4VGAU4/NcFMWpNXDgfqZvo7SofXqzKdM2iPh2GCsJvEkT4Ly2nCKluAIfbAz aP1fDrMXzXsh/iQ1/BciZJ4gTMPBnUkgeUQQFMUy+Qrtx+EVlw5PcYvGrRYLKpLkx7C9oDyP xDMS2oANR/Tfxp5dTfE3dCyeTvHW8IvPI71KAV8qgnQI22zCZibCbRsyjZ47j0kMnH/xeWgM pcF9me2IhG1xYpzSP0O4uCgx91q3e7e2mlC7HWVfxYe2PrCKe5iOL1d8AtxuejvFsjMkADaO jFwSzkUGQe0Tkn+FcsmcHlQcP3cUPUD0B1wBRpjAv6G02lY8AGE4PL6MuD3lLYEaazm4ZYQE GjvSTLlD3++gxQuVGhAhz7tqaBxAPOPWMO9KccPgOHUc76YsgwaAi/JocbDoAzONuKS/5MxW wRAO0QDOXk=
- Ironport-hdrordr: A9a23:KFWTIar0rI37n3/h83YIYSoaV5oGeYIsimQD101hICG9E/bo7v xG+c5w6faaskdyZJhNo6HiBEDiexPhHPxOkO0s1N6ZNWGMhILCFvAE0WKN+UyHJwTOssBYkY hte7VjE9HrZGIK6PrS0U2XF5IPzrC8n5xARt2z856ud2xXgm1bgTuRwzz7LnFL
- Ironport-phdr: A9a23:YdjYmRbrq0SogJ+oAVvNsS//LTED2oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1wWPBd2QsaMe1beempujcFJDyK7CikxKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizewb61+I A+qoQnNucUan49vJrgwxxbJv3BFZ/lYyWR0KF2cmBrx+t2+8Jl//SpOpvkv7dRAUaL0f6Q5S bxXEjErOH0r6cPoqBfOUxKB6mMTXWsKnBVIBRPF7AzhUZfqriT6rOt91zKEMsDwULs5RC6t7 6ZvSB/vlScHKzs0+3zZh8BskK5Wpg+qqhpiyIDWfY6VLuJzcazdc90URmRPQ9hfWDBaD4ymc 4cCFfAMMfpEo4T/oVYFsBuwBROrBOPq0jJGhWX53bc90+Q6FQHJxhIgFM8TvXvOttX6LqESU eerzKLVyjjDbO9Z2Tbn6IfSchEsouqBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvGeH4eR6T +2vl3InpB9rojip3soihIvEiI0bx17E+yt03IY7KN+kREN4fNKpEJhduz+HOoZqQM4vQG5mt Tg1x7AGvZO2cjQHxZQ5yxDQd/GKbYaF7xT+X+iSOTd1nGxpdK67ihqo8kWtyvfwWtSq3FtJt CZJj9rBum0L2hfO9MWHTuZ9/ly92TmRzQDd9+BEIEEqmqfDN5IsxKM7mIAJvkTZBCD2nV37j K+IeUUg/eil8+Hnba/npp+YLoN1ig//Prk3lsyxHOg1MRUCU3KU+eS7073j8kn5T6tQgvIql anZtYjWJcUdpqGnHw9Yypgv5wq7Aju809kVnWMLIE9bdB+ElYTlJlLDLO3gAfe6mVuskTNrx /7cPr3mB5XANnvDn6vgfbZn8UFdyAk+wMtQ55JREL4BIfbzVlXtu9zfCx81Kwq0zP3/B9Vny oweQX6PArOeMK7KrFOE/vgvLPWUZI8JpDb9LOAo6OLpjX8ggFMSYa2p3YYMZ32jBfRnI0CZY WL2jdsbEGcKuBA+TO3wh1GYXz5TfSX6Y6Vp7TYiTYmiEI3rR4a3gbXH0j3oMIdRYzVnA0qLC nPhac2uUu0FbiWMaptimT0eXKnxY4Ak3BCq8gT9zuw0faLv5iQEuMe7h5BO7OrJmERqndQVJ 8GU0mXXCnpxgntNXTg9mqZ2vU16zF6Hl6l+mf1RU9JJtLtSSglvE5nawqRhDszqHBrbd4KKQ 1e8S8T2KT40R9M1hdQJZhU1AM2s2yjKxDHiGLoJj/qODZ0w/Ljb2i3yLMdnwmeW/KYkhlgiB MBIMD7unbZxoi7UAYOBiECFj+CqeKAbiTbK73uGxHGSsVtwVQdxVeDUQilaaBKG9JL24UTNS 7LoArMiWudY4eiFLKYCKtjgjFEcAezmJMybeWW63WG5GRePwLqIKovsYWQUmivHWgAClEgI8 HCKOBJbZG/pqn/CDDFoCVPkYl/9ueh4pnShS0YozgaMJ0R/3rux8xQRiLSSUfQWlr4DvS4gr X1zEjPfl5rVANuarhsxVKpZaNI5plxA0CORtgBwOIChM7E3nkQXIEx8u0Lj0QkyC50Vy5B76 iN3ilMoeeTBgAoSElHQlYr9MbDWNGToqRWmaqqMn0rbzM7T4KAErvIxt1TkugitUEsk6XRul ddPgB7+rt3HChQfVZXpXwM57R9/8vvZaSgn7pKE/XJpOKiw9DTF3ph6YYltggblZNpZPK6eQ UXxGMwADtn+AOMvklmtKBkDOaoBvL5xNMSgefyc3aetN+s1hzOqg1NM54Vl216N/S5xIgLR9 64M2OrQng6OVjOmyUykrtiyg4dPIzcbAmu4zyHgQo9XfKx7O4gRWy+iJMi+x9M2gJCIOTYQ9 1WiHVoXiOemfBOTaxr22ggY2UkMoHOhkDe11HQuy2Bv/vfZhXaehb2yLVIOISZTSXNnjEvwL ITR7ZhSR0WuYwUz1VOk6Uv826lHtfF6JmjXT11Penu+JGVjX62s87uaNpQXudV47GMOCrT6O ADDGduf61MA3ijuHnVT3mU+fjCu4NDimgBizXiaJzB1pWbYfsd5wVHe4sbdTLhfxGljJmEwh D/JC1y7J9Ts88+TksKJseu/TWuwBrVcdCDqycWLsy7xtggISVWv2uu+nNHqC11w0iT6zdB7B Q3HqR/9Zs/g0KHwYqp3O0JvAlH78c9zHIpzx5AxiJ8n0n8fnpyJ/HADnDSWU50TyefkYXEKX zJO38/N7V2vxhh4NnzQjdGxRjCHz8BmfdX/fm4Gxnd38ZVREKnNid4M1Spt/gjj8ESIMKA7x GtCj6NpsiJSgvlV6lRxiH/GWfZLQxEeZWu1xlyJ94zs8vsRPT71N+D2jA0kxbXDRPmDul0OB ii/IMtzW38oqJ04agqE0WWvuN6+PoCMK4tC7FvM1E6Qx+lNdMBuyrxT33chYSSl+iR7roxzx R12gcPj5NjBcjoyuvL/WlkCb3X0f59Bo262y/8PwoDOmdjoR8spGy1XDsGwHLT4TXRL76Shb 0HXT1he4j+aAeaNR1bBrho26SueSdbzcCjGbHgBkYc4HUfbfhcOxltOGm19x89xAAmuwIaJn F5RwDcX6xa4rxJNzrgtLBzjSiLFowzubD4oSZ+ZJR4Q7wdY5k6TP9bMpuR0VzpV+JGstmnvY iSSehhIAGcVW0eFG0GrP7+g4sPF+vSZAez2JuXHYLGHo+hTH/mSwpfn3oxj9jeKfsKBWxsqR +U8wVZGVGtlFt7xnjwOT2kGiHuIYZfL/VGz/Sp4qs35+/PuGUru6YaJF7pOIIBv9hSx0sLhf 6abgCd0Lyod14tZnyeZjuhCmgdI22c3J2D+dNZI/TTAR6/RhKJNWhsSaicpcdBN87p5xA5Gf 8jSltLy0Ld8yP8zEVZME1L7yaTLLYQHJX+wMFTfCQOFLrODcHfIyMDtaLLsYbJVheRQ8Ra3v HzIdi2rdiTGjDTvWx21ZKtUizqHORVFpIynWhNkCGymXc2/LxPiYIYxgjoxzrk5wHjNMCRPV Fo0O1MIpbqW4yRCh/x5EGEU9XtpI96PnCOB5vXZIJIb2ROEKitxnuNepn89zukMhMmlbPl8m S+Xv8E35l//wrDJxT1gXx5D7D1MgdDT1a2HEarc/5hEH33D+UBVhVg=
- Ironport-sdr: 681df996_1GEH+JP3RToi+RlSKWjyQQ9g9OQeugtc1ocSQ6g7D238Fwr 4y1SnQQ80xYadamoCralVGOnTCUuB7bacliOsbA==
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?
- [Coq-Club] The chicken or the egg problem in the foundation of mathematics, Iaroslav Baranov, 05/09/2025
- Re: [Coq-Club] The chicken or the egg problem in the foundation of mathematics, Pierre Courtieu, 05/15/2025
- Re: [Coq-Club] The chicken or the egg problem in the foundation of mathematics, Marco Servetto, 05/15/2025
- Re: [Coq-Club] The chicken or the egg problem in the foundation of mathematics, Iaroslav Baranov, 05/16/2025
Archive powered by MHonArc 2.6.19+.