502 – Propositional logic | A kind of library

502 – Propositional logic

1. Introduction

These notes follow closely notes originally developed by Alexander Kechris for the course Math 6c at Caltech.

Somewhat informally, a proposition is a statement which is either true or false. Whichever the case, we call this its truth value.

Example 1 “There are infinitely many primes”; “ ${5>3}$ ”; and “14 is a square number” are propositions. A statement like “ ${x}$ is odd,” (a “propositional function”) is not a proposition since its truth depends on the value of ${x}$ (but it becomes one when ${x}$ is substituted by a particular number).

Informally still, a propositional connective combines individual propositions into a compound one so that its truth or falsity depends only on the truth or falsity of the components. The most common connectives are:

Not (negation), ${\lnot,}$
And (conjunction), ${\wedge,}$
Or (disjunction), ${\vee,}$
Implies (implication), ${\rightarrow,}$
Iff (equivalence), ${\leftrightarrow.}$

A word of warning is in order: The precise mathematical meaning of a connective (say, ${\rightarrow}$ ) should not be confused with the somewhat ambiguous meaning of the word (say, “implies”) used to name it. The intended mathematical meanings of the connectives are as follows:

“Not” ( ${\lnot}$ ) is a unary connective, i.e., it applies to only one proposition, and negates its truth value. There are other, less common, unary connectives: One that always returns a false value regardless of the truth or falsity of the proposition it is applied to, one that always returns a true value, and one that simply returns the same value of the proposition it is applied to. The other connectives mentioned above are binary, i.e., they bind two propositions:
A proposition combining its components with “and” ( ${\wedge}$ ) is true when, and only when both of its components are true.
A proposition combining its components with “or” ( ${\vee}$ ) is true whenever either or both of its components are true. That is, ${\vee}$ is the so-called “inclusive or.”
The “iff” (“if and only if”) or equivalence connective ( ${\leftrightarrow}$ ) is true precisely when both of its components have the same truth value, be it true or false.
Unlike the previous connectives, the “implication” ( ${\rightarrow}$ ) is not symmetric: ${p\rightarrow q}$ is not the same as ${q\rightarrow p.}$ When we use ${p\rightarrow q,}$ we intend to convey the meaning that whenever ${p}$ is true, ${q}$ must also be. So if ${p}$ is true, ${p\rightarrow q}$ is true if and only if ${q}$ is also true. If, on the other hand, ${p}$ is false, then ${p\rightarrow q}$ is also true (we say it is “vacuously” true). The statement that ${p\rightarrow q}$ does not carry any “causal” connotation, unlike the English phrases we use (for lack of anything better) to pronounce it (such as “ ${p}$ implies ${q}$ ” or “if ${p,}$ then ${q}$ ”).

We can summarize the meanings of these connectives using truth tables:

Of course, there are other binary connectives, and there are also ternary connectives, and connectives of even higher arity.

There are many different ways of expressing a compound statement, and corresponding to these there are different equivalent ways of combining propositions using these connectives: Their truth values are the same for any truth values of the original propositions. Here are some examples:

The statements
$\displaystyle (\lnot p)\vee (\lnot q) \quad\text{and}\quad \lnot(p \wedge q)$

are equivalent. This is one of what are known as De Morgan’s Laws.
The law of the double negative says that ${\lnot\lnot p}$ and ${p}$ are equivalent. That is, if something is not false, it is true, and vice versa.
The statements
$\displaystyle (p\rightarrow q) \quad\text{and}\quad (\lnot q)\rightarrow(\lnot p)$

are equivalent. The latter statement is called the contrapositive of the first. Note that because of the law of the double negative, the first statement is also equivalent to the contrapositive of the second.
Yet another way to say that ${p\rightarrow q}$ is
$\displaystyle (\lnot p)\vee q.$

One consequence of this is that we could, if we wanted to, do without the ${\rightarrow}$ connective altogether.
Two more related statements which are not equivalent to ${p\rightarrow q}$ are the converse, ${q\rightarrow p,}$ and the inverse, ${(\lnot p)\rightarrow (\lnot q).}$ The converse and inverse are contrapositives of each other, however, so they have the same truth value.

We now proceed to develop the theory of propositions in a rigorous setting.

2. Syntax of propositional logic

