7
$\begingroup$

In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established sentence and the last line is the goal. Computers can easily verify proofs like these using the rules of first-order logic.

In dependent type theory, proofs come in the form of programs, and you know your proof is correct if it can be compiled (or type-checked).

Do there exist logics/foundations where rigorous proofs can not be checked by computers? Or where a checking program might never terminate for a correct proof?

Improve this question
$\endgroup$
6
  • 2
    $\begingroup$ And a "rigorous" proof is what exactly? And by computer you mean physical computers or theoretical computers such as Turing machines? $\endgroup$
    – Somos
    Commented Oct 11, 2018 at 4:12
  • 1
    $\begingroup$ If a proof does not have a verification process, what use is the proof? Or are you imagining something that resembles a proof in some ways and not in others? Gerhard "Too Philosophical For This Forum?" Paseman, 2018.10.10. $\endgroup$
    – Gerhard Paseman
    Commented Oct 11, 2018 at 4:20
  • 1
    $\begingroup$ @Somos I mean theoretical computers. I left the notion of rigor undefined because I'm curious if there are systems which define it in a way that isn't computationally verifiable. $\endgroup$
    – Eben Kadile
    Commented Oct 11, 2018 at 4:53
  • 1
    $\begingroup$ @GerhardPaseman Good question, I'm not sure how such proofs could be considered proofs, which is why I'm so curious about it. Perhaps it's my post that is too philosophical for the forum, but this seemed like the site where it would be the most likely to get an answer. $\endgroup$
    – Eben Kadile
    Commented Oct 11, 2018 at 4:56
  • $\begingroup$ This post may answer your question: math.andrej.com/2016/08/09/what-is-a-formal-proof $\endgroup$
    – L. Garde
    Commented Oct 11, 2018 at 5:09

3 Answers 3

Reset to default
18
$\begingroup$

There are logical systems whose formal proofs are not computer verifiable. One such example is infinitary logic in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not normally considered to properly reflect the actual human activity of proving mathematical statements.

All logical systems (first-order logic, higher-order logic, type theory, etc.) whose purpose is to capture the notion of proof as done in practice, have machine verifiable proofs. The formal property needed here is semidecidability.

Supplemental: Noah Schweber points out another example of a formal logic which is not comuputer-verifiable. Namely, we could take as the axioms of our logical system all statements that are true in a certain class of mathematical structures. Depending on what this class of structures is, we might end up with a non-computable set of axioms, which then presents a problem for verifiability. Here are some examples:

  1. If we take ordinary Peano arithmetic and add to it as axioms all true sentences, we get a non-verifiable system by Gödel's incompleteness.

  2. If we take all equations in the language of a group (so we can use the group unit, operation and inverses) which hold in every group, we will get a set of equations that is already generated by the standard axioms for a group theory, and therefore semidecidable (computer-verifiable).

Improve this answer
$\endgroup$
12
  • 3
    $\begingroup$ I think this answer is slightly misleading, since after all higher-order logic has two different semantics, and the OP might not be aware of this. To the OP: under the "standard semantics," it does not have a good notion of proof, and is indeed extremely poorly behaved. It is better-behaved with respect to the "Henkin semantics," but in that guise it's really just a rephrasing of first-order logic. $\endgroup$
    – Noah Schweber
    Commented Oct 11, 2018 at 15:32
  • 2
    $\begingroup$ I disagree. Firstly because the OP asks about logical systems, not semantics. Secondly, because higher-order logic has a perfectly good notion of proof. The so-called "problem" with set-theoretic semantics (which you call "standard") is just the simple observation that particular family of models is not complete for higher-order logic. This is no surprise at all. Once we accept a wide enough class of models of higher-order logic, we obtain all the usual soundness and completeness results. (For example, we could take semantics in boolean toposes, that will do it easily.) $\endgroup$
    – Andrej Bauer
    Commented Oct 11, 2018 at 16:15
  • 3
    $\begingroup$ I would say that the semantics is part of a logical system. Regardless, my point was that if the OP googles the topic, they'll find information that appears to contradict your statement, and that can be preempted by pointing out this issue. (And in my defense, "standard semantics" isn't my term.) $\endgroup$
    – Noah Schweber
    Commented Oct 11, 2018 at 16:24
  • 1
    $\begingroup$ I know it's not your term. In any case, thanks for pointing out that there's another common way of making a non-verifiable theory: just throw in all true sentences as axioms. $\endgroup$
    – Andrej Bauer
    Commented Oct 11, 2018 at 16:29
  • 5
    $\begingroup$ It seems to me that the appropriateness of calling a particular semantics "standard" for some deductive system is, at least to some extent, a historical issue: Was the system invented in order to describe a particular structure ("standard model") or situation. So I would be comfortable talking about the standard model of Peano Arithmetic or of Euclidean geometry, or the standard semantics of second-order logic, but not, for example, a standard model of group theory. $\endgroup$
    – Andreas Blass
    Commented Oct 11, 2018 at 22:15
