# 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 /\ B D

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.