In order to rigorously prove results about the structure and truth of propositions and their connectives, we begin by developing a formal language, the language of propositional logic. Later, just as in the example of the tree system presented before, we will assign a semantic to this language.

Definition 1 In the language of propositional logic we have the following list of symbols:

Propositional variables. This is an infinite list ${p_1,p_2,p_2,\dots}$ of symbols. We often use ${p,q,r,\dots}$ to denote propositional variables.

Symbols for the propositional connectives ${\lnot}$ and ${\rightarrow.}$

Parentheses: ${(, ).}$

It does not matter what the propositional variables or the connectives actually are, for example, we can begin with any (countable) infinite set, and decide that its elements are the propostional variables. Our only requirement is that the symbols ${\lnot,\rightarrow,(,}$ and ${)}$ are distinct from one another, and from the propositional variables.

We could also have symbols for ${\land,\lor,\leftrightarrow}$ and for additional connectives. In order to simplify the presentation, I will restrict myself to the language above.

As before, a string or word is any finite sequence of the symbols in the language, including the empty string. Its length is its domain, just as before. Unlike the example of the tree-system, now we are only interested in certain strings, those that “represent” formulas. There are several conventions we could follow; for example, we could state that ${p\rightarrow q,}$ ${(p\rightarrow q),}$ or ${(p)\rightarrow(q)}$ are formulas. To simplify the presentation, we restrict ourselves to only one of these options.

We will refer to the “grammatically correct” strings (those formed according to the conventions below) as well-formed formulas (wffs) or just formulas.

Definition 2 (Well-Formed Formulas)

Every propositional variable ${p}$ is a wff.

If ${A}$ is a wff, so is ${\lnot A.}$

If ${A,B}$ are formulas, so is ${(A\rightarrow B).}$

Thus a string ${A}$ is a wff exactly when there is a finite sequence

$\displaystyle A_1,\dots ,A_n$

(called a parsing sequence) such that ${A_n=A}$ and for each ${1\leq i\leq n,}$ one of the following holds:

${A_i}$ is a propositional variable, or
For some ${j<i,}$ ${A_i=\lnot A_j,}$ or
For some ${j,k<i,}$ ${A_i=(A_j\rightarrow A_k).}$

Example 2

${(p\rightarrow (q\rightarrow r))}$ is a wff with parsing sequence
${p,}$ ${q,}$ ${r,}$ ${(q\rightarrow r),}$ ${(p\rightarrow (q\rightarrow r)).}$

Note that

${q,}$ ${r,}$ ${(q\rightarrow r),}$ ${p,}$ ${(p\rightarrow (q\rightarrow r))}$

is another parsing sequence, so parsing sequences are not unique.

${(\lnot (p\rightarrow q)\rightarrow (\lnot p\rightarrow \lnot q))}$ is a wff with parsing sequence
${p,}$ ${q,}$ ${(p\rightarrow q),}$ ${\lnot (p\rightarrow q),}$ ${\lnot p,}$ ${\lnot q,}$ ${(\lnot p\rightarrow\lnot q),}$ ${(\lnot (p\rightarrow q)\rightarrow(\lnot p\rightarrow\lnot q)).}$

${p\rightarrow qr,}$ ${)p\leftrightarrow,}$ ${\rightarrow (q\lnot ),}$ and ${p\rightarrow (q\rightarrow r)}$ are not wff, but to prove this requires an argument.

Remark 1 Just as in the case of the tree system, we have not yet assigned any “meaning” to any of the symbols in our formal language. Eventually, we intend to interpret symbols such as ${\rightarrow}$ in a way analogous to the propositional connective “implies,” at present they are simply symbols that we are manipulating formally.

3. Induction on formulas

We can prove properties of formulas by induction on the length of a formula. Suppose ${\Phi (A)}$ is a property of a formula ${A.}$ For example, ${\Phi (A)}$ could mean “ ${A}$ has the same number of left and right parentheses.” If ${\Phi (A)}$ holds for all formulas of length 1 (i.e. the propositional variables) and whenever ${\Phi (A)}$ holds for all formulas ${A}$ of length ${\leq n,}$ then it holds for all formulas of length ${n+1,}$ we may conclude, by induction, that ${\Phi (A)}$ holds for all formulas.

However, because of the way formulas are defined, it is most useful to use another form of induction, sometimes called induction on the construction of wff (or just induction on formulas):

