The Suszkian Odyssey

How many logical values are there? Generalized compositionality for many-valued logics [HowMany 201?].

(forthcoming)

Classical resolution for many-valued logics [Resolution 2016].

A new generic resolution-based proof method for finite-valued logics is introduced, based on a transformation that adds new variable symbols that help in appropriately encoding the structure and preserving the satisfiability of the metalogical statements resulting from the bivalent reduction of the given logics. The resulting hyper-resolution proof method lies in between internal proof systems that take advantage of syntactic features of the original logics and external proof systems that formalise reasoning about the logics in a classical logical framework.

Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics [GenComp 2015].

The paper concentrates on computational generalizations of compositionality, obtained by extending the canonical notions of subformula property, analyticity, formula complexity, and effectiveness. Input: an arbitrary finite-valued logic. Outputs: (i) a mechanism for producing a classic-like description of it in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent semantics so obtained, uniform (classically-labeled) cut-free standard analytic tableaux with possibly branching invertible rules and paired with proof strategies designed to guarantee termination of the associated proof procedure; (iii) a mechanism to also provide, for the same logic, a uniform cut-based tableau system with linear rules, allowing in principle for a polynomial simulation of truth-tables. Full details and all proofs included. Running examples: Lukasiewicz's logics L_n and Gödel's logics G_n.

Classic-like cut-based tableau systems for finite-valued logics [Cut-based 2012].

Tableau systems with analytic cuts are produced for any finite-valued logic. The advantage in terms of complexity is that such systems can polynomially simulate truth-tables, while the worst-case scenario for standard tableau systems (as in WoLLIC 2009) is known to suffer from particularly nasty combinatorial explosion phenomena. Running example: Lukasiewicz's logic L_3.

Many-valuedness meets bivalence: Using logical values in an effective way [MVL&SC 2011].

Survey paper. Running examples: Gödel's logics G_3 and G_4 (negation-implication fragment), the first one in detail, and the last one demanding a conservative extension. Comparison between these logics done through tableaux. Shows that the conservative extension used, if necessary, for turning the logic sufficiently expressive may be done by the addition of 0-ary constructors. Shows the relation between genuine K-valuedness and the Leibniz congruence from Abstract Algebraic Logic. Corrects Suszko's claim on the so-called 'Fregean Axiom', presenting an example of a 3-valued logic that enjoys the replacement property, and showing the correct relation between truth-functionality and the replacement property. Simple 2-valued example of a logic with a nondeterministic semantics and no finite- nor infinite-valued deterministic semantics.

The value of the two values [2Val 2011].

Two distinct slices of Belnap's four-valued bilattice are studied and contrasted to each other: a paraconsistent logic is obtained first by choosing a single truth-value to be undesignated, and a dual paracomplete logic is obtained by choosing a single truth-value to be designated. Here the problem in distinguishing between these two logics does not lie in having them based on different collections of `algebraic values', but in using the same values with different meanings in each case. Reduction to classic-like presentations, this time, help in establishing proof-theoretic formalisms that not only help in setting these two logics apart but also in characterizing their duality in precise terms. Proof strategy is simplified by taking the (definable) separators as primitive.

Two many values: An algorithmic outlook on Suszko's Thesis [AlgOut 2010].

Superseded by the paper MVL&SC 2011.

Automatic generation of proof tactics for finite-valued logics [EPTCS 2010].

Running example: Lukasiewicz's logic L_4. The need to simplify the closure rules corresponding to the unobtainable semantic assignments is highlighted for the first time (correcting a small source of incompleteness in the WoLLIC 2009 paper). Example, using L_4, illustrating the need of following a proof strategy in applying rules to formulas whose patterns can be matched with the heads of more than one tableau rule. Comments on rule-based implementation of the fully automated cut-free proof tactics in Isabelle, using rewriting.

Classic-like analytic tableaux for finite-valued logics [WoLLIC 2009].

Running examples: Lukasiewicz's logics L_n. Special detail on L_3 (using a separating formula different from the one used in MSoL 2009), full version of the signed clauses, and simplified version. New axiom extraction method with closuring sequences of binary prints and corresponding closure rules: obtainment, for the first time, of a sound and complete cut-free proof system (tableaux), with detailed proofs, improving on the earlier strategy sketched in the HUMBUG. The problem of non-termination is illustrated also for the first time, when a clever proof strategy is not followed in applying tableau rules. To solve it, a new non-canonical complexity measure is introduced, customized to each finite-valued logic given as input. An associated decision procedure is guaranteed to exist, in each case. An extended version of analyticity, relativized to this complexity measure, is introduced. Finally, emphasis is also put on the fact that the separating formulas, in each case, may be either primitive or introduced by abbreviation.

Towards fully automated axiom extraction for finite-valued logics [MSoL 2009].

Implements (in ML) the algorithm proposed in the HUMBUG paper. Running example: Lukasiewicz's logic L_3 (using negation for the separation of the truth-values). Detailed output of corresponding theory for Isabelle 2005. Exemplifies proofs of derived rules using Isabelle's tacticals.

Automatic extraction of axiomatizations in terms of two-signed tableaux for finite-valued logics [AutExt 2008].

Superseded by the paper MSoL 2009.

Two's company: "The humbug of many logical values" [HUMBUG 2005 - 1st ed].

Suszko's Thesis revived. Reductive results from the viewpoint of Universal Logic. The trouble about effectively separating truth-values. First algorithm for extracting a sound and complete bivaluation semantics for each sufficiently expressive finite-valued logic. Running examples: Lukasiewicz's logics (in particular detail, L_5), logic C_1 (infinite-valued), logics P^1_3 and P^1_4, 3-valued logic LFI1 (this one with the truth-values separated by \bullet), Belnap's logic. Definition of a gentzenian semantics, of a (quasi) tabular logic, and of a dyadic semantics. Sketch of adequate two-signed tableaux (endowed in general with a non-eliminable dual-cut rule). A conjecture about the sufficiency of analytic cuts is advanced.

Suszko's Thesis and dyadic semantics [Pre1-CLC 2003].

(preprint)

Dyadic semantics for many-valued logics [Pre2-CLC 2003].

(preprint)