# 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: X0, X1, X2 ...
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 A
(/\E1)
 A/\B B
(/\E2)

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

#### Or

Introduction Elimination
 A A\/B
(\/I1)
 B A\/B
(\/I2)
 A\/B [A]...C [B]...C
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 B
(=>E)

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

 C(B => D) C /\ BD

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 or 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 or implication
 p:A q:B (p,q):A/\B
(/\I)
 q:A inl(q):A\/B
(\/I1)
 r:B inr(r):A\/B
(\/I2)
 [x:A] ... e:B (λx:A).e:A=>B
(=>I)

#### Elimination Rules

and or implication
 r:(A/\B) fst(r):A
(/\E1)
 r:(A/\B) snd(r):B
(/\E2)
 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 or 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.

### Related Pages

• Specifically about how constructors and deconstructors relate to introduction and elimination see page here

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

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.