====================================================================
Demonstration of the “Obelisk” proof assistant.
Variant: higher-order logic
Author: Georgy Dunaev
Email: contact@obelisk.mozmail.com
Date: Tue Sep 29 10:46:56 2026
License: All rights reserved.©
====================================================================
1) Propositional logic:

Axm. A01:
(⟦ ⟧→(⟦ ⟧→⟦ ⟧))

Axm. A02:
((⟦ ⟧→(⟦ ⟧→⟦ ⟧))→((⟦ ⟧→⟦ ⟧)→(⟦ ⟧→⟦ ⟧)))

Axm. A03:
((⟦ ⟧∧⟦ ⟧)→⟦ ⟧)

Axm. A04:
((⟦ ⟧∧⟦ ⟧)→⟦ ⟧)

Axm. A05:
(⟦ ⟧→(⟦ ⟧→(⟦ ⟧∧⟦ ⟧)))

Axm. A06:
(⟦ ⟧→(⟦ ⟧∨⟦ ⟧))

Axm. A07:
(⟦ ⟧→(⟦ ⟧∨⟦ ⟧))

Axm. A08:
((⟦ ⟧→⟦ ⟧)→((⟦ ⟧→⟦ ⟧)→((⟦ ⟧∨⟦ ⟧)→⟦ ⟧)))

Axm. A09:
((¬⟦ ⟧)→(⟦ ⟧→ ))

Axm. A10:
((⟦ ⟧→⟦ ⟧)→((⟦ ⟧→¬⟦ ⟧)→¬⟦ ⟧))

Axm. A11:
( →⟦ ⟧)

Axm. A12:
(⟦ ⟧∨¬⟦ ⟧)

Rule Modus Ponens:
⟦ ⟧
(⟦ ⟧→⟦ ⟧)
-----------------------------------------⟦ ⟧

(MP)

2) Predicate logic:

Axm. Discourse domain is non-empty:
(∃

)

Rule Forall Instantiation:
⟦term
is free for substitution instead of all samely typed free occurences of
the variable
in the formula ⟧
------------------------------------------ (FI)
((∀
⟦ ⟧ ⟦ ⟧)→⟦ [ / ]⟧)

Rule Exists Instantiation:
⟦term
is free for substitution instead of all samely typed free occurences of
the variable
in the formula ⟧
------------------------------------------ (EI)
(⟦ [ / ]⟧→∃
⟦ ⟧ ⟦ ⟧)

Rule Forall Abstraction:
⟦name
does not occure free as a variable of type
(⟦ ⟧→⟦ ⟧)
------------------------------------------ (FA)
(⟦ ⟧→∀
⟦ ⟧ ⟦ ⟧)

in formula

⟧

in formula

⟧

Rule Exists Abstraction:
⟦name
does not occure free as a variable of type
(⟦ ⟧→⟦ ⟧)
------------------------------------------ (EA)
((∃
⟦ ⟧ ⟦ ⟧)→⟦ ⟧)

Rule Generalisation (admissible rule):
⟦ ⟧
-----------------------------------------(∀
⟦ ⟧ ⟦ ⟧)

(Gen)

3) Set/class-theoretic foundations of mathematics:

Rule Class comprehension:
⟦( :
)⟧
⟦( : )⟧
-----------------------------------------((
∈
⟦ ⟧ )⟷((
set)∧⟦ ⟧))

(CCR)

Def. “Is a set” predicate:
(∀

((

set)⟷(∃

( ∈ ))))

Def. “Is a proper class” predicate:
(∀

((

proper)⟷(¬(

set))))

Def. Empty set:
( =

)

Def. Universal class:
( =

)

Def. Subclass relation:
(∀

∀

(( ⊆ )⟷(∀

(( ∈ )→( ∈ )))))

Thm. Example: “The empty class is a subclass of any class” statement:
(∀

( ⊆ ))

Axm. “Membership respects equality from the left”:
(∀

∀

(( = )→∀

(( ∈ )⟷( ∈ ))))

Axm. “Membership respects equality from the right”:
(∀

∀

(( = )→∀

(( ∈ )⟷( ∈ ))))

Axm. “Extensionality”:
(∀

∀

((∀

(( ∈ )⟷( ∈ )))→( = )))

