Agler (5.1) Symbolic Logic: Syntax, Semantics, and Proof, "Proof Construction", summary

 

by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]

[Central Entry Directory]
[Logic & Semantics, Entry Directory]
[David Agler, entry directory]
[Agler’s Symbolic Logic, entry directory]

[The following is summary. Boldface (except for metavariables) and bracketed commentary are my own. Please forgive my typos, as proofreading is incomplete. I highly recommend Agler’s excellent book. It is one of the best introductions to logic I have come across.]

 

 

 

Summary of

 

David W. Agler

 

Symbolic Logic: Syntax, Semantics, and Proof

 

Ch.5: Propositional Logic Derivations

5.1 Proof Construction

 

 

 

Brief summary:

We can use a natural deduction system in order to make proofs for the conclusions of arguments. Such a system provides derivation rules, which allow us to move forward in a proof by obtaining new propositions on the basis of previously established ones. When a conclusion is provable by means of such a system, we say that the conclusion is a syntactical consequence of, or that that it is syntactically entailed by, the premises. And to signify this we use the turnstile symbol, as for example in this argument: R∨S, ¬S ⊢ R.  If we have simply ⊢P, that means there is a proof of P or that P is a theorem. In our proofs, there are three columns. The left column gives the line number. The central column shows the proposition. And the right column gives the justification, which is either that the proposition is a premise, in which case we write ‘P’, or that it is derived from other propositions, in which case we list the line numbers of those other propositions and write the abbreviation for the derivation rule that was used.

 

 

Summary

 

Ch.5: Propositional Logic Derivations

 

In chapters 3 and 4, we used truth tables and truth trees to test for certain semantic properties of singular propositions (tautology, contradiction, contingency), sets of propositions (consistency, inconsistency, equivalence), and arguments (validity). While these tests using tables and trees are useful for these purposes, “These tests do not, however, correspond to the reasoning that takes place in daily life” (161). So in this chapter we will examine a system of natural deduction. We learn rules for deriving new propositions from given ones, and all of this is modeled on normal human reasoning.

A natural deduction system is a set of derivational rules (general steps of reasoning) that mirror everyday reasoning in certain noteworthy ways. The particular system will be called a system of propositional derivations, or PD for short. Unlike truth tables and truth trees, PD is a system of syntactic rules insofar as they are formulated on the basis of the structure of everyday reasoning.

(161)

After we learn the basics of PD, we then examine more advanced systems and study certain strategies, which will not be like normal everyday reasoning, but it can still make reasoning more efficient (161).

 

 

5.1 Proof Construction

 

The purpose of learning this system of natural deduction is to solve proofs. Agler defines proof in the following way.

Proof: A proof is a finite sequence of well-formed formulas (or propositions), each of which is either a premise, an assumption, or the result of preceding formulas and a derivation rule.

(Agler 161)

 

Agler then works through the definition part-by-part. “A proof is a finite sequence of well-formed formulas...” It is finite, meaning that it will terminate as some point. And it is made of wffs, so they should follow the formation rules we saw in section 2.3.3. The end point we call the conclusion. Continuing: “...well-formed formulas (or propositions), each of which is either a premise, an assumption, or the result of preceding formulas and a derivation rule.” Agler says that

A derivation rule is an explicitly stated rule of PD that allows for moving forward in a proof. For example, if there is a derivation rule that says whenever you have ‘P’ and ‘Q,’ you can move a step forward in the proof to the proposition ‘P∧Q,’ then this derivation rule would justify (or legitimate) ‘P∧Q’ in a proof involving ‘P’ and ‘Q.’

(Agler 162)

 

In prior chapter we used the single turnstile symbol ⊢ simply to indicate that we were dealing with a set of propositions constituting an argument. The ⊢ came right before the proposition that served as the conclusion. Now we give ⊢ a more specific sense. It means syntactical entailment. [The idea seems to be the following. Suppose we have a set of propositions with the ⊢ symbol coming before the last of them, which is the conclusion of the argument. The ⊢ means that a proof can be made on the basis of the premises, making the conclusion true. Let me quote.]

In this chapter, ‘⊢’ takes on a more precise meaning, namely, that of syntactic entailment. Thus,

P∧R ⊢ R

means that there is a proof of ‘R’ from ‘P∧R,’ or ‘R’ is a syntactic consequence of ‘P∧R.’ In the above example, ‘R’ is the conclusion of the proof, whereas ‘P∧R’ are its premises. In addition,

⊢R

means that there is a proof of ‘R,’ or that ‘R’ is a theorem. In the above example, ‘R’ is the conclusion of a proof with no premises.

The simple idea of a proof then is one that begins with a set of premises and in which each subsequent step in the proof is justified by a specified rule

(Agler 162)

There are three main columns in a proof. On the far left we give the line number. In the center we have the propositions. And on the right we have the justification or an indication of the proposition being a premise. So consider the argument:

R∨S, ¬S ⊢ R

Let us set up the premises first.

As we continue with making the proof, we will use derivation rules, which will be indicated as justifications, along with the lines they are operating on.

Our proof is complete as soon as we have arrived upon the conclusion. In the above example, we concluded the proof in line 3, since R was the conclusion of the argument: R∨S, ¬S ⊢ R. (Agler 163)

 

 

 

 

Agler, David. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman & Littlefield, 2013.