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:

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 (right adjoint) as follows:

Cright adjoint(B => D)
C /\ Bright adjointD

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]
flag flag flag flag flag flag Sets for Mathematics - This is a book about sets from category theory point of view.

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.

cover 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.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.