Explicit analyses of proof/refutation interaction for constructible falsity and Heyting–Brouwer logic

2020 ◽  
Vol 30 (8) ◽  
pp. 1505-1540
Author(s):  
Thomas Macaulay Ferguson
Keyword(s):  
Intuitionistic Logic ◽  
The Other ◽  
Justification Logic ◽  
Formal Proofs ◽  
Multiple Agent ◽  
Distinct Category ◽  
Explicit Analysis ◽  
Competing Interaction

Abstract Nelson’s logic of constructible falsity  $\textsf{N}$ and Rauszer’s Heyting–Brouwer logic  $\textsf{HB}$ are well-known cases of extensions of intuitionistic logic $\textsf{Int}$ enriched with novel connectives. Wansing has suggested that Gödel’s provability interpretation of $\textsf{Int}$ can be extended to these systems by pairing the category of formal proofs with a distinct category of formal refutations. In this paper, we extend the framework of Artemov’s justification logic to provide explicit analyses of $\textsf{N}$ and $\textsf{HB}$ (and the dual-intuitionistic logic $\textsf{DualInt}$) that respect a distinction between proofs and refutations. The application distinguishes the categories by reinterpreting the agents of multiple-agent justification logic as devices that operate exclusively on one or the other category. The analyses reveal that differences between $\textsf{N}$ and $\textsf{HB}$ can be reduced to competing interaction principles characterizing the coordination between proofs and refutations. We conclude by reappraising some of the unusual features of $\textsf{HB}$ in light of the explicit analysis of $\textsf{HB}$.

scholarly journals A Conflict Tolerant Logic of Explicit Evidence

2021 ◽  
Vol 27 (1) ◽  
pp. 124-144
Author(s):  
Thomas Studer
Keyword(s):  
Modal Logic ◽  
Quantum Physics ◽  
Thought Experiment ◽  
The Other ◽  
Justification Logic ◽  
Epistemic Modal ◽  
Epistemic Reasoning ◽  
Basic Properties

Standard epistemic modal logic is unable to adequately deal with the FrauchigerRenner paradox in quantum physics. We introduce a novel justification logic CTJ, in which the paradox can be formalized without leading to an inconsistency. Still CTJ is strong enough to model traditional epistemic reasoning. Our logic tolerates two different pieces of evidence such that one piece justifies a proposition and the other piece justifies the negation of that proposition. However, our logic disallows one piece of evidence to justify both a proposition and its negation. We present syntax and semantics for CTJ and discuss its basic properties. Then we give an example of epistemic reasoning in CTJ that illustrates how the different principles of CTJ interact. We continue with the formalization of the Frauchiger–Renner thought experiment and discuss it in detail. Further, we add a trust axiom to CTJ and again discuss epistemic reasoning and the paradox in this extended setting.

Paraconsistency, self-extensionality, modality

2018 ◽  
Vol 28 (5) ◽  
pp. 851-880
Author(s):  
Arnon Avron ◽  
Anna Zamansky
Keyword(s):  
Intuitionistic Logic ◽  
Modal Logics ◽  
The Other ◽  
Paraconsistent Logics ◽  
Classical Negation ◽  
Inconsistent Theories ◽  
Replacement Property ◽  
General Method

Abstract Paraconsistent logics are logics that, in contrast to classical and intuitionistic logic, do not trivialize inconsistent theories. In this paper we take a paraconsistent view on two famous modal logics: B and S5. We use for this a well-known general method for turning modal logics to paraconsistent logics by defining a new (paraconsistent) negation as $\neg \varphi =_{Def} \sim \Box \varphi$ (where $\sim$ is the classical negation). We show that while that makes both B and S5 members of the well-studied family of paraconsistent C-systems, they differ from most other C-systems in having the important replacement property (which means that equivalence of formulas implies their congruence). We further show that B is a very robust C-system in the sense that almost any axiom which has been considered in the context of C-systems is either already a theorem of B or its addition to B leads to a logic that is no longer paraconsistent. There is exactly one notable exception, and the result of adding this exception to B leads to the other logic studied here, S5.

