In 2019 Hernandez-Tello et al. introduce a more restricted concept of paracompleteness, namely the genuine paracompleteness. A genuine paracomplete logic is a logic rejecting ` '; :' and :( _ : ) `. This conditions are dual to those rejected by genuine paraconsistent logic: '; :' ` and ` :(' ^ :'), introduced by Beziau in 2016. HernandezTello et al. make a semantical analysis of the genuine paracompleteness in the context of three-valued logics and nd two genuine paracomplete logics that conservatively extend the positive fragment of Classical Propositional logic, namely, L3AD!1 and L3B!D1 . We present here a deep analysis of the paracomplete logic L3AD!1 . We provide a sound and complete Hilbert-type axiomatic system for L3AD!1 logic. The completeness proof is a direct proof using Kalmar's technique adapted for a three-valued logic, which means that a general technique to nd the proof of any theorem in a systematic way is obtained.
The relation between mathematics, logic, and philosophy can be traced back to ancient times. Greek philosophers asserted that there are three basic principles of thinking that are fundamental to making correct reasoning. Classical reasoning is expected to conform to these logical principles, also called the laws of thought, namely: 1. The Law of Identity: `A thing is what it is.' 2. The Law of Excluded Middle: `It is impossible to be and not to be the same thing.' 3. The Law of Contradiction: `It is impossible for any being to possess a quality, and at the same time not to possess it.'
Nowadays logicians have shown that it is possible to de ne logical systems
that do not obey some of these laws obtaining some interesting and useful
nonclassical logics. In 1908 Brouwer, in a paper entitled `The untrustworthiness of
the principles of logic', challenged the belief that the rules of the classical logic,
which have come down to us essentially from Aristotle (384{322 B.C.) have an
absolute validity, independent of the subject matter to which they are applied
[
The problem when one wants to formalize the laws in terms of formal logic is that there are several ontological, doxastic and semantic versions for each of these laws, unfortunately in most of the cases they are not equivalent. We are interested in the semantic point of view, but even in that context, minimum changes in the interpretation of the laws can conduct to di erent formalizations. For instance the Law of Contradiction, whose intuitive meaning is `it is not the case that ' and :' are simultaneously true', could be formalized in terms of (multiple-conclusion) consequence relations as either of the following: (LC) ' ^ :' ` or (LC0) ` :(' ^ :')
On the other hand we have the Law of Excluded Middle, the intuitive meaning in this case is `it is not the case that ' and :' are simultaneously false', and it could be formalized as either of the following: (LEM) ` ' _ :'
or (LEM0) :(' _ :') `
In [
However as highlighted by Beziau in [
In general, the interest in paracomplete and in paraconsistent logic has grown
in the last decades, we can nd some interesting theoretical results about these
families of logics in [
We introduce the syntax of the logical formulas considered in this paper, later the notions of consequence relation and logic, some de nitions related to connectives as well as some concepts related to logic semantics.
We use a formal propositional language L = hatom(L); C; Ai, where atom(L) is an enumerable set, whose elements are called atoms and are denoted by lowercase letters; C = f:; _; ^; !g is the set of connectives, also known as signature, and A is the set of auxiliary symbols (comma and parenthesis in our case). Formulas are constructed as usual and will be denoted by lowercase Greek letters. Given a language L the set of all formulas of the language is denoted by F orm(L). Theories are sets of formulas and will be denoted by uppercase Greek letters.
De nition 1. Given a formal propositional language, a (tarskian) consequence relation ` between theories and formulas is a relation satisfying the following properties, for every theory [ [ f'g: (Re exivity) if ' 2 (Monotonicity) if (Transitivity) if , then ` ' and ` ' and ` '; `
, then for every ` '; 2 , then ` '.
Other desirable properties of consequence relations are structurality (for every L-substitution , it holds that ` ' implies ( ) ` (')) and non-triviality (there exist some non-empty theory and some ' such that 6` ').
A logic can be de ned in terms of consequence relations (either semantical or proof-theoretical) as follows: De nition 2. Given a formal language L, a logic is a pair L = hL; `Li, where `L is a structural and no trivial consequence relation, satisfying the rule known as Modus Ponens (MP), which means that for any formulas ' and holds that ' ! ; ' `L .
The notation `L ' could be read as ' can be inferred from Whenever the logic is clear the subscript will be dropped.
in L.
De nition 3. [
` . and ; .
` .
In [
` ;
It is not di cult to prove in the context of tarskian consequence relations that the notions of implication in De nition 3 and De nition 4 agree. The usual manner to de ne many-valued logics is by means of a matrix.
De nition 5. A matrix for a language L, is a structure M = hV; D; F i, where: V is a non-empty set of truth values (domain); D is a subset of V (set of designated values); F := ffcjc 2 Cg is a set of truth functions, with a function for each logical connective in L.
De nition 6. Given a language L, a function v : atom(L) atoms into elements of the domain is a valuation. ! V that maps
It can be extended to all formulas v : F orm(L) ! V as usual, i.e. applying recursively the truth functions of logical connectives in F . Now we can de ne the notion of model.
De nition 7. Given a matrix M , we say that v is a model of the formula ', if v(') 2 D and we denote it by v j=M '. A formula ' is a tautology in M if every valuation is a model of ', it is denoted by j=M '.
Whenever the matrix is clear the subscript will be dropped. It is also possible to de ne a consequence relation by means of a matrix.
De nition 8. [
There are more restrictive conditions than those on De nition 3 for
connectives such as the following de nition.
De nition 10. [
v(:') 2 D i v(') 2 D. 2. ^ is a Neoclassical conjunction, if it holds that: 3. _ is a Neoclassical disjunction, if it holds that: v(' ^
) 2 D i v(') 2 D and v( ) 2 D. v(' _
) 2 D i v(') 2 D and v( ) 2 D. 4. ! is a Neoclassical implication, if it holds that: v(' !
) 2 D i v(') 2 D or v( ) 2 D.
Speci cally, we have that items 2 and 3 on De nition 10 imply items 2 and 3 on De nition 3. Moreover, item 1 on De nition 10 is equivalent to item 1 on De nition 3.
of arity k ( : V k ! V ) is a: Conservative extension of an m-valued function : V1k ! V1 where V1 ( V and jV1j = m, if the restriction of to V1 coincide with (i.e.
jV1 = ).
Molecular if the range of it is a proper subset of V . [
The notion of genuine paracomplete logic, is presented in [
1. Intuitionistic Propositional Logic IPL is paracomplete, but it is not genuine paracomplete: the formula :(' _ :') is unsatis able. 2. The Belnap-Dunn logic F OU R (with the truth ordering) and Nelson logic
N4 are both genuine paraconsistent and genuine paracomplete.
3. The 3-valued logic MH, introduced in [
Authors in [
In that paper the authors perform a complete semantical analysis of the concept of genuine paraconsistency. In this paper we start a study of the concept from the proof-theoretical point of view. Particularly we focus on the logic L3AD!1 in order to nd a Hilbert-Type axiomatic system for it. 4
The logic L3AD
!1 In this section we present the logic L3AD!1 , a genuine paracomplete three-valued logic and some remarks about it.
De nition 13. The logic L3AD!1 is the three-valued logic induced by the matrix
M = hf0; 1; 2g ; f2g ; Oi over the signature C = f:; _; ^; !g and whose truth
tables are:
Remark 1. Some of the results about L3AD!1 presented in [
The connective _ is a disjunction, it is a neoclassical disjunction and it is a conservative extension of the classical disjunction and it is not molecular. The connective ^ is a conjunction, it is a neoclassical conjunction and it is a conservative extension of the classical conjunction and it is not molecular and corresponds to the minimum function in the natural order.
The connective ! is an implication, is a neoclassical implication and it is a conservative extension of the classical implication and it is not molecular. The logic satis es the positive fragment of classical logic.
The non implicative fragment of L3AD!1 is a logic dual to the genuine
paracomplete logic L3A de ned in [
The constants ? and > are de nable as ?:= ' ^ :' and > := :(' ^ :') for any formula '.
A Hilbert Calculus for L3AD !1 Up to this point we have de ned the logic L3AD!1 and we have revisited some properties from the semantic point of view. It is time to switch to the proof theoretical approach. In this section the Hilbert Calculus LL3AD!1 for the logic L3AD!1 is presented, some basic results are stated and nally the adequacy of the calculus is proved. In order to de ne an axiomatic theory for L3AD!1 over the signature C = f:; _; ^; !g we are going to introduce the following abbreviations for the sake of the simplicity: De nition 14. Let C be the signature f:; _; ^; !g then:
' := ' ! (' ^ :') G0(') := :' N 0(') := :(' _ :') D0(') := : ' ! (' ^ :') = : ' $ := (' ! ) ^ ( ! ')
' Considering these new connectives we can proceed to de ne the axiomatic theory for the logic L3AD!1 as follows.
De nition 15. Let LL3AD be an axiomatic theory whose axioms are the schemes !1 listed below and whose rule of inference is Modus Ponens (MP).
Pos1 : ' ! (
! ') Pos2 : ' ! ( ! ) ! (' ! Pos3 : (' ^ ) ! ' Pos4 : (' ^ ) ! Pos5 : ' ! ! (' ^ ) Pos6 : ' ! (' _ ) Pos7 : ! (' _ ) Pos8 : ' ! ! ( ! ) ! (' _ Pos9 : (' ! ) _ ' REM : :' _ ::' EXP : ' ! (:' ! ) ENN : ::' $ :' ENC : :(' ^ ) $ (:' _ : ) END : :(' _ ) $ ENI : :(' ! ) $ (' ^ : ) ( ' ^ : ) _ (:'^
) With ` we denote a deduction of with as the set of hypotheses, when = ; we write ` or simply , which means that it is possible to prove without assumptions. As usual ; ' ` denotes [ f'g ` .
Some general properties of LL3AD!1 are the following.
Theorem 1. Let ,
be theories and ', be formulas, the following properties hold in LL3AD!1 : i) Monotonicity (Mon) If ` ', then ; ` '. ii) Deduction Theorem (DT) ; ' ` i ` ' ! . iii) Cut If ` ' and ; ' ` , then ; iv) AND-Rules(R-AND) ` ' ^ i ` ' y ` . v) Weak Proof by Cases (WPC) ; :' ` and ; ::' ` i ` . ` .
Proof. The proof of properties i) iv) is straightforward. Let us check the last property.
` ::' ! Suppose ; :' ` and ; ::' ` . By DT we have that . Using Pos8 and Mon we obtain ` (:' ! ` :' ! and ) ! (::' ! ) ! ((:' _ ::') ! ) y applying Modus Ponens with ` :' ! , we conclude that ` (::' ! ) ! ((:' _ ::') ! ). Once again by Modus Ponens between the last step and ` ::' ! , it follows that ` (:' _ ::') ! . Separately, by Mon and REM, ` :' _ ::'. Finally we obtain that ` by means of Modus Ponens. On the other hand, if we suppose that ` , by Mon ; :' ` and ; ::' ` .
The Lemma 1 encloses a list of properties of LL3AD . Particularly items f ), !1 h), i) and axiom Pos9 suggest that behaves as classical negation. Just take in Pos9 as ' ^ :' to obtain ' _ ' recovering somehow the excluded middle principle. As shown in Table 1 the connective is a neoclassical negation, see De nition 10.
Note 1. From the semantical point of view, connectives G0, N 0 and D0 act as identi ers of the truth values 0, 1 and 2 respectively, see Table 1. The reading from the semantical point of view of property s) as well as the results in Lemmas 1 and 2 is very intuitive. Lemma 1. If ', , , are formulas in LL3AD!1 the following properties hold: a) ` ' ! ::' b) ` (:: ! ::') $ (:' ! : ) c) ` :' $ :::' d) ` (:' ! ) ! (: ! ::') e) ::'; :: ` ::(' _ ) f ) '; ' ` g) :' ` ' h) ` ' $ ' i) ` (' ! ) $ ( ! ') j) ' ` :' k) '; ` (' _ ) l) '; ::' ` N 0(') m) N 0(') ` ' n) N 0('); ' ` o) N 0(') ` ::' p) ` D0(') $ ' q) D0(') ` ::' r) If ' ` and : ' ` , then ` . s) G0(') ` , N 0(') ` , D0(') ` imply ` .
Thanks to the identi ers G0, N 0 and D0 Lemma 2 re ects the semantical behavior of the four primitive connectives of the logic L3AD!1 into the proof theory. For instance, given a formula ' and a valuation v, if v(') = 0 then we have that v is a model of G0('). On the other hand if v(') = 1, then v models N 0('), and if v(') = 2, then v models D0(') (see De nition 16). Particularly, N1 states that: if ' takes the value 0 identi ed as G0('), then its negation :' must take the value 2, i.e. D0(:'). Similarly, N2 states that: if ' takes the value 1, N 0('), then its negation must take the value 0, G0(:'). Finally N3 asserts that if a formula takes the value 2 its negation must take the value 0. Therefore, by showing that N1, N2 and N3 are theorems in LL3AD , we prove !1 that the negation connective : matches with the truth tables of the connective in L3AD!1 . Analogously, D1-D6 do the job for disjunction, C1-C6 check the case of conjunction and I1-I5 model the behavior of implication.
D0(:') G0(:')
G0(:') G0(') ! N 0(') !
D0(') ! then ' is a tautology L3AD!1 .
Theorem 2 (Soundness). Let ' be a formula. If ' is a theorem in LL3AD!1 , Proof. The proof is straightforward by checking that all axioms are tautologies and that MP preserves tautologies.
To simplify the completeness proof, De nition 16 formally introduce a
transformation over formulas of L3AD!1 using G0, N 0 y D0. This transformation
generalizes the transformation proposed in the well known Kalmar's lemma used to
proof completeness of Classical Propositional Logic [
De nition 16. Given a valuation v and ' a formula in the language of L3AD!1 : 'v = 8G0(') > <
if v(') = 0;
N 0(') if v(') = 1; >:D0(') if v(') = 2:
we have that v = f'vj' 2
Using the previous de nition, Lemma 3 states that given a valuation, the
set of the transformed atoms of a formula derives the transformed formula. This
lemma is a generalization of the Kalmar's lemma [
Lemma 3. Let ' be a formula and v be a valuation in L3AD!1 . Then in LL3AD!1 it holds that Atoms(')v ` 'v.
Proof. The proof is by induction over the complexity of '.
Basis: ' is an atom, e.g. ' = p. In this case Atoms(')v = f'vg = fpvg, so it is enough to prove that 'v ` 'v. But it follows directly by monotonicity.
than ' it holds that Atoms( )v ` v. of L3AD!1 with lower complexity Induction step: It is divided into four sub-cases, namely, ' = : , ' = _ , ' = ^ and ' = ! such that the complexity of and are lower that those of '. We present here only the last case, namely, ' = ! , the remaining ones are proved similarly.
By inductive hypothesis it holds that:
Atoms(')v ` v (1) and
Atoms(')v ` v (2) According to the truth values of assigned by v to lowing cases. and to we have the fol
Case 1: v( ) 2 D. Regardless the value of we have that v(') 2 D, i.e. v(') = 2, then 'v = D0(') = D0( ! ). Considering the values of we have the following sub cases.
Sub-case 1a: If v( ) = 0, then v = G0( ). By I1 and DT, G0( ) ` D0( ! ), equivalently, v ` 'v. Using Cut between (1) and the last formula we obtain Atoms(')v ` 'v.
Sub-case 1b: If v( ) = 1, then v = N 0( ). By I2 and DT it follows that N 0( ) ` D0( ! ). Analogously to the previous sub-case, by applying Cut between (1) and the last formula we obtain Atoms(')v ` 'v.
Case 2: v( ) 2 D. Now regardless the value of , we have v(') 2 D. As a result 'v = D0(') = D0( ! ) and v = D0( ). Now by I3 and DT, D0( ) ` D0( ! ), equivalently v ` 'v; by Cut with (2), we can conclude that Atoms(')v ` 'v. orem in LL3AD!1 .
Case 3: v( ) 2 D and v( ) 2 D. Then v = D0( ) and v(') 2 D, also v(') = v( ) and there are two options for the truth value of .
Sub-case 3a: If v( ) = 0, then v(') = 0, 'v = G0(') = G0( ! ) and v = G0( ). On one hand, since Atoms(')v ` v and Atoms( )v ` v by RAND we obtain that Atoms(')v ` v ^ v. On the other hand, D0( ) ^ G0( ) ` G0( ! ) (DT(I4)), or equivalently v ^ v ` 'v. Finally by Cut between Atoms(')v ` v ^ v and v ^ v ` 'v we conclude that Atoms(')v ` 'v.
Sub-case 3b: If v( ) = 1, then v(') = 1, 'v = N 0(') = N 0( ! ) and v = N 0( ). As in the previous sub-case we have that Atoms(')v ` v ^ v and D0( ) ^ N 0( ) ` N 0( ! ) (DT(I5)). One application of Cut lead us to, Atoms(')v ` 'v.
Therefore if ' is a formula and v a valuation in L3AD!1 , then Atoms(')v ` 'v. Theorem 3 (Completeness). If ' is a tautology in L3AD!1 , then ' is a theLL3AD!1 .
Proof. Suppose that ' is a tautology in L3AD!1 . Let = Atoms('). For any valuation v(') = 2, therefore 'v = D0('). By Lemma 3 it holds that v ` D0(') and by the item p) of Lemma 1 we have that ` D0(') ! '. Applying MP to the last results we obtain that for any valuation v it holds that v ` '. Let p be an atom in and := n fpg. For any valuation v, v ` ', equivalently v; pv ` ' . Since we have three truth values, there will be three di erent values for p and we will have that v; G0(p) ` ', v; N 0(p) ` ' and v; D0(p) ` '. By item s) of Lemma 1 we can conclude that v ` '. One can repeat the previous technique to eliminate another atom in and after a nite number of steps all atoms in will be eliminated. As a result we have that ` ', i.e. that ' is a theorem in
Thanks to Theorem 2 and Theorem 3 we have that the logic L3AD!1 is sound and complete with respect to the calculus LL3AD!1 which is the main contribution of this paper. 6
Making a demonstration of completeness in a direct way consists in taking a
tautology and constructing its formal proof. When doing so, not only the
theorem of completeness is obtained, but a general technique for nding the proof
of any theorem systematically is derived too. In [
Examples: Let be ' = :p ! :q and v a valuation such that v(p) = 2 and v(q) = 1. Then we have that Atoms(')v = fD0(p); N 0(q)g = f: p; :(q _ :q)g and 'v = : ' = : (:p ! :q). By Lemma 3 it holds that : p; :(q _ :q) ` : (:p ! :q). Let us construct the proof following the meta-proof suggested by Lemma 3.
Let and be the formulas surrounded by the horizontal brackets :
z p; :(q _ :q) ` : 'v }| { ( :p ! :q ) |{z} |{z} Then v( ) = v(:p) = 0 and v( ) = v(:q) = 0. This corresponds to the Case 1, Sub-case 1a of Lemma 3 and the proof becomes: 1. Atoms(')v ` ::p 2. ::p ` : (:p ! :q) 3. Atoms(')v ` : (:p ! :q) (*) Induction hypothesis
I1 and DT Cut (1,2)
Now lets prove the Induction hypothesis (*). Let surrounded by the horizontal brackets: and
be the formulas :
'v p; :(q _ :q) ` z: :}| p {
|{z} | {'z }
In this case v( ) = v(p) = 2 which corresponds to one of the cases of negation in which N3 is used.
The proof of (**) is direct since : can be rewritten as: 1. Atoms(')v ` : 2. : p ` ::p 3. Atoms(')v ` ::p
p 1. ` : p 2. ` :(q _ :q) 3. : p ` ::p 4. ` ::p 5. ::p ` : (:p ! :q) 6. ` : (:p ! :q) 7. : p; :(q _ :q) ` : (**)Induction Hypothesis
N3 and DT
Cut (1,2) p 2 Atoms(')v, and the complete proof (:p ! :q)
Hypothesis
Hypothesis N3 and DT
Cut (1,3) I1 and DT Cut (4,5) 1-6 7
The logic L3AD!1 is a genuine paracomplete logic that conservatively extends the
positive fragment of classical propositional logic. It was de ned by
HernandezTello et al. in [
It is important to nd the axiomatization of other genuine paracomplete logics in order to have a better picture of the concept and its relation with other paracomplete logics, we have considered it as future work. We are interested in exploring as many properties as possible to compare the whole family of threevalued paracomplete logics, where L3AD!1 is just the tip of the iceberg. However, we consider the results presented in this paper relevant for settle down a starting point in the study of genuine paracomplete logics.