Pure Isabelle

IFOL CTT HOL LK

ZF LCF

Modal

logics
FOL

1

x x

n

1

x 1

1

xn

1

x 1

1 n

x2 x2 x2

x 1

1 n

x2 x2 x2

x 1

1 n

x2 x2 x2

Diagram 1. Isabelle's object-logics

Diagram 2. Infinite binary tree

Diagram 3.

Infinite-branching tree