Let ${\Phi (A)}$ be a property of formulas ${A.}$ Suppose:

Basis of the induction: ${\Phi (A)}$ holds, when ${A}$ is a propositional variable.
Induction step: If ${\Phi (A),\Phi (B)}$ hold for two formulas ${A,B,}$ then
$\displaystyle \Phi (\lnot A),\Phi ((A\rightarrow B))$

hold as well.

Then ${\Phi (A)}$ holds for all formulas ${A.}$ We can prove the validity of this procedure using standard mathematical induction, and the existence of a parsing sequence for any wff.

Example 3 One can easily prove, using this form of induction, that every formula ${A}$ has the same number of left and right parentheses. This result can be used to show that certain strings, for example ${)p\rightarrow,}$ are not wffs, because they have unequal numbers of left and right parentheses.

Example 4 We can easily prove by induction on the construction of wff that a nonempty proper initial segment of a formula either consists of a string of ${\lnot}$ ‘s or else has more left than right parentheses. Another easy induction shows that no formula can be empty or just a string of ${\lnot}$ ‘s, so using also the previous example, no proper initial segment of a wff is a wff.

This can also be used to show certain strings, for example, ${p\rightarrow qr,}$ are not wffs, as they contain proper initial segments that are wffs (in the example, ${p}$ ). Similar methods can be used for other non-wffs.

4. Unique readability

While parsing sequences are not unique, there is a sense in which all alternative parsing sequences offered for a given wff are “the same”: they break the wff down in the same way, to the same components, albeit in a different order. Using induction on formulas, we can prove that this will always be the case. This is called unique readability.

Theorem 3 (Unique Readability Theorem) Every wff is in exactly one of the forms:

${p}$ (i.e., a propositional variable);

${\lnot A}$ for ${A}$ a uniquely determined wff;

${(A\rightarrow B),}$ for uniquely determined wff’s ${A,B.}$

Proof: By induction on the construction of formulas, it is straightforward that any formula must be of one of these forms. To prove uniqueness first notice that no wff can be in more than one of the forms (1), (2), (3). Obviously no two propositional variables are the same, and if ${\lnot A = \lnot B,}$ then ${A=B.}$

So it is enough to show that in case (3), if ${(A\rightarrow B)=(C\rightarrow D),}$ then ${A=C}$ and ${B=D.}$ First notice that, by eliminating the left parenthesis, we have that ${A\rightarrow B)=C\rightarrow D).}$ From this it follows that either ${A}$ is an initial segment of ${C}$ or vice versa. If ${A\neq C,}$ then one of ${A,C}$ is a proper initial segment of the other, which is impossible, as they are both formulas. So we must have ${A=C.}$ Thus ${\rightarrow B)=\rightarrow D)}$ and so ${B=D.}$ $\Box$

Remark 2 Similar arguments would have given the same result if we had followed a different convention when defining formulas. For example, if we had stated that whenever ${A}$ and ${B}$ are formulas, then so is ${(A)\rightarrow(B).}$ However, not all conventions would work. For example, if we had used ${A\rightarrow B,}$ a formula such as ${A\rightarrow B\rightarrow C}$ would be “ambiguous.”

Definition 4 In form (2) we call ${\lnot}$ the main connective and in (3) we call the ${\rightarrow}$ connecting the formulas denoted above by ${A}$ and ${B,}$ the main connective. Thus the main connective is the one applied last in a parsing sequence.

Example 5 In ${((p\rightarrow (q\rightarrow p))\rightarrow q)}$ the main connective is the third “ ${\rightarrow}$ ” (from left to right).

Given a formula ${A,}$ it might be hard to recognize immediately which is the main connective. Consider for example the following formula:

$\displaystyle (((((p\rightarrow\lnot q)\rightarrow\lnot r)\rightarrow ((\lnot p\rightarrow (s\rightarrow\lnot r))\rightarrow ((q\rightarrow s)\rightarrow p)))\rightarrow$

$\displaystyle (((\lnot q\rightarrow\lnot r)\rightarrow s)\rightarrow (s\rightarrow (\lnot r\rightarrow q))))\rightarrow ((p\rightarrow (\lnot r\rightarrow s))\rightarrow (s\rightarrow\lnot r)))$