scholarly journals CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE

2016 ◽  
Vol 22 (1) ◽  
pp. 1-104 ◽  
Author(s):  
MICHAEL BEESON
Keyword(s):  
Intuitionistic Logic ◽  
Euclidean Geometry ◽  
The Other ◽  
Field Theories ◽  
Kripke Models ◽  
Square Roots ◽  
The Third ◽  
Euclidean Field ◽  
Euclidean Field Theory ◽  
Independence Results

AbstractEuclidean geometry, as presented by Euclid, consists of straightedge-and-compass constructions and rigorous reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. This involves finding “uniform” constructions where normally a case distinction is used. For example, in finding a perpendicular to line L through point p, one usually uses two different constructions, “erecting” a perpendicular when p is on L, and “dropping” a perpendicular when p is not on L, but in constructive geometry, it must be done without a case distinction. Classically, the models of Euclidean (straightedge-and-compass) geometry are planes over Euclidean fields. We prove a similar theorem for constructive Euclidean geometry, by showing how to define addition and multiplication without a case distinction about the sign of the arguments. With intuitionistic logic, there are two possible definitions of Euclidean fields, which turn out to correspond to different versions of the parallel postulate.We consider three versions of Euclid’s parallel postulate. The two most important are Euclid’s own formulation in his Postulate 5, which says that under certain conditions two lines meet, and Playfair’s axiom (dating from 1795), which says there cannot be two distinct parallels to line L through the same point p. These differ in that Euclid 5 makes an existence assertion, while Playfair’s axiom does not. The third variant, which we call the strong parallel postulate, isolates the existence assertion from the geometry: it amounts to Playfair’s axiom plus the principle that two distinct lines that are not parallel do intersect. The first main result of this paper is that Euclid 5 suffices to define coordinates, addition, multiplication, and square roots geometrically.We completely settle the questions about implications between the three versions of the parallel postulate. The strong parallel postulate easily implies Euclid 5, and Euclid 5 also implies the strong parallel postulate, as a corollary of coordinatization and definability of arithmetic. We show that Playfair does not imply Euclid 5, and we also give some other independence results. Our independence proofs are given without discussing the exact choice of the other axioms of geometry; all we need is that one can interpret the geometric axioms in Euclidean field theory. The independence proofs use Kripke models of Euclidean field theories based on carefully constructed rings of real-valued functions. “Field elements” in these models are real-valued functions.

Scheduling Multiple Sports Leagues with Travel Distance Fairness: An Application to Argentinean Youth Football

2020 ◽  
Author(s):  
Guillermo A. Durán ◽  
Mario Guajardo ◽  
Agustina F. López ◽  
Javier Marenco ◽  
Gonzalo A. Zamorano
Keyword(s):  
Mathematical Programming ◽  
Round Robin ◽  
Travel Distance ◽  
The Other ◽  
Alternative Solution ◽  
Professional Football ◽  
Youth Football ◽  
Explicit Analysis ◽  
Sports Leagues ◽  
Travel Distances

The first division clubs in Argentinean professional football maintain teams in each of six youth leagues, classed by age as major divisions (Under-20, Under-18, Under-17) and minor divisions (Under-16, Under-15, Under-14). Regular season play in these leagues typically follows a single round-robin format; the minor divisions play the same schedule as the majors but with the home-away status of the matches reversed. This setup can give rise to very significant differences in travel distances between the major and minor division teams of a given club, which is a frustrating situation for club officials, coaches, and players alike but almost impossible to avoid with manual season scheduling techniques. Nor are these methods able to take into account any number of other criteria that go into the design of a satisfactory match calendar. This paper reports on models developed using mathematical programming to simultaneously schedule multiple leagues while also meeting a series of other desirable conditions. The central criterion is a better balance in the travel distances of the various teams, pursued through the application of two alternative solution approaches: one based on regional team clusters and the other on explicit analysis of actual distances between the teams’ home venues. The solutions generated by these approaches have been used by the organizers of the Argentinean youth leagues to draw up their season schedules since 2018, which has resulted in a series of benefits for all stakeholders.

