China
Africa
Explore chapters and articles related to this topic
Miscellaneous
Published in Dan Zwillinger, CRC Standard Mathematical Tables and Formulas, 2018
Propositional calculus is the study of statements: how they are combined and how to determine their truth. Statements (or propositions) are combined by means of connectives such as and (∧ ) , or (V), not(¬,or $ (\neg , or $ sometimes ∼ ) , implies (→ ) , and if and only if (Reject, sometimes written ⇔or``iff'') $ \Leftrightarrow or \hbox{``}iff\hbox{''}) $ . Propositions are denoted by letters {p, q, r, . . For example, if p is the statement“x= 3 and q the statement y = 4 then p ∨ ¬q would be interpreted as “x = 3 or y ≠ 4.” To determine the truth of a statement, truth tables are used. Using T (for true) and F (for false), the truth tables for these connectives are as follows:
Knowledge Representation and Processing
Published in Clarence W. de Silva, Intelligent Control, 2018
Propositional calculus is the branch of logic in which propositions (i.e., statements that are either true or false) are used in logic “calculations”. Note that calculus in the present terminology implies “the approach of calculation”. We have primarily discussed propositional calculus. Predicate calculus is a generalized version of propositional calculus in which, in a predicate statement, a predicate serves a purpose similar to that of a mathematical function and may be applied to a constant or variable argument. Hence, a logic statement in this case will take the form Predicate (Argument)
Assertive graphs
Published in Journal of Applied Non-Classical Logics, 2018
F. Bellucci, D. Chiffi, A.-V. Pietarinen
For Peirce, however, the difference between the occurrence of a sentence as asserted and its occurrence as unasserted has not to be expressed by an ad hoc sign of assertion. This does not mean that such a difference ought not to be expressed by any means. In fact, what is asserted is the formula associated with the main connective, so that to determine whether a sentence S, simple or complex, is asserted in a truth-functional context T it is sufficient to check whether the main connective of S coincides with the main connective of T. For example, take the axiom given in Figure 1 in Peirce’s 1885 notation for his propositional calculus, later named Peirce’s Law:
On the modal interpretation of the connective of realisation
Published in Journal of Applied Non-Classical Logics, 2021
An axiom system consists of (2a) as well as the schemata: The rules of Modus Ponens and the rule of mutual interchange of quasi-formulas equivalent in Classical Propositional Calculus: are the unique primitive rules of inference.
Axiomatic and dual systems for constructive necessity, a formally verified equivalence
Published in Journal of Applied Non-Classical Logics, 2019
Lourdes del Carmen González-Huesca, Favio E. Miranda-Perea, P. Selene Linares-Arévalo
Other line of research that we are currently tackling consists of the treatment of other modal logics for necessity and possibility. In the first case , Kavvos (2017) explores dual systems K, K4 and GL (Gödel-Löb Logic of Provability). For the last logic, the proposed introduction rule for necessity is: We conjecture that this rule can be simplified by means of our transference process, but further investigation is required. For the second case, an extension of the here presented results with the possibility operator ⋄ would yield constructive characterisations of possibility, covering the full constructive logic S4. The extension of the axiomatic system , by adding the corresponding axioms for possibility, seems to be straightforward. However, in the case of natural deduction, the inference rules need to handle conclusions for truth and possibility, namely and . Recall that in , all conclusions are of the form , though we omitted the explicit mention to the true judgment for the sake of simplicity. Besides tackling other aspects of modal logic proof theory, such as the study of the sequent calculus of Hakli and Negri (2012), or others (Negri, 2011), as modal logics are commonly defined as an extension of classical logic, where possibility is defined as a dual notion of necessity by means of classical negation, it is mandatory to pursuit formal verification for such formalisms. This could be challenging since some of the usual mathematical reasoning around classical logic is done by non-constructive proof styles not directly available in Coq. Last but not least, we intend to investigate the benefits of our current implementation and the mentioned extensions, in pursuing actual verification cases, like the formalisation of modal lambda calculus of Ghani, de Paiva, and Ritter (1998) or lax logic in Fairtlough and Mendler (1997), as well as the mechanisation of Gödel's interpretation of intuitionistic propositional calculus in S4 (Gödel, 1986). To do so, we need to turn our current implementations into a Coq library providing tactics for modal reasoning. This is also relevant for teaching modal logic to undergraduate students (see Henz & Hobor, 2011 for a related experience).