(it turns out to be the 5th “ ${\rightarrow}$ ”). There is however an easy algorithm for determining the main connective: In the formula ${(A\rightarrow B)}$ the main connective ${\rightarrow}$ is the first binary connective (from left to right) such that in the string preceding it the number of left parentheses is exactly one more than the number of right parentheses.

5. Recursive definitions

One can use the unique readability theorem to justify the following principle of definition by recursion on the construction of formulas:

Let ${X}$ be a set and let ${f : \{p_1,p_2,\dots\}\rightarrow X,}$ ${f_\lnot : X\rightarrow X,}$ and ${f_\rightarrow: X^2\rightarrow X}$ be given functions. Then there is a unique function ${g}$ from the set of all formulas into ${X}$ such that

${ g(p) = f(p)}$ for all propositional variables ${p,}$
${ g(\lnot A) = f_\lnot (g(A))}$ for any formula ${A,}$ and
${g((A\rightarrow B)) = f_\rightarrow(g(A),g(B))}$ for any formulas ${A}$ and ${B.}$

Without unique readability, the existence and uniqueness of ${g}$ would be called into question: If there were two different ways of breaking down a formula, then the corresponding compositions of the ${f}$ s might yield different values of ${g}$ for the same formula. But now that we know unique readibility, ${g}$ is well defined and unique.

Example 6

Let ${L}$ be defined according to the following clauses:

${ L(p) = 1,}$

${ L(\lnot A) = L(A)+1,}$

${ L((A\rightarrow B)) = L(A)+L(B)+3.}$

Then it is easy to see that ${L(A)=\vert A\vert =}$ the length of ${A.}$

Let

${C(P) =0,}$

${ C(\lnot A) =C(A)+1,}$

${ C((A\rightarrow B)) =C(A)+C(B)+1.}$

Then ${C(A)=}$ the number of connectives in ${A.}$

Let ${p}$ be a propositional variable and ${P}$ a formula. We define for each formula ${A}$ the formula ${g(A) = A[p/P]}$ according to the following clauses:

${ g(p) = P,}$

${ g(q) = q \quad\text{ if }q\neq p,}$

${ g(\lnot A) = \lnot g(A),}$

${ g((A\rightarrow B)) = (g(A)\rightarrow g(B)).}$

Then it is easy to see that ${A[p/P]}$ is the formula obtained by substituting every occurence of ${p}$ in ${A}$ by ${P.}$

For example, if ${A=(\lnot p\rightarrow (q\rightarrow p))}$ and ${P=(r\rightarrow q),}$ then

$\displaystyle A[p/P]=(\lnot (r\rightarrow q)\rightarrow (q\rightarrow (r\rightarrow q))).$

The parse tree ${T_A}$ of a formula ${A}$ is defined recursively as follows: The tree has a root ${\emptyset,}$ with a unique immediate successor.

In the parse tree ${T_p}$ of a propositional variable ${p,}$ this successor is labelled ${p,}$ and this is the whole tree.

In the parse tree ${T_{\lnot A},}$ this successor is labelled ${\lnot,}$ and following it there is a copy of ${T_A,}$ with the root removed.

In the parse tree ${T_{(A\rightarrow B)},}$ this successor is labelled ${\rightarrow,}$ and following it there are two immediate successors, to which we attach a copy of ${T_A}$ and a copy of ${T_B,}$ with the roots removed.

Here is an example. For clarity, I use other connectives rather than just ${\rightarrow.}$ Say that ${A=(\lnot (p\wedge q)\leftrightarrow (\lnot p\vee\lnot q)).}$ Then its parse tree is

where, again for clarity, we have omitted the root, and labelled the nodes by formulas rather than connectives.

The parse tree, starting now from the bottom up, gives us various ways of constructing a parsing sequence for the formula; for example:

${p,}$ ${q,}$ ${(p\wedge q),}$ ${\lnot (p\wedge q),}$ ${\lnot p,}$ ${\lnot q,}$ ${(\lnot p\vee\lnot q),}$ ${(\lnot (p\wedge q)\leftrightarrow (\lnot p\vee \lnot q)).}$

By unique readability, all parsing sequences can be obtained in this manner. Thus the parse tree extracts the “common part” referred to above, out of each parsing sequence.

