Dit voorstel vervolgt een huidige onderzoekslijn in het gebruik van bewijsbaarheidslogica's in de ordinaalanalyse van wiskundige theoriën. Ons doel bestaat erin de eigenschappen te onderzoeken van bewijsbaarheidslogica's die voor ordinaalsystemen voor impredicatieve ordinalen gebruikt werden, en deze te gebruiken om uitspraken te specificeren die onafhankelijk van corresponderende impredicatieve theorieën zijn.