Index

Gödel numbering

PA

$\alpha$-equivalent

Boolean algebra

$\beta$-contraction

bounded

$\beta$-normal form

$\beta$-redex

$\beta$-reduction

base theory of arithmetic

canonically coded

Church numeral

complemented

composition

context

decide

decidable

decidable

distributive

filter

force

forcing

fixed-point combinator

Heyting algebra

height

Heyting homomorphism

$H$-valid

$H$-valuation

IPC

Kripke model

$\lambda$-abstraction

$\lambda$-application

lattice

$\lambda$-definable

$\lambda$-define

lpa

Lindenbaum-Tarski algebra

$\lambda$-term

minimisation

persistence

partial recursive

partial recursive function

prime

primitive recursion

primitive recursive

principal

projection

proper

principal up-set

recursive

recursive

recursive

reduces

redex

reduction

recursively enumerable

represent

represented

representable

representation

recursively inseparable

state

simply typed $\lambda$-term

successor

term

total recursive

typability relation

terminal segment

Takahashi translation

type

$\lambda$-term

term

valuation

world

zero