Proofs checkable by a computer

Question

Propositional logic is decidable, meaning that for every formula we can check whether it is a logical consequence of the theory $T$ (using truth-table method for example). Also we can give a formal proof of that logical consequence in the Hilbert's axiomatic system. So both methods can prove logical validity of an argument and we can even check it by a computer in both cases. So both types of proof have the same "rigorousness". Till now I have thought that we say that a proof is formal iff it is done in a proof theory way, e.g. in Hilbert's axiomatic system. But I wouldn't call the proof by a truth-table informal since it is also checkable by a computer. The word "informal" has this connotation of not being very rigorous - meaning not checkable by a computer. I wonder how do we call then in mathematics these kinds of rigorous proofs which we can check by a computer? I mean if there is some word like "bulletproof argument" and "not bulletproof argument" mathematicians use to distinguish between the types of rigorousness of an argument?

(I'm not able to come up with a title appropriate for this question so any suggestions are appreciated)

Answer 1

The term is indeed "formal proof." The point is that there are different formal proof systems; in the context of propositional logic, truth table checking is one such system. At its most abstract, a formal proof system is just a computably enumerable set of pairs of strings (with each pair meaning "from $a$, deduce $b$").

That said, we may in some circumstances want to differentiate between such systems. For example, maybe we want to look at systems which operate by manipulating strings, so that we have a family of deduction rules $\leadsto_1,...,\leadsto_n$ taking $i_1,...,i_n$-many input strings respectively and outputting new strings, and we say that $\varphi$ is a consequence of $\Gamma$ if there is some set of "$\leadsto$-deductions" which produce $\varphi$ from the sentences in $\Gamma$. Truth table evalutation does not have this form, and so amongst the broad formal systems described above there is a particularly nice family into which truth table evaluation doesn't fall.

But ultimately I would say: "formal proof" refers to any procedure which deduces one string from a given set of strings in an accepted computer-checkable system.

• Note that the plurality of formal systems in the broad sense, with various strengths and weaknesses, is handled by theorems asserting the appropriate equivalence of these systems.

---

Motivated by the comments below, let me add that there's nothing special about propositional logic here. First-order logic also has appropriate formal proof systems, including Hilbert- and sequent-style systems; this is the content of the completeness theorem for first-order logic (which is much harder than the completeness theorem for propositional logic - see e.g. here). Indeed, propositional logic is so incredibly weak that outside of a few specialized contexts it's not really interesting; the fact that first-order logic is appropriately simple is a much more important fact.

• As a technical aside, note that there are logics which don't have appropriate formal proof systems, such as second-order logic (with the standard semantics, anyways) and infinitary logic. Such logics are generally rather complicated to study, and in some sense impossible to "actually work with." That said, such logics aren't always totally mysterious; for example, the infinitary logic $\mathcal{L}_{\omega_1,\omega}$ enjoys analogues of the compactness and completeness theorems, and a weak version of the downward Lowenheim-Skolem theorem. (Second-order logic, however, is basically always terrible; only its very weak fragments, like monadic second-order logic over very weak structures, are tame in any sense.) If you're interested in the various properties which different logics can have, the relevant term is abstract model theory - for example, Lindstrom proved that first-order logic is in a precise sense the strongest logic with the downward Lowenheim-Skolem property which has an "appropriate" proof system.