Hongkai Yin

We further investigate the metalogical properties of the ordered fragment. First, we provide a simplified proof of the satisfiability invariance under A. Herzig’s translation of the ordered fragment into modal logic $$\textbf{KD}$$. Second, based on the notion of bisimulation developed by B. Bednarczyk and R. Jaakkola, we show that each ordered formula is equivalent to a disjunction of ‘ordered types’. Third, we show that the fragment enjoys uniform interpolation, and that uniform interpolants can be effectively constructed from ‘ordered types’. Finally, we establish the Łoś-Tarski Preservation Theorem for the fragment, and therefore conclude that the ordered fragment is nice.

We investigate the relational syllogistic as a fragment of the Quantified Argument Calculus (Quarc). The language contains polyadic predicates (together with their reordered forms) and singular terms. A truth-valuational semantics is provided for the fragment. A sound and complete tableau calculus is formulated, which is the first time semantic tableau is used in the study of Quarc. With certain techniques for analyzing and transforming tableaux, we prove that the satisfiability problem is decidable and is NLogSpace-complete with or without reordered predicates. Besides, when singular arguments are absent, the logic also admits a proof system consisting of syllogistic rules.

We introduce a two-valued and a three-valued truth-valuational substitutional semantics for the Quantified Argument Calculus (Quarc). We then prove that the 2-valid arguments are identical to the 3-valid ones with strict-to-tolerant validity. Next, we introduce a Lemmon-style Natural Deduction system and prove the completeness of Quarc on both two- and three-valued versions, adapting Lindenbaum’s Lemma to truth-valuational semantics. We proceed to investigate the relations of three-valued Quarc and the Predicate Calculus (PC). Adding a logical predicate T to Quarc, true of all singular arguments, allows us to represent PC quantification in Quarc and translate PC into Quarc, preserving validity. Introducing a weak existential quantifier into PC allows us to translate Quarc into PC, also preserving validity. However, unlike the translated systems, neither extended system can have a sound and complete proof system with Cut, supporting the claim that these are basically different calculi.