Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Wann = und wann \equiv
Hallo,
muss man bei äquivalenten, aber nicht syntaktisch gleichen Formeln, das LaTeX-Äquivalenz zu \equiv verwenden oder reicht das = aus?
LG Gabriel
\equiv wird afair in GLoIn für logische Äquivalenz genutzt. = wird für syntaktische Gleichheit genutzt, ggf. modulo einer Operation auf der Metaebene. Beispiele:
A -> true \equiv true
B = B
C -> B = C -> B
(A -> true)[A |-> B] = B -> true // Per Definition der Substitution
(\x. y)[y |-> x] = \z. x // Aber auf = \w. x. Das ist eine nichttriviale Sache von Substitutionen, um Capture-Avoidance zu vermeiden.Später in ThProg wird =_{alpha,beta,eta} dafür genutzt auch modulo \alpha, \beta, \eta-Reduktion & -Expansion Gleichheit zu haben. Es wird also bisschen schwammiger.
Allgemein empfiehlt es sich immer über die eigene Nutzung von = nachzudenken. Inwiefern ist 1 + 1 = 2? Unter welchem Formalismus? Wenn f,g: X → Y zwei Funktionen und \forall x. f(x) = g(x), ist dann f = g? Unter welchem Axiom? (Stichwort “functional extensionality”) Inwiefern ist R x R = R^2? Ist das Gleichheit oder nur ein Vektorraumisomorphismus? 