> > A program is a piece of a text. > But, a program is more than a text, it is a structure, parsed from text with the rules of the language . Yes, you are ri

> > A program is a piece of a text. > But, a program is more than a text, it is a structure, parsed from text with the rules of the language . Yes, you are right. By "text" I actually meant "term" or "abstract syntax tree". > Execution of the program is when we give it some input and run it. So there would be similarly an input to proofs. Proof would need to be "proven correct" for EVERY valid input, that is what compiler does for programs, proving the result of the program must be of its declared result-type. Not necessarily, not all programs require input and similarly not all proofs require input. But yes, for most cases you're right: Just as the program "output a prime number larger than <>" requires an input, so does a proof of the statement "there is a prime number larger than <>". > But a proof which proves anything is not really a proof as said by someone, it corresponds to a non-halting program. So in this sense doesn't a proof ALWAYS require that we "run" it, to prove that it terminates, and thus is a valid proof actually? Indeed, in general, running a proof and observing that it terminates is one way to ensure that it's a valid proof. However, all the proof systems (logics) used in mathematical practice correspond, under Curry–Howard correspondence, to programming languages in which any well-typed program terminates. (These programming languages are therefore in some sense quite impoverished; they are definitely not Turing-complete. However they are still rich enough to interpret all of mathematics!) Thus to ensure that a proof is valid it suffices to ensure that the corresponding program is well-typed. For the traditional proof systems used in mathematics (e.g. Zermelo–Fraenkel set theory), this is decidable, that is, it's easy to write a proof checker. For newer proof systems (e.g. homotopy type theory) the same holds, but type inference might not be decidable; therefore we declare that in order to give a full proof one also has to give all the types. > Does this require some meta-logic? Proving that a proof terminates? :-) Indeed! One possible choice for the meta-logic is "common human reasoning". Of course this is not formal, so the usual problems with informal reasoning apply. A popular alternative is PRA, "primitive-recursive arithmetic". All standard results you'll find in logics textbooks, such as Gödel's incompleteness phenomena or the Curry–Howard correspondence, can be formalized and proven within PRA. The reason why PRA is well-suited to study logical systems is because PRA itself is very weak, that is, easy to trust. In contrast, the usual logical systems used in mathematics are quite powerful, therefore conceivably (though extremely unlikely) inconsistent. In case you'd like me to upgrade "extremely unlikely" to "provably", then I have bad news for you: PRA proves that if (PRA is able to prove that any of the standard systems is consistent), then (PRA is inconsistent). So there are just two options: Either PRA itself cannot be trusted, in which case all hell breaks lose (http://spikedmath.com/183.html); http://spikedmath.com/183.html); or PRA is trustworthy, in which case PRA is not inconsistent, in which case we know that PRA is not able to verify the consistency of any of the usual proof systems. (In this analysis, I'm assuming the law of excluded middle. Without it, it's not clear that these two options are the only ones.) If you enjoyed the movie Inception, then you'll appreciate that we need a meta-meta-logic in order to talk about correctness of proofs formulated in PRA. This meta-meta-logic is almost always taken to be "common human reasoning". It could be substituted for a more formal version, for instance PRA again, but at some meta level you have to stop anyway and fall back to informality, so most logicians stop already at the meta-meta-level. (There are diminishing returns of further formalization.) Welcome to the wondrous world of mathematical logic! :-) In case you want to learn the glory details, have a lot of time at your hands and can understand German, you can watch a series of lectures I gave a couple months ago: https://www.youtube.com/playlist?list=PLR-3Jx6BfhkgjagoGM3Z15G0j5hv5i66v https://www.youtube.com/playlist?list=PLR-3Jx6BfhkgjagoGM3Z1...