Formale Induktion über zwei Variablen

Das Argument meines Beispiels erfordert, wenn es richtig ist, dass Induktion auf Prädikate der Form angewendet werden kann$P(m,n)$.$(1)$Warum ist dies möglich/Warum ist dies formal möglich?

Beachten Sie, dass Sie in dem von Ihnen angegebenen Beispielbeweis das beheben$n$, und führen Sie dann eine Induktion durch$m$. Also in diesem Sinne die Formel$P(m,n)$hat wirklich nur eine Variable:$m$.

$(2)$Ich habe auch die folgende Frage Vollständige Induktion über zwei Variablen gelesen , in der die Antwort definiert$Q(x)=\forall y P(x,y)$. Allerdings ist$Q(x)$dann ein gültiges unäres Prädikat, das heißt, wenn$P(x,y)$ist dann ein Prädikat$\forall y P(x,y)$ist ein unäres Prädikat?

Hier wird das noch deutlicher$Q(x) = \forall y P(x,y)$ist eine Formel mit einer unbeschränkten Variablen$x$. Das Prädikat $P(x,y)$ist immer noch ein 2-stelliges Prädikat, aber die Formel $\forall y P(x,y)$hat nur eine freie Variable. Also ja, das passt gut zum Peano-Axiom-Schema.

$(3)$Ich habe auch die folgende Frage Doppelte Induktion gelesen . Hier sagt die Antwort, dass die Formel$\forall m P(m,n)$ist kein Satz und kann somit nicht bewiesen werden. Allerdings hinein$(*)$Ich habe einen ähnlichen Ausdruck. Habe ich in meiner Argumentation oben etwas falsch gemacht?

Auch hier begann Ihr Argument damit, dass Sie das sagten$n$eine willkürliche Zahl ist: Sie ist der Anfang jedes universellen Beweises, den wir zu beweisen versuchen$\phi(n)$und da$n$angenommen wurde, dass es willkürlich ausgewählt wurde, können wir daraus schließen$\forall n \ \phi(n)$. In diesem Kontext eines universellen Beweises können wir also behandeln$\forall m P(m,n)$als Satz, auch wenn wir nicht wissen was$n$genau ist, und weiß daher auch nicht was$\forall m P(m,n)$genau sagt.

Ein einfacher Grund, warum Induktion funktioniert$n$-äre Formeln/Prädikate ist, dass Sie eine iterierte Induktion für unäre Formeln verwenden können, um die Induktion abzuleiten$n$-ary Prädikate. Es gibt auch die Methode, die Sie angeben. Schauen wir uns ersteres an. Angenommen, Sie wollen es beweisen$\forall n\in\mathbb{N} \forall m\in\mathbb{N} \phi(n,m)$. Wir können dies durch Induktion nach tun$n$in der Formel$\forall m\in\mathbb{N} \phi(n,m)$. Dies ist in der Tat eine Formel. Da es sich um eine Formel mit einer freien Variablen handelt, ähnelt sie einem unären Prädikat. Es könnte einfach nicht atomar sein. Nun ist unser Problem durch Induktion auf den Beweis reduziert worden$\forall m\in\mathbb{N}\phi(0,m)$und das zeigen$\forall n\in\mathbb{N}(\forall m\in\mathbb{N}\phi(n,m)\rightarrow\forall m\in\mathbb{N}\phi(S(n),m))$. Beweisen$\forall m\in\mathbb{N}\phi(0,m)$kann durch Induktion über die Formel erfolgen$\phi(0,m)$, dh zeigen$\phi(0,0)$Und$\phi(0,m)$impliziert$\phi(0,S(m))$. In ähnlicher Weise kann man unter Annahme der Induktionsannahme beweisen$\forall m\in\mathbb{N}\phi(S(n),m)$durch Induktion an$m$.

Also formell$n$-äre Induktion kann auf iterierte unäre Induktion reduziert werden. Dies wird jedoch in der Praxis nicht immer gemacht. Sie werden, wie Sie bereits erwähnt haben, Beweise der Form „man nehme eine Willkür“ sehen$n\in\mathbb{N}$, und beweisen$\phi(n,m)$durch Induktion an$m$. Dies ist oft wirtschaftlicher als iterierte Induktion. Der formale Grund dieser Arbeit liegt im Konstruktor für abhängige Funktionen ($\Pi$-Typen). Manchmal (meistens im Zusammenhang mit dem natürlichen Abzug) wird dies genannt$\forall$-Einführung.

Beiseite - Der Grund, warum die Induktion funktioniert, liegt an den Eliminatorregeln für den Typ$\mathbb{N}$. Verwenden der Eliminatorregeln für$\mathbb{N}$und den Konstruktor für verwenden$\Pi$-Typen mit der Annahme$(n : \mathbb{N})$beide dienen dazu, dasselbe zu tun – definieren Sie eine abhängige Funktion aus$\mathbb{N}$.