Strong completeness of fragments of the propositional calculus

1951 ◽  
Vol 16 (3) ◽  
pp. 204-204 ◽  
Author(s):  
Alan Rose
Keyword(s):  
Propositional Calculus ◽  
Modus Ponens ◽  
Primitive Function ◽  
Strong Completeness ◽  
Substitution Rule ◽  
Material Implication ◽  
Rules Of Procedure

There has recently been developed a method of formalising any fragment of the propositional calculus, subject only to the condition that material implication is a primitive function of the fragmentary system considered. Tarski has stated, without proof, that when implication is the only primitive function a formulation which is weakly complete (i.e., has as theorems all expressible tautologies) is also strongly complete (i.e., provides for the deduction of any expressible formula from any which is not a tautology). The methods used by Henkin suggest the following proof of theTheorem. If in a fragment of the propositional calculus material implication can be defined in terms of the primitive functions, then any weakly complete formalisation of the fragmentary system which has for rules of procedure the substitution rule and modus ponens is also strongly complete.

Formalisations of further ℵ0-valued Łukasiewicz propositional calculi

1978 ◽  
Vol 43 (2) ◽  
pp. 207-210 ◽  
Author(s):  
Alan Rose
Keyword(s):  
Propositional Calculus ◽  
Rational Numbers ◽  
Modus Ponens ◽  
Truth Values ◽  
Rules Of Procedure ◽  
C And N ◽  
Image Position ◽  
Propositional Calculi

It has been shown that, for all rational numbers r such that 0≤ r ≤ 1, the ℵ0-valued Łukasiewicz propositional calculus whose designated truth-values are those truth-values x such that r ≤ x ≤ 1 may be formalised completely by means of finitely many axiom schemes and primitive rules of procedure. We shall consider now the case where r is rational, 0≥r≤1 and the designated truth-values are those truth-values x such that r≤x≤1.We note that, in the subcase of the previous case where r = 1, a complete formalisation is given by the following four axiom schemes together with the rule of modus ponens (with respect to C),the functor A being defined in the usual way. The functors B, K, L will also be considered to be defined in the usual way. Let us consider now the functor Dαβ such that if P, Dαβ take the truth-values x, dαβ(x) respectively, α, β are relatively prime integers and r = α/β thenIt follows at once from a theorem of McNaughton that the functor Dαβ is definable in terms of C and N in an effective way. If r = 0 we make the definitionWe note first that if x ≤ α/β then dαβ(x)≤(β + 1)α/β − α = α/β. HenceLet us now define the functions dnαβ(x) (n = 0,1,…) bySinceit follows easily thatand thatThus, if x is designated, x − α/β > 0 and, if n > − log(x − α/β)/log(β + 1), then (β + 1)n(x−α/β) > 1.

A semantics of evidence for classical arithmetic

1995 ◽  
Vol 60 (1) ◽  
pp. 325-337 ◽  
Author(s):  
Thierry Coquand
Keyword(s):  
Winning Strategy ◽  
Propositional Calculus ◽  
Modus Ponens ◽  
Point Of View ◽  
Consistency Proof ◽  
Game Theoretic ◽  
Classical Point ◽  
Classical Arithmetic ◽  
Consistency Proofs ◽  
Natural Formulation

If it is difficult to give the exact significance of consistency proofs from a classical point of view, in particular the proofs of Gentzen [2, 6], and Novikoff [14], the motivations of these proofs are quite clear intuitionistically. Their significance is then less to give a mere consistency proof than to present an intuitionistic explanation of the notion of classical truth. Gentzen for instance summarizes his proof as follows [6]: “Thus propositions of actualist mathematics seem to have a certain utility, but no sense. The major part of my consistency proof, however, consists precisely in ascribing a finitist sense to actualist propositions.” From this point of view, the main part of both Gentzen's and Novikoff's arguments can be stated as establishing that modus ponens is valid w.r.t. this interpretation ascribing a “finitist sense” to classical propositions.In this paper, we reformulate Gentzen's and Novikoff's “finitist sense” of an arithmetic proposition as a winning strategy for a game associated to it. (To see a proof as a winning strategy has been considered by Lorenzen [10] for intuitionistic logic.) In the light of concurrency theory [7], it is tempting to consider a strategy as an interactive program (which represents thus the “finitist sense” of an arithmetic proposition). We shall show that the validity of modus ponens then gets a quite natural formulation, showing that “internal chatters” between two programs end eventually.We first present Novikoff's notion of regular formulae, that can be seen as an intuitionistic truth definition for classical infinitary propositional calculus. We use this in order to motivate the second part, which presents a game-theoretic interpretation of the notion of regular formulae, and a proof of the admissibility of modus ponens which is based on this interpretation.

