Deductive argument in which every step and premises are explicitly stated?

Question

Is there in philosophy a word/term describing an argument in which all the premises and rules for derivation from those premises are stated explicitly so that even a computer can check it? I know that for example in the propositional logic it is possible to prove logical consequence easily by checking whether the formula is true in all cases in which the formulas of a theory T are true (e.g. by a truth-table). There is even a second option for proving it, which is formally using Hilbert's axiomatic system. The first proof is informal, the second proof is formal, yet both are equally "rigorous". Is there a word/term by which philosophers or mathematicians call an argument or a proof which is "maximally rigorous" (meaning everything is explicitly stated and it could be checked by a computer if rewritten to a programming language)? Is there also a word/term for a "weaker" form of an argument or proof (meaning that not all the steps of the reasoning are explicit - even in Hilbert's calculus if we don't explicitly state all the rules we use, I would call it in this sense "weaker" proof)?

I have found that those types of an argument are called argumentum a priori or deductive arguments. However those terms don't describe an argument in which every step is necessary explicitly stated or written down on a paper - therefore there could be a room for ambiguity if a person doesn't know anything about the propositional logic or any other system.

Answer 1

I'm not sure how closely the concepts I'm familiar with might match what you're aiming for, but I do have some familiarity with the development of Proof Theory, and your search for terms seems to line up with some ideas we've explored in that field.

In proof theory, particularly in discussions around Natural Deduction, we sometimes talk about a proof or argument being in Normal Form. A Normal Form argument is one that has been written in "the most basic way", which is to say we've formally looked at all and only the necessary premises of the argument, broken them down into component syntactic parts (via "elimination rules"), then reassembled them to structure the desired conclusions (via "introduction rules").

Not all formal arguments, or even all validly constructed formal natural deduction proofs, are in Normal Form. However, many formal systems aim to show something like a Normalization Theorem, to the effect that when any non-minimal use of our logical rules is invoked, we could without loss of generality rewrite the argument to eliminate it. One of the main proponents of this kind of work was Dag Prawitz, whose thesis on the Proof-theoretic analysis of natural deduction helped inform a lot of the philosophical writing around proof, inference and computation that would follow.

A valuable concept Prawitz introduces in his work is the notion of an "Argument Skeleton". (see his On the Idea of a General Proof Theory for a more accessible overview). This is a generalization of the tree structures involved in formal natural deduction arguments or proofs, in that we allow not only that we are working from logical axioms as premises to conclusions (which we call a Closed argument), but also that we can allow unproved antecedents that lead to consequents via the same kind of logical rules of inference - these "open argument" structures are also Argument Skeletons.

(Natural deduction often tries to do without Axioms altogether in its structures, rather deferring everything that is "purely logical" to the application of structural inference rules.)

So perhaps some useful turns of phrase might be these: your "weaker" formal arguments are Open Arguments, and their "proofs" are Argument Skeletons, since they hint at a structure of proof that could potentially be further developed. Your "stronger" arguments are Closed Arguments, in that their skeletons do not leave extra-logical assumptions dangling, and the most syntactically minimal version of such an argument (ideally suited for machine processing) would be its Normal Form.

There are alternative interpretations of this kind of work in other forms of Proof theory. Where Prawitz makes use of Argument Skeletons to support his Natural Deduction system, the more common Sequent Calculus technology developed from Hilbert's system by Gerhard Gentzen allows us to capture transformation rules for inferences, collapsing the distinction between open and closed arguments. However, understanding that distinction can help in getting a grasp for what the Sequent Calculus is doing differently, and how we can put the principles of consistency and soundness-preserving argument transformations to use in mechanically manipulating proof strings.

Answer 2

See this post about the spectrum of formality of a mathematical argument. What you described as "every step and premises are explicitly stated" would be classified as "absolutely formal" (and "formal proof" without any qualification often means this). Most mathematical arguments are not expressed as absolutely formal proofs, but rather fall under "reasonably formal". You asked for a term for proofs in a deductive system that do not explicitly state the rules used, but there is no such term because formal systems are typically designed so that it can be mechanically verified whether the rules are followed or not, and hence there is no necessity to specify which rule is used at each step, except to improve the efficiency of the verification process.

However, you seem to have a misconception about the nature of the proof of a propositional tautology via truth tables. While it is reasonable to consider it informal in the sense that you draw a table and say "look these are all the cases and the statement is true in every case", it can actually be expressed no less formally than a Hilbert-style or Fitch-style or sequent-style proof. All you need to do is to write out the table one row at a time in a systematic order (e.g. lexicographic order; for 3 variables A,B,C you would have the rows 000,001,010,011,100,101,110,111 denoting the truth-values of A,B,C), and the truth-value of the statement for each row (which can be mechanically computed). This is sometimes called a semantic proof, because it proceeds by checking the statement's truth-value (according to the semantics of propositional logic) in every situation (truth-assignment of variables). In contrast, a proof in some deductive system is a syntactic proof, because it is 'just' a matter of symbol-pushing with no regard for 'meaning'. Nevertheless, semantic proofs can clearly be just as formal as syntactic proofs, since you still need some mechanical process of verifying a syntactic proof, no less complex than a mechanical process that verifies a truth-table!

But as always, it is worth emphasizing that although we can have semantic proofs for propositional logic, it is impossible to have semantic proofs for full first-order logic (because the incompleteness theorems applied to PA− shows that there cannot be a program that can decide in finitely many steps whether an input sentence of the form "X ⇒ Y" in the language of PA is a tautology or not, where "X" is the conjunction of the axioms of PA−). So syntactic proofs remain the only fully adequate method of proof for first-order logic.