Symbolic Logic

The basic symbols are "(", ")", and "->" (or ""), and the "letters" "a", "a´", "a´´", etc.

A finite concatenation of these symbols is called a "formula", but we will be interested here only in certain "well-formed formulae" ("wff"s).

Definitions

Any letter is a wff.
If "p" and "q" are wffs, "(p->q)" is also a wff.
If "p" and "q" are wffs, "(p->(q->p))" is a theorem.
If "p", "q" and "r" are wffs, "((p->q)->((p->(q->r))->(p->r)))" is a theorem.
If "p" and "(p->q)" are theorems and "q" is a wff, "q" is also a theorem. This rule is known as modus ponens.

Exercises

a. Show that if "p" is a wff, "(p->p)" is a theorem.

b. Suggest a definition of "proof".

Readers are invited to give their answers below.

a. Premise is true by (1), since "p" is a letter. Conclusion is trivially true by (2) and trivial replacement of "q" by "p".

No, that only shows that "(p->p)" is a wff. Wff's apparently superset theorems. [That is, not all wffs are theorems.]

b. "Proof" is a chain of any number of applications of the axioms to any valid initial wff.

This is neither satisfactory nor clear - it seems to insist there is an initial wff, uses the undefined term "valid", and is vague as to what "any number of applications of the axioms" means.

Naw...

There is an initial wff, yes; you have to apply the axioms to something. Notice that each member of "the set of letters" is an initial wff, in the above.
"Valid" did not intend to introduce an undefined term, it meant "whatever the system at hand says is a starting point"
What is so unclear about "any number"? It means zero or more.
See SemiThueGrammar?s if this entire approach is puzzling you. Fully formal proofs are equivalent to string rewriting systems. E.g. the Peters-Ritchie result.

Definition of "proof". A proof is a sequence of theorems each of which may be seen to be a theorem by an application of one of the definitions above where, for an application of #5, the theorems there denoted "p" and "(p->q)" both appear earlier in the sequence. It may be said to be a proof of the last theorem in the sequence; it may readily be converted into a proof (in the usual informal sense) that the last theorem in the sequence really is a theorem.

[That is excellent - the only change I would make is to require the sequence to be finite.]

It may be better, for some purposes, to define a proof to be a sequence of <theorem,annotation> pairs, where the annotations indicate which definitions are being applied, what wffs have been used in place of their metasyntactic variables, and (for applications of #5) which earlier theorems are being used. This makes no difference to whether any given wff has a proof.

[Good point. Such a sequence can be called an annotated proof.]

The technical name for the annotation in Natural Deduction Proofs is a "Justification" see http://ruccs.rutgers.edu/~logic/naturalDeduction2.pdf page 3

Proof that (p->p) is a theorem for any wff p.

(p->(q->p)) [#3, p, q];
((p->(q->p))->((p->((q->p)->p))->(p->p))) [#4, p, (q->p), p];
((p->((q->p)->p))->(p->p)) [#5, (p->(q->p)), ((p->((q->p)->p))->(p->p)), previous two theorems];
(p->((q->p)->p)) [#3, p, (q->p)];
(p->p) [#5, (p->((q->p)->p)), (p->p), previous two theorems].

[Almost 100%. I corrected a couple of bracketing slips in the second step.]

Note that we've effortlessly moved from basic symbols and definitions to "metasyntactic variables", etc. We've proved a metatheorem!

I (GarethMcCaughan, who put in those answers to the exercises) have a confession to make: I'm a pro (kinda sorta, anyway; PhD in pure mathematics), so the answers ought to have been good :-). The only reason why I didn't say "finite sequence" is that I was careless, by the way.

If "L" is some list of (starting) wffs, we now extend the above definition to allow any wff in L to appear, and call the resulting sequence a proof from L. An annotated proof from L is defined as you would expect. Each wff, "p", in such a sequence is termed a theorem from L,and we write "L p".

Note that when this notation is used, the fifth rule above is subtly amended so that "theorems" and "theorem" become "theorems from L" and "theorem from L".

"" is "Single Turnstile" LaTeX \vdash. It means "p is derivable from L". We sometimes use " " for mutual derivability.

One (another turnstile gif) can be found at

The next exercise is to show that if L,p q (where L is a list of wffs, and "p" and "q" are wffs), L (p->q).

SymbolicLogic is the assembler language of mathematics. But then again, so is LambdaCalculus. So is CombinatoryLogic. So is CategoryTheory. TuringMachine.

Is there a single starting point from which the others can be derived? Or does the problems of Hilbert's Program prevent this

Each can be derived from the others - they are all equivalent, just as Lisp is computationally equivalent to a TuringMachine. Each can model any or all of the others.

Can someone provide hints as to these derivations? For instance there is the ChurchTuringThesis that connects LambdaCalculus and TuringMachine s but how about LambdaCalculus to CategoryTheory etc? Is there a preferred order? ie though Lisp and turing machines are equivalent, TMs would be considered more fundamental (a theory) than Lisp (an artifact).

[See links at the end of CategoryTheory page relating to TuringMachine and LambdaCalculus]

The next stage is to introduce symbols for "and", "or" and "not". This will give us the "propositional calculus" (whereas we were previously developing the "implication calculus").

Specifics please? For instance in ISBN 0-486-26404-1 (page 12), "~" and "^" are taken as axiomatic, a v b is defined as ~(~a ^ ~b), (a -> b) is defined as ~(a ^ ~b). What makes one axiomization "better" than the other and in the one above, how would "and" and "or" be introduced?

Later, various goodies, including "exists" and "forall", can be introduced to obtain the much more powerful "predicate calculus".

The word "better" isn't really appropriate in this context. [There is no hard and fast rule as to which theorems are chosen as axioms.] You can go for (1) as few concepts as possible (so using just implication is nice), or (2) as few axioms and rules of inference as possible (in which case, there are other formalizations of the propositional calculus that use fewer), or (3) as intuitive and easy to find proofs in as possible (in which case you'd want to take "and", "or", "not", etc, as primitive and have lots of axioms and inference rules).

You can't define "and", "or" and "not" in terms of implication alone, but given implication and any one of them you can define the others. So we'll need at least one new axiom when moving from the "implication calculus" to the "propositional calculus". Another thing we could add instead of "and", "or" or "not" is "false".

Thanks. Would be grateful to have the new axiom added (say, with "and") together with the definition of the others in terms of it.

There's no great advantage in minimizing the number of axioms. We introduce the symbols "", "" and "~", which may be pronounced "and", "or" and "not", respectively. (Elsewhere, the symbol "" is often used for "not".) The axioms are augmented to involve these as shown below.

Any letter is a wff.
- If "p", "q" and "r" are wffs,
"(p->q)" is also a wff...
- and "(p q)", "(p q)" and "~p" are also wffs.
(p->(q->p))
((p->q)->((p->(q->r))->(p->r)))
p, (p->q) q (modus ponens)
(p->(q->(p q)))
((p q)->p)
((p q)->q)
(p->(p q))
(q->(p q))
((p->r)->((q->r)->((p q)->r)))
((p->q)->((p->~q)->~p))
(~~p->p)

[Having given the above, I'm beginning to doubt whether they are sufficient. It's an easy consequence that

~(p

~p), but I'm not able to show other results that I would like to be able to obtain.] Yours seems to be a good start compare http://math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf page 5 they are able to prove completeness with the same 13.

[Thanks. That is an excellent document. Completeness is indeed established, but clearly some steps need to be included here, else the exercise below is more difficult than intended.]

Exercise: show that (p q) ~(p ~q).

Here is one way to prove the first half, i.e., that (p q) ~(p ~q).

  1. (p -> q)                                                (in initial list)
  2. ((p -> q) -> ((p  ~q) -> (p -> q)))                   (Axiom 3)
  3. ((p  ~q) -> (p -> q))                                 (by Axiom 5)
  4. ((p  ~q) -> p)                                        (Axiom 7)
  5. (((p  ~q) -> p) -> (((p  ~q) -> (p -> q)) -> ((p  ~q) -> q)))  (Axiom 4)
  6. (((p  ~q) -> (p -> q)) -> ((p  ~q) -> q))            (by Axiom 5)
  7. ((p  ~q) -> q)                                        (by Axiom 5, using 3, 6)
  8. (((p  ~q) -> q) -> (((p  ~q) -> ~q) -> ~(p  ~q)))  (Axiom 12)
  9. (((p  ~q) -> ~q) -> ~(p  ~q))                        (by Axiom 5)
 10. ((p  ~q) -> ~q)                                       (Axiom 8)
 11. ~(p  ~q)                                              (by Axiom 5)

See http://us.metamath.org/mpegif/iman.html 5 steps but each "ref" has to be clicked to unwind the whole proof as these are intermediate theorems we have not yet proved. They seem to be using the same axioms and it is a good link to complement this page. MetaMath? really goes into detail.

[Thanks again. I had briefly looked at that site, but hadn't realized how useful it is. However, it seems to use a slightly different set of axioms.]

[The initial axioms have been rewritten using the "" notation.]

My understanding of "|- S" is as an abbreviation for "{} |- S" where curly brackets are the usual set notation (a theorem is a statement derivable from the empty set). In either case are "|-","," "{",and "}" metasymbols or are they part of the calculus itself? Sorry to be so picky but would be grateful for the clarification.''

Where the "" is the leading character, it is understood to be preceded by an empty list (rather than set), so no punctuation is needed. Sets are not defined yet (wait for the predicate calculus). The "" is a metasymbol. Commas and spaces are currently being used as punctuation for clarity. There's not really any difference between saying that and saying they are metasymbols. In contrast, the symbols (such as "{" and "}") needed for set theory are formally added to the (predicate) calculus when we come to introduce set theory.

The proof for a slightly different problem than the one above is given below in the format I am more familiar with (NaturalDeduction? or ND). It would be interesting to compare the proof using 1-5 + others above to see if it is longer or shorter, and number of parentheses. Also how do Assumptions ("A") and Hypotheses (indenting with "|") map to a proof of the same using axioms 1-5 + others (perhaps they could be numbered also?). I can elaborate as to what "vI","~E" etc mean but here I am just comparing forms of derivation.

Ref: http://us.metamath.org/mpegif/imor.html

 Prove:{p->q} |- ~p v q (the converse is 11 lines long)
   1 p->q       [A]
   2 |~(~p v q) [A]
   3 ||~p       [A]
   4 ||~p v q   [3 vI]
   5 ||~(~p v q)[2 R]
   6 |p         [3-5 ~E]
   7 |q         [1,6 ->E]
   8 |~p v q    [7 vI]
   9 |~(~p v q) [2 R]
  10 ~p v q     [2-9 ~E]

I am thinking of a comparison along the lines of http://cs.wallawalla.edu/KU/Logic/sequents.html which discusses Sequent/ND Systems and their advantages, disadvantages and cross-links to http://cs.wallawalla.edu/KU/Logic/Axioms.html which discusses systems such as 1-5 above also highlighting pros and cons. But it would help to compare a specific example such as the one here. Is there an algorithm that can transform an Axiomatic proof to an ND derivation or vice versa?

Here is an example of an annotated proof - it derives a rule which can be helpful in deriving further results.

To show that (p q) (~q ~p)

 1. (p -> q)                                          (in initial list)
 2. ((p -> q) -> ((p -> ~q) -> ~p))                   (Axiom 12)
 3. ((p -> ~q) -> ~p)                                 (by Axiom 5)
 4. (((p -> ~q) -> ~p) -> (~q -> ((p -> ~q) -> ~p)))  (Axiom 3)
 5. (~q -> ((p -> ~q) -> ~p))                         (by Axiom 5)
 6. (~q -> (p -> ~q))                                 (Axiom 3)
 7. ((~q -> (p -> ~q)) -> ((~q -> ((p -> ~q) -> ~p)) -> (~q -> ~p)))  (Axiom 4)
 8. ((~q -> ((p -> ~q) -> ~p)) -> (~q -> ~p))         (by Axiom 5)
 9. (~q -> ~p)                                        (by Axiom 5, using 5, 8)

An interesting paper on the historic development of SymbolicLogic (especially as it relates to programs) is at http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf. It can be seen that the formulation at the top of this page is essentially the same as Frege's (1879), which was generalized by Gentzen (1934) by his system of "Natural Deduction" which uses introduction and elimination rules for connectives. He also created an alternative formulation called the SequentCalculus?. The LambdaCalculus of AlonzoChurch (1932) was shown to correspond to Natural Deduction by W.A. Howard (1969) by the CurryHowardCorrespondence?.

The following PrologLanguage code simulates the solution to problem (a) above. It does not search for a solution (though this could be added) but executes the steps specified by the p_a rule at the program start. This calls predicate s(-LineNumber?,-Justification,-RuleAndVariables?,+Result) and passes each result to the next line. This predicate calls a() which holds each axiom. These axioms do build a structure based on the RuleAndVariables? so it helps the user experiment with different axioms and results from previous steps. The output (run in SWI-Prolog) is:

  1 p->q->p                         just([X],rule(#3))
  2 (p->q->p)->(p->(q->p)->p)->p->p just([X],rule(#4))
  3 (p-> (q->p)->p)->p->p           just([1,2],rule(#5))
  4 p->(q->p)->p                    just([X],rule(#3))
  5 p->p                            just([4,3],rule(#5))

just() is the justification (annotation) and prolog does some simplification of parentheses automatically based on associativity so it is not exactly the same as the answer at the top of page. If nothing else it shows one way of representing such axioms in a programming language.

  %Program Start
  %To Run copy/paste/save in a text file, load using consult() then type "p_a." at the "?" prompt.
  p_a :- %prob a
    s(1,['X'],['#3',p,q],S1),         %'X' means apply an aXiom
    s(2,['X'],['#4',p,(q->p),p],S2),
    s(3,[1,2],['#5',S1,S2],S3),       %use line 1 and 2
    s(4,['X'],['#3',p,(q->p)],S4),
    s(5,[4,3],['#5',S4,S3],S5),
    nl,
    wl(['//',S1,' |- ',S5]).

  %implicational calculus
  s(N,J,[D|F],S) :- %do one step
    a(F,S,D),
    wl([N,' ',S,'  ',just(J,rule(D))]).

  %rules
  a([P],P,'#1').
  a([P,Q],(P->Q),'#2').
  a([P,Q],(P->(Q->P)),'#3').
  a([P,Q,R],((P->Q)->(P->(Q->R))->(P->R)),'#4').
  a([P,(P->Q)],Q,'#5').%MP

  a([P,Q],(P->(Q->(and(P,Q)))),'#6').
  a([P,Q],(and(P,Q)->P),'#7').
  a([P,Q],(and(P,Q)->Q),'#8').
  a([P,Q],(P->or(P,Q)),'#9').
  a([P,Q],(Q->or(P,Q)),'#10').
  a([P,Q,R],((P->R)->((Q->R)->(or(P,Q)->R))),'#11').
  a([P,Q],((P->Q)->((P->not(Q))->not(P))),'#12').
  a([P],(not(not(P))->P),'#13').

  wl([]) :- nl. %write a list
  wl([A|R]) :-
    write(A),
    wl(R).
  %Program End

The wffs (p q), (p q), (p q) and ~p may be given truth assignments according to the table (T=true, F=false)

  p  q  (p  q)  (p  q)  (p  q)  ~p
  -------------------------------------
  T  T     T         T        T      F
  T  F     F         F        T      F
  F  T     T         F        T      T
  F  F     T         F        F      T

A wff A is a Tautology if and only if A is assigned T for every truth assignment of it's variables. Written as |= A. If W is a set of wffs, W |= A if every truth assignment that satisfies W also satisfies A. For both Axiomic and Natural Deduction (ND) systems they are said to be Sound and Complete if the following can be proved:

Soundness: If W A then W |= A
Completeness: If W |= A then W A

(Nice symmetry, eh?) The axioms 1-13 above can be shown to satisfy both properties. Note "axiom" #5 is really a "Rule of Inference" also known as Modus Ponens (MP) and sometimes written as

  p,p->q                           i p->q
  ------      or in the ND form:   j p
     q                             k q      [i,j MP] (or [i,j ->E])

CategoryLogic