Proof systems for BAT consequence relations

An ongoing debate about the differences between formal provability in an axiomatic system and informal provability of mathematical claims in mathematics as a whole resulted in the construction of various logics whose main purpose is to capture the inferential behaviour of the notion of informal provability, just as multiple logics of formal provability capture the behaviour of the concept of formal provability. Known logics of informal provability, based on classical logic, are unable to incorporate all intuitive principles of informal provability (most notably, reflection, which says that whatever is provable is true). One solution to this problem is to treat informal provability as an operator (Shapiro, 1985, North Holland; Reinhardt, 1986, J. Philos. Log., 15, 427–74; Koellner, 2016, Oxford University Press). Another solution is to weaken some of the intuitively adequate principles (Horsten, 2002, Hansel-Hohenhausen). Recently, in yet another approach to the issue, two three-valued non-deterministic logics of informal provability have been developed (Pawlowski and R. Urbaniak, 2016, Rev. Symbo. Log.) to overcome this difficulty. Alas, the logics have been characterized semantically and no proof systems for them are available. The purpose of this article is to define tree-like proof systems for those logics and to prove the corresponding soundness and completeness theorems.An ongoing debate about the differences between formal provability in an axiomatic system and informal provability of mathematical claims in mathematics as a whole resulted in the construction of various logics whose main purpose is to capture the inferential behaviour of the notion of informal provability, just as multiple logics of formal provability capture the behaviour of the concept of formal provability. Known logics of informal provability, based on classical logic, are unable to incorporate all intuitive principles of informal provability (most notably, reflection, which says that whatever is provable is true). One solution to this problem is to treat informal provability as an operator (Shapiro, 1985, North Holland; Reinhardt, 1986, J. Philos. Log., 15, 427–74; Koellner, 2016, Oxford University Press). Another solution is to weaken some of the intuitively adequate principles (Horsten, 2002, Hansel-Hohenhausen). Recently, in yet another approach to the issue, two three-valued non-deterministic logics of informal provability have been developed (Pawlowski and R. Urbaniak, 2016, Rev. Symbo. Log.) to overcome this difficulty. Alas, the logics have been characterized semantically and no proof systems for them are available. The purpose of this article is to define tree-like proof systems for those logics and to prove the corresponding soundness and completeness theorems.A