Proof Systems for Sentential Logic - Johns Hopkins University

Proof Systems for Sentential Logic

Mathematical Logic I Fall 2019

Robert Rynasiewicz

October 23, 2019

Real Life

In real life, when one is trying to determine whether an argument is valid or that a conjecture is true you do one of two things.

1. If the argument is invalid (resp., the conjecture is false), then produce a counterexample.

2. If the argument is valid (resp., the conjecture true), then prove the conclusion (resp., conjecture).

Of course, if you're not sure which, you spend some time looking for a counterexample, then some time trying to set out a proof, and back and forth until eventually you eventually succeed (you hope).

SENTENTIAL LOGIC IS COMPLETELY ANOMALOUS in this regard: with a finite premise set (finite antecedent), you have a decision procedure that either finds a counterexample or else establishes that no counterexample exists.

WHAT SORTS OF PROOF PROCEDURES ARE AVAILABLE IN SENTENTIAL LOGIC FOR REAL LIFE?

Constraints on a System of Proof

Before proceeding, it will help to have some compact notation.

Notation. s indicates that is provable from in system s. Now, if proofs are supposed to convince us beyond a shadow of a doubt that the conclusion follows from the premises (resp., the conjecture is true), then certain requirements will have to be satisfied.

1. The proof system s must be sound, i.e., it must be the case that for arbitrary and that if s , then |= .

2. The proof system s must be s.t. there is an effective procedure for determining whether a given finite construction is a proof of from , for arbitrary and any decidable .

The first constraint tells you that the proof system can be trusted, the second that correctness is transparent, and thus that certainty can accompany the derivation.

Other Desiderata

There are two additional desiderata.

First, we presume that a proof is a finite syntactic object. Traditionally, systems of proof have construed them to be (finite) sequences of wff's, or partially ordered sets of wff's, or something of that flavor. Technically, there is nothing wrong with counting, say, the construction of a truth table as a proof; but it helps to be able to emphasize the distinction between logical entailment and provability by pointing out that the former is essentially a semantic concept, while the latter need not be.

Second, it's nice if there is a proof system s that is not only sound, but also complete in the sense that if |= , then s , for arbitrary and . In general, there is no guarantee that such a system exists. One does for sentential logic, as well as for 1st-order logic, but not for 2nd-order logic (as will be shown next semester).

A Lazy System

Suppose we work with just the Boolean complete set of connectives {?, }. The simplest system to institute for sentential logic is as follows. Logical Axioms: the set of all tautologies. Rules of Inference: just modus ponens (MP), which "says" that from a wff of the form ( ) and the wff , one is entitled to the wff . Def. A proof of from is a finite sequence 0, . . . , n of wff's such that n = and for each i n, (i) i is a member of , or (ii) i is a logical axiom, or (iii) there exist j, k < i s.t. i follows from j and k by MP. Then, provided is decidable, whether or not a particular finite sequence of wff's is a proof of from is also decidable. (Why?)

More on Rules of Inference

Just what is a rule of inference? In our definition of MP we invoked the notion being entitled to a wff given certain others. But what does that mean? It turns out we don't really need it. We can instead view rules of inference as sets of tuples. In particular, MP is the set of triples:

MP =df { , , | , WFF}. Then we can rewrite the third clause on the previous slide as: (iii) there exist j, k < i s.t. j , k , i MP. Proceeding in this fashion, logical axioms can also be viewed as rules of inference, viz., as sets of 1-tuples. This is not a particularly economical system. We can drop many tautologies from the set of axioms w/o loss of strength (i.e., w/o giving up completeness, although we have not shown this system complete).

A Hilbert System

It turns out that, if we restrict ourselves to the Boolean complete set of connectives {?, }, all that we need to retain as axioms are tautologies of the following three types.

Type I: ( ).

Type II: ( ( )) (( ) ( )).

Type III: (? ?) ( )

We retain MP as the sole rule of inference and carry over the definition of what constitutes a proof of from .

We get an economical system in the sense that nothing further can be dropped w/o loosing strength. But it can be notoriously difficult to work within this system.

E.g., for starters, try establishing just H (A A), where H is the Hilbert system.

This should suffice to make you suspect that, in general, there may be no effective procedure for constructing proofs.

Hilbert Theorems of a Set of Wff's

Def. is a Hilbert theorem of iff H .

Def. () =df { | H }.

So, () is just the set of Hilbert theorems of .

This definition is straightforward. But it is instructive to consider two other ways of characterizing ( ) that mimic the "bottom-up" and the "top-down" definitions of the set of wffs generated from an initial stock of sentence letters, respectfully.

The "bottom-up" method exploits the similarities between a construction sequence for building wff's and a Hilbert proof. Let n() be the set of all wff's s.t. there is a Hilbert proof of from of length n + 1. If is the set of logical axioms, then 0() = . Obviously, 0() 1() 2() ? ? ? . Now, define

() =df n().

nN

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

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

Google Online Preview   Download