8
$\begingroup$

If you take "proof" as a convincing argument (to error probability smaller than arbitrary epsilon) that a proposition is true, then two other possibilities come to mind:

  • Probabilistically checkable proofs, where you have a conventional first-order proof (like your secret unpublished proof of RH) and you can convince me through a cryptographic-like protocol that you really do have a proof, without revealing how the proof works. Zero-knowledge proofs are related to this; and

  • (Due to L. Levin) if you believe there are physically realizable ways of generating algorithmically random numbers (e.g. by rolling dice), you can make almost-certainly-true but unprovable statements, like that the string produced by 1000 bits of coin flips can't be compressed to less than half its original length (this is an assertion about the Kolmogorov complexity, which is uncomputable).

It follows from the second example above that the physics assertion that you can generate random numbers through quantum processes is scientifically unverifiable, if you believe the Church-Turing thesis.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Very interesting examples! :) $\endgroup$
    – paul garrett
    Commented Oct 11, 2018 at 22:32
3
$\begingroup$

There are, of course, various constructivist and intuitionistic foundational theories which take the notion of an absolute, intuitive notion of proof as the basic primitive notion. It is well known that it cannot coincide with any mechanically checkable notion of proof (if one sticks to any standard intuitionistic logic, then the totality of axioms cannot be decidable). It is, though, debatable just how rigorous this then is.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Could you please provide some references to such foundational theories? $\endgroup$
    – Andrej Bauer
    Commented Oct 11, 2018 at 19:11
  • $\begingroup$ @AndrejBauer If I recall correctly, Brouwer was strongly opposed to axiomatic approaches to intuitionism. Does that count? $\endgroup$
    – Noah Schweber
    Commented Oct 11, 2018 at 19:13
  • 1
    $\begingroup$ Well, no, because Brouwer did not actuallly specify anything that we might call a formal system. My understanding of Brouwer is that his position and views would be closer to a kind of semantics of truth, not a formal system. But there might be some accounts of Brouwer's that explain the Brouwerian position in terms of formal systems, which I would be interested to see. $\endgroup$
    – Andrej Bauer
    Commented Oct 11, 2018 at 19:16
  • 1
    $\begingroup$ @Andrej Bauer: as a contemporary example, I think that many of the works in intuitionistic Reverse Mathematics prefer not to specify any formal system - occasionally they will accept "Bishop's system", but their work is not intended to be read as formalized in any particular formal base theory. $\endgroup$
    – Carl Mummert
    Commented Oct 12, 2018 at 15:09
  • $\begingroup$ @CarlMummert: that's a good point. Come to think of it, early versions of Per Martin-Löf's treatment of type theory probably come close to what I am asking for. He is very formal but also considers the formalism to be inextricably linked to the meaning explanations. Early versions of his type theory had strange features. Decidability of type-checking was a later development. $\endgroup$
    – Andrej Bauer
    Commented Oct 13, 2018 at 7:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .