A non-trivial and complete LFI with a transparent truth predicate

PAILOS, FEDERICO MATÍAS

Campinas

Workshop; 2nd Workshop CLE-Buenos Aires Logic Group; 2015

CLE-Unicamp

We will present an LFI based on Coniglio & Silvestrini [2014] first order three-valued matrix logic called ?MPT1?. There are two main differences with between MPT1 and the matrix presented here, that we will call, for short, ?MT?. The first one is that MT admits a transparent truth predicate. The second one is that the conditionals of the two matrices treat differently formulas like φ→ψ, where v(φ)=1/2 and v(ψ). In MPT1, those conditionals receive value 0. In MT, they are valued with ½. This also has important consequences in the way they treat biconditionals, and those consequences helps MT dealing with self-reference sentences. In particular, with biconditionals that can be read as expressing in the language ?The Liar? or a ?Curry sentence?. But MT matrix is non-monotonic, and this makes harder finding a fixed-point interpretation of the truth predicate, and thus proving the non-triviality of the theory. In order to reach this goal, we will use a three-side disjunctive sequent semantic, named MTDS, based on the one that Ripley [2012] use to prove the completeness of his paraconsistent truth theory STTT. MTDS ?traduces? MPTTT into a disjunctive sequent language, because it can be proved that Γ⊧MPTTT* Δ iff Γ│Δ│Δ MPTTT** is valid. We will present a proof system for MTDS called LTDS, and show that LTDS is non-trivial. That will show, via the completeness proof of MTDS with respect to LTDS, that MT is also non-trivial. This proof will involve a cut-elimination proof for LTDS. This is reach through an induction over the index of a cutproof, and adopts notions developed in Paoli [2013].