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.

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.

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.

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.

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.

Modus ponens under hypotheses

1965 ◽  
Vol 30 (1) ◽  
pp. 26-26 ◽  
Author(s):  
A. F. Bausch
Keyword(s):  
Mathematical Logic ◽  
Propositional Calculus ◽  
Modus Ponens ◽  
Inference Rules ◽  
Classical Calculus ◽  
New Formulation ◽  
Image Position ◽  
Classical Propositional Calculus

The Stoic “indemonstrables” were inference rules; a rule about rules was the synthetic theorem: if from certain premisses a conclusion follows and from that conclusion and certain further premisses a second conclusion follows, then the second conclusion follows from all the premisses together. Similar things occur as medieval “rules of consequence”, although not usually on a metametalevel; and (with the same proviso) the following might be deemed a contemporary avatar of that Stoic theorem.If every formula which occurs once or more often in the list A1, A2, …, An, B1, B2, …, Bm occurs also at least once in the list C1, C2, …, Cr then:This rule [Church: Introduction to Mathematical Logic, 1956, pp. 94, 165], which may be called the rule of modus ponens under hypotheses (MPH), is worthy of attention for the following reasons:A. MPH and the axioms A ⊃ A yield precisely the positive implicative calculus (and very easily, too).B. MPH and the axioms A ⊃ f ⊃ f ⊃ A yield a new formulation of the full classical propositional calculus (in terms of f and ⊃).C. MPH and the axioms ∼A ⊃ A ⊃ A and A ⊃. ∼A ⊃ B yield the classical calculus in terms of ∼ and ⊃.

Hilbert-style proof Calculus for Propositional Logic in ABC notation

2019 ◽  
Author(s):  
Matheus Pereira Lobo
Keyword(s):  
Propositional Logic ◽  
Inference Rule ◽  
Modus Ponens ◽  
Axiomatic System ◽  
First Contact

All nine axioms and a single inference rule of logic (Modus Ponens) within the Hilbert axiomatic system are presented using capital letters (ABC) in order to familiarize the beginner student in hers/his first contact with the topic.

Pythagorean fuzzy full implication multiple I method and corresponding applications

2021 ◽  
pp. 1-15
Author(s):  
TaiBen Nan ◽  
Haidong Zhang ◽  
Yanping He
Keyword(s):  
Decision Making ◽  
Modus Ponens ◽  
Pythagorean Fuzzy Set ◽  
Implication Operator ◽  
Continuity Properties ◽  
Fuzzy Implication ◽  
Decision Making Problem ◽  
Fuzzy Implication Operator ◽  
Degree Of Similarity ◽  
Fuzzy Modus Ponens

The overwhelming majority of existing decision-making methods combined with the Pythagorean fuzzy set (PFS) are based on aggregation operators, and their logical foundation is imperfect. Therefore, we attempt to establish two decision-making methods based on the Pythagorean fuzzy multiple I method. This paper is devoted to the discussion of the full implication multiple I method based on the PFS. We first propose the concepts of Pythagorean t-norm, Pythagorean t-conorm, residual Pythagorean fuzzy implication operator (RPFIO), Pythagorean fuzzy biresiduum, and the degree of similarity between PFSs based on the Pythagorean fuzzy biresiduum. In addition, the full implication multiple I method for Pythagorean fuzzy modus ponens (PFMP) is established, and the reversibility and continuity properties of the full implication multiple I method of PFMP are analyzed. Finally, a practical problem is discussed to demonstrate the effectiveness of the Pythagorean fuzzy full implication multiple I method in a decision-making problem. The advantages of the new method over existing methods are also explained. Overall, the proposed methods are based on logical reasoning, so they can more accurately and completely express decision information.

scholarly journals On Basic Probability Logic Inequalities

Mathematics ◽  
2021 ◽  
Vol 9 (12) ◽  
pp. 1409
Author(s):  
Marija Boričić Joksimović
Keyword(s):  
Probability Theory ◽  
Inference Rule ◽  
Modus Ponens ◽  
Probability Logic ◽  
Modus Tollens ◽  
Short Overview ◽  
Basic Probability ◽  
Probabilistic Version ◽  
Hypothetical Syllogism

We give some simple examples of applying some of the well-known elementary probability theory inequalities and properties in the field of logical argumentation. A probabilistic version of the hypothetical syllogism inference rule is as follows: if propositions A, B, C, A→B, and B→C have probabilities a, b, c, r, and s, respectively, then for probability p of A→C, we have f(a,b,c,r,s)≤p≤g(a,b,c,r,s), for some functions f and g of given parameters. In this paper, after a short overview of known rules related to conjunction and disjunction, we proposed some probabilized forms of the hypothetical syllogism inference rule, with the best possible bounds for the probability of conclusion, covering simultaneously the probabilistic versions of both modus ponens and modus tollens rules, as already considered by Suppes, Hailperin, and Wagner.

Sign in / Sign up

Export Citation Format

Share Document