Tegenwoordig is metamathematica een standaard onderdeel van het landschap van de wiskundige logica.
Enerzijds moet het meeste werk aan de grondslagen van de wiskunde waarschijnlijk als metamathematisch worden beschouwd. De standaardbasis is set-theoretisch, waarbij ZFC en zijn varianten de gebruikelijke formaliseringen zijn. Maar dit is verreweg niet de enige optie en er is bijvoorbeeld recent werk aan wat we nu univalente grondslagen noemen, gebaseerd op de abstracte homotopietheorie. In zekere zin ligt dit misschien dichter bij Principia dan bij ZFC, aangezien typetheorie een serieuze rol speelt. Aan de andere kant is de benadering echt categorietheoretisch, en waren categorieën in de tijd van Principia nog niet echt bedacht. Hoewel deze nieuwe benadering veel aandacht krijgt, begint de logische gemeenschap in het algemeen pas de reikwijdte en mogelijkheden ervan te begrijpen. Een recente reeks discussies op de FOM-e-maillijst (foundations of mathematics) illustreert de huidige spanning.
Een groot deel van het onderzoek op standaardgebieden van wiskundige logica wordt gedreven door metamathematische overwegingen , ook al is het niet in de zin van herziene grondslagen.
Bijvoorbeeld, omgekeerde wiskunde (ook genoemd in een ander antwoord) bestudeert de vraag welke axioma's van set-existentie eigenlijk nodig zijn voor standaard wiskundige argumenten. Typische resultaten hier betogen dat een standaardstelling (zoals de tussenwaardestelling in klassieke analyse) equivalent is aan, of op zijn minst impliceert (over een redelijk zwakke achtergrondtheorie waar de discussie plaatsvindt) een abstract 'bestaansaxioma' (bijv. elke oneindige binaire boom heeft een oneindige vertakking) of een voorbeeld van wiskundige inductie.
Bewijstheorie behandelt theorieën als wiskundige objecten en bestudeert hun sterkte, gebaseerd op de lengte van bewijzen (passend gedefinieerd) in vergelijking met sommige standaardopties, of op meer subtiele manieren (zoals overwegingen van het zogenaamde bewijs -theoretische rangtelwoorden). Binnen Peano-rekenkunde, het standaard eerste-orde-systeem van axioma's voor getaltheorie, kunnen we bijvoorbeeld gemakkelijk Turing-machines definiëren, de gebruikelijke formalisering van "computerprogramma's". We kunnen dan aangeven of een binaire relatie < 'op de natuurlijke getallen recursief is, wat betekent dat er een algoritme (een Turing-machine) is dat kan beslissen uit elk paar getallen n, m, al dan niet n<'m. Veel recursieve relaties zijn eigenlijk goed geordend, en gegeven een dergelijke relatie R en een theorie T (uitbreiding van Peano-rekenkunde) kunnen we ons afvragen of T kan beweren dat R een goede ordening is. In het algemeen is de lengte van de aantoonbare putorden significant klein in vergelijking met de lengte van alle recursieve putjes. We kunnen dan theorieën vergelijken door na te gaan welke theorieën goed ordenen van langere (recursieve) well-ordeningen kunnen aantonen. Op basis van deze beschrijving lijkt dit een beetje excentriek, maar dit hangt nauw samen met hoeveel transfiniete inductie de theorie kan formaliseren en bewijzen, dus deze bewijstheoretische rangtelwoorden zijn eigenlijk heel redelijke maatstaven van de macht. van expressie en kracht van theorieën.
In de verzamelingenleer is een van de standaardthema's de vergelijking van de consistentiekracht van theorieën. Uit het werk van Goedel weten we dat een redelijke theorie T zijn eigen consistentie niet kan bewijzen, dus als een theorie T erin slaagt de consistentie van een theorie S te bewijzen, geeft dit ons een natuurlijke manier waarop T sterker is dan S. hiërarchie is een fascinerend wiskundig object. Het blijkt dat we voor natuurlijke extensies T van ZFC de neiging hebben om een groot kardinaal axioma te identificeren dat, wanneer toegevoegd aan ZFC, resulteert in een theorie die gelijk is aan T. Dit geeft ons een grote kardinale metgezel van T, en de puur wiskundige studie van grote kardinalen weerspiegelt dan de studie van sterke punten van theorieën. Dat er überhaupt zoiets bestaat, is opmerkelijk. Innerlijke modeltheorie is het gebied van de verzamelingenleer dat zich het meest rechtstreeks bezighoudt met het proberen dit fenomeen te verklaren. De feitelijke identificatie van de begeleider van een theorie is tegenwoordig echter een overwegend combinatorische vraag, dankzij Cohen's ontwikkeling van de forceringsmethode.
Referenties over univalente stichtingen zijn hier en hier te vinden. Zie voor omgekeerde wiskunde bijvoorbeeld hier naast de link bij het andere antwoord. Kijk hier over bewijstheorie. Zie hier voor de hiërarchie van consistentiekracht in de verzamelingenleer, hoewel veel artikelen en toespraken van John Steel ook relevant zijn. Ook hebben veel van mijn berichten in MathOverflow en Math.Stackexchange betrekking op dit onderwerp. Laat me deze noemen.