Propositional Logic

The propositional calculus is a great first logistic system to study.

Introduction

Propositional Logic, or the Propositional Calculus, is a formal logic for reasoning about propositions, that is, atomic declarations that have truth values.

[It is] an example of a system with a purpose — to represent part of the architecture of logical thought. The concepts ... are very few in number, and they are very simple, precise concepts. ... The propositional calculus can easily be extended to include other fundamental aspects of reasoning. (GEB, p. 195)

Classical propositional logic is a kind of propostional logic in which the only truth values are true and false and the four operators not, and, or, and if-then, are all truth functional. That's the kind of logic described on this page.

The Formal System

We'll use Hofstadter's formalization.

Syntax

The symbols are:

p  q  r  '  <  >  ~  ∧  ∨  ⊃  [  ]

The set of formulae, also known as well-formed strings, is defined recursively as follows, with v ranging over variables, and A and B over forumulae:

Variable ::= p | q | r | v'
Formula  ::= v
          |  ~A
          |  <A∧B>
          |  <A∨B>
          |  <A⊃B>

Inference Rules

Here A and B stand for arbitrary formulas.

Rule of Joining: If A and B are theorems, so is <A∧B>.
Rule of Separation: If <A∧B> is a theorem, then A and B are also theorems.
Double-Tilde Rule: The string ~~ can be deleted from any theorem to make a new theorem. The string ~~ can be added into any theorem to make a new theorem, provided the resulting string is well-formed.
Fantasy Rule: If assuming A to be a theorem leads to B being a theorem, then <A⊃B> is a theorem.
Carry-over Rule: Inside a fantasy, any theorem from the reality one level higher can be brought in and used.
Rule of Detachment: If A and <A⊃B> are theorems, then B is a theorem.
Contrapositive Rule: <A⊃B> and <~B⊃~A> are interchangeable.
DeMorgan's Rule: <~A∧~B> and ~<A∨B> are interchangeable.
Switcheroo Rule: <A∨B> and <~A⊃B> are interchangeable.

Example Derivations ("Proofs")

[
  <p∧q>          -- assumption
  p              -- separation
  q              -- separation
  <q∧p>          -- joining
]
<<p∧q>⊃<q∧p>>    -- fantasy

[
  p              -- assumption
  [
    q            -- assumption
    p            -- carry-over
    <p∧q>        -- joining
  ]
  <q⊃<p∧q>>      -- fantasy
]
<p⊃<q⊃<p∧q>>>    -- fantasy

[
  p               -- assumption
  ~~p             -- double-tilde
]
<p⊃~~p>           -- fantasy
<~~~p⊃~p>         -- contrapositive
<~p⊃~p>           -- double-tilde
<p∨~p>            -- switcheroo

Semantics

Informal Semantics

The intended interpretations of the symbols are:

~A means "not A"
<A∧B> means "A and B are both true"
<A∨B> means "A or B (or both) are true"
<A⊃B> means "if A is true then so is B"

Do the rules make sense, intuitively, under this interpretation? Here are informal arguments to justify five of the nine rules:

(Joining) A, B ⊢ <A∧B> — agrees with our definition of "and"
The Fantasy Rule and the Rule of Detachment agree with our notion of "if-then."
The Contrapositive Rule has two parts to justify:
- <A⊃B> ⊢ <~B⊃~A> — Given A implies B. Now if you don't have B, you can't have had A.
- <~B⊃~A> ⊢ <A⊃B> — Given ~B implies ~A. Now if you do have A, you can't have had ~B, so you must have B.
The Switcheroo Rule has two parts to justify:
- <A∨B> ⊢ <~A⊃B> — Given one or both of A or B is true. Now if A is false, then B must be true.
- <~A⊃B> ⊢ <A∨B> — Given ~A implies B. Now is A is true, well A is true. But is A is false, then B is true. Either way, one of A or B is true!

Exercise: Justify the rest of the rules.

A Formal Semantics

A formal semantics is given by defining a truth function, which when given a formula, produces a truth value. The truth function must be relative to an interpretation which gives meanings to the variables.

type Interpretation = Variable → {true, false} E : Formula → Interpretation → {true, false} E p φ = φ(p) E ~A φ = true, if E A φ = false; else false E <A ∧ B> φ = true, if E A φ = true and E B φ = true; else false E <A ∨ B> φ = false, if E A φ = false and E B φ = false; else true E <A ⊃ B> φ = E <~A ∨ B> φ

Exercise: Given the semantics of classical propositional logic, evaluate:

E((~p ∧ (r ⊃ ~q)) ∨ p){p → true, q → false, r → true}

Metalogical Concerns

Soundness

There is a soundness proof for Propositional Logic. Of course, it requires logical machinery outside of the system.

Exercise: Find a soundness proof for propositional logic on the web. Skim it. You don't have to fully understand it, but try to get a sense for what is required in such a proof.

Exercise: Think about a system powerful enough that it could prove its own soundness.

Completeness

Propositional logic is complete as well. Every true statement is provable, that is, for every possible true statement, there exists a theorem.

Exercise: Find a completeness proof for propositional logic on the web. Skim it. You don't have to fully understand it, but try to get a sense for what is required in such a proof.

Decidability

Because it is sound and complete, Classical Propositional Logic is decidable. Evaluating the semantic truth function is all you need to do. If you get true, you have a theorem; if you get false, you have a nontheorem. You can also use truth tables.

x	y	~x	<x ∧ y>	<x ∨ y>	<x ⊃ y>
T	T	F	T	T	T
T	F	F	F	T	F
F	T	T	F	T	T
F	F	T	F	F	T

Usefulness

There is one area in which classical propositional logic doesn't quite sound like human thought: contradictions cannot be contained. Specifically:

[
  <p∧~p>
  p
  ~p
  [
    ~q
    p
    ~~p
  ]
  <~q⊃~~p>
  <~p⊃q>
  q
]
<<p∧~p>⊃q>

This says: from a contradiction, anything follows.

This is a result of the logic being bivalent and having the principle of the excluded middle. That is, every formula gets a truth value of true or false — no exceptions, no unknowns. So if you can show that something false is true, well, then, yeah, everything is true, and your whole mental conception of the world breaks down into meaningless where all truth values are equal.

How do humans deal with contradictions? They jump outside the system and try to repair it.

Does the propositional calculus need to be repaired? It depends on what you are using it for.

In mathematics, it works fine.
To try to mimic human thought, we can try relevance logic or paraconsistent logic.

The important thing is to understand that ⊃ only claims to be material implication and is not pretending at all to express causality.