Кіріспе
Классикалық бірінші реттік логиканың кеңейтілуі
Тәуелсіздікке бейім логика (IF логика; Жаакко Хинтикка және Габриэль Санду 1989 жылы ұсынған) – бұл формасы және болатын қисық кванторлар арқылы классикалық бірінші реттік логиканың (FOL) кеңейтілуі, мұнда – шекті айнымалылар жиыны. -ның мағынасы – «-тағы айнымалылардан функционалдық тәуелсіз болатын элемент бар» болып түсіндіріледі. IF логикасы айнымалылар арасындағы тәуелділіктің бірінші реттік логикадағыға қарағанда жалпы үлгілерін білдіруге мүмкіндік береді. Осы жалпылау деңгейінің артуы экспрессивтік қуаттың нақты өсуіне әкеледі; IF сөйлемдер жиыны экзистенциалдық екінші реттік логика сияқты құрылымдардың бірдей сыныптарын сипаттай алады. Мысалы, ол тармақталған квантор сөйлемдерін, мысалы, бос қолтаңбадағы шексіздікті білдіретін формула сияқты білдіре алады; бұл FOL-де мүмкін емес. Сондықтан, бірінші реттік логика, жалпы алғанда, тек және ғана , және тәуелділіктің осы үлгісін білдіре алмайды, және IF логикасы тармақталған квантификаторлардан жалпы, мысалы, ол транзитивті емес тәуелділіктерді білдіре алады, мысалы, квантификатор префиксі , ол тәуелді , және тәуелді , бірақ тәуелді емес. IF логикасын енгізуге бірінші реттік логиканың ойын семантикасын кемелсіз ақпарат ойындарына кеңейту әрекеті себеп болды. Шын мәнінде, IF сөйлемдерінің семантикасы осы ойын түрлеріне байланысты (немесе, балама ретінде, экзистенциалдық екінші реттік логикаға аударма процедурасы арқылы) берілуі мүмкін. Ашық формулалар үшін семантика Тарски семантикасы түрінде берілмейді; адекват семантика формуланың бір тапсырмамен қанағаттанғаннан гөрі ортақ айнымалы доменнің (команданың) тапсырмалар жиынтығымен қанағаттандырылуы үшін не қажет екенін нақтылауы керек. Мұндай командалық семантиканы Ходжес әзірледі. Тәуелсіздікке бейім логика – бұл сөйлемдер деңгейінде командалық семантикаға негізделген басқа логикалық жүйелермен, мысалы, тәуелділік логикасы, тәуелділікке бейім логика, алып тастау логикасы және тәуелсіздік логикасы сияқты аударма эквиваленті; соңғысын қоспағанда, IF логикасы осы логикаларға ашық формулалар деңгейінде де бірдей экспрессивті екені белгілі. Алайда, IF логикасы жоғарыда аталған барлық жүйелерден өзгеше, өйткені оған жергіліктілік жетіспейді: ашық формуланың мағынасын формуланың еркін айнымалылары тұрғысынан ғана сипаттауға болмайды; ол формула пайда болған контекстке байланысты. Тәуелсіздікке бейім логика бірінші реттік логикамен бірқатар металогикалық қасиеттерді бөліседі, бірақ кейбір айырмашылықтар бар, соның ішінде (классикалық, қарама-қайшылықты) теріске шығарудың болмауы және формулалардың жарамдылығын шешудің күрделілігі. Кеңейтілген IF логикасы жабылу проблемасын шешеді, бірақ оның ойын теориясының семантикасы күрделірек, және мұндай логика екінші реттік логиканың үлкен фрагментіне сәйкес келеді. Хинтикка IF және кеңейтілген IF логикасы математика негіздерінің негізі ретінде қолданылуы керек деп мәлімдеді; бұл ұсыныс кейбір жағдайларда күмәнмен қаралды.
Independence friendly logic (IF logic; proposed by Jaakko Hintikka and lt=Gabriel Sandu in 1989) is an extension of classical first order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second order logic
For example, it can express branching quantifier sentences, such as the formula which expresses infinity in the empty signature; this cannot be done in FOL. Therefore, first order logic cannot, in general, express this pattern of dependency, in which depends only on and , and depends only on and IF logic is more general than branching quantifiers, for example in that it can express dependencies that are not transitive, such as in the quantifier prefix , which expresses that depends on , and depends on , but does not depend on
The introduction of IF logic was partly motivated by the attempt of extending the game semantics of first order logic to games of imperfect information. Indeed, a semantics for IF sentences can be given in terms of these kinds of games (or, alternatively, by means of a translation procedure to existential second order logic). A semantics for open formulas cannot be given in the form of a Tarskian semantics; an adequate semantics must specify what it means for a formula to be satisfied by a set of assignments of common variable domain (a team) rather than satisfaction by a single assignment. Such a team semantics was developed by Hodges. Independence friendly logic is translation equivalent, at the level of sentences, with a number of other logical systems based on team semantics, such as dependence logic, dependence friendly logic, exclusion logic and independence logic; with the exception of the latter, IF logic is known to be equiexpressive to these logics also at the level of open formulas. However, IF logic differs from all the above mentioned systems in that it lacks locality: the meaning of an open formula cannot be described just in terms of the free variables of the formula; it is instead dependent on the context in which the formula occurs. Independence friendly logic shares a number of metalogical properties with first order logic, but there are some differences, including lack of closure under (classical, contradictory) negation and higher complexity for deciding the validity of formulas. Extended IF logic addresses the closure problem, but its game theoretical semantics is more complicated, and such logic corresponds to a larger fragment of second order logic, a proper subset of
Hintikka argued that IF and extended IF logic should be used as a basis for the foundations of mathematics; this proposal was met in some cases with skepticism.
Синтаксисі
Әдебиетте тәуелсіздікке қатысты логиканың бірнеше сәл өзгеше ұсыныстары пайда болды; біз осы жерде Mann et al (2011) жұмысын негізге аламыз.
Терминдар мен атомдық формулалар
Белгілі бір қолтаңба σ үшін, терминдер мен атомдық формулалар теңдікпен бірге бірінші реттік логикадағыдай нақты анықталады.
IF сөйлемдері
IF формуласы – бұл IF сөйлем.
Семантика
IF логикасының семантикасын анықтау үшін үш негізгі тәсіл ұсынылған. Бірінші екеуі, сәйкесінше, толық емес ақпарат ойындарына және Skolemization-ге негізделген, көбінесе тек IF сөйлемдерін анықтау үшін қолданылады. Біріншісі, толық ақпарат ойындарына негізделген, бірінші реттік логика үшін ұқсас тәсілді кеңейтеді. Үшінші тәсіл – командалық семантика – Тарски семантикасының дәстүріндегі құрастырмалы семантика. Дегенмен, бұл семантика формуланың бір тапсырмамен (емес, тапсырмалар жиынтығымен) қанағаттандырылуын не білдіретінін анықтамайды. Бірінші екі тәсіл IF логикасы туралы бұрынғы жарияланымдарда жасалған, ал үшіншісі 1997 жылы Ходжес жасады. Осы бөлімде біз үш тәсілді әртүрлі индекс қолдану арқылы ажыратамыз, себебі үш тәсіл негізінен эквивалентті болғандықтан, мақаланың қалған бөлігінде тек символ қолданылады.
Ойын теориясы семантикасы
Ойын теориялық семантикасы IF сөйлемдерге толымсыз ақпаратты 2 ойыншылық ойындардың қасиеттеріне сәйкес шындық мәндерін тағайындайды. Түсіндіруді жеңілдету үшін ойынды тек сөйлемдермен ғана емес, формулалармен де байланыстыру ыңғайлы. Нақтырақ айтқанда, IF формуласы, құрылым және тағайындамадан тұратын әрбір үштік үшін ойындар анықталады.
Ойыншылар
Семантикалық ойынның екі ойыншысы бар, Элоиза (немесе Растаушы) және Абелард (немесе Жалғаншы) деп аталады.
Ойын ережесі
Семантикалық ойынның рұқсат етілген амалдары қарастырылып отырған формуланың синтаксистік құрылымымен анықталады. Қарапайымдылық үшін, бастапқыда бұл теріске шығарудың нормалық түрінде деп есептейміз, онда теріске шығару белгілері тек атомдық субформулалардың алдында ғана болады. Егер сөзбе-сөз болса, ойын аяқталады, және егер ол (бірінші реттік мағынада) шын болса, Элоиза жеңеді; әйтпесе, Абелард жеңеді. Егер болса, Абелард субформулалардың біреуін таңдайды, және тиісті ойын ойналады. Егер болса, Элоиза субформулалардың біреуін таңдайды, және тиісті ойын ойналады. Егер болса, Абелард жинағынан бір элементті таңдайды, және ойын ойналады. Егер болса, Элоиза жинағынан бір элементті таңдайды, және ойын ойналады. Көбінесе, егер бұл теріске шығарудың нормалық түрінде болмаса, онда теріске шығару ережесі бойынша, ойынға жеткен кезде ойыншылар қос ойынды бастайды, онда Растаушы мен Жалғандаушының рөлдері ауыстырылады.
Тарих
Бейресми түрде, ойынның қимылдар тізбегі – тарих. Әрбір тарихтың соңында, белгілі бір субойын ойналады; біз байланысты тапсырманы және байланысты субформуланың пайда болуын атаймыз. Егер ең сыртқы логикалық оператор болса немесе , онда тарихқа байланысты ойыншы Элоиза, ал егер ол немесе болса, Абелард болады. Тарихтың рұқсат етілген қимылдар жиыны егер ең сыртқы оператор болса немесе болса, онда ; ал егер ең сыртқы оператор болса немесе болса, онда ( екі түрлі нысан, «сол» және «оң» символдайды). Бір домендегі екі тапсырманы қарастыра отырып, және егер кез келген айнымалы үшін біз жазамыз. Ойынға толық емес ақпарат енгізіледі, егер кейбір тарихтар байланысты ойыншы үшін ажыратылмайтын болса; ажыратылмайтын тарихтар «ақпарат жиынтығын» құрайды. Интуитивті түрде, егер тарих ақпарат жиынтығында болса, онда оған байланысты ойыншы өзінің басқа тарихта немесе басқа бір тарихта екенін білмейді. Екі тарихты қарастырайық, егер олар (немесе) түріндегі бірдей субформуланың пайда болуы болса; егер одан әрі , онда біз (егерде) немесе (егерде) деп жазамыз, екі тарихтың Элоиза үшін, сәйкесінше Абелард үшін ажыратылмайтынын көрсету үшін. Сондай-ақ, жалпы, осы қатынастың рефлексивтілігін белгілейміз: егер , онда ; және егер , онда .
The set of allowed moves in a history is if the most external operator of is or ; it is ( being any two distinct objects, symbolizing 'left' and 'right') in case the most external operator of is or
Given two assignments of same domain, and we write if on any variable
Imperfect information is introduced in the games by stipulating that certain histories are indistinguishable for the associated player; indistinguishable histories are said to form an 'information set'. Intuitively, if the history is in the information set , the player associated to does not know whether he is in or in some other history of Consider two histories such that the associated are identical subformula occurrences of the form ( or ); if furthermore , we write (in case ) or (in case ), in order to specify that the two histories are indistinguishable for Eloise, resp. for Abelard. We also stipulate, in general, reflexivity of this relation: if , then ; and if , then .
Стратегиялар
Белгілі бір ойын үшін, Элоиза қатысқан тарихтар жиыны үшін жазыңыз, және сол сияқты Абелард тарихтарының жиыны үшін де. Ойындағы Элоизаның стратегиясы – бұл Элоизаның ойын кезегі келетін кез келген мүмкін тарихқа заңды қимыл тағайындайтын кез келген функция; дәлірек айтқанда, кез келген функция, әр тарих үшін. Абелардтың стратегиясын осыған сәйкес анықтауға болады. Элоизаның стратегиясы біртекті болады, егер, кез келген уақытта ,; Абелард үшін, егер болса, онда . Элоизаның стратегиясы жеңіске жететін стратегия болып есептеледі, егер Элоиза осы стратегия бойынша ойнау арқылы қол жеткізілетін әрбір соңғы тарихта жеңіске жетсе. Абелард үшін де осыған ұқсас.
A strategy for Eloise is winning if Eloise wins in each terminal history that can be reached by playing according to Similarly for Abelard.
Шындық, жалғандық, белгісіздік
IF сөйлем, егер Илоизаның ойында жеңіске жететін сенімді стратегиясы болса, дұрыс болады. Егер Абелардтың жеңіске жететін стратегиясы болса, онда бұл сөйлем жалған. Егер екі ойыншының да – Илоизаның да, Абелардтың да – жеңіске жететін стратегиясы болмаса, нәтижесі анықталмайды.
It is false if Abelard has a winning strategy. It is undetermined if neither Eloise nor Abelard has a winning strategy.
Консервативтілік
IF логикасының осылай анықталған семантикасы бірінші реттік семантиканың консервативті кеңейтімі болып табылады, мына мағынада. Егер бос қисық сызық жиындарымен IF сөйлем болса, оған бірінші реттік формуласын сәйкес қойыңыз, ол одан бірдей, бірақ әрбір IF сандық анықтауышы тиісті бірінші реттік сандық анықтауышымен алмастырылады. Содан кейін Тарский мағынасында екендігімен, ал Тарский мағынасында екендігімен тең.
Skolem Семантикасы
IF сөйлемдер үшін шындықтың анықтамасын экзистенциалды екінші реттік логикаға аудару арқылы да беруге болады. Бұл аударма бірінші реттік логиканың Сколемизация процедурасын кеңейтеді. Жалғандық, Крейзелизация деп аталатын кері процедура арқылы анықталады.
Мектепке түсу
IF формуласы берілген жағдайда, ең алдымен оның шекті айнымалылар жиынағына қатысты skolemization-ын анықтаймыз. Формуланың ішінде кездесетін әрбір экзистенциалдық квантор үшін, жаңа функция символын ("Сколем функциясы") енгіземіз. айнымалысының формула ішіндегі барлық бос кездесуін терминімен ауыстырып жазамыз. -қа қатысты Skolemization-ы, белгісімен келесі индуктивті шарттар арқылы анықталады: егер - бұл литерал. . , мұндағы - IF сөйлемдегі айнымалылар тізімі. Егер IF сөйлем болса, оның (қатыстырмалы емес) Skolemization-ы ретінде анықталады.
if is a literal. . , where is a list of the variables in
If is an IF sentence, its (unrelativized) Skolemization is defined as .
Крейзелизация
IF формуласы берілген болса, онда кездесетін әрбір жалпы кванторға жаңа функция символын ("Крейзель функциясы") қосыңыз. Содан кейін, шекті айнымалылар жиынына қатысты Крейзелизация келесі индуктивті шарттармен анықталады: егер – бұл литерал болса. . , мұндағы – формуладағы айнымалылардың тізімі. Егер – IF сөйлем болса, оның (неғұрлымша емес) Крейзелизациясы ретінде анықталады.
if is a literal. . , where is a list of the variables in
If is an IF sentence, its (unrelativized) Kreiselization is defined as .
Шындық, жалғандық, белгісіздік
Экзистенциалды кванторлары бар IF сөйлем, құрылым және тиісті арлықтары бар функциялар тізімі берілгенде, біз функцияларды Skolem функцияларының интерпретациясы ретінде тағайындайтын құрылымның кеңейтілуін деп белгілейміз.
An IF sentence is true on a structure , written , if there is a tuple of functions such that Similarly, if there is a tuple of functions such that ; and iff neither of the previous conditions holds. For any IF sentence, Skolem Semantics returns the same values as Game theoretical Semantics.
IF сөйлем құрылымда дұрыс деп жазылса, онда функциялардың бір туыры бар, сонда ; және егер функциялардың бір туыры болса ; ал егер бұл екі шарттың екеуі де орындалмаса, онда . Кез келген IF сөйлем үшін Skolem Семантикасы ойын теориялық Семантикасымен бірдей мәндерді қайтарады.
An IF sentence is true on a structure , written , if there is a tuple of functions such that Similarly, if there is a tuple of functions such that ; and iff neither of the previous conditions holds. For any IF sentence, Skolem Semantics returns the same values as Game theoretical Semantics.
Командалық семантика
Командалық семантика арқылы IF логикасының семантикасын құралымдық тұрғыдан түсіндіруге болады. Шындық және жалғандық "формуланың командамен қанағаттандырылуы" ұғымына негізделген.
Командалар
Келіңіздер, құрылым болсын және келіңіздер, айнымалылардың шекті жиыны болсын. Содан кейін, доменімен команда – доменімен тапсырмалар жиыны, яғни -тан -ға функциялар жиыны.
Топтарды қайталау және толықтыру
Көбейту және толықтыру – командаларға қатысты екі операция, олар жалпы және жеке сандық өлшеудің семантикасымен байланысты. Егер құрылым және айнымалы берілген болса, көбейту командасы – команда. Егер команда, функция және айнымалы берілген болса, толықтыру командасы – команда. Бұл екі операцияның қайталап қолданылуын қысқаша жазумен алмастыру қалыпты жағдай, мысалы .
It is customary to replace repeated applications of these two operation with more succinct notations, such as for .
Топтардағы бірыңғай функциялар
Жоғарыда айтылғандай, егер екі тапсырманың айнымалылар домені бірдей болса, онда егер әрбір айнымалы үшін , деп жазамыз. Егер құрылымдағы команда және айнымалылардың шекті жиынтығы берілген болса, функция біркелкі деп аталады, егер кез келген уақытта .
Given a team on a structure and a finite set of variables, we say that a function is uniform if whenever .
Шындық, жалғандық, белгісіздік
Командалық семантика бойынша, егер IF сөйлем бір элементті командамен қанағаттандырылса, онда ол құрылымда дұрыс деп есептеледі. Сол сияқты, егер , онда ол құрылымда жалған деп есептеледі; егер және болса, онда ол анықталмаған деп есептеледі.
Similarly, is said to be false on if ; it is said to be undetermined if and .
Теңдестік ұғымдары
IF логикасы қалыпты жағдайда үш мәнді болғандықтан, формула теңдестігінің әртүрлі ұғымдары қызығушылық тудырады.
Формулалардың теңдестігі
Екі IF формуласын қарастырайық. (Шындықтан келіп шығады) егер кез келген құрылым үшін және кез келген команда үшін егер
(Шындыққа балама) егер және
(Жалғандықтан келіп шығады) егер кез келген құрылым үшін және кез келген команда үшін егер
(Жалғандыққа балама) егер және
(Күшті келіп шығады) егер және
(Күшті балама) егер және .
( is truth equivalent to ) if and
( falsity entails ) if for any structure and any team such that
( is falsity equivalent to ) if and
( strongly entails to ) if and
( is strongly equivalent to ) if and .
Сөйлемдердің теңдестігі
Жоғарыдағы анықтамалар IF сөйлемдері үшін былай маманданады. Егер екі IF сөйлем бірдей құрылымдарда дұрыс болса, олар шындыққа эквивалентті; егер олар бірдей құрылымдарда бұрыс болса, олар жалғандыққа эквивалентті; егер олар бірдей құрылымдарда шындыққа да, жалғандыққа да эквивалентті болса, олар күшті эквивалентті. Интуитивті түрде, күшті эквиваленттілік қолдану IF логикасын 3 мәнді (дұрыс/белгісіз/бұрыс) деп қарастырумен бірдей, ал шындық эквиваленттілігі IF сөйлемдерін 2 мәнді (дұрыс/бұрыс) деп қарастырғанмен тең.
Контекстке қатысты баламалық
IF логикасының көптеген логикалық ережелерін тек формуланың қолданылуы мүмкін контекстін ескеретін, эквиваленттіліктің тар ауқымды ұғымдары арқылы ғана толыққанды түсіндіруге болады. Мысалы, егер шекті айнымалылар жиыны болса және , онда формуласы -қа қатысты шындыққа эквивалентті деп айтуға болады, егер кез келген құрылым және доменінің кез келген тобы үшін бұл орындалса.
Сөйлем деңгейі
IF сөйлемдері Skolemization процедурасы арқылы (функционалдық) экзистенциалдық екінші реттік логиканың сөйлемдеріне шындықты сақтай отырып аударылуы мүмкін (жоғарыда қараңыз). Керісінше, кез келген сөйлем, бөлшектеп реттелген квантификаторларға арналған Уолко-Эндертон аударма процедурасының түрі арқылы IF сөйлемге аударылуы мүмкін. Басқаша айтқанда, IF логикасы және сөйлемдер деңгейінде экспрессивтік эквивалентті. Бұл эквиваленттікті келесі қасиеттердің көптегенін дәлелдеу үшін пайдалануға болады; олар экзистенциалдық екінші реттік логикадан мұраға алынған және көп жағдайда FOL қасиеттеріне ұқсас. Біз IF сөйлемдерінің (мүмкін шексіз) жиынын белгілейміз. Лёвенхайм-Сколем қасиеті: егер жиын шексіз модельге немесе кез келген үлкен шекті модельдерге ие болса, онда оның әрбір шексіз кардиналдыққа модельдері бар. Экзистенциалдық тығыздық: егер әрбір шекті жиын модельге ие болса, онда жиын да модельге ие. Дедуктивті тығыздықтың орындалмауы: мұндай жиындар бар, мұнда , бірақ кез келген шекті жиын үшін бұл FOL-ден өзгешелік. Бөлу теоремасы: егер IF сөйлемдері өзара қайшы болса, онда FOL сөйлем бар, мұнда және Бұл Крейгтің FOL үшін интерполяция теоремасының салдары. Берджесс теоремасы: егер IF сөйлемдері өзара қайшы болса, онда IF сөйлем бар, мұнда және (бір элементтік құрылымдардан басқа). Атап айтқанда, бұл теорема IF логикасының жоқтығы шындық эквивалентіне қатысты семантикалық операция емес екенін көрсетеді (ақиқатқа эквивалентті сөйлемдер эквивалентті емес жоқтарға ие болуы мүмкін). Шындықтың анықталуы: Пьяно арифметикасының тілінде, кез келген IF сөйлем үшін IF сөйлем бар, мұнда (Гёдель нөмірлеуін білдіреді). Бұл мәлімдеме Пьяно арифметикасының стандартты емес модельдері үшін де әлсіз нұсқада қолданылады.
Кеңейтілген IF логикасы
IF логикасы классикалық жоққа шығару бойынша жабық емес. IF логикасының бульдік жабылуы кеңейтілген IF логикасы деп аталады және ол (Figueira және басқалар, 2011) фрагментімен эквивалентті. Хинтикка (1996, 196-бет) «классикалық математиканың дерлік барлық бөлігі принципі бойынша кеңейтілген IF бірінші реттік логикасында жүзеге асырылуы мүмкін» деп мәлімдеген.
Қасиеттері мен сын
IF логикасының бірқатар қасиеттері логикалық эквиваленттіліктен туындайды және оны бірінші реттік логикаға жақындатады, оның ішінде тығыздық теоремасы, Лёвенхайм-Сколем теоремасы және Крейг интерполяция теоремасы. (Väänänen, 2007, 86-бет.) Дегенмен, Väänänen (2001) IF логикасының жарамды сөйлемдерінің Гёдель сандарының жиынтығы, кем дегенде бір бинарлық предикат символы бар болғанда (ValIF деп белгіленеді), бір бинарлық предикат символы бар сөздіктегі жарамды (толық) екінші реттік сөйлемдердің Гёдель сандарының жиынтығымен рекурсивті изоморфты екенін дәлелдеді (Val2 деп белгіленеді). Бұдан әрі, Väänänen Val2 толық Π2 анықталатын бүтін сандар жиынтығы екенін, және ол Val2 кез келген шекті m және n үшін жатпайтынын көрсетті. Väänänen (2007, 136–139-беттер) күрделілік нәтижелерін былайша қорытындылайды:
predicate symbol (set denoted by ValIF) is recursively isomorphic with the corresponding set of Gödel numbers of valid (full) second order sentences in a vocabulary that contains one binary predicate symbol (set denoted by Val2). Furthermore, Väänänen showed that Val2 is the complete Π2 definable set of integers, and that it is Val2 not in for any finite m and n. Väänänen (2007, pp. 136–139) summarizes the complexity results as follows:
Мәселе | Бірінші реттік логика | IF/тәуелділік/ESO логикасы | Шешім (r. e.) | Жарамсыздық (co r. e.) | Тұрақтылық | Тұрақсыздық
Феферман (2006) Хинтикаға қарсы, Вейненнің 2001 жылғы нәтижесін келтіріп, қанағаттандыру бірінші реттік мәселе болуы мүмкін екенін, бірақ барлық құрылымдардағы Verifier үшін жеңімпаз стратегия бар ма деген сұрақ "бізді толық екінші реттік логикаға жеткізеді" (Феферманның баса назары). Феферман сондай-ақ кеңейтілген IF логикасының пайдалылығына күмәндік білдірді, себебі жиынтықтағы сөйлемдер ойын теориялық интерпретацияға ие емес.