### Not a Knot II

This post belongs to LoPSE popularization (#pop) series written both in English and in Polish.

ENGLISH VERSION [POLISH VERSION BELOW]

In a previous post we presented the background needed to follow Paula Teijeiro in her Not a knot. Now we're ready to move to the paper discussed during the seminar, which raises two key points. First, it is possible to provide a syntactic characterization of Knot. This is done in a proof system which is a bit different from what one might see in an intro to logic class, but there are no clear reasons not to call this a proof-theoretic characterization.

Since the notion of a conservative extension doesn't help here, the question arises as to whether there is a similar criterion in the vicinity that would allow to establish that Knot in some sense hasn't been properly introduced. One strategy, that Teijeiro investigates, is to define a new notion: that of a preservative extension. Roughly speaking, the idea here is that preservative extensions do not change the validity of meta-inference rules (which instead of telling us what one can infer from the premises, tell us what rules govern the inference relation itself). The addition of Knot invalidates some of such rules - for instance, the rule of substitution of logically equivalent formulas.

Teijeiro discusses two reasons why one might think that Knot is nasty. One reason is that it invalidates certain selected intuitively correct meta-rules. This is not a fatal problem - one may just switch to a proof theory which makes those meta-inferences available. Alternatively, one might claim that the introduction of a new meaningful connective in general should not subtract valid inferences. This means that the logic with the newly introduced connective should be preservative.

Now, the conservativeness requirement seemed quite important: it protected the new system from logical explosion. The preservativeness requirement does not have such a force - after all, if you make the original system weaker by extending its language, no threat of logical explosion arises.

Teijeiro briefly discusses other possible motivations for preservativeness. Perhaps, the meanings of logical expressions can be established and understood in isolation and so once we do understand a logical connective, no learning of a new concept can change which inferences containing only the old one we consider valid. This, however, is a fairly strong philosophical position that needs to be defended.

POLISH VERSION

W poprzednim poście opisaliśmy dyskusję, którą mniej więcej trzeba prześledzić, żeby zrozumieć, co w Not a knot robi Paula Teijeiro.Teraz możemy powiedzieć, jak się wiąże z tymi kwestiami tekst Pauli. Teijeiro pokazuje, że istnieje syntaktyczna charakteryzacja dla spójnika Knot, oraz że Knot nie jest funktorem problematycznym. Charakteryzacja syntaktyczna podana jest za pomocą niestandardowego systemu dowodowego, jednakże nie ma żadnych powodów, aby uznać ten system za niepoprawny.

Z racji tego, że pojęcie konserwatywnego rozszerzenia nie jest w stanie nam pomóc, pytanie brzmi, czy istnieją inne sensowne kryteria, które pozwolą nam pokazać, że Knot nie został wprowadzony poprawnie. Jednym z takich kryteriów, które rozważa Teijeiro, jest wymóg, aby rozszerzenie powstające w wyniku dodania nowego funktora, było zachowujące (preservative). Rozszerzenia zachowujące są to takie rozszerzenia, które nie zmieniają poprawności meta-zasad, czyli zasad, które zarządzają samą relacją wynikania, ale nie informują nas o tym, które wyrażenia są wyprowadzalne z których. Rozszerzenie poprzez dodanie Knot nie jest zachowujące, ponieważ, na przykład, w tym rozszerzeniu nie działa zasada podstawiania wyrażeń logicznie równoważnych.

Teijeiro argumentuje, że Knot nie jest problematyczny. Rozważa dwa główne argumenty za tym, że jest odwrotnie. Można myśleć, że Knot jest dyskusyjny, ponieważ jego dodanie sprawia, że niektóre intuicyjnie poprawne meta-zasady przestają być poprawne. To jednak nie jest silny zarzut - można bowiem zmienić teorię dowodu na taką, która sprawia, że owe zasady są poprawne.

Drugi argument bazuje na intuicji, że w ogólności, dodanie nowego spójnika posiadającego znaczenie, nie powinno zmniejszać ilości poprawnych wnioskowań. To znaczy, że rozszerzenie za pomocą tego spójnika powinno być zachowujące. Zauważmy, że wymóg konserwatywności zdawał się być ważny, gdyż gwarantował brak sprzeczności. Natomiast rozszerzenia zachowujące takiej gwarancji nie dają.

Teijeiro krótko omawia inne motywacje przemawiające na korzyść rozszerzeń zachowujących. Być może znaczenie wyrażeń logicznych może istnieć w izolacji, przez co wprowadzenie i zrozumienie nowego spójnika nie wpływa na to, które wyrażenia złożone ze starych spójników uznajemy za uzasadnione lub poprawne. Jest to jednak silna filozoficzna teza i powinna być poparta argumentami na jej korzyść (Teijeiro pobieżnie krytykuje tę tezę pod koniec swojego artykułu).

Paweł Pawłowski, Rafał Urbaniak, Weronika Majek, Małgorzata Stefaniak