Subprevarieties versus extensions. Application to the logic of paradox

2000 ◽  
Vol 65 (2) ◽  
pp. 756-766 ◽  
Author(s):  
Alexej P. Pynko
Keyword(s):  
General Result ◽  
Classical Logic ◽  
Modus Ponens ◽  
Galois Connection ◽  
Normal Extension ◽  
Material Implication ◽  
Element Chain ◽  
Class Of Matrices ◽  
The One ◽  
Logic Of Paradox

AbstractIn the present paper we prove that the poset of all extensions of the logic defined by a class of matrices whose sets of distinguished values are equationally definable by their algebra reducts is the retract, under a Galois connection, of the poset of all subprevarieties of the prevariety generated by the class of the algebra reducts of the matrices involved. We apply this general result to the problem of finding and studying all extensions of the logic of paradox (viz., the implication-free fragment of any non-classical normal extension of the relevance-mingle logic). In order to solve this problem, we first study the structure of prevarieties of Kleene lattices. Then, we show that the poset of extensions of the logic of paradox forms a four-element chain, all the extensions being finitely many-valued and finitely-axiomatizable logics. There are just two proper consistent extensions of the logic of paradox. The first is the classical logic that is relatively axiomatized by the Modus ponens rule for the material implication. The second extension, being intermediate between the logic of paradox and the classical logic, is the one relatively axiomatized by the Ex Contradictione Quodlibet rule.

Modal propositional logic on an orthomodular basis. I

1974 ◽  
Vol 39 (3) ◽  
pp. 478-488 ◽  
Author(s):  
L. Herman ◽  
R. Piziak
Keyword(s):  
Boolean Algebra ◽  
Algebraic Logic ◽  
Propositional Calculus ◽  
Natural Generalization ◽  
Point Of View ◽  
Material Implication ◽  
Transformation Rules ◽  
Orthocomplemented Lattice ◽  
Modal Propositional Logic

A common method of obtaining the classical modal logics, for example the Feys system T, the Lewis systems, the Brouwerian system etc., is to build on a basis for the propositional calculus by adjoining a new symbol L, specifying new axioms involving L and the symbols in the basis for PC, and imposing one or more additional transformation rules. In the jargon of algebraic logic, which is the point of view we shall adopt, the “necessity” symbol L may be interpreted as an operator on the Boolean algebra of propositions of PC. For example, the Lewis system S4 may be regarded as a Boolean algebra ℒ together with an operator L on ℒ having the properties: (1)Lp ≤ p for all p in ℒ, (2)L1 = 1, (3) L(p → q) ≤ Lp → Lq for all p, q in ℒ, and (4) Lp = L(Lp) for all p in ℒ. Here, of course, → denotes the material implication connective: p→q = p′ ∨ q. It is easy to verify that property (3) may be replaced by either (3′) L(p ∧ q) = Lp ∧ Lq for all p, q in ℒ, or by (3″) L(p → q) ∧ Lp ≤ Lq for all p, q in ℒ. In particular, it follows from (1) through (4) above that L is a decreasing, idempotent and isotone operator on ℒ. Such mappings are often called interior operators.In a previous paper [5], we considered the problem of introducing an implication connective into a quantum logic. This is greatly complicated by the fact that the quantal propositions band together to form an orthocomplemented lattice which is only “locally” distributive. Such lattices are called orthomodular. For definitions and further discussion, the reader is referred to that paper. In it, we argued that the Sasaki implication connective ⊃ defined by p ⊃ q = p′ ∨ (p ∧ q) is a natural generalization of material implication when the lattice of propositions is ortho-modular. Indeed, if unrestricted distributivity were permitted, p ⊃ q would reduce to the classical material implication p → q. For this reason, we choose ⊃ to play the role of material implication in an orthomodular lattice. Further properties of ⊃ are enumerated in Example 2.2(1) and Corollary 2.4 below.

