Maths - Intuitionistic Logic

Intuitionistic logic sounds like a contradiction in terms, this is we think of intuition as being the opposite of logic. An alternative name is 'constructive logic' and perhaps this better describes the nature of this form of logic.

In intuitionistic logic a statement is true only if it is proven to be true and it is false only if it is proven to be false, so for instance we can't imply something is true just because it is not false. In other words we do not use the law of the excluded middle.

This is the way that we construct information in the everyday world and it is the basis of mathematical constructivism.

Heyting Algebra

Unlike boolean algebra we do not have 'not' operation, instead we have a 'pseudo complement'.

Boolean boolean lattice A Boolean algebra is a full lattice where a \/ ¬a is 1 (true)
Heyting heyting lattice This does not apply for Heyting algebra, that is no: 'Law of excluded middle'

We do have a \/ operation but it does not have the property that: a \/ ¬a = 1.

A Heyting lattice (pseudo boolean lattice) is a relativly complemented lattice.

We can express Heyting algebra properties in terms of this pseudo complement or, alternativly, we can express Heyting algebra properties using the 'implication operation
'->'. Where:

x -> b is the largest element whose intersection with x is contained in b.

a ^ x ≤ b b is pseudo complement of a relative to x
a < (x -> b)

Equivalently this can be expressed in terms of the 'implication operation
'->'.

So a Heyting algebra is a lattice with a binary operation x->y satisfying the double-horn sentence:

a < (x -> b) iff a ^ x ≤ b

Example: 'A' is pseudo complement of 'BC' relative to 'ABC'

A ^ BC ≤ ABC
A < BC -> ABC

where:

  • BC represents B^C
  • ABC represents A^B^C
pseudo comp I have drawn this diagram so we can get the 'pseudo complement' relative to A^B^C by reflecting in the red line.
x y x /\ y x \/ y x -> y
ø ø ø ø ø
A ø ø A ø
B ø ø B ø
A/\B ø ø A/\B ø
ø A ø ø ø
A A A A A
B A ø A/\B ø
A/\B A A A/\B ø
ø B ø B ø
A B ø A/\B ø
B B B B B
A/\B B B A/\B ø
ø A/\B ø A/\B ø
A A/\B A A/\B A
B A/\B B A/\B B
A/\B A/\B A/\B A/\B A/\B

BHK Interpretation

Where BHK is 'Brouwer, Heyting, Kolmogorov'

Heyting's formalization

For logical connectives p & q:

  1. A mathematical proposition p always demands a mathematical construction with certain given properties; it can be asserted as soon as such a construction has been carried out.
  2. p /\ q can be asserted if and only if both p and q can be asserted.
  3. p \/ q can be asserted if and only if at least one of the propositions p and q can be asserted.
  4. p can be asserted if and only if we possess a construction which from the supposition that a construction p were carried out, leads to a contradiction.
  5. The implication p -> q can be asserted, if and only if we possess a construction r, which, joined to any construction proving p (supposing that the latter be effected), would automatically effect a construction proving q.
  6. |- (for allx)p(x) means that p(x) is true for every x in Q [over which x ranges]; in other words, we possess a general method of construction which, if any element a of Q is chosen, yields by specialization the construction p(a).
  7. (there existsx)p(x) will be true if and only if an element a of Q for which p(a) is true has actually been constructed.

 

The language language has:

The (well-formed) formulas of language are defined inductively as follows.

In general, we use

A, B, C as metavariables for well-formed formulas

x, y, z as metavariables for individual variables.

Anticipating applications (for example to intuitionistic arithmetic) we use s, t as metavariables for terms; in the case of pure predicate logic, terms are simply individual variables.

An occurrence of a variable x in a formula A is bound if it is within the scope of a quantifierfor allx orthere existsx, otherwise free. Intuitionistically as classically, "(A <-> B)" abbreviates "(A -> B) & (B -> A)," and parentheses are omitted when this causes no confusion.

 

 

A |- B means that B follows from A

A might be treated as negation or it might be treated as an abbreviation for (A -> _|_)

_|_ = false

T = true

Axioms

  1. a -> (a /\ a)
  2. (a /\ b) -> (b /\ a)
  3. (a -> b) -> ((a /\ c)-> (b /\ c))
  4. ((a -> b) /\ (b -> c)) -> (a -> c)
  5. b -> (a -> b)
  6. (a /\ (a -> b)) -> b
  7. a -> (a \/ b)
  8. (a \/ b) -> (b \/ a)
  9. ((a -> c) /\ (b -> c)) -> ((a \/ b) -> c)
  10. a -> (a -> b)
  11. ((a -> b) /\ (a -> b)) -> a

intuitionistic lattice

Rules of Inference

There are three rules of inference:

Fomulas

 


metadata block
see also:
  • Stanford - Development of Intuitionistic Logic
  • Stanford - Intuitionistic Logic
  • Youtube video

    Advanced Topics in Programming Languages Series: Parametric Polymorphism and the Girard-Reynolds Isomorphism. This talk is based on a series of papers by Philip Wadler, a principal designer of the Haskell programming language. Featured are a number of double-barreled names in computer science:

    • Hindley-Milner (Strong typing without having to type the types)
    • Wadler-Blott (Making ad-hoc polymorphism less ad-hoc with parametricity)
    • Curry-Howard (Isomorphism between types and theorems, terms and proofs)
    • Girard-Reynolds (Isomorphism between types and terms in the presence of parametricity)
  • or Djinn code see here.
  • Parametricity
  • "Propositions as Types" by Philip Wadler
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)

Terminology and Notation

Specific to this page here:

 

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

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