A diákoknak feladatként szoktam feladni: ha existence property van, akkor Gödel-tétel nem lehet a logikában (egyik sem).
Mármint az adott konstruktivista logikában (konkrétan, a Hilbert-kalkulus egy változata, finitizmus, a PRA-n alapul).
Ugye itt az ep fontosságát általánosságban is(!) az adja, hogy mindig van effektív definíció tételhez (nem-konstruktivista logikában is).
------>Általában azonban az ep a Gödel-tétel hiányát NEM implikálja.
Először is, halmazelméleti, vagy metaelméleti tétel, hogy "létezik hagyományos rendezésben első k szám, hogy k a Gödel-száma Peano-független formulának". Ez egyúttal definíciót is jelent, hiszen egyértelmű. De ez használhatatlan, hiszen nem kapjuk meg k értékét.
Ugyanígy használhatatlan lehet, hogy ha a Goldbach-sejtés mondjuk hamis, és ez PA-igazolható, és k az első egy jóldefiniált rendezésben, hogy a Goldbach nem teljesül. Ez is definíciót ad meg.
Ezért az ep általános esetben nem elegendő arra, hogy ne legyen Gödel-tétel, hiszen a független formulák halmaza nem válik rekurzív függvény értékkészletévé.
Mivel a véges természetes számok felsorolhatók, persze többféleképpen is, egy Strong Existence Property kell: f rekurzív függvény, amely a modellt felsorolja, és f értékkészletében a felsorolás szerint rendezést definiálunk, és a tételnek azt kell kimondania, hogy "az Rf szerint rendezett modellben az n-edik elem F tulajdonságú", ha tétel, hogy
'létezik x F(x)'.
Azt szeretnénk, persze, hogy f a véges természetes számok hagyományos felsorolása legyen, +1 szerint.
Van olyan logika, amely ezt tudja.
Másrészt az ep sokkal gyengébb is lehet, ha a modell elemei rekurzívan nem sorolhatók fel. Ilyen egy ZFC-modell, mondjuk. De ekkor is lehet az ep viszonylag értékes: a definíció bonyolultsága legyen a legkevésbé komplex. Ilyen rendszert viszont nem ismerek, ez csak elméleti lehetőség.
Végül meg kell jegyezni, hogy existence property-nek azt a nyilvánvaló elvárást is szokták hívni, amikor az egzisztenciális kvantor érvényessége esetén (F tulajdonságra) igazolható a metaelméletben, hogy a modellben egy absztrakt objektum F tulajdonságú.
Ebben az értelmezésben már Hilbert számára világos volt a kapcsolat az AC-vel.
De ma már nem ez az elfogadott értelmezés.