Implicational formulas in intuitionistic logic

1974 ◽  
Vol 39 (4) ◽  
pp. 661-664 ◽  
Author(s):  
Alasdair Urquhart
Keyword(s):  
Propositional Calculus ◽  
Modus Ponens ◽  
Equivalence Classes ◽  
Alternative Proof ◽  
Hilbert Algebra ◽  
Hilbert Algebras ◽  
Free Generators ◽  
Finite Set ◽  
Image Position ◽  
The Right

In [1] Diego showed that there are only finitely many nonequivalent formulas in n variables in the positive implicational propositional calculus P. He also gave a recursive construction of the corresponding algebra of formulas, the free Hilbert algebra In on n free generators. In the present paper we give an alternative proof of the finiteness of In, and another construction of free Hilbert algebras, yielding a normal form for implicational formulas. The main new result is that In is built up from n copies of a finite Boolean algebra. The proofs use Kripke models [2] rather than the algebraic techniques of [1].Let V be a finite set of propositional variables, and let F(V) be the set of all formulas built up from V ⋃ {t} using → alone. The algebra defined on the equivalence classes , by settingis a free Hilbert algebra I(V) on the free generators . A set T ⊆ F(V) is a theory if ⊦pA implies A ∈ T, and T is closed under modus ponens. For T a theory, T[A] is the theory {B ∣ A → B ∈ T}. A theory T is p-prime, where p ∈ V, if p ∉ T and, for any A ∈ F(V), A ∈ T or A → p ∈ T. A theory is prime if it is p-prime for some p. Pp(V) denotes the set of p-prime theories in F(V), P(V) the set of prime theories. T ∈ P(V) is minimal if there is no theory in P(V) strictly contained in T. Where X = {A1, …, An} is a finite set of formulas, let X → B be A1 →····→·An → B (ϕ → B is B). A formula A is a p-formula if p is the right-most variable occurring in A, i.e. if A is of the form X → p.

Some calculi with strong negation primitive

1968 ◽  
Vol 33 (1) ◽  
pp. 97-100
Author(s):  
J. Jay Zeman
Keyword(s):  
Propositional Calculus ◽  
Strong Negation ◽  
Material Implication ◽  
Unary Operator ◽  
Modal Systems

We shall take “strong negation” to be a unary operator with some of the properties usually associated with negation, and such that the strong negation of a statement implies the “ordinary” negation ofthat statement, but not vice-versa. This paper will consider two varieties of strong negation: first, strong negation set in the context of the propositional calculus, specifically, the intuitionist PC, and secondly, strong negation in modal systems, that is, strong negation as impossibility. In the latter part of the paper, we shall present axiomatizations of several classical Lewis-modal systems having only material implication and impossibility primitive.

A formal reduction of the general problem of expressibility of formulas in the Gödel-Löb provability logic

2002 ◽  
Vol 12 (3) ◽  
Author(s):  
M.F. Ratsa
Keyword(s):  
Modal Logic ◽  
Intuitionistic Logic ◽  
General Problem ◽  
Propositional Calculus ◽  
Finite System ◽  
Provability Logic ◽  
Substitution Rule ◽  
Extension Rule

AbstractIt is a well-known idea to embed the intuitionistic logic into the modal logic in order to interprete the modality 'provable' as the deducibility in the Peano arithmetics with also well-known difficulties. P. M. Solovay and A. V. Kuznetsov introduced into consideration the Gödel-Löb provability logic whose formulas are constructed from propositional variables with the use of the connectives &, v, ⊃, ¬, and Δ (Gödelised provability). This logic is defined by the classic propositional calculus complemented by the three Δ-axiomsΔ (p ⊃ q) ⊃ (Δp ⊃ Δq), Δ(Δp ⊃ Δp) Δp, Δp ⊃ ΔΔp,and the extension rule (the Gödel rule). A formula F is called (functionally) expressible in terms of a system of formulas ∑ in logic L if, on the base of ∑ and variables, it is possible to obtain F with the use of the weakened substitution rule and the rule of change by equivalent in L. The general problem of expressibility in a logic L requires to give an algorithm which for any formula F and any finite system of formulas ∑ recognises whether F is expressible in terms of ∑ in L.In this paper, it is proved that in the Gödel-Löb provability logic and in many of extensions of this logic there is no algorithm which recognises the expressibility. In other words, the general expressibility problem is algorithmically undecidable in these logics.

