Online research in philosophy

We prove a finite model theorem and infinitary completeness result for the propositional -calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.

In this paper the PA-completeness of modal logic is studied by syntactical and constructive methods. The main results are theorems on the structure of the PA-proofs of suitable arithmetical interpretationsS of a modal sequentS, which allow the transformation of PA-proofs ofS into proof-trees similar to modal proof-trees. As an application of such theorems, a proof of Solovay's theorem on arithmetical completeness of the modal system G is presented for the class of modal sequents of Boolean combinations of formulas of the form p i,m i=0, 1, 2, ... The paper is the preliminary step for a forthcoming global syntactical resolution of the PA-completeness problem for modal logic.

We give a self-contained geometric proof of the completeness theorem for the infinite-valued sentential calculus of Łukasiewicz.

It might seem that three of Godel’s results - the Completeness and the First and Second Incompleteness Theorems - assume so little that they are reasonably indisputable. A version of the Completeness Theorem, for instance, can be proven in RCA0, which is the weakest system studied extensively in Simpson’s encyclopaedic Subsystems of Second Order Arithmetic. And it often seems that the minimum requirements for a system just to express the Incompleteness Theorems are sufficient to prove them. However, it will be shown that a particular sub-system of Peano Arithmetic is powerful enough to express assertions about syntax, provability, consistency, and models, while being too weak to allow the standard proofs of the theorems to go through. An alternative proof is available for the First Incompleteness Theorem, but is of such a different nature that the import of the theorem changes. And there are no alternative proofs for (certainly) the Completeness and (apparently) the Second Incompleteness Theorems. It is therefore perfectly rational for someone to be skeptical about Godel’s results.

The proof of correctness and completeness of a logical calculus w.r.t. a given semantics can be read as telling us that the tautologies (or, more gen erally, the relation of consequence) specified in a model theoretic way can be equally well specified in a proof theoretic way, by means of the calculus (as the theorems, resp. the relation of inferability of the calculus). Thus we know that both for the classical propositional calculus and for the clas sical predicate calculus theorems and tautologies represent two sides of the same coin. We also know that the relation of inference as instituted by any of the common axiom systems of the classical propositional calculus coin cides with the relation of consequence defined in terms of the truth tables; whereas the situation is a little bit more complicated w.r.t. the classical predicate calculus (the coincidence occurs if we restrict ourselves to closed ∀xFx is inferable from Fx without being its conse formulas; otherwise..

A general strategy for proving completeness theorems for quantified modal logics is provided. Starting from free quantified modal logic K, with or without identity, extensions obtained either by adding the principle of universal instantiation or the converse of the Barcan formula or the Barcan formula are considered and proved complete in a uniform way. Completeness theorems are also shown for systems with the extended Barcan rule as well as for some quantified extensions of the modal logic B. The incompleteness of Q°.B + BF is also proved.

In this paper the completeness theorems for the finite-valued ukasiewicz logics are proved with the use of the Lindenbaum algebra.

New propositional and first-order paraconsistent logics (called L ω and FL ω , respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding theorems of L ω and FL ω into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple semantics for L ω and FL ω are proved. The cut-elimination theorems for L ω and FL ω are shown using both syntactical ways via the embedding theorems and semantical ways via the completeness theorems.

Urquhart and Méndez and Salto claim to establish completeness theorems for the system C and two of its negation extensions. In this note, we do the following three things: (1) provide a counterexample to all of these alleged completeness theorems, (2) attempt to diagnose the mistakes in the reported completeness proofs, and (3) provide complete axiomatizations of the desired systems.

Urquhart and Méndez and Salto claim to establish completeness theorems for the system C and two of its negation extensions. In this note, we do the following three things: (1) provide a counterexample to all of these alleged completeness theorems, (2) attempt to diagnose the mistakes in the reported completeness proofs, and (3) provide complete axiomatizations of the desired systems.