3

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.

  • The following subject areas have a section they teach under what is deemed logic: Philosophy, Psychology, Rhetoric (such as seen in modern Law or Politics), Mathematics & Computer science. I mention this because the term logic is often a misunderstood term & could mean different things in those contexts. Some terminology are NOT used universally. The same words can mean something different depending on which of the topics listed teaches the so called logic. Deductive reasoning is a larger set of what logic falls under. Deductive reasoning is about certainty not the others kinds of reasoning. – Logikal May 9 at 16:04
  • 4
    @Logikal, the questioner's use of terminology is entirely appropriate. Please knock it off with the obsessive insistence that everyone in the field is mistaken. – Paul Ross May 9 at 16:26
  • 1
    Formal proof or derivation. – Mauro ALLEGRANZA May 9 at 16:36
  • See also Automated theorem proving – Mauro ALLEGRANZA May 9 at 16:46
  • 1
    @Logikal It is rather ironic that in trying to correct others about matters of logic you write "all logic is not mathematical" when you intend to say that logic is not all math. – Eliran May 9 at 17:22
4

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.

| improve this answer | |
  • 2
    Several parts of this are excellent and very relevant, like the reference to Prawitz’s argument skeletons; but I think the suggestion of “normal form” as an answer to OP’s question is really erroneous. Being in normal form is a much stronger property than being given as a fully formal argument like the OP describes — proofs written for computer verification systems like Mizar and Coq are almost never in normal form (even once fully elaborated by the type checker), and it would be infeasible to require them to be, since normalisation typically incurs massive size blowup. – Peter LeFanu Lumsdaine May 10 at 18:39
  • Thanks for your comment Peter - it is a very strong degree of formalization, and I suppose my wonder is whether there is more sense to be made of what the questioner means by "maximally rigorous" if something less rolled-out than normal form would suffice to meet their needs. Perhaps retaining this terminology for normal form might help explicate that "something a little less than maximally rigorous" is what the OP is aiming at? – Paul Ross May 10 at 18:55
4

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.

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.