"Egyrészt világos, hogy a végtelenségre tett igen komoly, nemkonstruktív (nem finit) megkötések (pl. nagy számosságok, AD) kellhetnek ahhoz, hogy egy adott fi igaz-e minden véges modellen"
Ha szemléletes, általam "valóságosnak" vélt dolgok igazolásához olyasmiket kell feltenni, amiről semmi intuicióm nincs, hogy "hihető-e" az nagy kár. Persze lehet majd sfejlődik a szemléletem és a nagy számosságok is ugyanolyan szemléletes dolgok lesznek mint a természetes számok, de nem hinném.
"Például van olyan konstruktivizmus..."
Olvastam picit a konstruktivizmus különböző fajtáiról. A Markov-féle valamennyire szimpatikus is volt, hogy Turing-gépekre és algoritmusokra építi fel a matekot. De összességében nem tetszik ez az irányzat, túl sok intuitíve igaz dolog nem lesz itt igaz.
"ami logikailag feltételezi, amit eddig nem tettél fel, hogy valamilyen értelemben - esetleg a téridőn kívül - létezik az összes véges modell"
Egy megszámlálható nyelv összes véges modellje szerintem ugyanúgy létezik, mint az öszes természetes szám, összes Turing-gép, összes véges gráf stb.
"Vedd észre, hogy ez ellentétben van azzal a hilbertiánus meggyőződéseddel, hogy Te csak levezetgetni szeretnél, mégpedig finit és intuitív módon, és eredményeket kapni."
Nem csak levezetgetni szeretnék. Szeretném ha a levezetgetések a "valóságban igaz" eredményt adnának (legaláb ott ahol beszélhetünk objektív ellenőrizhetőségről). Például ne tudjon a legújabb szuperszámítógép találni egy olyan számot, amire valamely számelméleti tételünk nem igaz. Vagy egy olyan véges modellt megadni, amiben nem igaz az a formula, amiről beláttuk, hogy minden véges modellben igaz.
Ilyen kényelmetlen történések elkerülésének garanciáját, pedig abban látom, hogy ha az axiomák "igazak" a "valóságban".
Számomra "igazak" például a PA, a valósak másodrendű szokásos axiómái, a kiv ax megszámlálható változata.
Másrészt vannak olyanok amikről nincs (még) ilyen erős meggyőződésem, pl regularitási ax. Bár utóbbinak a szép következményeit látom persze.