Thm. “Intensionality”(admissible):
(∀
∀
(( ∈ )⟷( ∈ )))→( = ))))

(((

set)∧(

set))→((∀

Axm. “Heredity”(a subclass of a set is also a set):
(∀

∀

((( ⊆ )∧(

set))→(

set)))

Axm. “Exponent”(powerclass of a set is also a set):
(∀

((

set)→(( ) set)))

Axm. “Regularity”(only universal class is equal to its powerclass):
(∀

((( )⊆ )→( ⊆ )))

Def. Transitivity predicate:
(∀

(

( )⟷(∀

Def. Ordinality predicate:

(( ∈ )→( ⊆ )))))

(∀

(

( )⟷(

( )∧∀

(( ∈ )→

( )))))

Def. Class of all ordinal sets(ordinal numbers):
(

=

( ) )

Thm. The class of all ordinals is an ordinal class:
(

)

Def. Union of the elements of a class:
(∀

(⋃ =

∃

(( ∈ )∧( ∈ )) ))

Def. Intersection of the elements of a class:
(∀

(⋂ =

∀

(( ∈ )→( ∈ )) ))

Def. Domain (includes arguments with proper class values):
(∀

(

( )=

∃

(

∈ ) ))

Def. IF-THEN-ELSE-FI(meta,semantic,Class-specific,WIP, TODO: add side
condition that v is not free in psi, add (W,G|-<... = ... >):
(∀
(⟦ ⟧∧(

∀
∈ ))∨((¬⟦ ⟧)∧(

∀
∈ )) ))

∀

((IF ⟦ ⟧ THEN

ELSE

FI)=

Def. if-then-else-fi(meta,syntactic,polymorphic over one type,nondependent,TBI):
(ToDo: “simple_if”, a non-dependent type-theoretic verison of the conditional,
which works not only for Class, but also for any other type)

Def. If-Then-Else-Fi(meta,syntactic,polymorphic over one
value,dependent,TBI):
(ToDo: Add “typeof(if b then t1 else t2) := [| simple_if b then typeof(t1) else
typeof(t2) fi |]”; simple_if is an instance using polymorphic over one metatype
variable; The expression inside [|-|] brackets has type Type.)

Def. Evaluation of a [function|class-function|family]:
ELSE

(∀
FI)))

∀

(

=(IF (∃

(

=

(

∈ )) THEN ⋃

Def. Image class:
(∀

∀

∃

(( ∈ )∧(

= )) ))

Def. “Has exactly one element” predicate:
(∀

((

singleton)⟷(∃!

( ∈ ))))

Def. “Is set-valued” predicate:
(∀

((

set-valued)⟷(∀

(( ∈

( ))→(

set)))))

∈

Def. “Has concentrated set values” predicate:
(∀
set)→∃!

(( concentrated set values)⟷(∀
∈ ))))))

(

(( ∈

( ))→((

Def. “Has flat proper values” predicate:
(∀

((

proper)→∀

((

flat proper values)⟷(∀
∈ )→( singleton)))))))

(( ∈

( ))→((

Def. “Is a family” predicate:
(∀

((

family)⟷((

concentrated set values)∧(

flat proper

values))))

Def. “Is a class-function” predicate:
(∀

((

class-function)⟷((

family)∧(

set-valued))))

Def. “Is injective” predicate:
(((( ∈

(∀
( ))∧( ∈

(( injective)⟷(∀
∀
( )))∧(
=
))→( = )))))

Def. “Is a function” predicate:
(∀

((

function)⟷((

class-function)∧(

set))))

Def. “Is not strictly larger than” binary relation:
(∀
function)∧(

⊆ ))∧(

∀
(( ≼ )⟷(∃
injective)))))

(((

class-

Def. Class cardinality:
(∀

(| |=(

∩⋂

( ∈

)∧( ≼ ) )))

Def. “Is strictly smaller than” binary relation:
(∀

∀

(( ≺ )⟷(¬( ≼ ))))

Axm. Size limitation axiom related statement:
(∀

(( ∈ )⟷(| |≺| |)))

Def. “Is hereditary” predicate:
(∀
(( ⊆ )→( ∈ ))))))

(

( )⟷(∀

(( ∈ )→∀

Def. “Is powerful” predicate:
(∀

(

( )⟷(∀

(( ∈ )→(( )∈ )))))

Def. “Is pairful” predicate:
(∀
∈ )))))

