English Wikipedia @ Freddythechick:Notability comparison test/Proof

The test states that: For any topic (x) of a Wikipedia article under consideration for deletion and for any topic (y) of another Wikipedia article, if x has more coverage (per the notability guideline) than or equal amount of coverage compared to that of y, and a Wikipedia article on x does not violate what Wikipedia is not, then:

• If y is notable (meriting an article in Wikipedia), then x is also notable.
• If x is not notable, then y is also not notable (meaning that both the article on x and the article on y must be deleted).

which, in formal form, becomes:

$(\forall x)(\forall y)([n(x)\geq n(y)]\rightarrow [((y\in W)\rightarrow (x\in W))\wedge ((x\notin W)\rightarrow (y\notin W))])$

where $n$ is a notability function whose domain are the topics of Wikipedia articles and whose range $n(x)$ is the set of natural numbers ℕ, $x$ and $y$ are variables that can stand in for any topics, and $W$ is the set of notable topics (each of them meriting an article in Wikipedia)

Empirical premises

1. The amount of coverage on a topic is graded and ordered from low to high, as can be seen when one compares the coverage on the United States with the coverage on Sacramento, California.

   Thus, the notability function's range $n(x)$, which is the amount of coverage on a topic, is the set of natural numbers ℕ = {0, 1, 2, 3, …}. This also implies that $n(x)$ is a totally ordered set.

2. Every article on Wikipedia is subjected to the same standard of notability. There is a threshold in the amount of coverage, in other words, a certain amount of coverage such that if a topic has a greater amount of coverage than that certain amount, then the topic is notable. The specific notability guidelines (such as that of astronomical objects) for different subjects are for determining an article's coverage level given the context of the article within that subject.

   Thus, any topic that has enough coverage to be notable for Wikipedia must have a coverage level higher than a certain threshold.

Axioms, theorems, syntaxes, and definitions used

• 4 axioms of propositional logic (see here)
• 7 axioms of predicate logic with equality (see here)
• Zermelo-Fraenkel axioms
• All theorems of, syntaxes used in, and definitions used in the above formal systems

Additional definitions used (based on the empirical premises)

• $x$ and $y$ are variables that can stand in for any article's topic.
• $n$ is a notability function whose domain is the topics of Wikipedia articles and whose range $n(x)$ is the set of natural numbers ℕ, which are the individual amount of coverage.
• $W$ is the set of topics worthy of inclusion in Wikipedia.
• $\tau$ is the threshold coverage level for inclusion.
• $(x\in W)\leftrightarrow [(\tau \leq n(x))\wedge \neg (n(x)=\tau )]$

Main body

Step	Proposition	Justification
1	$(y\in W)\wedge (n(y)\leq n(x))$	Assumption for CP
2	$y\in W$	1, simp.
3	$[\tau \leq n(y)]\wedge \neg [n(y)=\tau ]$	2, def. of (x ∈ W)
4	$\tau \leq n(y)$	3, simp.
5	$n(y)\leq n(x)$	1, simp.
6	$\tau \leq n(x)$	4, 5, transitivity of ≤ (Theorem 9325)
7	$n(x)=\tau$	Assumption for RAA
8	$n(y)\leq \tau$	5, 7, substitution
9	$(\tau \leq n(y))\wedge (n(y)\leq \tau )$	4, 8 conj.
10	$n(y)=\tau$	9, antisymmetry of ≤
11	$\neg (n(y)=\tau )$	3, simp.
12	$(n(y)=\tau )\wedge \neg (n(y)=\tau )$	10, 11 conj.
13	$\neg (n(x)=\tau )$	7 - 12, RAA
14	$(\tau \leq n(x))\wedge \neg (n(x)=\tau )$	6, 13 conj.
15	$x\in W$	14, def. of (x ∈ W)
16	$[(y\in W)\wedge (n(y)\leq n(x))]\rightarrow (x\in W)$	1 - 15 CP (deduction theorem)
17	$[(y\in W)\wedge (n(x)\geq n(y))]\rightarrow (x\in W)$	16, ≤ being a converse of ≥
18	$[(n(x)\geq n(y))\wedge (y\in W)]\rightarrow (x\in W)$	17, commutative property of conjunction
19	$(n(x)\geq n(y))\rightarrow [(y\in W)\rightarrow (x\in W)]$	18, exportation
20	$(n(x)\geq n(y))$	Assumption for CP
21	$(y\in W)\rightarrow (x\in W)$	19, 20 modus ponens
22	$\neg (x\in W)\rightarrow \neg (y\in W)$	21, transposition
23	$[(y\in W)\rightarrow (x\in W)]\wedge [\neg (x\in W)\rightarrow \neg (y\in W)]$	21, 22 conj.
24	$[(y\in W)\rightarrow (x\in W)]\wedge [(x\notin W)\rightarrow (y\notin W)]$	23, def. of ∉
25	$[n(x)\geq n(y)]\rightarrow [((y\in W)\rightarrow (x\in W))\wedge ((x\notin W)\rightarrow (y\notin W))]$	20 - 24, CP (deduction theorem)
26	$(\forall x)(\forall y)([n(x)\geq n(y)]\rightarrow [((y\in W)\rightarrow (x\in W))\wedge ((x\notin W)\rightarrow (y\notin W))])$	25, axiom of universal generalization

End of proof