Tree-Like Proof Systems for Finitely-Many Valued Non-deterministic Consequence Relations
- PDF / 321,738 Bytes
- 14 Pages / 439.37 x 666.142 pts Page_size
- 42 Downloads / 148 Views
Logica Universalis
Tree-Like Proof Systems for Finitely-Many Valued Non-deterministic Consequence Relations Pawel Pawlowski Abstract. The main goal of this paper is to provide an abstract framework for constructing proof systems for various many-valued logics. Using the framework it is possible to generate strongly complete proof systems with respect to any finitely valued deterministic and non-deterministic logic. I provide a couple of examples of proof systems for well-known manyvalued logics and prove the completeness of proof systems generated by the framework. Mathematics Subject Classification. Primary 03B60, 03B50. Keywords. Non-deterministic logics, Proof systems, Many valued logics.
1. Motivations In this paper, we’ll present an abstract framework for constructing tree-like (tableaux) proof systems for finitely-many valued deterministic and nondeterministic consequence relations.1 Non-deterministic logics were constructed2 by Avron and Lev [5] as a generalization of many-valued deterministic logics. Non-deterministic logics are characterized by means of non-deterministic matrices. Roughly speaking, The work was completed with the support of Polish National Science Centre (NCN) Grant Sonatina 2 2018/28/C/HS1/00251. I wish to thank to Rafal Urbaniak and Frederik Van De Putte for all the comments and discussions that we had on the previous versions of this paper. I am also in debt to two anonymous reviewers for their feedback. The early work on this has been supported by FWO. 1 This proof systems are in the spirit of Carnielli [14]. For a very nice introduction to this method see Priest [27]. The whole framework can be seen as a generalization of the systems presented in Priest [27]. 2 To be fair, Rescher [29], Ivlev [21], Kearns [22], and Quine [28] suggested something similar to a non-deterministic matrix.
P. Pawlowski
Log. Univers.
in such matrices an interpretation may ascribe sets of values instead of a single value. This means that these logics are not truth-functional. In their paper, Avron and Lev constructed an abstract framework for sequent-based proof systems which was further studied in [1–3]. A recipe for constructing tree-like (or tableaux) proof systems for nondeterministic semantics will be provided.3 This is at least as interesting as providing alternative proof systems for any other kind of logic. Here the main advantage of the framework is that it is quite general and that we do not find sequent based proof systems particularly handy when it comes to actually reasoning within the system. One of the other advantages of these systems over sequent-based systems is that there is a nice mechanical procedure for finding a counter-model for any invalid inference. In this setting it is possible to keep track of values of formulas that appear on a tree. This allows to find valuations under which the premises have the designated value and the conclusion doesn’t. Tree-like proof systems are also easy to handle for both humans and computers and they have a nice visual representation. Moreover, it see
Data Loading...