On ‘Listening’ in Music Education Brian Loane

1984 ◽  
Vol 1 (1) ◽  
pp. 27-36 ◽  
Author(s):  
Brian Loane
Keyword(s):  
Music Education ◽  
The Other ◽  
Musical Experience ◽  
Crucial Difference ◽  
Musical Activity ◽  
Supportive Role ◽  
Explicit Analysis ◽  
And Performance ◽  
The One ◽  
Musical Activities

The article suggests that ‘Composing / Performing / Listening’ may be an inadequate way to categorise musical activities, particularly because any musical activity is a sort of listening. There is a discussion of the educationally crucial difference between ‘audience-listening’ on the one hand, and ‘composition-listening’ and ‘performance-listening’ on the other. It is suggested that musical experience is itself thinking embodied in sound, and that explicit ‘analysis-of-listening’ plays a supportive role.In this light, the article proposes an alternative way to categorise musical activities, and indicates some possible conclusions for the curriculum and for assessment.

On Being in a Quandary

2021 ◽  
pp. 209-260
Author(s):  
Crispin Wright
Keyword(s):  
Intuitionistic Logic ◽  
Subject Matter ◽  
Classical Logic ◽  
The Other ◽  
Sorites Paradox ◽  
Metaphysical Realism ◽  
Specific Kind ◽  
Epistemic Conception ◽  
Broad Form

This chapter addresses three problems: the problem of formulating a coherent relativism, the Sorites paradox, and a seldom noticed difficulty in the best intuitionistic case for the revision of classical logic. A response to the latter is proposed which, generalized, contributes towards the solution of the other two. The key to this response is a generalized conception of indeterminacy as a specific kind of intellectual bafflement—Quandary. Intuitionistic revisions of classical logic are merited wherever a subject matter is conceived both as liable to generate Quandary and as subject to a broad form of evidential constraint. So motivated, the distinctions enshrined in intuitionistic logic provide both for a satisfying resolution of the Sorites paradox and a coherent outlet for relativistic views about, for example, matters of taste and morals. An important corollary of the discussion is that an epistemic conception of vagueness can be prised apart from the strong metaphysical realism with which its principal supporters have associated it, and acknowledged to harbour an independent insight.

Formalising Overlap Algebras in Matita

2011 ◽  
Vol 21 (4) ◽  
pp. 763-793 ◽  
Author(s):  
CLAUDIO SACERDOTI COEN ◽  
ENRICO TASSI
Keyword(s):  
Intuitionistic Logic ◽  
Scientific Collaboration ◽  
Optimal Solution ◽  
The Other ◽  
Theorem Prover ◽  
Topological Spaces ◽  
Algebraic Structures ◽  
Size Information ◽  
Predicative Logic

We describe some formal topological results, formalised in Matita 1/2, presented in predicative intuitionistic logic and in terms of Overlap Algebras.Overlap Algebras are new algebraic structures designed to ease reasoning about subsets in an algebraic way within intuitionistic logic. We find that they also ease the formalisation of formal topological results in an interactive theorem prover.Our main result is the existence of a functor between two categories of ‘generalised topological spaces’, one with points (Basic Pairs) and the other point-free (Basic Topologies). This formalisation is part of a wider scientific collaboration with the inventor of the theory, Giovanni Sambin. His goal is to verify in what sense his theory is ‘implementable’, and to discover what problems may arise in the process. We check that all intermediate constructions respect the stringent size requirements imposed by predicative logic. The formalisation is quite unusual, since it has to make explicit size information that is often hidden.We found that the version of Matita used for the formalisation was largely inappropriate. The formalisation drove several major improvements of Matita that will be integrated in the next major release (Matita 1.0). We show some motivating examples, taken directly from the formalisation, for these improvements. We also describe a possibly sub-optimal solution in Matita 1/2, which is exploitable in other similar systems. We briefly discuss a better solution available in Matita 1.0.

