Maths - Propositional Logic- Martin Baker

Maths - Propositional Logic

The Language

The language in which propositions or assertions are written consists of a recursively defined term:

A term (formula) is either:

The alpha set A is a finite set of elements called
proposition symbols or propositional variables,
otherwise referred to as atomic formulae or
terminal elements.

A variable: X₀, X₁, X₂ ...

Or the omega set Ω is a finite set of elements called
operator symbols or logical connectives. The set
Ω is partitioned into disjoint subsets as follows:

A /\ B	A and B
A \/ B	A or B
A => B	A implies B
A <=> B	A if and only B
¬A	not A
_\|_	false

The zeta set Z is a finite set of transformation rules that
are called inference rules when they acquire logical
applications.

The iota set I is a finite set of initial points that are
called axioms when they receive logical interpretations.

where A and B are further terms, metavariables used to describe the language.

Arguments, proofs or derivations in this language.

Assumption Rule

'A' a given term is taken to be true.

And

Introduction

Elimination

A B

A/\B

(/\I)

A/\B

(/\E₁)

A/\B

(/\E₂)

I have named these rules (in red) so that we can refer to them.

Or

Introduction

Elimination

A\/B

(\/I₁)

A\/B

(\/I₂)

A\/B

[A]
...
C

[B]
...
C

(\/E)

If A\/B then we can't say anything about A and B individually but we can say that at least one of them is true. To codify this more formally we use assumptions:

The box, like this:

[A]
...
C

means that [A] is an assumption.

That is, if we assume A is true then C is true. These assumptions are only temporary so we draw them in boxes to partition them off from the main sequence of logic.

So the elimination rule (\/E) says that if:

we have a rule that proves C from A
and we have a rule that proves C from B
and either A, B or both are true

then C is true because we know that we can use one or both of these rules.

Implication and Modus Ponens

Introduction

Elimination

(modus ponens)

[A]
...
B

A=>B

(=>I)

A A=>B

(=>E)

Alternatively we can represent modus ponens using context () as follows:

(B => D)

C /\ B

There is a good explanation of this in [1] (appendix A page 198)

Programming

I have implemented some logic using the Axiom/FriCAS program as described on the page here.

Formation Rules

Rules of syntax for the language of propositions.

What the types of the system are.

In the bottom row we convert to types (Curry-Howard)

and

implication

A is a formula B is a formula

(A/\B) is a formula

(/\F)

A is a formula B is a formula

(A\/B) is a formula

(\/F)

A is a formula B is a formula

(A=>B) is a formula

(=>F)

A is a type B is a type

Record(A,B) is a type

(/\F)

A is a formula B is a type

Union(A,B) is a type

(\/F)

A is a formula B is a type

(A->B) is a type

(=>F)

Introduction Rules

Which expressions are members of which types.

and

implication

p:A q:B

(p,q):A/\B

(/\I)

q:A

inl(q):A\/B

(\/I₁)

r:B

inr(r):A\/B

(\/I₂)

[x:A]

...

e:B

(λx:A).e:A=>B

(=>I)

Elimination Rules

and

implication

r:(A/\B)

fst(r):A

(/\E₁)

r:(A/\B)

snd(r):B

(/\E₂)

p:(A \/ B) f:(A=>C) g:(B=>C)

cases p f g :C

(\/E)

q:A=>B a:A

(q a):B

(=>E)

Computation Rules

How to evaluate expressions.

and

implication

fst(p,q)->p
snd(p,q)->q

cases inl(q) f g -> f q
cases inr(r) f g -> f r

(λx:A).e a -> e[a/x]

β-reduction

Bibliography

[1]

Sets for Mathematics - This is a book about sets from category theory point of view.

EuclideanSpace

home

Prerequisites

Mathematical logic or symbolic logic is related to:

boolean algebra
set theory

For more information about type theory see page here
Specifically about how constructors and deconstructors relate to introduction and elimination see page here
For more information about proofs using Idris see page here

Programming

I have implemented some logic using the Axiom/FriCAS program as described on the page here.

Logic Notation

Symbols used in Logic:

notation	example	meaning
/\		conjunction, and , intersection (in set), greatest lower bound (in order)
\/		disjunction, or , union (in set), least upper bound (in order)
T		Top (true)
_\|_		Bottom (false)
=>	A => B	Implication A => B means A implies B
	Tφ	φ is a theorem of T that is: φ is deducible from T In contrast to 'implication' above this is a statement about statements usually written only when we mean φ follows from T, wheras A => B is a statement we may consider as a conjecture . See [Lawvere,Rosebrugh page 198] Not to be confused with right adjoint in category theory.
		for all (quantifier)
		there exists (quantifier)

For more information about notation see this page.

Sets for Mathematics - This is a book about sets from category theory point of view.

Writing Logic Code Using a CAS Program

Curry-Howard Correspondence

There is a relationship between computer programs and mathematical proofs, this is known as the Curry-Howard correspondence.

A type in λ-calculus has the same mathematical structure as a proposition in intuitionistic logic.

A constructor for that type corresponds to a proof of the proposition. The following table has some specific types with their corresponding propositions:

Proposition	Type
true formula	unit type
false formula	empty type
implication	function type
conjunction	product type
disjunction	sum type
universal quantification	generalised product type (Π type)
existential quantification	generalised sum type (Σ type)

For more information about the Curry-Howard correspondence see the page here.

metadata block

see also:

For more information about type theory see page here
Specifically about how constructors and deconstructors relate to introduction and elimination see page here
For more information about proofs using Idris see page here

I have implemented some logic using the Axiom/FriCAS program as described on the page here.

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

Modern Graph Theory (Graduate Texts in Mathematics, 184)

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

This site may have errors. Don't use for critical systems.

Maths - Propositional Logic

The Language

Arguments, proofs or derivations in this language.

Assumption Rule

And

Or

Implication and Modus Ponens

Programming

Formation Rules

Introduction Rules

Elimination Rules

Computation Rules

Bibliography

EuclideanSpace

Prerequisites

Related Pages

Programming

Logic Notation

Writing Logic Code Using a CAS Program

Curry-Howard Correspondence

Related Pages

metadata block

see also:	Related Pages For more information about type theory see page here Specifically about how constructors and deconstructors relate to introduction and elimination see page here For more information about proofs using Idris see page here I have implemented some logic using the Axiom/FriCAS program as described on the page here.
Correspondence about this page
Book Shop - Further reading. Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.	Modern Graph Theory (Graduate Texts in Mathematics, 184)
Commercial Software Shop Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.