Formal Methods: Sentential Logic 1.3 Proofs - Johns Hopkins University

Formal Methods: Sentential Logic 1.3 Proofs

Johns Hopkins University, Fall 2018

Das Entscheidungsproblem

Historically, das Entscheidungsproblem, the decision problem, was the problem of whether there exists a decision procedure for determining what conclusions follow logically from a given [finite] set of premises.

What is a decision procedure? , The procedure has a finite instruction set. , Each instruction can be mechanically implemented, i.e., the

instruction requires no guessing, no oracles. , The procedure always terminates after a finite number of steps. In short, one can program a computer to handle the job.

Example: Determining whether an argument with a finite number of premises is truth-functionally valid by constructing a truth table.

Thus, das Entscheidungsproblem is resolvable in the affirmative for sentential logic.

The General Case

Unfortunately, the complexity of the truth table procedure grows exponentially with the number of sentence letters involved.

More significantly, it was proved in the 1930s that, in general, there is no positive resolution of das Entscheidungsproblem when one moves to logics for more sophisticated, finer-grained formal languages: there no longer is, even in principle, a grind-it-out method that can tell you which conclusions follow from which premises, in particular, which conclusions follow from the empty set.

So how is one to assess the validity of arguments in general? , To establish that an argument is invalid, find a counterexample (a

scenario in which each premise is true but the conclusion false). , To establish that an argument is valid, prove the conclusion from

the premises (in a system of derivation that is deductively sound). That there is no general decision procedure indicates that there is no method telling you which of the two options to pursue.

Real Life

So, how is one to proceed when, say, trying to resolve a conjecture? (We can think of a conjecture as having the form: Suppose blah-blah-blah. Then yah-di-dah. So one wants to know whether yah-di-dah is a logical consequence of blah-blah-blah.)

Example: , Blah-blah-blah = Peano axioms for arithmetic; , Yah-di-dah = Goldbach's conjecture, i.e., that every even number

greater than 2 is the sum of two primes. If the conjecture strikes you as correct, then search for a proof of yah-di-dah from blah-blah-blah. If you can't find a proof, you might change your mind and come to believe the conjecture is incorrect, in which case you would want to search for a counterexample. If that doesn't look promising, you might change your mind again and renew your search for a proof. And so on.

No Royal Road

In general, there is no algorithm or effective procedure for finding a counterexample if one exists (except in sentential logic).

Similarly, there is in general no algorithm or effective procedure for generating a proof of the conclusion from the premises if the argument is valid (except in sentential logic).

Even in sentential logic, the rules governing proof construction are only rules of permission telling you what you may do, not what you must do.

Thus, in constructing a proof, you need to adopt a strategy perhaps together with sub-strategies in order to derive the conclusion from the premises.

This is very different than calculating or performing a computation.

Frege's Begriffschrift

Lots of different proof systems have been developed since 1879, when Gottlieb Frege published his Begriffsschrift (literal translation: "Concept Writing") in which he set out the first syntactically rigorous system of derivation.

Innovations introduced by Frege: , Invention of a formal language , Rules of derivation s.t. proofs are syntactic constructions out of that

formal language , Whether or not a given syntactic construction is a proof of the

conclusion from the premises is decidable.

N.B. Whether a proof exists is not in general decidable, only whether a given finite construction is indeed a proof.

Whether a construction is a proof or not is decidable because the rules of proof involve only the manipulation of symbols of the formal language, and thus correctness can be judged by inspection.

Examples from the Begriffsschrift

Figure: Frege's notation for the conditional: pa pb aqq.

Figure: Frege's notation for the conditional: ppc pb aqq ppc bq pc aqqq.

Sample Argument

Consider the following argument: If Alice studies, then Alice gets good grades. If Alice doesn't study, then Alice enjoys college. If Alice doesn't get good grades, then she doesn't enjoy college. Therefore, Alice gets good grades.

Valid or not? (You should be able to figure this out with a truth table.) But, on the face of it, you might think that this argument is invalid. For how could conditional premises entail a categorical conclusion? If you do judge (1) invalid, you owe us a counterexample. If you change your mind and suspect that (1) is valid, then try proving the conclusion from the premises!

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download