The Classical Sentential Calculus

1989 ◽  
pp. 97-118
Author(s):  
Jan Wolenski
Keyword(s):  
Sentential Calculus

The sentential calculus using rule of inference Re

1960 ◽  
Vol 25 (2) ◽  
pp. 143-143 ◽  
Author(s):  
R. B. Angell
Keyword(s):  
Modus Ponens ◽  
Sentential Calculus

Axiomatizations of the sentential calculus which use Rmp (modus ponens), have been shown equivalent to axiomatizations similar in all respects except that Rmp is replaced by the less restricted rule Re (rule of excision)1:Re. If S and (…(S⊃S') …), then (… S' …).

The Sentential Calculus

1952 ◽  
pp. 15-17
Author(s):  
Joseph T. Clark
Keyword(s):  
Sentential Calculus

Extensions of the Lewis system S5

1951 ◽  
Vol 16 (2) ◽  
pp. 112-120 ◽  
Author(s):  
Schiller Joe Scroggs
Keyword(s):  
Broad Class ◽  
Characteristic Matrix ◽  
Normal Extension ◽  
Strict Implication ◽  
Finite Characteristic ◽  
Material Implication ◽  
Sentential Calculus ◽  
The Third ◽  
Simple Class ◽  
Definition Of

Dugundji has proved that none of the Lewis systems of modal logic, S1 through S5, has a finite characteristic matrix. The question arises whether there exist proper extensions of S5 which have no finite characteristic matrix. By an extension of a sentential calculus S, we usually refer to any system S′ such that every formula provable in S is provable in S′. An extension S′ of S is called proper if it is not identical with S. The answer to the question is trivially affirmative in case we make no additional restrictions on the class of extensions. Thus the extension of S5 obtained by adding to the provable formulas the additional formula p has no finite characteristic matrix (indeed, it has no characteristic matrix at all), but this extension is not closed under substitution—the formula q is not provable in it. McKinsey and Tarski have defined normal extensions of S4* by imposing three conditions. Normal extensions must be closed under substitution, must preserve the rule of detachment under material implication, and must also preserve the rule that if α is provable then ~◊~α is provable. McKinsey and Tarski also gave an example of an extension of S4 which satisfies the first two of these conditions but not the third. One of the results of this paper is that every extension of S5 which satisfies the first two of these conditions also satisfies the third, and hence the above definition of normal extension is redundant for S5. We shall therefore limit the extensions discussed in this paper to those which are closed under substitution and which preserve the rule of detachment under material implication. These extensions we shall call quasi-normal. The class of quasi-normal extensions of S5 is a very broad class and actually includes all extensions which are likely to prove interesting. It is easily shown that quasi-normal extensions of S5 preserve the rules of replacement, adjunction, and detachment under strict implication. It is the purpose of this paper to prove that every proper quasi-normal extension of S5 has a finite characteristic matrix and that every quasi-normal extension of S5 is a normal extension of S5 and to describe a simple class of characteristic matrices for S5.

On formulas in which no individual variable occurs more than twice

1966 ◽  
Vol 31 (1) ◽  
pp. 1-6 ◽  
Author(s):  
Stanisław Jaśkowski
Keyword(s):  
Sentential Calculus ◽  
Individual Variable ◽  
Individual Variables

In Jaśkowski [1], some properties of the consequences of formulas of the sentential calculus with no more than two occurrences of any variable have been settled. Analogous problems may be raised concerning the consequences of equalities in which the same restriction relates to individual variables. In the present paper, problems of this kind are solved and more general theorems are proved about the logical consequences of some formulas, called here multiconditionals.

The complexity of the modal predicate logic of “true in every transitive model of ZF”

1997 ◽  
Vol 62 (4) ◽  
pp. 1371-1378
Author(s):  
Vann McGee
Keyword(s):  
Lower Bound ◽  
Set Theory ◽  
Predicate Logic ◽  
Alternative Conception ◽  
Predicate Calculus ◽  
Modal Formula ◽  
Sentential Calculus ◽  
Transitive Model ◽  
Modal Predicate Logic

Robert Solovay [8] investigated the version of the modal sentential calculus one gets by taking “□ϕ” to mean “ϕ is true in every transitive model of Zermelo-Fraenkel set theory (ZF).” Defining an interpretation to be a function * taking formulas of the modal sentential calculus to sentences of the language of set theory that commutes with the Boolean connectives and sets (□ϕ)* equal to the statement that ϕ* is true in every transitive model of ZF, and stipulating that a modal formula ϕ is valid if and only if, for every interpretation *, ϕ* is true in every transitive model of ZF, Solovay obtained a complete and decidable set of axioms.In this paper, we stifle the hope that we might continue Solovay's program by getting an analogous set of axioms for the modal predicate calculus. The set of valid formulas of the modal predicate calculus is not axiomatizable; indeed, it is complete .We also look at a variant notion of validity according to which a formula ϕ counts as valid if and only if, for every interpretation *, ϕ* is true. For this alternative conception of validity, we shall obtain a lower bound of complexity: every set which is in the set of sentences of the language of set theory true in the constructible universe will be 1-reducible to the set of valid modal formulas.

scholarly journals Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity

2021 ◽  
pp. 41-57
Author(s):  
Joanna Golińska-Pilarek ◽  
Taneli Huuskonen ◽  
Michał Zawidzki
Keyword(s):  
Propositional Logic ◽  
Decision Procedure ◽  
Classical Propositional Logic ◽  
Complexity Bound ◽  
Sentential Calculus ◽  
Truth Values

AbstractSentential Calculus with Identity ($$\mathsf {SCI}$$ SCI ) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In $$\mathsf {SCI}$$ SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of $$\mathsf {SCI}$$ SCI -formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for $$\mathsf {SCI}$$ SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for $$\mathsf {SCI}$$ SCI (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.

Sign in / Sign up

Export Citation Format

Share Document