-
Notifications
You must be signed in to change notification settings - Fork 0
/
pnp.tex
1575 lines (1426 loc) · 132 KB
/
pnp.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\documentclass[letterpaper]{article}
\usepackage[us]{datetime}
\usepackage{CJKutf8}
\usepackage[T1,T2A]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{varwidth}
\usepackage{lastpage}
\usepackage{fancyhdr}
\usepackage{appendix}
\settimeformat{ampmtime}
\pagestyle{fancy}
\newcommand{\myfooters}{
\rfoot{\small electronic mail\\ \url{mailto:justina@colmena.biz?subject=P_vs_NP}}
\cfoot{\small \textbf{[\begin{NoHyper}Page\ \thepage\ of\ \pageref{LastPage}\end{NoHyper}]}}
\lfoot{\small justina colmena\\\today\ @\currenttime}
\renewcommand{\footrulewidth}{\headrulewidth}
}
\myfooters
\fancypagestyle{plain}{
\fancyhf{}
\lhead{\textit{TITLE PAGE}}
\rhead{\textit{Nothing to see here. Please move along.}}
\myfooters
}
%\usepackage{lmodern}
\usepackage[numbers]{natbib}
\usepackage[finnish,swedish,french,german,spanish,italian,russian,latin,english]{babel}
\bibliographystyle{plainnat}
\usepackage[hyphens,lowtilde]{url}
\usepackage{wrapfig}
\usepackage[justification=centering]{caption}
\usepackage{hyperref}
\hypersetup{
colorlinks=true, %set true if you want colored links
linktoc=all, %set to all if you want both sections and subsections linked
linkcolor=blue, %choose some color if you want links to stand out
}
%\usepackage[hyphenbreaks]{breakurl}
\usepackage{color} %May be necessary if you want to color links
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{thmtools}
\usepackage{marvosym,wasysym,textcomp,dictsym}
\usepackage{mathrsfs}
\usepackage{algpseudocode}
\usepackage{algorithm}
\usepackage[]{backnaur}
\usepackage{newfloat}
%\usepackage{syntax}
%\grammarindent=80pt
\usepackage{scalerel}
\usepackage{graphicx}
\graphicspath{{images/}}
\usepackage{svg}
\renewcommand{\includesvg}[1]{%
\immediate\write18
{inkscape --batch-process -D --export-latex #1.svg --export-filename=#1.pdf}%
\input{#1.pdf_tex}%
}
\usepackage{float}
\newsavebox\Volleyball
\savebox\Volleyball{\includesvg{images/b14f1090776e99712331d0c24973afc6}}
\newcommand{\Axiom}{{\large\Bearing}}
\declaretheorem[numberwithin=section,qed={\Axiom}]{axiom}
\newcommand{\AxiomSchema}{{\large\LooseBearing}}
\declaretheorem[sibling=axiom,name=Axiom Schema,qed={\AxiomSchema}]{axiomschema}
\newcommand{\Theorem}{\raisebox{0.5ex}{\large\Beam}}
\declaretheorem[numberwithin=section,qed={\Theorem}]{theorem}
\newcommand{\Lemma}{{\large\FlatSteel}}
\declaretheorem[sibling=theorem,qed={\Lemma}]{lemma}
\newcommand{\Corollary}{\CircPipe}
\declaretheorem[sibling=theorem,qed={\Corollary}]{corollary}
\newcommand{\Definition}{\raisebox{-0.25ex}{\large\dsliterary}}
\declaretheorem[sibling=theorem,style=definition,qed={\Definition}]{definition}
\newcommand{\Circumlocution}{{\large\dsmedical\dsjuridical}}
\declaretheorem[sibling=theorem,style=definition,qed={\Circumlocution}]{circumlocution}
\newcommand{\Construction}{{\large\dsmathematical}}
\declaretheorem[sibling=theorem,style=definition,qed={\Construction}]{construction}
\newcommand{\Remark}{\raisebox{-0.125ex}{\large\Coffeecup}}
\declaretheorem[numbered=no,style=remark,qed={\Remark}]{remark}
\newcommand{\Exercise}{\raisebox{-0.75ex}[0ex][0ex]{\scaleto{\usebox{\Volleyball}}{3ex}}}
\declaretheorem[style=remark,qed={\Exercise}]{exercise}
\renewcommand{\qedsymbol}{\textbf{\textsc{q.e.d.}}}
%opening
\title{\textbf{Liars' oracles}\\ Relativizing the $P$ vs.\ $NP$ question}
\author{Justina Colmena\footnote{\url{https://www.colmena.biz/~justina/pnp/}, B.S. Mathematics, B.S. Computer Science: University of Alaska Fairbanks, of ``HAARP'' fame \cite[etc.]{haarp,haarp.net,begich2002angels,burks2010haarp,want2016haarp,smith1998haarp,freeland2014chemtrails} ... \url{mailto:justina@colmena.biz?subject=P_vs._NP}}}
\begin{document}
\sloppy
\phantomsection\addcontentsline{toc}{section}{Title}\maketitle
\phantomsection\addcontentsline{toc}{section}{Abstract}
\begin{abstract} {\color{red}\textbf{WORK IN PROGRESS:}}
A somewhat whimsical investigation into the possibility of the formal independence of the $P$ vs.\ $NP$ question based on an oracle of Hartmanis and Hopcroft.
\end{abstract}
\begin{figure}
\includegraphics[width=1.0\textwidth]{images/guy_fawkes_mask.jpg}
\caption[\texttt{(float)0x63/0x64}]{\texttt{(float)0x63/0x64} \cite{anon2012}}
\end{figure}
\phantomsection\addcontentsline{toc}{section}{Contents}\tableofcontents
\phantomsection\addcontentsline{toc}{section}{List of Figures}\listoffigures
\phantomsection\addcontentsline{toc}{section}{List of Algorithms}\listofalgorithms
\phantomsection\addcontentsline{toc}{section}{List of Tables}\listoftables
\section{Copyright}
This work is placed in the public domain by its author.\footnote{\url{https://github.com/justinacolmena/pnp/blob/master/LICENSE}} Questions of attribution are academic, and not intended to be enforced by copyright law. The style of this document is mostly intended for working copy. This author raises no objection to adaptation of this document or its style for commercial or other publication. Other authors who wish to take a particular portion of this document and expand upon it at greater length into their own work are encouraged to do so. For this reason, \LaTeX\textsuperscript{\textregistered} source code\footnote{\url{https://github.com/justinacolmena/pnp}} is distributed with this original work.
Those who wish to cite this (unfinished) paper are encouraged to quote or paraphrase the portions they are referring to in sufficient detail that their work does not depend on this remaining exactly as it is. They are encouraged to make their mathematical arguments on mathematical merits rather than engaging in \foreignlanguage{latin}{\textit{ad hominem}} arguments of one author's claim against another, unless the latter really is the subject they wish to address.
To compile this entire paper it is necessary to have Inkscape and ImageMagick installed, and to use the \texttt{-shell-escape} switch with \texttt{pdflatex}. For some reason, it seems necessary to specify \texttt{-shell-escape} \textit{before} other switches on the command line.
\section{Introduction}
The purpose of this article is to expand on some comments originally made online by the author in a somewhat offhand manner \cite{myinfo2016,myinfo2016a,annorlunda2016}. We attempt to show that the $P$ vs.\ $NP$ question remains undecided by any formal system $F$ capable of sufficient arithmetic and not containing a proof of its own inconsistency.
This is a work in progress.
\section{Turing machines}
Turing machines are named after Alan Turing (1912--1954), Figure~\ref{turing}, the British computer scientist and code-breaker who was chemically castrated as punishment for homosexuality in spite of his valiant efforts that were not only crucial to winning the war but of great scientific merit in peacetime, given the freedom that victory affords us to study his and others' related work. An inquisition has yet to be made into the formal verdict of his death by suicide.
\begin{figure}
\centering
\includegraphics[width=1\textwidth]{images/alan-turing-school-photo.jpg}
\caption[Alan Turing]{Alan Turing as a school-child \cite{hodges2017}.}
\label{turing}
\end{figure}
\begin{definition}
A \textbf{deterministic accept/reject Turing machine} is a 'tuple
\begin{equation}
(\sigma,\Sigma,S,T,R,\delta),\label{dtuple}
\end{equation}
where $\sigma$ is a finite set of states, $\Sigma$ is a finite alphabet of at least two different symbols\footnote{$\Sigma=\{0,1\}$ is a minimal acceptable alphabet for a Turing machine.} that does not include the symbol $\triangleright$,\footnote{We do not teach, as do others, the so-called ``disjoint union'' \mbox{$\Sigma\sqcup\{\triangleright\}$}, which they attempt to define without regard to whether or not \mbox{$\triangleright\in\Sigma$}, since this is not a well-founded set by any of the axioms of Zermelo--Fraenkel set theory; we feel that it is necessary and sufficient to state explicitly that \mbox{$\triangleright\notin\Sigma$}. Those who have such a strong preference for the term ``disjoint union'' may simply state that the union \mbox{$\Sigma\cup\{\triangleright\}$} is disjoint because \mbox{$\Sigma\cap\{\triangleright\}=\emptyset$}.} $S\in\sigma$ is an initial or start state, $T\subset\sigma$ is a set of accepting final or halt states, $R\subset\sigma$ is a set of rejecting final or halt states, $T\cap R=\emptyset$, and $\delta$ is its \textbf{state transition table}, a function
\begin{equation}
\delta:\big((\sigma\backslash(T\cup R))\times(\Sigma\cup\{\triangleright\})\big)\longrightarrow\big((\Sigma\cup\{\triangleright\})\times\{\leftarrow,\rightarrow\}\times\sigma)\big)
\end{equation}
subject to the restrictions\footnote{The tick-mark after the delta $\delta`$ refers to an \textit{image} under the function $\delta$....}
\begin{align}
\delta`(\sigma\backslash(T\cup R)\times\{\triangleright\})&\subset \{\triangleright\}\times\{\rightarrow\}\times\sigma,\label{noback}\\
\delta`(\sigma\backslash(T\cup R)\times\Sigma)&\subset \Sigma\times\{\leftarrow,\rightarrow\}\times\sigma.\label{abuse1}
\end{align}
\end{definition}
\begin{remark}
Such a Turing machine is considered to have a tape, infinite in one direction only, readable and writable with the symbols of the alphabet $\Sigma$, and with the unique symbol \mbox{$\triangleright\notin\Sigma$} permanently engraved at the beginning of the tape.\footnote{The purpose of these restrictions is to prevent the read/write head from (\ref{noback}) overwriting the symbol $\triangleright$ and backing off the beginning of the tape or (\ref{abuse1}) misusing the symbol $\triangleright$ in an inappropriate context: recall from (\ref{dtuple}) that \mbox{$\triangleright\notin\Sigma$}. If we were to omit the restriction (\ref{abuse1}), a Turing machines would be allowed to cut tape like a malfunctioning automatic cash register and leave receipts for various discarded intermediate computations all over the floor.} The state transition table $\delta$ is interpreted to specify, for a given symbol read from the tape by the read/write head in a given state, a new symbol to be written to replace the symbol just read from the tape, a new direction to move the read/write head by one position on the tape, and a new state to enter upon completing this step of computation.
\end{remark}
\begin{definition}
A \textbf{non-deterministic Turing machine} is defined similarly, except that its state transition function is defined more generally
\begin{equation}
\Delta:\big((\sigma\backslash(T\cup R))\times(\Sigma\cup\{\triangleright\})\big)\longrightarrow\mathscr P\big((\Sigma\cup\{\triangleright\})\times\{\leftarrow,\rightarrow\}\times\sigma)\big)\backslash\{\emptyset\},
\end{equation}
subject to the restrictions
\begin{align}
\Delta`((\sigma\backslash(T\cup R))\times\{\triangleright\})&\subset\mathscr P\big(\{\triangleright\}\times\{\rightarrow\}\times\sigma\big)\backslash\{\emptyset\},\\
\Delta`((\sigma\backslash(T\cup R))\times\Sigma)&\subset\mathscr P \big(\Sigma\times\{\leftarrow,\rightarrow\}\times\sigma\big)\backslash\{\emptyset\},
\end{align}
which are straightforward generalizations of (\ref{noback}--\ref{abuse1}), where again, \mbox{$\triangleright\notin\Sigma$}, and $\mathscr P$ denotes the \textbf{power set} \mbox{$\mathscr P(X)=\{x|x\subset X\}$}. See \Axiom \ref{powerset} and \AxiomSchema \ref{comprehensionschema}.
\end{definition}
\begin{definition}
An \textbf{alternating Turing machine} is a non-deterministic accept/reject Turing machine with some of its states (including the initial state) quantified as either universal or existential: A path of computation leading into a universal state is considered to accept if and only if all possible paths continuing on from that state accept. A path leading into an existential state is considered to accept if and only at least one path continuing on from that state accepts.
\end{definition}
\begin{definition}
\textbf{Oracle or query machine?}
\end{definition}
\begin{definition}
{\color{red}\textbf{Other variants...}}
\end{definition}
\section{Complexity classes}
\subsection{Formal definitions}
Information, references, and less formal definitions are available online at Scott Aaronson's ``Complexity Zoo'' \cite{aaronson-zoo}.
\subsubsection{Polynomial time}
\begin{definition}
A language $L\subset\Sigma^{*}$, where $\Sigma^{*}$ is the set of strings over some some finite alphabet $\Sigma$, is said to belong to the class $P$, i.e. $L\in P$ if there exist a deterministic Turing machine $M$ and a polynomial $p$, such that for all $s\in\Sigma^{*}$, the computation of $M$ begun from its initial state on the input $s$ terminates in a number of steps not more than $p(|s|)$,\footnote{By $|s|$ is denoted the \textit{length} of the string $s$.} in an accepting state whenever $s\in L$ and in a rejecting state whenever $s\notin L$.
\end{definition}
\begin{definition}
A language $L\subset\Sigma^{*}$, where $\Sigma^{*}$ is the set of strings over some some finite alphabet $\Sigma$, is said to belong to the class $NP$, i.e. $L\in NP$ if there exist a non-deterministic Turing machine $N$ and a polynomial $q$, such that for all $s\in\Sigma^{*}$, all possible paths of computation of $N$ beginning at its initial state on the input $s$ terminate in a number of steps not more than $q(|s|)$, at least one path in an accepting state whenever $s\in L$ and all paths in a rejecting state whenever $s\notin L$.
\end{definition}
\subsubsection{Exponential time}
\begin{definition}
The classes $EXP$ and $NEXP$ are defined similarly to $P$ and $NP$, except that the number of steps allowed for the computation is exponential in the polynomial, i.e., $2^{p(|s|)}$ and $2^{q(|s|)}$, respectively. It is known that $EXP=NEXP$ [\S \ref{bgsa}].
\end{definition}
\subsubsection{Recursion}
\begin{definition}
A language belongs to the class $PR$ of \textbf{primitive recursive} languages if it is recognizable by a deterministic Turing machine that halts on all inputs within a number of steps bounded by a \textit{primitive recursive function} \cite{robinson1949definability} of the length of the input.\footnote{The class of primitive recursive \textit{functions} is ``closed'' in a peculiar manner: any function, computable by a Turing machine in a number of steps bounded by a primitive recursive function of the length of the input, is itself primitive recursive.}
\end{definition}
\begin{definition}
A language belongs to the class $R$ of \textbf{general recursive} languages if it is recognizable by any deterministic Turing machine that halts on all inputs. General recursive languages are simply called ``recursive'' when it is not necessary to emphasize the distinction from primitive recursive languages.
\end{definition}
\begin{definition}\label{def-re}
The class $RE$ of \textbf{recursively enumerable} languages is defined similarly to $R$, except that the Turing machine is not required to halt on inputs that do not belong to the language in question.
\end{definition}
\subsection{\textit{P} vs.\ \textit{NP}}
The $P$ vs.\ $NP$ question is at its root a philosophical question of whether or not an existentially quantified non-determinism, or even a bounded alternation between universal and existential states, ($P$ vs.\ $PH$ \cite{meurant2014algorithms},) properly extends the class of computational problems that may be solved in polynomial time. Similar questions exist for other forms of non-determinism, such as those quantified not in an existential or universal sense but by classical probability measures, (e.g.,\ $ZPP=RP\operatorname\cap\textrm{co-}RP$ or $BPP$,) or quantum mechanical amplitudes, ($BQP$, etc.) However, as we do not wish to become entrapped in any untoward discussion of free will or other forms of indeterminism, as opposed to determinism,\footnote{Martin Luther \cite{lutherliber} weighs in with German stubbornness on a Catholic controversy over a passage of Scripture [Romans~8:28--31] which Paul intended to support a conclusion, namely, ``... If God be for us, who can be against us?'' No doubt the argument goes back even further than that, to the Greek philosophers to whom Paul was responding when he used such strong language of foreordination and predestination.} we leave off philosophizing on this particular matter.
\subsubsection{\textit{NP}-completeness and reduction}
Cook \cite{cook1971complexity}, Karp \cite{karp1972reducibility}, and Levin \cite{levin1973universal} discovered an important and diverse subclass of problems within $NP$ which they call $NP$-complete: the very problem of the existence of an accepting path of computation of a specified non-deterministic Turing machine with a specified polynomial time bound on an arbitrary input, can be ``reduced'' in polynomial time on a deterministic Turing machine, to an instance of any one of these problems. Thus any one of these so-called ``$NP$-complete'' problems is in $P$ only if $P=NP$.
$SAT$, or the problem of the satisfiability of an arbitrary Boolean expression, is perhaps \textit{the} canonical $NP$-complete problem. The reduction of $NP$ to $SAT$ involves constructing a Boolean expression representing a path of valid state transitions on a non-deterministic Turing machine from its inital state given an arbitrary input to an accepting final state, in polynomially bounded time and space. Such an expression is satisfiable if and only if an accepting computation exists for the Turing machine given that input.
These discoveries considerably sharpened the question of whether $P=NP$ or, as it seems for all practical purposes, $P\ne NP$, as all attempts to find a deterministic polynomial-time solution for an $NP$-complete problem have failed, despite a great deal of effort. Nor have attempts to prove that $P$ is a proper subclass of $NP$ met with any greater success.
\subsubsection{Oracles and relativization}\label{o-r}
\begin{definition}
If $O$ is an oracle, that is, any arbitrary language of strings over $\Sigma$, the classes $P^O$ and $NP^O$ are defined identically to $P$ and $NP$, except that the Turing machine $M$ or $N$ in the definition is endowed with an extra writable tape, and magically allowed to make a binary query of its contents at any time in a single step for membership in the language $O$. In defining $P^O$ and $NP^O$, we say that the classes $P$ and $NP$ have been relativized to the oracle $O$, and we call such a Turing machine an oracle or query machine.
\end{definition}
\subsubsection{The Baker--Gill--Solovay oracles}\label{bgs}
Baker, Gill, and Solovay discovered recursive oracles $A$ and $B$, such that $P^A=NP^A$ and $P^B\ne NP^B$. The major significance of this result is that no method of proof which relativizes to oracles can resolve the $P$~vs.~$NP$ question. For the proofs we refer to the original paper \cite{baker1975relativizations} and to various university lecture notes available online \cite{spielman2001adv, feigenbaum2010bgs,holenstein2010complex,moshkovitz2012rel}. Here we present our versions of their basic constructions and leave the details as exercises for the reader. We remark that $A$ is a powerful oracle such that $P^A=NP^A=EXP$, that $B$ involves a clever use of diagonalization in its construction, and that both $A$ and $B$ belong to the class $PR$ of primitive recursive languages, that is, languages that can be decided by a primitive recursive function \cite{robinson1950general}.
\begin{definition}\label{bgsa}
The BGS oracle $A$ is sometimes called $EXPCOM$. Let $\big(\Gamma(m)\big)_{m\in\mathbb N}$ be an acceptable enumeration of deterministic Turing machines, and let ``$1^n\,$'' represent a string of $n$ $1$s.
\begin{equation}
A:=\left\{(m,x,1^n)\left|\begin{array}{l}
\Gamma(m) \textrm{ halts in an accepting state} \\ \textrm{on input } x \textrm{ within } 2^n \textrm{ steps}
\end{array}\right.\right\}.
\end{equation}
\end{definition}
\begin{theorem}
$P^A=NP^A$.
\end{theorem}
\begin{proof}
See \cite{baker1975relativizations,spielman2001adv, feigenbaum2010bgs,holenstein2010complex,moshkovitz2012rel}. Alternatively, the following exercises.
\end{proof}
\begin{exercise}
Prove $P^A=EXP$ \cite{volleyball-icon}.
\end{exercise}
\begin{exercise}
Prove $NP^A=NEXP$.
\end{exercise}
\begin{exercise}
Prove $EXP=NEXP$.
\end{exercise}
\begin{definition}\label{bgsb}
The BGS oracle $B$ is the recursive set recognized by Algorithm~\ref{algb}.
\end{definition}
\begin{theorem}
$P^B\ne NP^B$
\end{theorem}
\begin{proof}
A technique of \textit{diagonalization} was employed in the construction of $B$ so that
\begin{equation}
U_B\in NP^B\operatorname\backslash P^B,
\end{equation}
where $U_B$ is the projection of $B$ onto $1^{*}$, that is,
\begin{equation}
U_B=\left\{1^n\left|(\exists b\in B)\,|b|=n\right.\right\}.
\end{equation}
Clearly
\begin{equation}
(\forall B\in\Sigma^{*})\,U_B\in NP^B,
\end{equation}
for an arbitrary string $x$ of the same length as the input may be chosen non-deterministically, and then the oracle queried for whether or not $x\in B$, all in linear, well within polynomial time on a non-deterministic query machine \cite{baker1975relativizations,spielman2001adv, feigenbaum2010bgs,holenstein2010complex,moshkovitz2012rel}.
\end{proof}
\begin{algorithm}
\caption{To recognize the set $B$, such that $P^B\ne NP^B$}\label{algb}
\begin{algorithmic}[5]
\State \textbf{input} string $x$
\State $\big(\Gamma'(n)\big)_{n\in\mathbb N}\gets$ acceptable enumeration of deterministic query machines
\State\hspace{\algorithmicindent} --- N.B. these query machines have no oracle attached, and when one
\State\hspace{\algorithmicindent}
--- of them has entered a query state, any attempt to continue its
\State\hspace{\algorithmicindent}
--- computation from that state will generate an exception.
\State $B'\gets\emptyset$;\quad $C'\gets\emptyset$
\For{$n= 1..\infty$ }
\State initialize the query machine $\Gamma'(n)$ for input $1^n$
\For{$i=1..2^{n-1}$}
\State \textbf{try} \label{algtrybegin}
\State\hspace{\algorithmicindent} execute the $i$th step of the computation of $\Gamma'(n)$ on input $1^n$
\State \textbf{catch exception} query string $q$ \textbf{handle}
\State\hspace{\algorithmicindent}\textbf{if} {$q\in B'$} \textbf{then}
\State\hspace{\algorithmicindent}\hspace{\algorithmicindent} supply a \textbf{yes} answer to the query
\State\hspace{\algorithmicindent}\textbf{else}
\State\hspace{\algorithmicindent}\hspace{\algorithmicindent} $C'\gets C'\cup\{q\}$
\State\hspace{\algorithmicindent}\hspace{\algorithmicindent} supply a \textbf{no} answer to the query
\State\hspace{\algorithmicindent}\textbf{end if}
\State \textbf{end try}\label{algtryend}
\If{the computation of $\Gamma'(n)$ on input $1^n$ has halted}
\State \textbf{break}
\EndIf
\EndFor
\If{$\Gamma'(n)$ has halted in a \textit{rejecting} state}
\State $s'\gets$ first string in lexicographical order $\in\Sigma^n\operatorname\backslash(B'\cup C')$
\State $B'\gets B'\cup\{s'\}$
\Else
\State $C'\gets C'\cup \Sigma^n$
\EndIf
\If{$x\in B'$}
\State \textbf{output yes} --- \textbf{accept} the string $x$
\State \textbf{halt} --- $x\in B$
\ElsIf{$x\in C'$}
\State \textbf{output no} --- \textbf{reject} the string x
\State \textbf{halt} --- $x\notin B$
\EndIf
\EndFor
\end{algorithmic}
\end{algorithm}
\begin{exercise}Verify that $U_B\notin P$ for the oracle $B$ recognized by Algorithm~\ref{algb}. (Cf. \cite{cpptry} \texttt{try} block, lines~\ref{algtrybegin}--\ref{algtryend}.)
\end{exercise}
\begin{exercise}
Explain these comments \cite[p.~436]{baker1975relativizations}:
\begin{quotation}
``The set $B$ \dots is sparse; for every $n$, there is at most one string $x$ in $B$ such that $n\leqq|x|<2^n$. An obvious modification \dots yields the following result: there are arbitrarily sparse recursive sets such that $\mathscr{P}^B\ne\mathscr{NP}^B$.
``Richard Ladner has shown that there are oracles $B$ recognizable deterministically in exponential time such that $\mathscr{P}^B\ne\mathscr{NP}^B$.''
\end{quotation}
Is the sparsity of the set $B$ evidence that probably $P\ne NP$? Is it true that $B\in EXP$ or is there some obvious modification to make this true?
\end{exercise}
\subsubsection{The Hartmanis--Hopcroft oracle}
Hartmanis and Hopcroft \cite{hartmanis1976independence} \cite[\S 2, pp.~5--7]{tr-76-296} demonstrated a primitive recursive oracle $L$, such that the problem of whether $P^L=NP^L$ or $P^L\ne NP^L$ is independent of any formal system of arithmetic or set theory under certain very reasonable assumptions of adequacy and consistency. They concluded:
\begin{quote}
``What we have just proven suggests the possibility that the unrelativized $P=NP$ problem could be independent of the axioms of set theory. It may be possible to have two completely consistent theories of computation, one in which $P=NP$ is an axiom and the other in which $P\ne NP$ is an axiom.''
\end{quote}
Except for a survey by Scott Aaronson \cite{aaronsonp}, this possibility has received little attention or further study: by far the majority of the research effort expended on the $P$ vs. $NP$ problem has had as its object an attempt to prove $P\ne NP$, in an almost unshaken conviction that this really is the case and that there really is some way to prove it. Notwithstanding, the investigation of a certain modification of the Hartmanis--Hopcroft ``independent'' oracle is to be the object of our present research.
\subsubsection{Natural proofs and Boolean complexity}
We do not pretend to understand ``natural proofs'' in the context of Razborov and Rudich, and the Boolean circuit complexity theory on which they are based is unfortunately outside our area of expertise; at the same time we would be remiss if we were to omit mention of their award-winning \cite{kehoe2007prize} paper \cite{razborov1997natural}. Our first impression of the general gist of their research is that they showed that if one-way functions exist, and in fact $P\ne NP$, then it will be very difficult, if even possible, to actually prove $P\ne NP$: in other words, an award-winning negative result in the context of the prevailing direction of research into the $P$ vs.\ $NP$ problem.
Another paper \cite{blum2017} has appeared on \href{https://arxiv.org/}{arXiv} claiming a solution to the ``P versus NP Problem,'' also apparently on the basis of Boolean complexity theory. This author claims a result that \mbox{$P\ne NP$}. We remain unconvinced of exponential lower bound proofs of time complexity for computational problems, but at the same time, there seems to be a group of researchers following a certain line of reasoning. We do not wish to discourage them, but we would like to see a ``primer'' or a more solid theoretical foundation based on theorem and proof --- as especially in the case of the Razborov and Rudich paper \cite{razborov1997natural} the claims made by the authors seem a little bit too elusive to nail down to precise logical propositions which may be rigorously stated in the language of set theory.
\subsubsection{The Millennium Prize}
At the turn of the millennium, the Clay Mathematics Institute \cite{claymath} offered prizes \cite{claymath-millenium-prize} of \$1,000,000 (USD) each for the solutions of seven outstanding mathematical problems, among them the $P$ vs.\ $NP$ problem considered herein, which are deemed especially important to the mathematical community. There are official problem descriptions, e.g.~\cite{claymath-pnp-problem-description}, rules \cite{claymath-millennium-prize-rules}, notes on the rules \cite{claymath-notes-on-rules}, and publication guidelines \cite{claymath-publication-guidelines}. There is a markedly patronizing and exclusive air about the whole thing. Furthermore, the offer of a \$1,000,000 sweepstakes-style prize, the broad dismissal of ``amateur'' research, and the open mockery even of professional and academic research, have created a very cramped and limited hang-out for discussion of these important mathematical problems, and as a consequence the development of our understanding of these important mathematical problems has stagnated in the open literature in recent years.
Our suspicions of the Millennium Prize are further raised by the fact that no money has actually been paid out as offered for the one problem that is widely acknowledged as solved \cite{perelman2002,perelman2003,perelman2003-2,rianovosti2010}.
We note that a showing of independence of the problem does not qualify for the prize according to the official rules: only a proof or disproof of the conjecture $P\ne NP$. At the same time, it is important to note that we cannot at this time rule out the existence of an unconditional proof or disproof of the conjecture $P\ne NP$ according to our present understanding of set theory, despite our attempts to do so, which we have documented in this paper.
By far the most serious attempt to date to claim the prize for the $P$ vs.\ $NP$ problem was a 2010 paper by Vinay Deolalikar \cite{deolalikar2010}. This paper was met with a strange reaction from the mathematical ``community'' --- quite a bit of excitement at first, and then vicious and merciless mockery, exaggerated suggestions of a ``flaw'' in the proof, as it were a beautiful woman looking in the mirror on which a speck of dust had settled. Our firm opinion is that such professional academic mathematicians ought to examine the beam in their own eye. They are so free to mock the work of others, and we have no doubt that they have worked on ``the problem'' themselves; yet we do not see these scoffers' attempted proofs in the literature.
\section{Liars' oracles}
We make two modifications of the Hartmanis--Hopcroft oracle, namely to introduce ``escape clauses'' into our version of the oracle ``$H$'' for those cases when the formal system does happen to be inconsistent, and along with the oracle $H$ to introduce a new ``equivalence'' postulate $E^H$, relating the relativized $P^H$ vs.\ $NP^H$ question to the unrelativized $P$ vs.\ $NP$ question. With these modifications we are able to extend their independence result to the original unrelativized problem of whether $P=NP$ or $P\ne NP$.
We also dispense with the postulate $E^H$ in order to introduce another version of the liar's oracle, $J$.
Let us work within some formal system $F$, assuming only that it is capable of sufficient arithmetic to prove G{\"o}del's incompleteness theorems \cite{sep-goedel-incompleteness}.
\begin{construction}\label{oq}
By $Q$ we denote the \textbf{unrelativized proposition} \mbox{$P=NP$}:
\begin{equation}
Q\quad\longleftrightarrow\quad P=NP.
\end{equation}
\end{construction}
\begin{construction}\label{oqo}
For an arbitrary oracle $O$, we denote by $Q^O$ the \textbf{relativized proposition} \mbox{$P^O=NP^O$}:
\begin{equation}
Q^O\quad\longleftrightarrow\quad P^O=NP^O.
\end{equation}
\end{construction}
\begin{construction}\label{oeo}
For an arbitrary oracle $O$, we denote by $E^O$ the \textbf{equivalence postulate} that the relativized proposition $P^O=NP^O$ is of equivalent truth value to the unrelativized proposition $P=NP$:
\begin{equation}
E^O\quad\longleftrightarrow\quad (Q^O\longleftrightarrow Q).
\end{equation}
\end{construction}
\begin{lemma}[Oracles of finite discrepancy]
\label{lemmadelta}
\begin{figure}
\centering
\includegraphics[width=0.40\textwidth]{images/Anonymous.png}
\caption[Examining the discrepancy]{Examining the discrepancy \cite{akshayhallur2014}.}\label{figdiscrepancy}
\end{figure}
If $U$ and $V$ are two oracles whose discrepancy (Figure~\ref{figdiscrepancy}), or symmetric set difference
\begin{equation}
U\operatorname{\triangle} V=\big(U\operatorname\backslash V\big)\cup\big(V\operatorname\backslash U\big)
\end{equation}
is of finite cardinality, that is, if
\begin{equation}
\left|U\operatorname{\triangle} V\right|<\aleph_0,
\end{equation}
then $P^U=P^V$ and $NP^U=NP^V$.
\end{lemma}
\begin{proof}
A finite number of exceptions can be managed within a constant time factor by modifying any Turing machine that queries the oracle.
\end{proof}
\begin{remark}
Hartmanis and Hopcroft state this lemma without proof \cite[\S 2, pp.~5--7]{tr-76-296}.
\end{remark}
\begin{corollary}
If $D$ is a finite set, then $P^D=P$ and $NP^D=NP$.
\end{corollary}
\begin{proof}
$P^\emptyset=P$ and $NP^\emptyset=P$. $D\operatorname\triangle\emptyset=D$ is finite.
\end{proof}
\begin{construction}\label{defgamma}
Let $\big(\gamma(n)\big)_{n\in\mathbb N}$ be an acceptable enumeration of primitive recursive algorithms.
\end{construction}
\begin{construction}\label{defL}
Let $L(\gamma(n))$ be the language recognized by $\gamma(n)$.
\end{construction}
\subsection{The liar's oracle \textit{H}}\label{h}
\subsubsection{Construction of \textit{H}}
\begin{construction}
Let $\eta(n)$ be a primitive recursive function, such that for all natural numbers $x$ and $n$, (as these are encoded as strings over the alphabet $\Sigma$,)
\begin{equation}
x\in L(\gamma(\eta(n)))\label{oeta0}
\end{equation}
if and only if
\begin{align}
\begin{gathered}\label{oeta1}
\Big(\big(F\vdash_{\#\le x}E^{L(\gamma(n))}\longrightarrow \lnot Q^{L(\gamma(n))}\big)
\quad\land \qquad\qquad\\\qquad \lnot\big(F\vdash_{\#\le x}E^{L(\gamma(n))}\longrightarrow Q^{L(\gamma(n))}\big)
\quad\land\quad x\in A\Big) \\
\lor\\
\Big(\big(F\vdash_{\#\le x}E^{L(\gamma(n))}\longrightarrow Q^{L(\gamma(n))}\big)
\quad\land \qquad\qquad\\\qquad \lnot\big(F\vdash_{\#\le x}E^{L(\gamma(n))}\longrightarrow \lnot Q^{L(\gamma(n))}\big)
\quad\land\quad x\in B\Big),
\end{gathered}
\end{align}
where, for example, ``$F\vdash_{\#\le x}S$'' denotes the existence in the formal system $F$ of a valid proof with G\"odel number not exceeding $x$ (in some acceptable enumeration) of the statement $S$, and $A$ and $B$ are primitive recursive oracles such that $P^A=NP^A$ and $P^B\ne NP^B$.
\end{construction}
\begin{theorem}\label{etafix}
The function $\eta$ has a fixed point $\psi$. We do \textbf{not} mean as one may expect from an elementary textbook definition, that $\eta(\psi)=\psi$, but we \textbf{do} mean that there exists a numeral, that is, a canonical representation of a real natural number, which when substituted for the variable $\psi$ makes the expression
\begin{equation}
L(\gamma(\eta(\psi)))=L(\gamma(\psi))\label{ofix}
\end{equation}
both true\footnote{That is, ``true'' in the disquotational sense that ``$X$'' and ``\,`$X$' is true'' both have exactly the same meaning.} and provable.
\end{theorem}
\begin{proof}
Refer to \cite[\S 2, pp.~5--7]{tr-76-296}. We stress the use of Kleene's $s^m_n$ and recursion theorems \cite{kleene1936}. We also recommend the proof of Kurt G\"odel's diagonalization lemma \cite{sep-goedel-incompleteness-sup2}. (See also \cite{lindstrom2006note}.)
\end{proof}
\begin{construction}
Having established the existence of the fixed point, which we now call simply $\psi$, we define the oracle
\begin{equation}
H:=L(\gamma(\psi)).\label{oh}
\end{equation}
in order to substitute equations (\ref{oh}) and (\ref{ofix}) into (\ref{oeta0}) to obtain (\ref{seta0}), and (\ref{oh}) into (\ref{oeta1}) to obtain (\ref{seta1}), so that we have for all $x\in\mathbb N$,
\begin{equation}
x\in H\label{seta0}
\end{equation}
if and only if
\begin{align}
\begin{gathered}\label{seta1}
\Big(\big(F\vdash_{\#\le x}E^H\rightarrow \lnot Q^H\big)
\land\lnot\big(F\vdash_{\#\le x}E^H\rightarrow Q^H\big)
\land x\in A\Big) \\
\lor\\
\Big(\big(F\vdash_{\#\le x}E^H\rightarrow Q^H\big)
\land\lnot\big(F\vdash_{\#\le x}E^H\rightarrow \lnot Q^H\big)
\land x\in B\Big);
\end{gathered}
\end{align}
where $A, B \in PR$, $P^A=NP^B$, $P^B\ne NP^B$. Recall from \Construction\Construction \ref{oq}--\ref{oeo} that
\begin{align}
Q\quad&\longleftrightarrow\quad P=NP;\label{sq}\\
Q^H\quad&\longleftrightarrow\quad P^H=NP^H;\label{sqh}\\
E^H\quad&\longleftrightarrow\quad (Q^H\longleftrightarrow Q)\label{seh}\\
\quad&\longleftrightarrow\quad\big(Q^H\land Q\big)\lor\big(\lnot Q^H\land\lnot Q\big)\label{sehv}\\
&\longleftrightarrow\quad \big(P^H=NP^H\land P=NP\big)\lor\big(P^H\ne NP^H\land P\ne NP\big).\label{sehx}
\end{align}
\end{construction}
\subsubsection{Theorems on \textit{H}}
\begin{theorem}
If the postulate $E^H$ can be refuted from the axioms of $F$, then $F$ is inconsistent.
\end{theorem}
\begin{proof}
If the formal system $F$ is inconsistent, then $H$ is a finite set, since in this case every statement is provable. If
\begin{equation}
F\vdash \lnot E^H,
\end{equation}
then from (\ref{sehx}),
\begin{equation}
F\vdash \big(P^H\ne NP^H\land P=NP\big)\lor\big(P^H=NP^H\land P\ne NP\big),
\end{equation}
in either case proving that $H$ is an infinite set. But if $H$ is an infinite set, then $F$ is consistent. Thus any refutation of $E^H$ from the axioms of $F$ implies a proof in $F$ that $F$ is consistent, and by G\"odel's second incompleteness theorem, $F$ is inconsistent in that case.
\end{proof}
\begin{theorem}\label{ehcnsv}
If the proposition $Q$, (i.e.~$P=NP$,) is provable or refutable from the axioms of $F$ under the supposition $E^H$, (i.e.~$Q^H\longleftrightarrow Q$,) then it is so provable or refutable from the axioms of $F$ alone.
\end{theorem}
\begin{proof}
\begin{align}
(F\vdash E^H\longrightarrow Q)\quad
&\longrightarrow\quad(F\vdash E^H\longrightarrow Q^H);\label{fehq0}\\
&\longrightarrow\quad(\lnot E^H\longrightarrow Q);\label{fehq1}\\
&\longrightarrow\quad(F\vdash\lnot E^H\longrightarrow Q);\label{fehq2}\\
&\longrightarrow\quad(F\vdash Q);\label{fehq3}\\
(F\vdash E^H\rightarrow\lnot Q)\quad
&\longrightarrow\quad(F\vdash E^H\longrightarrow\lnot Q^H);\label{fehnq0}\\
&\longrightarrow\quad(\lnot E^H\longrightarrow\lnot Q);\label{fehnq1}\\
&\longrightarrow\quad(F\vdash\lnot E^H\longrightarrow\lnot Q);\label{fehnq2}\\
&\longrightarrow\quad(F\vdash\lnot Q).\label{fehnq3}
\end{align}
The equivalences (\ref{fehq0}) and (\ref{fehnq0}) follow from (\ref{seh}); (\ref{fehq1}) and (\ref{fehnq1}) from the ``clever'' (\ref{seta0}--\ref{seta1}) construction of $H$; (\ref{fehq2}) and (\ref{fehnq2}) by necessitation. The conclusions (\ref{fehq3}) and (\ref{fehnq3}) follow from the premises (\ref{fehq0}) and (\ref{fehnq0}) and from (\ref{fehq2}) and (\ref{fehnq2}).
\end{proof}
\begin{remark}
As to the $P$ vs.\ $NP$ question, there is no loss of generality in adjoining the postulate $E^H$ to the axioms of $F$, for if this question is independent of $F$, then it is also independent of $F+E^H$. That is, if we can prove in $F$ that neither $F+E^H\vdash P=NP$ nor $F+E^H\vdash P\ne NP$, unless $F+E^H$ is inconsistent, then we also have a valid proof in $F$ that neither $F\vdash P=NP$ nor $F\vdash P\ne NP$, unless $F$ is inconsistent. The limitation remains that we cannot use the postulate $E^H$, without having proven it, to reason about the existence of proofs in $F$ or $F+E^H$, if we wish our reasoning to be valid in $F$ alone.
\end{remark}
\subsection{The liar's oracle \textit{J}}
\subsubsection{Construction of \textit{J}}
The construction of the liar's oracle $J$ is similar to that of $H$, but we have eliminated the ``equivalence postulate'' from its construction.
Recall $\gamma(n)$ and $L(\gamma(n))$ from \Construction\Construction \ref{defgamma} and \ref{defL}.
\begin{construction}
Let $\iota(n)$ be a primitive recursive function such that
\begin{equation}
x\in L(\gamma(\iota(n)))
\end{equation}
if and only if
\begin{align}
\begin{gathered}\label{oiota1}
\Big(\big(F\vdash_{\#\le x}\lnot Q^{L(\gamma(n))}\big)
\land\lnot\big(F\vdash_{\#\le x}Q^{L(\gamma(n))}\big)
\land x\in A\Big) \\
\lor\\
\Big(\big(F\vdash_{\#\le x}Q^{L(\gamma(n))}\big)
\land\lnot\big(F\vdash_{\#\le x}\lnot Q^{L(\gamma(n))}\big)
\land x\in B\Big).
\end{gathered}
\end{align}
\end{construction}
\begin{theorem}\label{iotafixedpoint}
The function $\iota$ has a fixed point $\phi$ such that
\begin{equation}
L(\gamma(\iota(\phi)))=L(\gamma(\phi)).
\end{equation}
\end{theorem}
\begin{proof}
\Theorem \ref{etafix}.
\end{proof}
\begin{construction}
With the fixed point $\phi$ of \Theorem \ref{iotafixedpoint}, the liar's oracle $J$ is defined
\begin{equation}
J:=L(\gamma(\phi))
\end{equation}
so that
\begin{equation}\label{siota0}
x\in J
\end{equation}
if and only if
\begin{align}
\begin{gathered}\label{siota1}
\Big(\big(F\vdash_{\#\le x}\lnot Q^J\big)
\land\lnot\big(F\vdash_{\#\le x}Q^J\big)
\land x\in A\Big) \\
\lor\\
\Big(\big(F\vdash_{\#\le x}Q^J\big)
\land\lnot\big(F\vdash_{\#\le x}\lnot Q^J\big)
\land x\in B\Big).
\end{gathered}
\end{align}
\end{construction}
\subsubsection{Theorems on \textit{J}}
\begin{lemma}\label{prqj}
To prove or refute the relativized proposition $Q^J$ from the axioms of $F$ is to prove or refute the corresponding unrelativized proposition $Q$ and at the same time to prove that the system $F$ is inconsistent:
\begin{align}
(F\vdash Q^J)&\longleftrightarrow(F\vdash Q)\land(F\vdash(F\vdash\bot));\\
(F\vdash\lnot Q^J)&\longleftrightarrow(F\vdash\lnot Q)\land(F\vdash(F\vdash\bot)).
\end{align}
\end{lemma}
\begin{proof}
If the system $F$ is inconsistent, then $J$ is a finite set, and by \Construction\Construction \ref{oq}--\ref{oeo} and \Lemma \ref{lemmadelta}, the relativized proposition $Q^J$ is equivalent to the unrelativized proposition $Q$.
($\longrightarrow$)
\begin{align}
(F\vdash Q^J)&\longrightarrow\lnot Q^J\lor(F\vdash\bot)\\
&\longrightarrow(F\vdash\lnot Q^J\lor(F\vdash\bot))\\
&\longrightarrow(F\vdash(F\vdash\bot)\land |J|<\aleph_0\land Q);\\
(F\vdash\lnot Q^J)&\longrightarrow\lnot Q^J\lor(F\vdash\bot)\\
&\longrightarrow(F\vdash Q^J\lor(F\vdash\bot))\\
&\longrightarrow(F\vdash(F\vdash\bot)\land |J|<\aleph_0\land\lnot Q).
\end{align}
($\longleftarrow$)
\begin{align}
(F\vdash Q\land(F\vdash\bot))&\longrightarrow (F\vdash |J|<\aleph_0\land Q^J);\\
(F\vdash\lnot Q\land(F\vdash\bot))&\longrightarrow (F\vdash |J|<\aleph_0\land\lnot Q^J).
\end{align}
\end{proof}
\begin{theorem}\label{jind}
To prove that the relativized proposition $Q^J$ is independent of the axioms of $F$ is equivalent to proving the independence of the unrelativized proposition $Q$:
\begin{equation}
(F\vdash(F\vdash Q^J)\longleftrightarrow(F\vdash\lnot Q^J))
\longleftrightarrow
(F\vdash(F\vdash Q)\longleftrightarrow(F\vdash\lnot Q)).
\end{equation}
\end{theorem}
\begin{proof}
($\longleftarrow$) If
\begin{equation}\label{jind0}
(F\vdash Q)\longleftrightarrow(F\vdash\lnot Q),
\end{equation}
then by \Lemma \ref{prqj}, $|J|<\aleph_0$ and
\begin{align}\label{jind1}
(F\vdash(F\vdash\bot))&\longrightarrow((F\vdash Q^J)\longleftrightarrow(F\vdash\lnot Q^J));\\
(F\nvdash(F\vdash\bot))&\longrightarrow ((F\nvdash Q^J)\land(F\nvdash\lnot Q^J))\label{jind2}\\
&\longrightarrow ((F\vdash Q^J)\longleftrightarrow(F\vdash\lnot Q^J));\label{jind3}
\end{align}
so in either case, (\ref{jind1}) or (\ref{jind2}--\ref{jind3}),
\begin{equation}
(F\vdash Q^J)\longleftrightarrow(F\vdash\lnot Q^J).\label{jind4}
\end{equation}
We have obtained (\ref{jind4}) as a logical consequence of (\ref{jind0}): if (\ref{jind0}) is \textit{provable} from the axioms of $F$, then so is (\ref{jind4}).
($\longrightarrow$)
\begin{align}
(F\vdash(F\vdash Q^J)\longleftrightarrow(F\vdash\lnot Q^J))
&\longrightarrow (F\vdash |J|<\aleph_0)\\
&\longrightarrow (F\vdash E^J)\\
&\longrightarrow (F\vdash(F\vdash E^J))\\
&\longrightarrow(F\vdash(F\vdash Q)\longleftrightarrow(F\vdash\lnot Q)).
\end{align}
\end{proof}
\subsubsection{Theorems relating \textit{J} to \textit{H}}
\begin{theorem}\label{ehimpej}
$E^H\longrightarrow E^J$.
\end{theorem}
\begin{proof}
Consider three cases: first, if both $Q$ and $\lnot Q$ are provable, then the formal system $F$ is inconsistent, both the antecedent and the consequent are true, and the implication is satisfied. Second, if neither $Q$ nor $\lnot Q$ is provable, then $H=J=\emptyset$ and likewise the antecedent and consequent are both true, satisfying the implication. We are left with the third case: the proposition $Q$ is either provable or refutable, but not both: under the supposition $E^H$, the proposition $Q^H$ is either provable or refutable, but not both.\footnote{See also \Theorem \ref{ehcnsv}.}
There are two sub-cases. If the formal system $F$ is sound with respect to proving or refuting $Q$, that is, if $(F\vdash Q)\land Q$ or $(F\vdash\lnot Q)\land\lnot Q$, then $Q^H$ is not of the same truth value as $Q$, and the antecedent $E^H$ is false, satisfying the implication vacuously.
If, on the other hand, $(F\vdash Q)\land\lnot Q$~\footnote{$F$ is $\Sigma_2$-unsound in this case.} or $(F\vdash\lnot Q)\land Q$,\footnote{$F$ is $\Sigma_1$-unsound in this case.} then $E^H$ is true, and it remains to prove $E^J$. If $Q^J$ is neither provable nor refutable, then $J=\emptyset$ and $E^J$ is true. Otherwise, $(F\vdash Q\land Q^J)\land\lnot Q\land\lnot Q^J$ or $(F\vdash\lnot Q\land\lnot Q^J)\land Q\land Q^J$.
\end{proof}
\begin{corollary}\label{ejcnsv}
If the proposition $Q$, (i.e.~$P=NP$,) is provable or refutable from the axioms of $F$ under the supposition $E^J$, (i.e.\ $Q^J\longleftrightarrow Q$,) then it is so provable or refutable from the axioms of $F$ alone:
\begin{align}
(F\vdash E^J\longrightarrow Q)\quad
&\longrightarrow\quad(F\vdash Q);\\
(F\vdash E^J\longrightarrow\lnot Q)\quad
&\longrightarrow\quad(F\vdash\lnot Q).
\end{align}
\end{corollary}
\begin{proof}
Theorems \ref{ehcnsv} and \ref{ehimpej}.
\end{proof}
\begin{remark}
\begin{align}
(F\vdash \lnot Q^J\longrightarrow Q)\quad
&\longrightarrow\quad(F\vdash Q);\\
(F\vdash Q^J\longrightarrow\lnot Q)\quad
&\longrightarrow\quad(F\vdash\lnot Q).
\end{align}
\end{remark}
\begin{theorem}\label{fejimpqjeqqh}
$(F\vdash E^J)\longrightarrow(Q^J\longleftrightarrow Q^H)$
\end{theorem}
\begin{proof}
If $F\vdash E^J$, then
\begin{align}
(F\vdash Q^J)&\longleftrightarrow(F\vdash Q);\\
(F\vdash\lnot Q^J)&\longleftrightarrow(F\vdash\lnot Q);
\end{align}
and by theorem~\ref{ehcnsv},
\begin{align}
(F\vdash Q^J)&\longleftrightarrow(F\vdash E^H\longrightarrow Q^H);\\
(F\vdash\lnot Q^J)&\longleftrightarrow(F\vdash E^H\longrightarrow\lnot Q^H);
\end{align}
so, taking into consideration how the oracle $J$ was constructed similarly to $H$, we have $Q^J\longleftrightarrow Q^H$ in all cases.
\end{proof}
\begin{corollary}\label{fqhimpejeqeh}
$(F\vdash E^H\lor E^J)\longrightarrow (E^J\longleftrightarrow E^H)\land(F\vdash E^H\land E^J)$.
\end{corollary}
\begin{proof}
\Theorem \ref{ehimpej}, \Theorem\ref{fejimpqjeqqh}.
\end{proof}
\begin{corollary}\label{ejeqeh}
$(F\vdash E^J)\quad\longleftrightarrow\quad(F\vdash E^H)$
\end{corollary}
\begin{proof}
\Corollary \ref{fqhimpejeqeh}.
\end{proof}
\begin{theorem}\label{theoremx}
If the postulate $E^H$ is provable from the axioms of $F$, then the symmetric difference between the oracles $H$ and $J$ is finite:
\begin{align}
(F\vdash E^H)\quad\longrightarrow\quad\left|H\operatorname\triangle J\right|<\aleph_0.
\end{align}
\end{theorem}
\begin{proof}
If $F\vdash E^H$, then by \Corollary \ref{ejeqeh}, $F\vdash E^J$ so
\begin{align}
(F\vdash Q)\quad
&\longleftrightarrow\quad(F\vdash E^H\longrightarrow Q^H) \\
&\longleftrightarrow\quad(F\vdash Q^J); \\
(F\vdash\lnot Q)\quad
&\longleftrightarrow\quad(F\vdash E^H\longrightarrow\lnot Q^H) \\
&\longleftrightarrow\quad(F\vdash\lnot Q^J).
\end{align}
Now by the construction of the oracles $H$ (\ref{seta0}--\ref{seta1}) and $J$ (\ref{siota0}--\ref{siota1}), their symmetric difference is finite, i.e., $\left|H\operatorname\triangle J\right|<\aleph_0$.
\end{proof}
\begin{theorem}
If $\left|H\operatorname\triangle J\right|<\aleph_0$, then
\end{theorem}
\begin{remark}
We are really more interested in the case where $|H\operatorname{\triangle}J|=\aleph_0$.\footnote{From the point of view of mainstream research, this is indeed the most likely case, if, as most researchers seem to believe, there is some proof of $P\ne NP$, or possibly even $P=NP$, from the axioms of a system like \textbf{ZFC}, and as long as we assume that $\textbf{ZFC}\nvdash(\textbf{ZFC}\vdash\bot)$.} In this case $E^H$ is neither provable nor refutable from the axioms of $F$. The proposition $Q$ is either provable or refutable, but not both, from the axioms of $F$. The oracle $J$ is the empty set, since $Q^J$ is neither provable nor refutable. Hence there is no proof in $F$ that $F$ is inconsistent. The proposition $Q^H$ is of the opposite truth value from that which $Q$ is proven to be, but neither provable nor refutable.
\end{remark}
In order to prove or refute $Q$, we need only consider the case where $H\operatorname{\triangle}J$ is finite, and we may further suppose that there already is some proof or refutation of $Q$.
Now either $F\vdash E^H\longrightarrow Q^H$ or $F\vdash E^H\longrightarrow\lnot Q^H$, and hence\footnote{Consider separately the case where $F$ is inconsistent.} either $F\vdash Q^J$ or $F\vdash\lnot Q^J$.
\begin{equation}
F\vdash(F\vdash\bot)
\end{equation}
\begin{theorem}
If the proposition $Q$, (i.e., $P=NP$,) is provable or refutable from the axioms of $F$ under the supposition $|J|<\aleph_0$, (i.e., $J$ is finite,) then it is so provable or refutable from the axioms of $F$ alone. \textbf{\color{red}???}
\end{theorem}
\begin{proof}
Suppose $F+\lnot Q\vdash (F\nvdash\bot)$. If $F+\lnot Q\vdash (F\nvdash Q)$, then by Kurt G\"odel's second incompleteness theorem, $F+\lnot Q$ is inconsistent, and $F\vdash Q$. If $F+\lnot Q\vdash (F\nvdash\lnot Q)$, then $(F\vdash\lnot Q)\longrightarrow(F\vdash\bot)$
\textbf{\color{red}???}
\end{proof}
\subsection{The liar's oracle \textit{K}}
\subsubsection{Construction of \textit{K}}
The construction of the liar's oracle $K$, like $J$, is similar to that of $H$, but the ``equivalence postulate'' $E^H$ has been replaced by the postulate that $K$ is a finite set.
Recall $\gamma(n)$ and $L(\gamma(n))$ from \Construction\Construction \ref{defgamma} and \ref{defL}.
\begin{construction}
Let $\kappa(n)$ be a primitive recursive function such that
\begin{equation}
x\in L(\gamma(\kappa(n)))
\end{equation}
if and only if
\begin{align}
\begin{gathered}\label{okappa1}
\Big(\big(F\vdash_{\#\le x}|L(\gamma(n))|<\aleph_0\longrightarrow \lnot Q^{L(\gamma(n))}\big)
\\\land\quad\lnot\big(F\vdash_{\#\le x}|L(\gamma(n))|<\aleph_0\longrightarrow Q^{L(\gamma(n))}\big)
\quad\land\quad x\in A\Big) \\
\lor\\
\Big(\big(F\vdash_{\#\le x}|L(\gamma(n))|<\aleph_0\longrightarrow Q^{L(\gamma(n))}\big)
\\\land\quad\lnot\big(F\vdash_{\#\le x}|L(\gamma(n))|<\aleph_0\longrightarrow \lnot Q^{L(\gamma(n))}\big)
\quad\land\quad x\in B\Big).
\end{gathered}
\end{align}
\end{construction}
\begin{theorem}\label{kappafixedpoint}
The function $\kappa$ has a fixed point $\lambda$ such that
\begin{equation}
L(\gamma(\kappa(\lambda)))=L(\gamma(\lambda)).
\end{equation}
\end{theorem}
\begin{proof}
\Theorem \ref{etafix}.
\end{proof}
\begin{construction}\label{constructk}
With the fixed point $\lambda$ of \Theorem \ref{kappafixedpoint}, the liar's oracle $K$ is defined
\begin{equation}
K:=L(\gamma(\lambda))
\end{equation}
so that
\begin{equation}\label{skappa0}
x\in K
\end{equation}
if and only if
\begin{align}
\begin{gathered}\label{skappa1}
\Big(\big(F\vdash_{\#\le x}|K|<\aleph_0\longrightarrow \lnot Q^K\big)
\land\lnot\big(F\vdash_{\#\le x}|K|<\aleph_0\longrightarrow Q^K\big)
\land x\in A\Big) \\
\lor\\
\Big(\big(F\vdash_{\#\le x}|K|<\aleph_0\longrightarrow Q^K\big)
\land\lnot\big(F\vdash_{\#\le x}|K|<\aleph_0\longrightarrow \lnot Q^K\big)
\land x\in B\Big).
\end{gathered}
\end{align}
\end{construction}
\subsubsection{Theorems on \textit{K}}
\begin{theorem}
If $|K|<\aleph_0$, then
\begin{equation}\label{tk0}
(F\vdash P=NP)\longleftrightarrow(F\vdash P\ne NP).
\end{equation}
\end{theorem}
\begin{proof}
Suppose (\ref{tk0}) is false. Then ``$P=NP$'' is either provable or refutable but not both. No formal system $F$, if it is consistent, can refute ``$K<\aleph_0$;'' otherwise $F$, proving its own consistency, would be inconsistent by G{\"o}del's second incompleteness theorem. Consequently ``$P=NP$,'' or equivalently $P^K=NP^K$, or $Q^K$, is either provable or refutable under the supposition ``$|K|<\aleph_0$,'' but not both. Hence $K$, by its construction \Construction\ref{constructk} (\ref{skappa0}--\ref{skappa1}), includes either all but finitely many elements of the infinite set $A$ or all but finitely many elements of the infinite set $B$, in either case contradicting the original supposition $|K|<\aleph_0$.
\end{proof}
\appendix
\section{Zermelo--Fraenkel set theory}\label{sect-zf}
\subsection{Introduction}
\begin{figure}
\centering
\begin{minipage}{2in}
\centering
\includegraphics[width=1.5in]{images/PortraitZurich-sw-nb-300.jpg}
\end{minipage}
\begin{minipage}{2.25in}
\centering
\includegraphics[width=1.75in]{images/Adolf_Abraham_Halevi_Fraenkel.jpg}
\end{minipage}
\caption[Ernst Zermelo and Abraham Fraenkel]{Set theorists Ernst Friedrich Ferdinand Zermelo \cite{mildenberger2014}, left; and Abraham Halevi ``Adolf'' Fraenkel \cite{fraenkel-photo}, right.}\label{zfphoto}
\end{figure}
Zermelo--Fraenkel set theory is a theory of well-founded sets named after the German-born set theorists Ernst Zermelo (1871--1953) and Abraham Fraenkel (1891--1965), both of whom are pictured in Figure \ref{zfphoto}. The men went their separate ways. Zermelo remained at the University of Berlin, where he had received his doctorate in 1894. Fraenkel was active in the Mizrachi religious Zionist movement \cite{cohen-mansfield2016}, and about the beginning of the Great Depression, he exercised what would later, after the war, become Israel's Law of Return to take a post as the first Dean of Mathematics at the Hebrew University of Jerusalem.
\begin{definition}\label{def-set}
In this theory, every \textbf{set} is a collection of things, and every thing in existence is a \textbf{set}.
\end{definition}
\begin{definition}
When a thing $x$ is a \textbf{member} or \textbf{element} of the collection $C$, we use the symbol $\in$, a stylized stick figure of the lower-case Greek letter epsilon,\footnote{Cf.\ elementhood symbol {\huge$\in$}, lower-case epsilon {\huge$\epsilon$}, set in huge type. This and many other symbols of set theory were invented by Giuseppe Peano \cite{peano1901}, Figure \ref{peanophoto}.} and we write \mbox{$x\in C$}. Alternatively we may say that the collection $C$ \textbf{includes} the element $x$, and write \mbox{$C\ni x$}.
\end{definition}
\begin{definition}\label{def-well-founded}
A set $X$ is said to be \textbf{well-founded} if there is \textbf{\textit{no}} infinite descending chain of membership or elementhood from $X$:
\begin{equation}
X\ni X_1
\land X_1\ni X_2
\land X_2\ni X_3
\land X_3\ni \cdots\label{idcx}
\end{equation}
\end{definition}
\begin{remark}
If there \textit{is} such an infinite descending chain (\ref{idcx}) from $X$, we say that the set $X$ is \textit{ill-founded}. The axioms of Zermelo--Fraenkel set theory preclude the existence of ill-founded sets.\footnote{Those who tell stories of ``turtles all the way down'' and other New Age nonsense are talking about an ill-founded world. Those of such beliefs who admit the existence of such sets may study instead Willard Van Orman Quine's New Foundations set theory \cite{sep-quine-nf} which is based on stratified types and does admit ``turtles all the way down.'' Many open questions remain, and although it is now many years old, New Foundations set theory has not yet undergone a sufficient critical assessment to determine its fitness to serve as a foundation for mathematics and computer science.}
\end{remark}
\begin{definition}
When every thing that is a member of a collection $B$ is also a member of the collection $C$, we write \mbox{$B\subset C$} and say that $B$ \textbf{is contained in} $C$, or that $C$ \textbf{contains} $B$; alternatively we may write \mbox{$C\supset B$}.
\end{definition}
\begin{definition}\label{def-eq}
We say that the sets $A$ and $B$ are \textbf{equal} and we write $A=B$ if $A\subset B$ and $B\subset A$.
\end{definition}
\begin{definition}
If $C$ contains $B$, and there exists some member of the collection $C$ that is not a member of the collection $B$, then we say that $C$ \textbf{properly contains}\footnote{Alternatively, ``\textbf{\textit{properly extends}}'' or similar language.} $B$. This is sometimes written \mbox{$C\supsetneqq B$}, or \mbox{$B\subsetneqq C$}. $P$ and $NP$ from the title of this paper, but we mention as an example at this point that while we know that $P\subset NP$, the whole $P$ vs.\ $NP$ question rests on whether or not $NP$ properly contains $P$.
\end{definition}
\begin{remark}
If a set $A$ is contained in the set $B$, then $A$ is either equal to $B$ or properly contained in $B$:
\begin{equation}
A\subset B\longrightarrow A=B\lor A\subsetneqq B.
\end{equation}
The entire $P$ vs.\ $NP$ question is the question of whether \mbox{$P=NP$} or \mbox{$P\subsetneqq NP$}, since we know that \mbox{$P\subset NP$}.
\end{remark}
\subsection{Language of set theory}
\begin{table}
\begin{bnf*}
\bnfprod{wff}
{\bnfpn{f5}}\\
\bnfprod{f5}
{\bnfpn{f4}\bnfor\bnfpn{f4}\longleftrightarrow\bnfpn{f4}}\\
\bnfprod{f4}
{\bnfpn{f3}\bnfor\bnfpn{f4}\longleftarrow\bnfpn{f3}}\\
\bnfprod{f3}
{\bnfpn{f2} \bnfor \bnfpn{f2} \longrightarrow \bnfpn{f3}}\\
\bnfprod{f2}
{\bnfpn{f1} \bnfor \bnfpn{f2} \lor \bnfpn{f1}}\\
\bnfprod{f1}
{\bnfpn{f0} \bnfor \bnfpn{f1} \land \bnfpn{f0}}\\
\bnfprod{f0}\label{fprod}
{\bnfpn{set}\bnfpn{b}\bnfpn{set}
\bnfor \lnot\bnfpn{f0}
\bnfor (\bnfpn{wff})}\\
&&{ \bnfor (\exists\bnfpn{var})\bnfpn{f0}
\bnfor (\forall\bnfpn{var})\bnfpn{f0}
\bnfor \top \bnfor \bot
}\\
\bnfprod{set}
{\bnfpn{s5}}\\
\bnfprod{s5}
{\bnfpn{s4}\bnfor\bnfpn{s4}\,\backslash\,\bnfpn{s5}}\\
\bnfprod{s4}
{\bnfpn{s3}\bnfor\bnfpn{s4}\,\triangle\,\bnfpn{s3}}\\
\bnfprod{s3}
{\bnfpn{s2}\bnfor\bnfpn{s3}\,\cup\,\bnfpn{s2}}\\
\bnfprod{s2}
{\bnfpn{s1}\bnfor\bnfpn{s2}\,\cap\,\bnfpn{s1}}\\
\bnfprod{s1}
{\bnfpn{s0}\bnfor\bnfpn{s1}\times\bnfpn{s0}\\}
\bnfprod{s0}
{\bnfpn{var}\bnfor\bigcup\bnfpn{s0}\bnfor\{\bnfpn{ss}\}\bnfor(\bnfpn{ss})}\\
&&{\bnfor\{\bnfpn{var}\in\bnfpn{set}|\bnfpn{wff}\}}\\
\bnfprod{ss}
{\bnfpn{set}\bnfor\bnfpn{ss},\bnfpn{set}}\\
\bnfprod{b}
{\in \bnfor \notin \bnfor \ni \bnfor \not\ni
\bnfor \subset \bnfor \not\subset
\bnfor \supset \bnfor \not\supset
\bnfor = \bnfor \neq
\bnfor \subsetneqq \bnfor \supsetneqq}\\
\bnfprod{var}\label{varprod}
{\textit{A}\bnfsk\textit{Z}
\bnfor \textit{a}\bnfsk\textit{z}
\bnfor \alpha \bnfsk \omega
\bnfor \bnfsk}
\end{bnf*}
\caption{Context-free grammar for set theory}\label{settheorygrammar}
\end{table}
\begin{definition}
A \textbf{well-formed formula} is best defined in Backus--Naur form as a context-free grammar as in Grammar~\ref{settheorygrammar}.
Beginning from the initial symbol $\bnfpn{wff}$, productions are carried out by replacing a symbol to the left of ``$\bnfpo$'' by one of the alternatives (sequences or strings of symbols) listed on the right, separated by vertical bars. Those symbols enclosed by angle brackets $\bnfpn{\dots}$ are non-terminal, and production must continue until all non-terminal symbols have been replaced by literal non-bracketed terminal symbols.
Whenever a well-formed formula is generated by Grammar~\ref{settheorygrammar}, rules for the scoping of variables ``$\bnfpn{var}$'' must be applied as expressions are generated by this grammar, in particular with respect to the ``binding'' productions
$(\exists\bnfpn{var})\bnfpn{f}$,
$(\forall\bnfpn{var})\bnfpn{f}$, and
$\{\bnfpn{var}\in\bnfpn{set}\,|\,\bnfpn{wff}\}$,
Any free variable $\bnfpn{var}$ occurring in a formula $\bnfpn{f}$ or $\bnfpn{wff}$ is considered to remain free until it is bound by the explicit use of an existential $(\exists\cdots)$ or universal $(\forall\cdots)$ quantifier or set-builder $\{\cdots\in\cdots\,|\,\cdots\}$ notation. A well-formed formula may be denoted at a more abstract ``meta'' level by a greek letter followed by its list of free variables (if any) in parentheses, e.g. $\varphi(x,y,z)$.
The major significance of the concept of ``well-formed formula'' is that such formulas are non-trivial to define, and the axiom schemata of Zermelo--Fraenkel set theory do depend on such a rigorous definition. We do not propose at this time that Grammar~\ref{settheorygrammar} is complete or correct or that it corresponds to common or accepted usage.
\end{definition}
\begin{definition}
The main \textbf{verbs} of the language of set theory are defined here.
\begin{align}
X\in Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} is an element of \textit{Y}.''}\\
X\notin Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} is not an element of \textit{Y}.''}\\
X\ni Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} includes (as an element) \textit{Y}.''}\\
X\not\ni Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} does not include \textit{Y}.''}\\
X\subset Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} is contained in \textit{Y}.''}\\
X\not\subset Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} is not contained in \textit{Y}.''}\\
X\supset Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} contains \textit{Y}.''}\\
X\not\supset Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} does not contain \textit{Y}.''}\\
X=Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} equals \textit{Y}.''}\\
X\ne Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} does not equal \textit{Y}.''}\\
X\subsetneqq Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} is properly contained in \textit{Y}.''}\\
X\supsetneqq Y \quad&\longleftrightarrow\quad \textrm{``\textit{X} properly contains \textit{Y}.''}
\end{align}
\end{definition}
\begin{definition}
The \textbf{binary set operations} of \textbf{intersection} (\ref{def-n}), union (\ref{def-u}), \textbf{difference} (\ref{def-diff}), \textbf{discrepancy} or \textbf{symmetric difference} (\ref{def-disc}), and \textbf{Cartesian product} (\ref{def-cart-prod}) are defined.
\begin{align}
X\cap Y&=\{x\in X|x\in Y\};\label{def-n}\\
X\cup Y&=\bigcup\{X,Y\};\label{def-u}\\
X\operatorname{\backslash}Y&=\{x\in X|x\notin Y\};\label{def-diff}\\
X\operatorname{\triangle}Y&=(X\operatorname{\backslash}Y)\cup(Y\operatorname{\backslash}X);\label{def-disc}\\
X\times Y
&=
\left\{
p\in\mathscr P\big(\mathscr P(X\cup Y)\big)
\left|
\begin{array}{r}(\exists y)\\(\exists x)\end{array}\left(\begin{array}{r}\big\{\{x\},\{x,y\}\big\}=p\\\land\, x\in X \land y\in Y\end{array}\right)
\right.
\right\}.\label{def-cart-prod}
\end{align}
\end{definition}
\subsection{Basic axioms}\label{sect-zf-axioms}
\begin{definition}
The symbol $\exists$, an upside-down stick figure of the upper-case letter `E,' is called the \textbf{existential quantifier}, and it is used to assert the existence of some thing satisfying the formula immediately following.
\end{definition}
\begin{definition}
The symbol $\forall$, an upside-down stick figure of the upper-case letter `A,' is called the \textbf{universal quantifier}, and it is used to make a statement that every thing in existence satisfies the formula immediately following.
\end{definition}
\begin{axiom}[Power Set]\label{powerset}
For any given set $q$, there is a set $p$ such that every subset of $q$ is an element of $p$.
\begin{equation}
(\forall q)(\exists p)(\forall s)(s\subset q\longrightarrow s\in p).
\end{equation}
\end{axiom}
\begin{axiom}[Union]\label{unionset}
If $w$ is a set, then there exists a set $u$ including all elements of elements of $w$.
\begin{equation}
(\forall w)(\exists u)(\forall z)\,\big(z\in u\longleftarrow(\exists x)(z\in x\land x\in w)\big).
\end{equation}
\end{axiom}
\begin{axiom}[Infinity] \label{infinityset}
There exists a non-empty set $\omega$ including, for every set $\alpha$, also a set $\beta$, being a proper superset of $\alpha$:
\begin{equation}
(\exists \omega)\bigg((\exists \alpha)\, \alpha\in \omega\land (\forall \alpha)\big(\alpha\in \omega\longrightarrow (\exists\beta)(\beta\in\omega\land\beta\supsetneqq\alpha)\big)\bigg)
\end{equation}
\end{axiom}
\subsection{Axiom schemata}\label{zf-sect-schemata}
\textbf{ZF} set theory is not finitely axiomatizable. It requires certain \textit{schemata}, which may not be used as such in a proof, but must be \textit{instantiated} on an arbitrary well-formed formula. These statements are considered valid of any well-formed formula, but an axiom schema may not be used in a proof unless it is instantiated upon a particular well-formed formula.
Basically, \textbf{Tarski's theorem on the undefinability of truth} prevents us from quantifying universally or existentially with respect to truth value, in any formal system capable of adequate arithmetic, over arbitrary well-formed formulas of that same system.\footnote{In order to express such a quantification on arbitrary formulas, we must strictly bound the number of alternations of quantification (between universal and existential) in the formula, express the formula in prenex form, and then quantify literally over the rudimentary part of the formula. Thus we may make statements of $\Sigma_1$-soundness, $\Sigma_2$-soundness, etc., but we may not make, within any sound formal system, an unbounded statement of the soundness of that system.}
\begin{axiomschema}[Comprehension]\label{comprehensionschema}
Let $\varphi(x)$ be a well-formed formula. Then for any set $t$ there is a set $s$ including exactly those elements $x$ of $t$ such that $\varphi(x)$ is true; i.e.,
\begin{equation}
[\textrm{wff }\varphi(x)]\qquad(\forall t)(\exists t)(\forall x)\big(x\in s\longleftrightarrow x\in t\land\varphi(x)\big).
\end{equation}
\end{axiomschema}
\begin{axiomschema}[Replacement]\label{replacementschema}
Let $\varphi(x,y)$ be a well-formed formula. If $w$ is a set and for every element $x$ of $w$ there exists $y$ satisfying $\varphi(x,y)$, then there exists a set $z$ including as an element such $y$ for every element $x$ of $w$.
\begin{equation}
\begin{array}{rl}
[\textrm{wff }\varphi(x,y)]
& (\forall w)\Big((\forall x)(x\in w\longrightarrow(\exists y)\varphi(x,y)) \\
&\qquad \longrightarrow (\exists z)(\forall x)\big(x\in w\longrightarrow (\exists y)(y\in z\land\varphi(x,y))\big)\Big).
\end{array}
\end{equation}
\end{axiomschema}
\begin{axiomschema}[Regularity]\label{regularityschema}
Let $\varphi(x)$ be a well-formed formula expressing some property of the arbitrary set $x$. If this property be true of the arbitrary set $y$ whenever it is true of all the elements $x$ of $y$, then it is true of all sets $x$.
\begin{equation}
[\textrm{wff }\varphi(x)]\qquad (\forall y)\big((\forall x)(x\in y\longrightarrow\varphi(x))\longrightarrow\varphi(y)\big)\longrightarrow(\forall x)\varphi(x).
\end{equation}
\end{axiomschema}