Logics without the contraction rule

1985 ◽  
Vol 50 (1) ◽  
pp. 169-201 ◽  
Author(s):  
Hiroakira Ono ◽  
Yuichi Komori
Keyword(s):  
Intuitionistic Logic ◽  
Formal System ◽  
The Other ◽  
Promising Tool ◽  
Nonclassical Logics ◽  
Relevant Logics ◽  
Exchange Rule ◽  
Distributive Law ◽  
Image Position ◽  
Partially Ordered Monoids

We will study syntactical and semantical properties of propositional logics weaker than the intuitionistic, in which the contraction rule (or, the exchange rule or the weakening rule, in some cases) does not hold. Here, the contraction rule means the rule of inference of the formif we formulate our logics in a Gentzen-type formal system. Some syntactical properties of these logics have been studied firstly by the second author in [11], in connection with the study of BCK-algebras (for information on BCK-algebras, see [9]). There, it turned out that such a syntactical method is a powerful and promising tool in studying BCK-algebras. Using this method, considerable progress has been made since then (see, e.g., [8], [18], [27]).In this paper, we will study these logics more comprehensively. We notice here that the distributive lawdoes not hold necessarily in these logics. By adding some axioms (or initial sequents) and rules of inference to these basic logics, we can obtain a lot of interesting nonclassical logics such as Łukasiewicz's many-valued logics, relevant logics, the intuitionistic logic and logics related to BCK-algebras, which have been studied separately until now. Thus, our approach will give a uniform way of dealing with these logics. One of our two main tools in doing so is Gentzen-type formulation of logics in syntax, and the other is semantics defined by using partially ordered monoids.

Completeness of global intuitionistic set theory

1997 ◽  
Vol 62 (2) ◽  
pp. 506-528 ◽  
Author(s):  
Satoko Titani
Keyword(s):  
Set Theory ◽  
Intuitionistic Logic ◽  
Classical Logic ◽  
Mathematical Object ◽  
The Other ◽  
Logical System ◽  
Logical Operators ◽  
Logical Symbol ◽  
Image Position ◽  
Intuitionistic Set Theory

Gentzen's sequential system LJ of intuitionistic logic has two symbols of implication. One is the logical symbol → and the other is the metalogical symbol ⇒ in sequentsConsidering the logical system LJ as a mathematical object, we understand that the logical symbols ∧, ∨, →, ¬, ∀, ∃ are operators on formulas, and ⇒ is a relation. That is, φ ⇒ Ψ is a metalogical sentence which is true or false, on the understanding that our metalogic is a classical logic. In other words, we discuss the logical system LJ in the classical set theory ZFC, in which φ ⇒ Ψ is a sentence.The aim of this paper is to formulate an intuitionistic set theory together with its metatheory. In Takeuti and Titani [6], we formulated an intuitionistic set theory together with its metatheory based on intuitionistic logic. In this paper we postulate that the metatheory is based on classical logic.Let Ω be a cHa. Ω can be a truth value set of a model of LJ. Then the logical symbols ∧, ∨, →, ¬, ∀x, ∃x are interpreted as operators on Ω, and the sentence φ ⇒ Ψ is interpreted as 1 (true) or 0 (false). This means that the metalogical symbol ⇒ also can be expressed as a logical operators such that φ ⇒ Ψ is interpreted as 1 or 0.

scholarly journals Control effects as a modality

2009 ◽  
Vol 19 (1) ◽  
pp. 17-26 ◽  
Author(s):  
HAYO THIELECKE
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Propositional Logic ◽  
The Other ◽  
Classical Propositional Logic ◽  
Double Negation ◽  
Other Hand

AbstractWe combine ideas from types for continuations, effect systems and monads in a very simple setting by defining a version of classical propositional logic in which double-negation elimination is combined with a modality. The modality corresponds to control effects, and it includes a form of effect masking. Erasing the modality from formulas gives classical logic. On the other hand, the logic is conservative over intuitionistic logic.

Sign in / Sign up

Export Citation Format

Share Document