3 ms·

I vaguely remember from my undergrad that formalising all proofs isn't possible, due to axiom of choice making some issues (and if you decide to abandon axiom o

• IngoBlechschmid 3y ago
  Two tiny additions: 1. In those proof assistants which don't have the axiom of choice built-in, you can still formalize proofs depending on this axiom by putting it as an extra assumption. One repository using this style which I particularly like is the one by Martín Escardó: https://www.cs.bham.ac.uk//~mhe/TypeTopology/index.html https://www.cs.bham.ac.uk//~mhe/TypeTopology/index.html He even takes care to explicitly put axioms as visible assumptions which are almost always taken for granted, such as function extensionality. 2. You don't need the axiom of choice to construct the real numbers, in fact several constructions are available (Dedekind cuts, Cauchy sequences, Cauchy processes, ...) and all do their job. It's just that without the (countable) axiom of choice, you cannot prove that the Cauchy real numbers are complete. But the other constructions work fine even in the absence of choice.
• Gajurgensen 3y ago
  Coq is constructive be default, but you can add the axiom of choice and the law of the excluded middle to make it classical (other common axioms are functional extensionality, propositional extensionality, and proof irrelevance). Perhaps you are recalling Godel's incompleteness theorem, which says that for any finite formal system (like Coq) there exists a true theorem it is unable to prove?