Note on a problem of Paul Bernays

1955 ◽  
Vol 20 (02) ◽  
pp. 109-114 ◽  
Author(s):  
Bolesław Sobociński
Keyword(s):  
Propositional Calculus ◽  
Modus Ponens ◽  
The Law ◽  
Image Position ◽  
Axiom Systems

In this Journal, vol. 18 (1953), p. 350 (Problem 7), Prof. P. Bernays proposed the following problem on propositional calculus: What is the smallest number n such that the propositional calculus, formulated with substitution and modus ponens as the only rules of inference, can be based on a set of initial formulas each of which contains at most n propositional letters (counted with multiplicity) ? In this note I give a solution to this problem, viz., that this number n = 5. For a system of propositional calculus in which the primitive functors are “C” (implication) and “N” (negation) and in which there are only two rules of inference, i.e. the rules of substitution and detachment (modus ponens), the following can be proved. (1) A set of propositional theses each of which contains at most 4 propositional letters is inadequate to give the complete bi-valued calculus of propositions. (2) There are axiom systems for this calculus in which each axiom contains at most 5 propositional letters. § 1. Consider the following normal metrix, in which the designated value is I: This satisfies the two rules of inference, and the following. (a) The law of commutation, i.e. the thesis CCpCqrCqCpr. (b) The following theses: Furthermore, in this matrix “N” is defined in such a way that: (c) For any well-formed formula α and any value m of this matrix, α = m if and only if NNα = m.

Antitheses in systems of relevant implication

1983 ◽  
Vol 48 (1) ◽  
pp. 97-99 ◽  
Author(s):  
Jean Porte
Keyword(s):  
Propositional Calculus ◽  
Propositional Variable ◽  
Material Implication ◽  
Relevant Implication ◽  
Classical Negation ◽  
Classical Propositional Calculus ◽  
Propositional Calculi

There are several ways for a formula to be “the contrary” of a thesis. When there is a negation we could call a formula an “antithesis” if it is the negation of a thesis—or its negation is a thesis—both properties being equivalent when the negation is classical.When there is no negation or when the connective called “negation” is very different from classical negation, we are forced to look for a different notion.Whence:Definition 1. In a propositional calculus, a substitution antithesis—or, for short, an s-antithesis—is a formula no instance of which is a thesis.There is another kindred notion, but only for calculi for which a deducibility has been defined:Definition 2. A deduction antithesis—for short, a d-antithesis—is a formula from which every formula is deducible.Both notions have been used in the study of the deducibility of certain systems (see below, §4).In the classical propositional calculus, the s-antitheses are simply the formulas which are negations of theses (and whose negations are theses).In S5 and in all the weaker modal propositional calculi, there are s-antitheses which are not negations of theses (and whose negations are not theses); typical examples are ¬(Mp ⊃ Lp) and ¬(p ⊃ Lp) where p is a propositional variable, and ⊃, ¬, M and L are respectively material implication, negation, possibility and necessity (see [8]).

Independence of two nice sets of axioms for the propositional calculus

1968 ◽  
Vol 33 (2) ◽  
pp. 265-270
Author(s):  
T. Thacher Robinson
Keyword(s):  
Propositional Calculus ◽  
Modus Ponens

Kanger [4] gives a set of twelve axioms for the classical prepositional calculus which, together with modus ponens and substitution, have the following nice properties:(0.1) Each axiom contains =⊃, and no axiom contains more than two different connectives.(0.2) Deletions of certain of the axioms yield the intuitionistic, minimal, and classical refutability1 subsystems of propositional calculus.

Sign in / Sign up

Export Citation Format

Share Document