Independence of Rose's axioms for m-valued implication

1969 ◽  
Vol 34 (2) ◽  
pp. 283-284 ◽  
Author(s):  
Ernest Edmonds
Keyword(s):  
Modus Ponens ◽  
Image Position

Rose has shown in [2] that the following axioms are sufficient, with modus ponens, for m-valued Łukasiewiczian implication.

Post completeness in modal logic

1972 ◽  
Vol 37 (4) ◽  
pp. 711-715 ◽  
Author(s):  
Krister Segerberg
Keyword(s):  
Modal Logic ◽  
Upper Bound ◽  
Modus Ponens ◽  
Proper Subset ◽  
Proper Extension ◽  
Image Position

Let ⊥, →, and □ be primitive, and let us have a countable supply of propositional letters. By a (modal) logic we understand a proper subset of the set of all formulas containing every tautology and being closed under modus ponens and substitution. A logic is regular if it contains every instance of □A ∧ □B ↔ □(A ∧ B) and is closed under the ruleA regular logic is normal if it contains □⊤. The smallest regular logic we denote by C (the same as Lemmon's C2), the smallest normal one by K. If L and L' are logics and L ⊆ L′, then L is a sublogic of L', and L' is an extension of L; properly so if L ≠ L'. A logic is quasi-regular (respectively, quasi-normal) if it is an extension of C (respectively, K).A logic is Post complete if it has no proper extension. The Post number, denoted by p(L), is the number of Post complete extensions of L. Thanks to Lindenbaum, we know thatThere is an obvious upper bound, too:Furthermore,.

Pure three-valued Łukasiewiczian implication

1966 ◽  
Vol 31 (3) ◽  
pp. 399-405 ◽  
Author(s):  
Storrs McCall ◽  
R. K. Meyer
Keyword(s):  
Modus Ponens ◽  
The Matrix ◽  
Image Position

The matrix defining Łukasiewicz's three-valued logic, constructed in 1920 and described at length in [1], is the following: This matrix was axiomatized in 1931 by Wajsberg (see [6]), who showed that the following axioms together with the rules of substitution and modus ponens were sufficient:

scholarly journals The number of proofs for a BCK-formula

1993 ◽  
Vol 58 (2) ◽  
pp. 626-628 ◽  
Author(s):  
Yuichi Komori ◽  
Sachio Hirokawa
Keyword(s):  
Normal Form ◽  
Modus Ponens ◽  
Basic Notion ◽  
Type Assignment ◽  
Natural Deduction System ◽  
Cartesian Closed Categories ◽  
Image Position ◽  
Coherence Theorem ◽  
Cartesian Closed ◽  
Necessary And Sufficient

In this note, we give a necessary and sufficient condition for a BCK-formula to have the unique normal form proof.We call implicational propositional formulas formulas for short. BCK-formulas are the formulas which are derivable from axioms B = (a → b) → (c → a) → c → b, C = (a→b→c)→b→a→c, and K = a→b→a by substitution and modus ponens. It is known that the property of being a BCK-formula is decidable (Jaskowski [11, Theorem 6.5], Ben-Yelles [3, Chapter 3, Theorem 3.22], Komori [12, Corollary 6]). The set of BCK-formulas is identical to the set of provable formulas in the natural deduction system with the following two inference rules.Here γ occurs at most once in (→I). By the formulae-as-types correspondence [10], this set is identical to the set of type-schemes of closed BCK-λ-terms. (See [5].) A BCK-λ-term is a λ-term in which no variable occurs twice. Basic notion concerning the type assignment system can be found [4]. Uniqueness of normal form proofs has been known for balanced formulas. (See [2,14].) It is related to the coherence theorem in cartesian closed categories. A formula is balanced when no variable occurs more than twice in it. It was shown in [8] that the proofs of balanced formulas are BCK-proofs. Relevantly balanced formulas were defined in [9], and it was proved that such formulas have unique normal form proofs. Balanced formulas are included in the set of relevantly balanced formulas.

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.

On the inconsistency of systems similar to

1978 ◽  
Vol 43 (1) ◽  
pp. 1-2 ◽  
Author(s):  
M. W. Bunder ◽  
R. K. Meyer
Keyword(s):  
General System ◽  
Modus Ponens ◽  
Combinatory Logic ◽  
Deduction Theorem ◽  
The Absolute ◽  
Image Position ◽  
Weakened Form

This note shows that the inconsistency proof of the system of illative combinatory logic given in [1] can be simplified as well as extended to the absolute inconsistency of a more general system.One extension of the result in [1] lies in the fact that the following weakened form of the deduction theorem for implication will lead to the inconsistency:Also the inconsistency follows almost as easily foras it does for ⊢ H2X for arbitrary X, so we will consider the more general case.The only properties we require other than (DT), (1) and Rule Eq for equality are modus ponens,andLet G = [x] Hn−1x⊃: . … H2x⊃ :Hx⊃ . x ⊃ A, where A is arbitrary. Then if Y is the paradoxical combinator and X = YG, X = GX.Now X ⊂ X, i.e.,

A note on the theory of quantification

1952 ◽  
Vol 17 (4) ◽  
pp. 243-244
Author(s):  
Moh Shaw-Kwei
Keyword(s):  
Modus Ponens ◽  
Logical Formula ◽  
Mechanical Process ◽  
Monadic Theory ◽  
Image Position

In the paper On the logic of quantification Prof. W. V. Quine showed that for the theory of quantification we have a mechanical process to determine whether or not a monadic expression is a valid logical formula, and that to deduce the polyadic theory from the monadic theory we need only the generalized modus ponens, which reads:If a conditional is valid, and its antecedent consists of zero or more quantifiers followed by a valid schema, then its consequent is valid, i.e.:That we have a mechanical process to determine the validity of a monadic expression was pointed out by Löwenheim long ago; Quine's method, however, has the merit that it is very simple and hence practical. The present paper is to show that we may deduce the polyadic theory by means of only a mechanical process and the ordinary modus ponens alone, i.e., the schema,or even by means of only the weakened modus ponens, i.e., the schema,For, if an expression becomes monadic when we omit the initial all-quantifiers (i.e., those preceding every existence-quantifier) and regard the corresponding variables as constants, then evidently we may determine by a mechanical process whether or not it is a valid formula by examining the resulting monadic expression. For example, the expressionis of the same validity as the expressionand hence as the expression

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.

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.

The McKinsey axiom is not compact

1992 ◽  
Vol 57 (4) ◽  
pp. 1230-1238 ◽  
Author(s):  
Xiaoping Wang
Keyword(s):  
Modal Logic ◽  
Modus Ponens ◽  
Intensional Logic ◽  
Normal System ◽  
Propositional Modal Logic ◽  
Modal Operators ◽  
Transformation Rules ◽  
Image Position ◽  
In The Beginning ◽  
Infinite Set

The canonicity and compactness of the KM system are problems historically important in the development of our understanding of intensional logic (as explained in Goldblatt's paper, The McKinsey axiom is not canonical). The problems, however, were unsolved for years in modal logic. In the beginning of 1990, Goldblatt showed that KM is not canonical in The McKinsey axiom is not canonical. The remaining task is to solve the problem of the compactness of KM. In this paper we present a proof showing that the KM system is not compact.The symbols of the language of propositional modal logic are as follows:1. A denumerably infinite set of sentence letters, for example, {p0, P1, p2, …};2. The Boolean connectives &, ⋁, ¬, →, ↔ and parentheses;3. The modal operators L and M where M is defined as ¬L¬.The formation rules of well-formed propositional modal formulae are the formation rules of formulae in classic propositional logic plus the following rule:If A is a well-formed formula, so is LA.A normal modal system is a set of formulae that contains all tautologies and the formulaand is closed under the following transformation rules:Uniform substitution. If A is a theorem, so is every substitution-instance of A.Modus ponens. If A and A → B are theorems, so is B.Necessitation. If A is a theorem, so is LA.Let L be a normal system. Then a set S of formulae is L-consistent if and only if for any formula B, which is the conjunction of some formulae in S, B is not included in L. A set S of formulae is maximal if and only if for every formula A, S either contains A or contains ¬A. A set S of formulae is maximal L-consistent if and only if it is both maximal and L-consistent.

The inconsistency of

1976 ◽  
Vol 41 (2) ◽  
pp. 467-468
Author(s):  
M. W. Bunder
Keyword(s):  
Fixed Point ◽  
Modus Ponens ◽  
The Other ◽  
Deduction Theorem ◽  
Image Position

In [4] Curry raised the possibility that his system proposed in ξ15C of [3] might be inconsistent. In this paper this inconsistency is proved using a method also employed in [1].From Curry's axiom ⊦LH, it follows thatholds for arbitrary X.The other results from that are required areModus Ponens, and the Deduction Theorem for implication:Assuming ⊦HA, we define as in [1]:and letwhere Y is the paradoxical (or fixed point) combinator.We have X = G2X, so, by (2), H X ⊦ X ⊃ G2X which is HX ⊦ X ⊃. H2X ⊃ G1X. Clearly HX ⊦ H(G1X) and, by (5), HX ⊦ H3X, so that, by (3), H X ⊦ H2X ⊃. X ⊃ G1X and by (5) and Modus Ponens HX ⊦ X ⊃ G1X. This is HX ⊦ X ⊃: HX ⊃. X ⊃ A which by (3) and Modus Ponens giveswhich gives, by (4), HX ⊦ X ⊃ A. Now, by (1) and (DT),which is ⊦G1X. But we have ⊦H2X so, by the (DT), ⊦H2X ⊃ G1X which is ⊦G2X. Thus we have proved ⊦X.

Sign in / Sign up

Export Citation Format

Share Document