The formulas occurring in the parse tree of a formula ${A}$ are called the subformulasof ${A.}$ These are the formulas that arise in the construction of ${A.}$ If we let ${{\rm subf}(A)}$ denote the set of subformulas of ${A,}$ then ${{\rm subf}}$ can be defined by the following recursion:

${ {\rm subf}(p) = \{p\},}$

${ {\rm subf}(\lnot A) = {\rm subf}(A)\cup\{\lnot A\},}$

${ {\rm subf}\bigl ((A\rightarrow B)\bigr ) = {\rm subf}(A)\cup{\rm subf}(B)\cup\{(A\rightarrow B)\}.}$

6. Recognizing formulas

We will next discuss an algorithm for verifying that a given string is a formula.

Given a string ${S,}$ let ${x}$ be a propositional variable not occurring in ${S}$ and let ${S(x)}$ the string we obtain from ${S}$ by substituting every propositional variable by ${x.}$

For any string ${T}$ containing only the variable ${x,}$ let ${T'}$ be the string obtained from ${T}$ as follows: If ${T}$ contains no substring (i.e. a string contained in ${T}$ as a consecutive sequence of symbols) of the form ${\lnot x}$ or ${(x\rightarrow x),}$ then ${T'=T.}$ Otherwise substitute the leftmost occurence of any one of these forms by ${x,}$ to obtain ${T'.}$ Notice that if ${T\neq T',}$ then the length of ${T'}$ is strictly smaller than that of ${T.}$

Now starting with an arbitrary string ${S,}$ form first ${S(x),}$ and then define recursively ${S_0=S(x),\ S_{n+1}=S'_n.}$ This process stops when we hit ${n_0}$ for which ${S_{n_0+1}=S'_{n_0}=S_{n_0},}$ i.e., ${S_n}$ has no substring of the above form. This must necessarily happen since otherwise we would have an infinite decreasing sequence of lengths, which is impossible.

We then have that if ${S_{n_0}=x,}$ then ${S}$ is a formula, and otherwise it is not.

Example 7

Let ${S}$ be ${((p\rightarrow (q\rightarrow \lnot p)\rightarrow (r\rightarrow (\lnot s \rightarrow t)))).}$ Then we have:

${((x\rightarrow (x\rightarrow\lnot x)\rightarrow (x\rightarrow (\lnot x\rightarrow x)))) = S(x)=S_0.}$

${ ((x\rightarrow (x\rightarrow x)\rightarrow (x\rightarrow (\lnot x\rightarrow x)))) = S_1.}$

${((x\rightarrow x\rightarrow (x\rightarrow (\lnot x\rightarrow x)))) = S_2.}$

${ ((x\rightarrow x\rightarrow (x\rightarrow (x\rightarrow x)))) = S_3.}$

${ ((x\rightarrow x\rightarrow (x\rightarrow x))) = S_4.}$

${((x\rightarrow x\rightarrow x)) = S_5=S_6.}$

So ${S}$ is not a wff.

Now let ${S}$ be ${((p\rightarrow\lnot q)\rightarrow (p\rightarrow (\lnot r\rightarrow s))).}$ Then we have:

${ ((x\rightarrow\lnot x)\rightarrow (x\rightarrow (\lnot x\rightarrow x))) = S(x)=S_0.}$

${ ((x\rightarrow x)\rightarrow (x\rightarrow (\lnot x\rightarrow x))) = S_1.}$

${ (x\rightarrow (x\rightarrow(\lnot x\rightarrow x))) = S_2.}$

${ ((x\rightarrow (x\rightarrow (x\rightarrow x))) = S_3.}$

${((x\rightarrow (x\rightarrow x)) = S_4.}$

${ (x\rightarrow x) = S_5.}$

${ x = S_6=S_7.}$

So ${S}$ is a wff.

Exercise 1 Prove the correctness of this algorithm.

7. Abbreviations

Sometimes in practice, in order to avoid complicated notation, we adopt various abbreviations in writing wff, if they do not cause any confusion.

First of all, we write ${(A\lor B)}$ instead of ${(\lnot A\rightarrow B),}$ ${(A\land B)}$ instead of ${\lnot(A\rightarrow\lnot B),}$ and ${(A\leftrightarrow B)}$ instead of the formula abbreviated by ${((A\rightarrow B)\land(B\rightarrow A)).}$

Also, we usually omit outside parentheses: We write ${A\wedge B}$ instead of ${(A\wedge B)}$ or ${(A\wedge B)\vee C}$ instead of ${((A\wedge B)\vee C),}$ etc.

We adopt an order of preference between the binary connectives, namely

$\displaystyle \wedge ,\vee ,\rightarrow ,\leftrightarrow$

where connectives from left to right bind closer, i.e., ${\wedge}$ binds closer than ${\vee ,\rightarrow , \leftrightarrow}$ ; ${\vee}$ binds closer than ${\rightarrow , \leftrightarrow}$ ; and ${\rightarrow}$ binds closer than ${\leftrightarrow.}$ So if we write ${p\wedge q\vee r}$ we really mean ${((p\wedge q)\vee r)}$ and if we write ${p\rightarrow q\vee r}$ we really mean ${(p\rightarrow (q\vee r)),}$ etc.

Finally, when we have repeated connectives, we always associate parentheses to the left, so that if we write ${A\wedge B\wedge C}$ we really mean ${((A\wedge B)\wedge C),}$ and if we write ${A\rightarrow B\rightarrow C\rightarrow D}$ we really mean ${(((A\rightarrow B)\rightarrow C)\rightarrow D).}$

All these are conventions that we follow (informally) in practice, although formally we have not introduced symbols to the language, or extended the notion of formula, and are just writing the unabbreviated forms each time.

8. A Hilbert-Type Proof System

We now describe a formal calculus of proofs. As in the example of the tree system, we start with axioms and use rules of inference to deduce consequences.

This style of arguing in formal logic, using axioms and rules, was introduced by David Hilbert and his school.

Hilbert was born in Königsberg, Prussia, in 1862, and died in Göttingen, Germany, in 1943. He is one of the most important mathematicians of the late 19-th and early 20-th century. A strong advocate of nonconstructive methods, this probably started with his work on “invariant theory,” where he proved a Basis Theorem without exhibiting an explicit basis. The paper appeared in Mathematische Annalen in 1888. (The result states that in any number of variables there is a finite set of generators for the invariants of quantics. A quantic is a symmetric tensor of a given degree constructed from tensor powers of a (finite dimensional) vector space. Invariance is measured under invertible operators of the space in itself.)

Gordon, the world expert in invariant theory, strongly opposed in vain to the publication of Hilbert’s result, due to its nonconstructive nature. On the other hand, Klein said of this result that “I do not doubt this is the most important work on general algebra that the Annalen has ever published.”

Hilbert’s work in number theory led to his book on the theory of algebraic number fields, recently translated into English. He started his work on logic with the publication in 1899 of the Grundlagen der Geometrie, where he advocates the axiomatic approach to mathematics.

In 1900 he delivered the invited address “Mathematical problems” to the Second International Congress of Mathematicians in Paris, where he listed 23 problems that in his opinion were essential for the progress of mathematics. From here comes his dictum “Here is the problem, seek the solution”. The inscription on his tombstone, “We must know, we will know” comes from a speech in Königsberg in 1938. His address can be found in the Bulletin of the AMS, vol 37, number 4 (2000).

His work on integral equations and calculus of variations led to functional analysis and the concept of Hilbert space. He also solved Waring’s problem, a well-known problem in number theory. His work in logic resulted in the development of proof systems and lead to the incompleteness theorems of K. Gödel.

8.1. Formal Proofs

A (logical) axiom is any formula of one of the following forms:

${A\rightarrow (B\rightarrow A),}$
${(A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C)),}$
${((\lnot B\rightarrow\lnot A)\rightarrow ((\lnot B\rightarrow A)\rightarrow B))}$

(for arbitrary formulas ${A,B,C}$ ).

We also have a rule of inference called modus ponens or MP: “From ${A}$ and ${A\rightarrow B,}$ derive ${B.}$ ” In formal calculi, a rule such as this for deriving one formula from others given, is sometimes written as follows:

$\displaystyle \begin{array}{c} A,\ A\rightarrow B\\ \hline B \end{array}.$

Modus ponens is short for latin “modus ponendo ponens” which means “proposing method.”.

Definition 5 Let ${S}$ be any set (finite or infinite) of formulas. A formal proof from ${S}$ is a finite sequence ${A_1, A_2,\dots ,A_n}$ of formulas such that each ${A_i}$ is either a logical axiom, belongs to ${S,}$ or comes by applying modus ponens to some ${A_j,A_k}$ with ${j,k<i}$ (i.e., ${A_k}$ is the formula ${A_j \rightarrow A_n}$ ). We call this sequence a formal proof of ${A_n}$ from ${S.}$

Definition 6 If there is a formal proof of a formula ${A}$ from ${S}$ we say that ${A}$ is a formal theorem of ${S}$ and write

$\displaystyle S\vdash A.$

If ${S=\emptyset,}$ we just write

$\displaystyle \vdash A$

and call ${A}$ a formal theorem.

Notice that ${S\vdash A}$ and ${S\subseteq S'}$ imply that ${S' \vdash A.}$ Also notice that if ${S'\vdash A}$ and ${S\vdash B}$ for all ${B\in S',}$ then ${S\vdash A,}$ since the formal proofs can simply be concatenated. Finally, ${S\vdash A}$ implies that there is finite ${S_0\subseteq S}$ with ${S_0\vdash A,}$ since a formal proof can only be finitely long and hence can only use finitely many formulas of ${S.}$

Example 8 Let ${S=\{(A\rightarrow B),\ A\rightarrow(B\rightarrow C), A\}.}$ Here is a formal proof of ${C}$ from ${S}$ :

${ A\rightarrow (B\rightarrow C)}$ (in ${S}$ ),

${((A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C)))}$ (axiom (2)),

${(A\rightarrow B)\rightarrow (A\rightarrow C)}$ (MP from 1, 2),

${A\rightarrow B}$ (in ${S}$ ),

${A\rightarrow C}$ (MP from 3, 4),

${ A}$ (in ${S}$ ),

${C}$ (MP from 5, 6)

In the proof above, I have listed next to each formula the reason why it can be written down. Just as in the case of proofs in the tree system, formally, the proof is just the sequence of formulas, without the companion explanations:

${ A\rightarrow (B\rightarrow C),}$ ${((A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C))),}$ ${(A\rightarrow B)\rightarrow (A\rightarrow C),}$ ${A\rightarrow B,}$ ${A\rightarrow C,}$ ${A,}$ ${C.}$