(

( )⟷(∀

∀

((( ∈ )∧( ∈ ))→(

Def. “Is tight” predicate:
(∀

(

( )⟷(∀

(( ⊆ )→(( ≺ )⟷( ∈ ))))))

Def. Singleton set:
(∀

(

=

=

))

Def. Unordered pair:
(∀

∀

(

=

( = )∨( = ) ))

Def. Set-theoretic models of natural numbers(TBI):
Def.:
Def.:
Def.:
Def.:
Def.:

(0:Class) = ∅
(1:Class) = {∅}
(2:Class) = {∅,{∅}}
(3:Class) = {∅,{∅},{∅,{∅}}}
...

Def. General definition of lists of classes which applicable not only for
sets, but for proper classes too(TBI):
Def.:
Def.:
Def.:
Def.:
Def.:

mark(A,n) = { {0,n} } ∪ { ( { {{a}} , n } : Class ) | (a ∈ A)}
[] = ∅
[A] = mark(A,1)
[A,B] = mark(A,1) ∪ mark(B,2)
...

Def. Ordered pair(Dunaev's):
Def.:

(A,B) = [A,B]

Def. Projections:
Def.:
Def.:
Def.:

pr1(L) = { a | ({{{a}},1} ∈ L)}
pr2(L) = { b | ({{{b}},2} ∈ L)}
...

Def. Ordered pair(Kuratowsky's):
(∀

∀

(

=

))

Def. Binary union:
(∀
Special Def.:
General Def.:

∀

(( ∪ )=

( ∈ )∨( ∈ ) ))

(x ∪ y) = ⋃{x,y}
(A ∪ B) = { z | (z ∈ A) ∨ (z ∈ B)}

Def. Binary intersection:
(∀

∀

(( ∩ )=

( ∈ )∧( ∈ ) ))

( bad def)
(good def)

Def. “Is inductive” predicate:
(∀

(

( )⟷(( ∈ )∧∀

(( ∈ )→(( ∪

)∈ )))))

Def. The intersection class of all inductive classes is called omega:
(∀

(( ∈ )⟷(∀

Special Def.:
General Def.:

(

( )→( ∈ )))))

ω = ⋂{ q | Ind(q) }
∀ x, (x ∈ ω) ⟷ (∀ Q, Ind(Q) → (x ∈ Q))

( bad def)
(good def)

Axm. “Infinity”(ω is a set):
(

set)

Thm. Class of all sets is inductive:
( )

Thm. Intersection of all inductive classes is an inductive class itself:
( )

Thm. Class of all ordinal numbers is inductive:
(

)

Thm. ω is transitive:
( )

Thm. ω is ordinal:
( )

Thm. ω is in the class of all ordinal numbers(=sets):
( ∈

)

Thm. “Is cardinal” predicate:
(∀

(

( )⟷(∃

(| |= ))))

Thm. ω is cardinal:
( )

Thm. On is a cardinal class:
(

)

Thm. Class of all sets is not a cardinal class:
(¬

( ))

Def. “Is a universe” predicate:
(∀
universe)⟷((( ∈ )∧((

((
( )∧

( ))∧(

( )∧

( ))))∧

( ))))

Thm. The class of all sets is a universe:
(

universe)

Axm. “Tarski's axiom”:
(∀

((

set)→∃

(((

universe)∧( ∈ ))∧(

set))))

Thm. General form of the induction principle on a transitive class:
(∀

∀

((

Axm. Soundness of the theory
(∀

:

(( ,[]⊢ )→eval( )))

Axm. Soundness of the theory
(∀

( )∧(( ∩( ))⊆ ))→( ⊆ )))

:

(( ,[]⊢ )→eval( )))

Def. Completeness of the theory
(∀

:

(eval( )→( ,[]⊢ )))

Axm. If a formula is derivable in
(∀

∀

, then it is derivable in

:

(( , ⊢ )→( , ⊢ )))

4) Metalogical laws(WIP: too much known errors in this section):

Axm. Instantiation(meta,WIP):
(∀
⊢‹(∀

∀
.
∀
∀
eval( ).
⟦ ⟧ ⟦ ⟧)→(let ⟦ ⟧ = ⟦ ⟧ in ⟦ ⟧)›))

∀

( ,⟦ ⟧

Axm. Generalisation(meta,WIP):
((¬(

(

(∀
)∈

∀
∀
∀
( )))→(( , ⊢ )→( , ⊢‹∀

⟦ ⟧›))))

(A theory
is assumed here to contain only formulas without free variables, so
the variable x has no free occurences in any formula of a set of formulas
[|Dec(Theory.Expression)(W)|]. (Strictly: even if the type is different from X?)
)

Rule CoNecessitation(meta,WIP):
If a formula <
is derived in

,Γ⊢ > is derived in
from the context Γ.

from the empty context, then the formula

Def. Quantifier “unique”(meta,WIP):
∧(let z =

(∀
((!
⟦ ⟧)⟷(∀
in ⟦ ⟧))→( = )))))

∀

Def. Quantifier “exists and unique”(meta,WIP):

((⟦ [( :Class)/‹z›]⟧

(∀

( ,[]⊢‹(∃!

⟦ ⟧)⟷((∃

⟦ ⟧)∧!

⟦ ⟧)›))

Axm. Class comprehension axiom schema(meta,WIP):
(∀
[]⊢‹(⟦ ⟧∈

∀
∀
⟦ ⟧ )⟷((⟦ ⟧ set)∧(let

.
(
(( :Class),‹ ›,( :Bool))→( ,
= ⟦ ⟧ in ⟦ ⟧))›)))

5) Tactics and inference rules:

Elementary theorems:
( ,[‹ ∈ ›]⊢‹∃
( ,[‹ ∈ ›]⊢‹∀
( ,[‹ ∈ ›]⊢‹(

( ∈ )›)
(( set)⟷(∃
set)⟷(∃
( ∈ ))›)

( ∈ )))›)

An example of inference rule:
( ,[‹ ∈ ›]⊢‹∃
( ∈ )›)
-----------------------------------------( ,[‹ ∈ ›]⊢‹ set›)

(def_to_intro th2)

An application of a deduction rule:
( ,[]⊢‹( ∈ )→(

set)›)

A simple theorem being proven using tactics:
( ,[‹∃
∀
⟦ ⟧›]⊢‹∃
⟦ ⟧›)
( ,[‹∀
⟦ ⟧›]⊢‹∃
⟦ ⟧›)
( ,[‹⟦ ⟧›]⊢‹∃
⟦ ⟧›)
( ,[‹⟦ ⟧›]⊢‹⟦ ⟧›)
Displaying the proof of that theorem:
Proof.
1
|( ,[‹⟦ ⟧›]⊢‹⟦ ⟧›)
2
|( ,[‹⟦ ⟧›]⊢‹∃
⟦ ⟧›)
3
|( ,[‹∀
⟦ ⟧›]⊢‹∃
⟦ ⟧›)
4
|( ,[‹∃
∀
⟦ ⟧›]⊢‹∃
5
|( ,[‹∃
∀
⟦ ⟧›]⊢‹∀
6
|( ,[]⊢‹(∃
∀
⟦ ⟧)→∀
Q.E.D.

⟦ ⟧›)
∃
∃

⟦ ⟧›)
⟦ ⟧›)

6) Incompleteness-related statements(WIP: too much known errors in this section):

Axm. Theories:
Let
be an arbitrary theory.
Let
be Robinson's arithmetic.
Let
be a recursively axiomatizable theory of classes. (The base theory of the
proof assistant.)
Let
be an extension(note: it is not recursively axiomatizable) of
(in the
language extended by adding all Henkin constants), which is complete and admits
the reflection axiom.
The introducing of the types allows to hide both Gödel's encoding and decoding,
and to keep all variables on the same metalevel.

Thm. Löb's theorem(WIP):

(∀

( ,[]⊢‹( ,[]⊢‹( ,[]⊢ )→⟦ ⟧›)→( ,[]⊢ )›))

Thm. Gödel's second incompleteness theorem(WIP):
( ,[]⊢‹(¬( ,[]⊢‹ ›))→¬( ,[]⊢‹¬( ,[]⊢‹ ›)›)›)