Example 9 The following formal proof shows that ${\vdash A\rightarrow A}$ :

${(A\rightarrow (\underbrace{(A\rightarrow A)}_{B} \rightarrow\underbrace{A}_{C})) \rightarrow ((A\rightarrow \underbrace{(A\rightarrow A)}_{B})\rightarrow (A \rightarrow\underbrace{A}_{C}))}$ (Ax. (2)),

${A\rightarrow (\underbrace{(A\rightarrow A)}_{B} \rightarrow A)}$ (Ax. (1)),

${((A\rightarrow (A\rightarrow A))\rightarrow (A \rightarrow A))}$ (MP 1, 2),

${A\rightarrow (A\rightarrow A)}$ (Ax. (1)),

${A\rightarrow A}$ (MP 3, 4).

Typeset using LaTeX2WP. Here is a printable version of this post.

This entry was posted on Monday, September 7th, 2009 at 3:01 pm and is filed under 502: Logic and set theory. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

	ปั่นสล็อต on 414/514 The theorems of Rieman…
	Richard Kimberly Hec… on Woodin’s proof of the se…
	Is there a Borel-mea… on 414/514 Examples of Baire clas…
	Simple bijectiveness… on 580 -Some choiceless results…
	Schur’s theore… on 580 -III. Partition calcu…
	Uncountable linearly… on 403/503 – Homework …
	What is a non-constr… on On strong measure zero se…
	function from Nmathb… on Hindsight
	Cauchy Schwarz Inequ… on 275 -Positive polynomials
	What is a Cantor-sty… on 580 -Some choiceless results…
	Question about Gener… on 580 -Some choiceless results…
	Set has Measure Zero… on On strong measure zero se…
	Non-measurable subse… on 580 -Cardinal arithmetic …
	hmeng1 on 414/514 The theorems of Rieman…
	580 -Cardinal arithm… on 580 -Cardinal arithmetic …

M	T	W	T	F	S	S
	1	2	3	4	5	6
7	8	9	10	11	12	13
14	15	16	17	18	19	20
21	22	23	24	25	26	27
28	29	30

A kind of library